From: yoni206 Date: Fri, 18 Sep 2020 17:12:04 +0000 (-0700) Subject: bv2int: quantifiers support (#5080) X-Git-Tag: cvc5-1.0.0~2835 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f92c4476e335322c1eeaa9e15ff5e1fda06181fe;p=cvc5.git bv2int: quantifiers support (#5080) This PR adds quantifiers support for bv2int preprocessing pass, and adds regressions that use quantifiers. --- diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 13ad086e8..2aca33df4 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -645,6 +645,21 @@ Node BVToInt::translateWithChildren(Node original, } break; } + case kind::BOUND_VAR_LIST: + { + returnNode = d_nm->mkNode(oldKind, translated_children); + break; + } + case kind::FORALL: + { + returnNode = translateQuantifiedFormula(original); + break; + } + case kind::EXISTS: + { + // Exists is eliminated by the rewriter. + Assert(false); + } default: { // In the default case, we have reached an operator that we do not @@ -679,6 +694,20 @@ Node BVToInt::translateNoChildren(Node original) { if (original.getType().isBitVector()) { + // For bit-vector variables, we create fresh integer variables. + if (original.getKind() == kind::BOUND_VARIABLE) + { + // Range constraints for the bound integer variables are not added now. + // they will be added once the quantifier itself is handled. + std::stringstream ss; + ss << original; + translation = d_nm->mkBoundVar(ss.str() + "_int", d_nm->integerType()); + } + else + { + // New integer variables that are not bound (symbolic constants) + // are added together with range constraints induced by the + // bit-width of the original bit-vector variables. Node newVar = d_nm->mkSkolem("__bvToInt_var", d_nm->integerType(), "Variable introduced in bvToInt " @@ -688,6 +717,7 @@ Node BVToInt::translateNoChildren(Node original) translation = newVar; d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize)); defineBVUFAsIntUF(original, newVar); + } } else if (original.getType().isFunction()) { @@ -954,6 +984,69 @@ Node BVToInt::createShiftNode(vector children, return ite; } +Node BVToInt::translateQuantifiedFormula(Node quantifiedNode) +{ + kind::Kind_t k = quantifiedNode.getKind(); + Node boundVarList = quantifiedNode[0]; + Assert(boundVarList.getKind() == kind::BOUND_VAR_LIST); + // Since bit-vector variables are being translated to + // integer variables, we need to substitute the new ones + // for the old ones. + vector oldBoundVars; + vector newBoundVars; + vector rangeConstraints; + for (Node bv : quantifiedNode[0]) + { + oldBoundVars.push_back(bv); + if (bv.getType().isBitVector()) + { + // bit-vector variables are replaced by integer ones. + // the new variables induce range constraints based on the + // original bit-width. + Node newBoundVar = d_bvToIntCache[bv]; + newBoundVars.push_back(newBoundVar); + rangeConstraints.push_back( + mkRangeConstraint(newBoundVar, bv.getType().getBitVectorSize())); + } + else + { + // variables that are not bit-vectors are not changed + newBoundVars.push_back(bv); + } + } + + // the body of the quantifier + Node matrix = d_bvToIntCache[quantifiedNode[1]]; + // make the substitution + matrix = matrix.substitute(oldBoundVars.begin(), + oldBoundVars.end(), + newBoundVars.begin(), + newBoundVars.end()); + // A node to represent all the range constraints. + Node ranges; + if (rangeConstraints.size() > 0) + { + if (rangeConstraints.size() == 1) + { + ranges = rangeConstraints[0]; + } + else + { + ranges = d_nm->mkNode(kind::AND, rangeConstraints); + } + // Add the range constraints to the body of the quantifier. + // For "exists", this is added conjunctively + // For "forall", this is added to the left side of an implication. + matrix = d_nm->mkNode( + k == kind::FORALL ? kind::IMPLIES : kind::AND, ranges, matrix); + } + + // create the new quantified formula and return it. + Node newBoundVarsList = d_nm->mkNode(kind::BOUND_VAR_LIST, newBoundVars); + Node result = d_nm->mkNode(kind::FORALL, newBoundVarsList, matrix); + return result; +} + Node BVToInt::createITEFromTable( Node x, Node y, diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index b84726878..41d8f4904 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -253,6 +253,16 @@ class BVToInt : public PreprocessingPass */ void addFinalizeRangeAssertions(AssertionPipeline* assertionsToPreprocess); + /** + * @param quantifiedNode a node whose main operator is forall/exists. + * @return a node opbtained from quantifiedNode by: + * 1. Replacing all bound BV variables by new bound integer variables. + * 2. Add range constraints for the new variables, induced by the original + * bit-width. These range constraints are added with "AND" in case of exists + * and with "IMPLIES" in case of forall. + */ + Node translateQuantifiedFormula(Node quantifiedNode); + /** * Reconstructs a node whose main operator cannot be * translated to integers. diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5f9465562..f78d51ad1 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2190,6 +2190,9 @@ set(regress_3_tests regress3/bmc-ibm-5.smtv1.smt2 regress3/bmc-ibm-7.smtv1.smt2 regress3/bv_to_int_and_or.smt2 + regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 + regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 + regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 regress3/eq_diamond14.smtv1.smt2 regress3/friedman_n6_i4.smtv1.smt2 regress3/hole9.cvc diff --git a/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 new file mode 100644 index 000000000..a2c964e9a --- /dev/null +++ b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-models +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-models +; EXPECT: sat +(set-logic BV) +(declare-fun s () (_ BitVec 3)) +(declare-fun t () (_ BitVec 3)) +(assert (not (and (=> (bvsge (_ bv0 3) t) (exists ((x (_ BitVec 3))) (bvsge (bvashr x s) t))) (=> (exists ((x (_ BitVec 3))) (bvsge (bvashr x s) t)) (bvsge (_ bv0 3) t))))) +(check-sat) +(exit) diff --git a/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 new file mode 100644 index 000000000..22656d17f --- /dev/null +++ b/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-unsat-cores +; EXPECT: unsat +(set-logic BV) +(declare-fun s () (_ BitVec 4)) +(assert (bvult s (_ bv4 4))) +(assert (forall ((x (_ BitVec 4))) (= (bvlshr x s) (_ bv0 4)))) +(check-sat) +(exit) diff --git a/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 new file mode 100644 index 000000000..576ebf962 --- /dev/null +++ b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --full-saturate-quant --cegqi-all --no-check-models +;EXPECT: sat +(set-logic BV) +(assert (exists ((c__detect__main__1__i_36_C (_ BitVec 32))) (bvslt ((_ sign_extend 32) c__detect__main__1__i_36_C) (_ bv0 64)))) +(check-sat) +(exit)