aboutsummaryrefslogtreecommitdiffstats
path: root/libs/ezsat/testbench.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-07-21 01:49:59 +0200
committerClifford Wolf <clifford@clifford.at>2014-07-21 02:01:32 +0200
commitb1d520949bdb5357f31f43d9dc4f4579dda9f269 (patch)
tree83b0774721024d166b5c710514a4efcbf530a69b /libs/ezsat/testbench.cc
parentade659e617922171ad1b678a51765ba2046c27d8 (diff)
downloadyosys-b1d520949bdb5357f31f43d9dc4f4579dda9f269.tar.gz
yosys-b1d520949bdb5357f31f43d9dc4f4579dda9f269.tar.bz2
yosys-b1d520949bdb5357f31f43d9dc4f4579dda9f269.zip
Added ezSAT::keep_cnf() and ezSAT::non_incremental()
Diffstat (limited to 'libs/ezsat/testbench.cc')
-rw-r--r--libs/ezsat/testbench.cc6
1 files changed, 6 insertions, 0 deletions
diff --git a/libs/ezsat/testbench.cc b/libs/ezsat/testbench.cc
index 8332ad919..d20258c37 100644
--- a/libs/ezsat/testbench.cc
+++ b/libs/ezsat/testbench.cc
@@ -64,6 +64,7 @@ void test_simple()
printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
ezMiniSAT sat;
+ sat.non_incremental();
sat.assume(sat.OR("A", "B"));
sat.assume(sat.NOT(sat.AND("A", "B")));
test(sat);
@@ -121,6 +122,8 @@ void test_xorshift32()
printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
ezMiniSAT sat;
+ sat.keep_cnf();
+
xorshift128 rng;
std::vector<int> bits = sat.vec_var("i", 32);
@@ -137,6 +140,9 @@ void test_xorshift32()
test_xorshift32_try(sat, rng());
test_xorshift32_try(sat, rng());
test_xorshift32_try(sat, rng());
+
+ sat.printDIMACS(stdout, true);
+ printf("\n");
}
// ------------------------------------------------------------------------------------------------------------