default = "true"
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"
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);
// 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;
}
* 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.
*/
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
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);
Trace("cegqi-bv") << "...failed to solve." << std::endl;
}
}
+ else
+ {
+ Trace("cegqi-bv") << "...no path." << std::endl;
+ }
}
Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
{
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)
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 \
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 \
--- /dev/null
+(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)
--- /dev/null
+; 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
+; )
+; )
+; )
+; )
+;)
projects / cvc5.git / commitdiff