diff options
author | Clifford Wolf <clifford@clifford.at> | 2014-07-21 01:49:59 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2014-07-21 02:01:32 +0200 |
commit | b1d520949bdb5357f31f43d9dc4f4579dda9f269 (patch) | |
tree | 83b0774721024d166b5c710514a4efcbf530a69b /libs/ezsat/testbench.cc | |
parent | ade659e617922171ad1b678a51765ba2046c27d8 (diff) | |
download | yosys-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.cc | 6 |
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"); } // ------------------------------------------------------------------------------------------------------------ |