aboutsummaryrefslogtreecommitdiffstats
path: root/libs/ezsat
diff options
context:
space:
mode:
Diffstat (limited to 'libs/ezsat')
-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
9 files changed, 46 insertions, 24 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");
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-12 15:34:39 +0000