diff options
| -rw-r--r-- | src/options/quantifiers_options.toml | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 15 | ||||
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.h | 13 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp | 14 | ||||
| -rw-r--r-- | test/regress/Makefile.tests | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/qbv-subcall.smt2 | 10 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/logiccell_help.sy | 119 |
7 files changed, 173 insertions, 8 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 055dfd545..f04f5abfd 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1502,6 +1502,14 @@ header = "options/quantifiers_options.h" help = "linearize adder chains for variables" [[option]] + name = "cbqiBvSolveNl" + category = "regular" + long = "cbqi-bv-solve-nl" + type = "bool" + default = "false" + help = "try to solve non-linear bv literals using model value projections" + +[[option]] name = "cbqiBvConcInv" category = "regular" long = "cbqi-bv-concat-inv" diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index b0f7a2cb8..3ff27366b 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -175,8 +175,12 @@ Node BvInverter::getPathToPv( return Node::null(); } -Node BvInverter::getPathToPv( - Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path) +Node BvInverter::getPathToPv(Node lit, + Node pv, + Node sv, + Node pvs, + std::vector<unsigned>& path, + bool projectNl) { std::unordered_set<TNode, TNodeHashFunction> visited; Node slit = getPathToPv(lit, pv, sv, path, visited); @@ -186,7 +190,14 @@ Node BvInverter::getPathToPv( // substitute pvs for the other occurrences of pv TNode tpv = pv; TNode tpvs = pvs; + Node prev_lit = slit; slit = slit.substitute(tpv, tpvs); + if (!projectNl && slit != prev_lit) + { + // found another occurrence of pv that was not on the solve path, + // hence lit is non-linear wrt pv and we return null. + return Node::null(); + } } return slit; } diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 59dc543ae..2d9e04281 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -59,9 +59,16 @@ class BvInverter * pvs (if pvs is non-null). If return value R is non-null, then : * lit.path = pv R.path = sv * R.path' = pvs for all lit.path' = pv, where path' != path + * + * If the flag projectNl is false, we return the null node if the + * literal lit is non-linear with respect to pv. */ - Node getPathToPv( - Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path); + Node getPathToPv(Node lit, + Node pv, + Node sv, + Node pvs, + std::vector<unsigned>& path, + bool projectNl); /** * Same as above, but does not linearize lit for pv. @@ -69,7 +76,7 @@ class BvInverter */ Node getPathToPv(Node lit, Node pv, std::vector<unsigned>& path) { - return getPathToPv(lit, pv, pv, Node::null(), path); + return getPathToPv(lit, pv, pv, Node::null(), path, false); } /** solveBvLit diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp index 0274d45cd..cf09cfa55 100644 --- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp @@ -991,8 +991,9 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, std::vector<unsigned> path; Node sv = d_inverter->getSolveVariable(pv.getType()); Node pvs = ci->getModelValue(pv); - Trace("cegqi-bv") << "Get path to pv : " << lit << std::endl; - Node slit = d_inverter->getPathToPv(lit, pv, sv, pvs, path); + Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl; + Node slit = + d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cbqiBvSolveNl()); if (!slit.isNull()) { CegInstantiatorBvInverterQuery m(ci); @@ -1017,6 +1018,10 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, Trace("cegqi-bv") << "...failed to solve." << std::endl; } } + else + { + Trace("cegqi-bv") << "...no path." << std::endl; + } } Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, @@ -1981,7 +1986,10 @@ void BvInstantiatorPreprocess::collectExtracts( { if (cur.getKind() == BITVECTOR_EXTRACT) { - extract_map[cur[0]].push_back(cur); + if (cur[0].getKind() == INST_CONSTANT) + { + extract_map[cur[0]].push_back(cur); + } } for (const Node& nc : cur) diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 98faf011e..39c8dd403 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1285,6 +1285,7 @@ REG1_TESTS = \ regress1/quantifiers/psyco-196.smt2 \ regress1/quantifiers/qbv-disequality3.smt2 \ regress1/quantifiers/qbv-simple-2vars-vo.smt2 \ + regress1/quantifiers/qbv-subcall.smt2 \ regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 \ regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 \ regress1/quantifiers/qbv-test-invert-bvcomp.smt2 \ @@ -1516,6 +1517,7 @@ REG1_TESTS = \ regress1/sygus/inv-unused.sy \ regress1/sygus/large-const-simp.sy \ regress1/sygus/list-head-x.sy \ + regress1/sygus/logiccell_help.sy \ regress1/sygus/max.sy \ regress1/sygus/multi-fun-polynomial2.sy \ regress1/sygus/nflat-fwd-3.sy \ diff --git a/test/regress/regress1/quantifiers/qbv-subcall.smt2 b/test/regress/regress1/quantifiers/qbv-subcall.smt2 new file mode 100644 index 000000000..5d6881411 --- /dev/null +++ b/test/regress/regress1/quantifiers/qbv-subcall.smt2 @@ -0,0 +1,10 @@ +(set-logic BV) +(set-info :status sat) +(declare-fun k_141 () (_ BitVec 16)) +(declare-fun k_140 () (_ BitVec 1)) +(declare-fun k_139 () (_ BitVec 16)) +(assert +(forall ((x (_ BitVec 2)) (y (_ BitVec 2))) +(= (bvadd (bvneg (concat #b0 x)) (bvadd (bvneg (concat #b0 y)) (concat (bvor (bvand ((_ extract 1 1) x) ((_ extract 1 1) y)) (bvor (bvand ((_ extract 0 0) x) (bvand ((_ extract 0 0) y) ((_ extract 1 1) y))) (bvand ((_ extract 0 0) x) (bvand ((_ extract 0 0) y) ((_ extract 1 1) x))))) (concat ((_ extract 0 0) (bvlshr k_141 (concat #b0000000000000 (concat ((_ extract 1 1) x) (concat ((_ extract 1 1) y) (bvand ((_ extract 0 0) x) (bvand ((_ extract 0 0) y) (bvnot k_140)))))))) ((_ extract 0 0) (bvlshr k_139 (concat #b0000000000000 (concat ((_ extract 0 0) x) (concat ((_ extract 0 0) y) #b0))))))))) #b000) ) +) +(check-sat) diff --git a/test/regress/regress1/sygus/logiccell_help.sy b/test/regress/regress1/sygus/logiccell_help.sy new file mode 100644 index 000000000..34f21ba55 --- /dev/null +++ b/test/regress/regress1/sygus/logiccell_help.sy @@ -0,0 +1,119 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic BV) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; Utils +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-sort Bit () (BitVec 1)) + +(define-fun bit2bool ((b Bit)) Bool + (= b #b1) +) + +(define-fun extend ((i (BitVec 4))) (BitVec 16) + (concat #b000000000000 i) +) + +(define-fun extractBit ((i (BitVec 4)) (x (BitVec 16))) Bit + ((_ extract 0 0) (bvlshr x (extend i))) +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; Arch +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-fun lut4 ((i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (lut_val (BitVec 16))) Bit + (extractBit (concat i0 i1 i2 i3) lut_val) +) + +(define-fun carry ((i0 Bit) (i1 Bit) (ci Bit)) Bit + (bvor (bvand i0 i1) (bvand i0 ci) (bvand i1 ci)) +) + +(define-fun mux2 ((s Bit) (i0 Bit) (i1 Bit)) Bit + ;(ite (bit2bool s) i0 i1) + (bvor (bvand s i0) (bvand (bvnot s) i1)) +) + +(define-fun logic-cell ( + (i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (c_in Bit) ; inputs + (s Bit) (lut_val (BitVec 16)) ;configs + ) (BitVec 2) ; Cout O + (let ( + (c_out Bit (carry i1 i2 c_in)) + (l_out Bit (lut4 i0 i1 i2 (mux2 s i3 c_in) lut_val)) + ) + (concat c_out l_out) +)) + +(define-fun plb2 ( + (i_0_0 Bit) (i_0_1 Bit) (i_0_2 Bit) (i_0_3 Bit) + (i_1_0 Bit) (i_1_1 Bit) (i_1_2 Bit) (i_1_3 Bit) + (c_in Bit) + (s_0 Bit) (lut_val_0 (BitVec 16)) ;configs + (s_1 Bit) (lut_val_1 (BitVec 16)) ;configs + ) (BitVec 3) + (let ((lc0 (BitVec 2) (logic-cell i_0_0 i_0_1 i_0_2 i_0_3 c_in s_0 lut_val_0))) + (let ((lc1 (BitVec 2) (logic-cell i_1_0 i_1_1 i_1_2 i_1_3 ((_ extract 1 1) lc0) s_1 lut_val_1))) + (concat lc1 ((_ extract 0 0) lc0)) + )) +) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; synth +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-fun extract2 ((i (BitVec 1)) (x (BitVec 2))) Bit + ((_ extract 0 0) (bvlshr x (concat #b0 i))) +) + +(synth-fun f ((x (BitVec 2)) (y (BitVec 2)) (c_in Bit)) (BitVec 3) ( + (Start (BitVec 3) ( + (plb2 #b0 (extract2 #b0 x) (extract2 #b0 y) #b0 + #b0 (extract2 #b1 x) (extract2 #b1 y) #b0 + Cin + S LUT_VAL + S LUT_VAL) + )) + (Cin Bit ( + c_in + (Constant Bit) + )) + (S Bit ( + (Constant Bit) + )) + (LUT_VAL (BitVec 16) ( + (Constant (BitVec 16)) + )) +)) + +(declare-var x (BitVec 2)) +(declare-var y (BitVec 2)) + +(constraint (= + (bvadd (concat #b0 x) (concat #b0 y)) + (f x y #b0) +)) + +(constraint (= + (bvadd (bvadd (concat #b0 x) (concat #b0 y)) #b001) + (f x y #b1) +)) + + +(check-synth) + +;(define-fun lut4_ite ((I0 Bit) (I1 Bit) (I2 Bit) (I3 Bit) (LUT_VAL (BitVec 16))) Bit +; (let ((s3 (BitVec 8) (ite (bit2bool I3) ((_ extract 15 8) LUT_VAL) ((_ extract 7 0) LUT_VAL)))) +; (let ((s2 (BitVec 4) (ite (bit2bool I2) ((_ extract 7 4) s3) ((_ extract 3 0) s3)))) +; (let ((s1 (BitVec 2) (ite (bit2bool I1) ((_ extract 3 2) s2) ((_ extract 1 0) s2)))) +; (let ((s0 (BitVec 1) (ite (bit2bool I0) ((_ extract 1 1) s1) ((_ extract 0 0) s1)))) +; s0 +; ) +; ) +; ) +; ) +;) |