aboutsummaryrefslogtreecommitdiffstats
path: root/libs
diff options
context:
space:
mode:
Diffstat (limited to 'libs')
-rw-r--r--libs/ezsat/demo_bit.cc4
-rw-r--r--libs/ezsat/demo_cmp.cc4
-rw-r--r--libs/ezsat/demo_vec.cc4
-rw-r--r--libs/ezsat/ezminisat.cc4
-rw-r--r--libs/ezsat/ezminisat.h4
-rw-r--r--libs/ezsat/ezsat.cc30
-rw-r--r--libs/ezsat/ezsat.h6
-rw-r--r--libs/ezsat/puzzle3d.cc6
-rw-r--r--libs/ezsat/testbench.cc8
-rw-r--r--libs/subcircuit/README4
-rw-r--r--libs/subcircuit/subcircuit.cc4
-rw-r--r--libs/subcircuit/subcircuit.h6
-rw-r--r--libs/subcircuit/test_large.spl2
13 files changed, 54 insertions, 32 deletions
diff --git a/libs/ezsat/demo_bit.cc b/libs/ezsat/demo_bit.cc
index 2a5099bf7..c7b11246c 100644
--- a/libs/ezsat/demo_bit.cc
+++ b/libs/ezsat/demo_bit.cc
@@ -2,11 +2,11 @@
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
diff --git a/libs/ezsat/demo_cmp.cc b/libs/ezsat/demo_cmp.cc
index b2df8a8d9..8d7ceb2b4 100644
--- a/libs/ezsat/demo_cmp.cc
+++ b/libs/ezsat/demo_cmp.cc
@@ -2,11 +2,11 @@
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
diff --git a/libs/ezsat/demo_vec.cc b/libs/ezsat/demo_vec.cc
index b994f00d6..eb8d75997 100644
--- a/libs/ezsat/demo_vec.cc
+++ b/libs/ezsat/demo_vec.cc
@@ -2,11 +2,11 @@
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index dee82a8df..e0ee6292d 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -2,11 +2,11 @@
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 5b5252d88..983e6fd0e 100644
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -2,11 +2,11 @@
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 8d232f335..177bcd8a3 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -2,11 +2,11 @@
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -1337,6 +1337,28 @@ void ezSAT::printInternalState(FILE *f) const
fprintf(f, "--8<-- snap --8<--\n");
}
+static int clog2(int x)
+{
+ int y = (x & (x - 1));
+ y = (y | -y) >> 31;
+
+ x |= (x >> 1);
+ x |= (x >> 2);
+ x |= (x >> 4);
+ x |= (x >> 8);
+ x |= (x >> 16);
+
+ x >>= 1;
+ x -= ((x >> 1) & 0x55555555);
+ x = (((x >> 2) & 0x33333333) + (x & 0x33333333));
+ x = (((x >> 4) + x) & 0x0f0f0f0f);
+ x += (x >> 8);
+ x += (x >> 16);
+ x = x & 0x0000003f;
+
+ return x - y;
+}
+
int ezSAT::onehot(const std::vector<int> &vec, bool max_only)
{
// Mixed one-hot/binary encoding as described by Claessen in Sec. 4.2 of
@@ -1350,7 +1372,7 @@ int ezSAT::onehot(const std::vector<int> &vec, bool max_only)
formula.push_back(expression(OpOr, vec));
// create binary vector
- int num_bits = ceil(log2(vec.size()));
+ int num_bits = clog2(vec.size());
std::vector<int> bits;
for (int k = 0; k < num_bits; k++)
bits.push_back(literal());
@@ -1373,7 +1395,7 @@ int ezSAT::manyhot(const std::vector<int> &vec, int min_hot, int max_hot)
if (max_hot < 0)
max_hot = min_hot;
-
+
std::vector<int> formula;
int M = max_hot+1, N = vec.size();
std::map<std::pair<int,int>, int> x;
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 0faaa6b8d..85b13685f 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -2,11 +2,11 @@
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -29,7 +29,7 @@
class ezSAT
{
- // each token (terminal or non-terminal) is represented by an interger number
+ // each token (terminal or non-terminal) is represented by an integer number
//
// the zero token:
// the number zero is not used as valid token number and is used to encode
diff --git a/libs/ezsat/puzzle3d.cc b/libs/ezsat/puzzle3d.cc
index aee0044b4..59f840f9e 100644
--- a/libs/ezsat/puzzle3d.cc
+++ b/libs/ezsat/puzzle3d.cc
@@ -2,11 +2,11 @@
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -253,7 +253,7 @@ int main()
}
for (size_t i = 1; i < vecvec.size(); i++)
ez.assume(ez.ordered(vecvec[0], vecvec[1]));
-
+
printf("Found and eliminated %d spatial symmetries.\n", int(symmetries.size()));
printf("Generated %d clauses over %d variables.\n", ez.numCnfClauses(), ez.numCnfVariables());
diff --git a/libs/ezsat/testbench.cc b/libs/ezsat/testbench.cc
index d20258c37..d6dc41fa9 100644
--- a/libs/ezsat/testbench.cc
+++ b/libs/ezsat/testbench.cc
@@ -2,11 +2,11 @@
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -220,12 +220,12 @@ void test_count(uint32_t x)
fprintf(stderr, "FAILED 6bit-no-clipping test!\n");
abort();
}
-
+
if (cv4 != sat.vec_count(v, 4, true)) {
fprintf(stderr, "FAILED 4bit-clipping test!\n");
abort();
}
-
+
printf("ok.\n");
}
diff --git a/libs/subcircuit/README b/libs/subcircuit/README
index 757a9f540..b1335681e 100644
--- a/libs/subcircuit/README
+++ b/libs/subcircuit/README
@@ -330,7 +330,7 @@ Mining for frequent SubCircuits
The solver also contains a miner for frequent subcircuits. The following code
fragment will find all frequent subcircuits with at least minNodes nodes and
-at most maxNodes nodes that occurs at least minMatches times:
+at most maxNodes nodes that occurs at least minMatches times:
std::vector<SubCircuit::Solver::MineResult> results;
mySolver.mine(results, minNodes, maxNodes, minMatches);
@@ -370,7 +370,7 @@ This package also contains a small command-line tool called "scshell" that can
be used for experimentation with the algorithm. This program reads a series of
commands from stdin and reports its findings to stdout on exit.
- $ ./scshell < test_macc22.txt
+ $ ./scshell < test_macc22.txt
...
diff --git a/libs/subcircuit/subcircuit.cc b/libs/subcircuit/subcircuit.cc
index cf14df0ac..7c7236833 100644
--- a/libs/subcircuit/subcircuit.cc
+++ b/libs/subcircuit/subcircuit.cc
@@ -3,11 +3,11 @@
* algorithm for coarse grain logic networks
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
diff --git a/libs/subcircuit/subcircuit.h b/libs/subcircuit/subcircuit.h
index d673af88d..5291c6421 100644
--- a/libs/subcircuit/subcircuit.h
+++ b/libs/subcircuit/subcircuit.h
@@ -3,11 +3,11 @@
* algorithm for coarse grain logic networks
*
* Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -115,7 +115,7 @@ namespace SubCircuit
private:
SolverWorker *worker;
-
+
protected:
virtual bool userCompareNodes(const std::string &needleGraphId, const std::string &needleNodeId, void *needleUserData,
const std::string &haystackGraphId, const std::string &haystackNodeId, void *haystackUserData, const std::map<std::string, std::string> &portMapping);
diff --git a/libs/subcircuit/test_large.spl b/libs/subcircuit/test_large.spl
index 74a47d94f..e33e26985 100644
--- a/libs/subcircuit/test_large.spl
+++ b/libs/subcircuit/test_large.spl
@@ -99,7 +99,7 @@ function makeGraph(seed, gates, primaryInputs, primaryOutputs)
foreach netDecl (unusedOutpus)
push primaryOutputs, netDecl;
-
+
return code;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-01 19:04:25 +0000