From c481454a4b05a78ea99e835ec7427a719a2d5c77 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Sat, 11 Jul 2020 04:39:56 -0700 Subject: Changing bv_to_int options (#4721) This PR changes --solve-bv-as-int from a numerical option (specifying the granularity) to an enum (specifying the approach). Currently we support only two modes: OFF and SUM. Future PRs will add more modes. The numerical value of the granularity is now captured by the new option --bvand-integer-granularity. Tests are updated accordingly. --- src/options/smt_options.toml | 21 ++++++++++++++++++--- src/preprocessing/passes/bv_to_int.cpp | 2 +- src/smt/process_assertions.cpp | 2 +- src/smt/set_defaults.cpp | 6 +++--- test/regress/regress0/bv/bv_to_int1.smt2 | 8 ++++---- test/regress/regress0/bv/bv_to_int2.smt2 | 6 +++--- test/regress/regress0/bv/bv_to_int_bitwise.smt2 | 4 ++-- test/regress/regress0/bv/bv_to_int_bvmul1.smt2 | 6 +++--- test/regress/regress0/bv/bv_to_int_bvmul2.smt2 | 2 +- test/regress/regress0/bv/bv_to_int_elim_err.smt2 | 2 +- test/regress/regress0/bv/bv_to_int_zext.smt2 | 2 +- test/regress/regress0/bv/bvuf_to_intuf.smt2 | 2 +- test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 | 2 +- test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 | 2 +- test/regress/regress2/bv_to_int_ashr.smt2 | 4 ++-- test/regress/regress2/bv_to_int_mask_array_1.smt2 | 2 +- test/regress/regress2/bv_to_int_mask_array_2.smt2 | 2 +- test/regress/regress2/bv_to_int_shifts.smt2 | 2 +- test/regress/regress3/bv_to_int_and_or.smt2 | 8 ++++---- 19 files changed, 50 insertions(+), 35 deletions(-) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 13791bfd6..80183b71f 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -639,11 +639,26 @@ header = "options/smt_options.h" [[option]] name = "solveBVAsInt" category = "undocumented" - long = "solve-bv-as-int=N" + long = "solve-bv-as-int=MODE" + type = "SolveBVAsIntMode" + default = "OFF" + help = "mode for translating BVAnd to integer" + help_mode = "solve-bv-as-int modes." +[[option.mode.OFF]] + name = "off" + help = "Do not translate bit-vectors to integers" +[[option.mode.SUM]] + name = "sum" + help = "Generate a sum expression for each bvand instance, based on the value in --solbv-bv-as-int-granularity" + +[[option]] + name = "BVAndIntegerGranularity" + category = "undocumented" + long = "bvand-integer-granularity=N" type = "uint32_t" - default = "0" + default = "1" read_only = true - help = "attempt to solve BV formulas by translation to integer arithmetic (experimental)" + help = "granularity to use in --solve-bv-as-int mode and for iand operator (experimental)" [[option]] name = "iandMode" diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 5b125b4b6..bb0bde2f9 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -269,7 +269,7 @@ Node BVToInt::bvToInt(Node n) n = makeBinary(n); vector toVisit; toVisit.push_back(n); - uint64_t granularity = options::solveBVAsInt(); + uint64_t granularity = options::BVAndIntegerGranularity(); while (!toVisit.empty()) { diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 4eedfd863..4fed33f3c 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -222,7 +222,7 @@ bool ProcessAssertions::apply(AssertionPipeline& assertions) { d_passes["bv-to-bool"]->apply(&assertions); } - if (options::solveBVAsInt() > 0) + if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) { d_passes["bv-to-int"]->apply(&assertions); } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 4ce4b8db8..11751079e 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -154,7 +154,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) logic.lock(); } - if (options::solveBVAsInt() > 0) + if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) { // not compatible with incremental if (options::incrementalSolving()) @@ -168,7 +168,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) throw OptionException( "solving bitvectors as integers is incompatible with --bool-to-bv."); } - if (options::solveBVAsInt() > 8) + if (options::BVAndIntegerGranularity() > 8) { /** * The granularity sets the size of the ITE in each element @@ -382,7 +382,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } - if (options::solveBVAsInt() > 0) + if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) { /** * Operations on 1 bits are better handled as Boolean operations diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 index 1df9ec2d6..d9190128e 100644 --- a/test/regress/regress0/bv/bv_to_int1.smt2 +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs -; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models --no-check-unsat-cores --no-check-proofs -; COMMAND-LINE: --solve-bv-as-int=3 --no-check-models --no-check-unsat-cores --no-check-proofs -; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic QF_BV) (declare-fun x () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2 index ab1bf10f3..00fd51baf 100644 --- a/test/regress/regress0/bv/bv_to_int2.smt2 +++ b/test/regress/regress0/bv/bv_to_int2.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models --no-check-unsat-cores ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2 index 52eb78830..4bcbac20c 100644 --- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs -; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 index d0d699b4d..ec4206812 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models --no-check-unsat-cores ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 index 541229813..05cd312d7 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic QF_BV) (declare-fun T4_180 () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 index 16731b01e..b17aeeacf 100644 --- a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 +++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models ; EXPECT: sat (set-logic QF_BV) (declare-fun _substvar_183_ () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2 index 3525cebb6..5c6be19b5 100644 --- a/test/regress/regress0/bv/bv_to_int_zext.smt2 +++ b/test/regress/regress0/bv/bv_to_int_zext.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic QF_BV) (declare-fun T1_31078 () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bvuf_to_intuf.smt2 index 7176f4012..c621aa112 100644 --- a/test/regress/regress0/bv/bvuf_to_intuf.smt2 +++ b/test/regress/regress0/bv/bvuf_to_intuf.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores ; EXPECT: sat (set-logic QF_UFBV) (declare-fun a () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 index 297bb2422..3db8e87ee 100644 --- a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 +++ b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 @@ -1,4 +1,4 @@ -;COMMAND-LINE: --solve-bv-as-int=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs +;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs ;EXPECT: unsat (set-logic QF_UFBV) diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 index 873acd6c4..8fbe96eab 100644 --- a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 +++ b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores ; EXPECT: sat (set-logic QF_UFBV) (declare-sort S 0) diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2 index e3fcb1790..3e0151076 100644 --- a/test/regress/regress2/bv_to_int_ashr.smt2 +++ b/test/regress/regress2/bv_to_int_ashr.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs -; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2 index c1f20a41b..a2d90be2d 100644 --- a/test/regress/regress2/bv_to_int_mask_array_1.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic ALL) (declare-fun A () (Array Int Int)) diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2 index b88f71064..9bab0c71c 100644 --- a/test/regress/regress2/bv_to_int_mask_array_2.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores --no-check-proofs ; EXPECT: sat (set-logic ALL) (declare-fun A () (Array Int Int)) diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2 index 39dace123..998234a17 100644 --- a/test/regress/regress2/bv_to_int_shifts.smt2 +++ b/test/regress/regress2/bv_to_int_shifts.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores ; EXPECT: sat (set-logic QF_BV) (declare-fun s () (_ BitVec 64)) diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2 index 54a491093..185f1b5ec 100644 --- a/test/regress/regress3/bv_to_int_and_or.smt2 +++ b/test/regress/regress3/bv_to_int_and_or.smt2 @@ -1,8 +1,8 @@ -; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs -; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic QF_BV) -(declare-fun a () (_ BitVec 8)) -(declare-fun b () (_ BitVec 8)) +(declare-fun a () (_ BitVec 4)) +(declare-fun b () (_ BitVec 4)) (assert (bvult (bvor a b) (bvand a b))) (check-sat) -- cgit v1.2.3 From 64a7db86206aa0993f75446a3e7f77f3c0c023c6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 11 Jul 2020 07:45:35 -0500 Subject: Cache explanations in TheoryEngine::getExplanation (#4722) For some hard verification benchmarks from Facebook, TheoryEngine::getExplanation was found to be the bottleneck, where the main loop of TheoryEngine::getExplanation would be run regularly 30k times, sometimes over 1 million times for a single conflict. This caches explanations in this loop, where now the loop is executed roughly 1k times at max for the same benchmark. One challenging benchmark that previously solved in 8 min 45 sec now solves in 2 min 45 sec. FYI @barrettcw . --- src/theory/theory_engine.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 851ae414e..2bbdcceb3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1787,6 +1787,8 @@ void TheoryEngine::getExplanation(std::vector& explanationVector new std::set(proofRecipe->getStep(0)->getAssertions())); } }); + // cache of nodes we have already explained by some theory + std::unordered_set cache; while (i < explanationVector.size()) { // Get the current literal to explain @@ -1868,7 +1870,15 @@ void TheoryEngine::getExplanation(std::vector& explanationVector continue; } } - + // We must cache after checking the timestamp in the block of code above. + // Afterwards, we can ignore this timestamp, as well as caching the Node, + // since any theory's explanation will suffice. + if (cache.find(toExplain.d_node) != cache.end()) + { + ++i; + continue; + } + cache.insert(toExplain.d_node); // It was produced by the theory, so ask for an explanation Node explanation; if (toExplain.d_theory == THEORY_BUILTIN) -- cgit v1.2.3