diff options
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/apply_substs.cpp | 5 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 1034 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_int.h | 261 | ||||
-rw-r--r-- | src/preprocessing/passes/int_to_bv.cpp | 26 | ||||
-rw-r--r-- | src/preprocessing/passes/learned_rewrite.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 41 | ||||
-rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 14 | ||||
-rw-r--r-- | src/preprocessing/passes/pseudo_boolean_processor.cpp | 7 | ||||
-rw-r--r-- | src/preprocessing/passes/real_to_int.cpp | 16 | ||||
-rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 7 | ||||
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 4 |
11 files changed, 98 insertions, 1319 deletions
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 99bded47a..82122fa7f 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -21,7 +21,7 @@ #include "context/cdo.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "theory/rewriter.h" +#include "smt/env.h" #include "theory/substitutions.h" namespace cvc5 { @@ -55,7 +55,8 @@ PreprocessingPassResult ApplySubsts::applyInternal( << std::endl; d_preprocContext->spendResource(Resource::PreprocessStep); assertionsToPreprocess->replaceTrusted( - i, tlsm.applyTrusted((*assertionsToPreprocess)[i])); + i, + tlsm.applyTrusted((*assertionsToPreprocess)[i], d_env.getRewriter())); Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i] << std::endl; } diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 33f3dd445..ac1edeb96 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -19,1054 +19,90 @@ #include "preprocessing/passes/bv_to_int.h" #include <cmath> -#include <sstream> #include <string> #include <unordered_map> #include <vector> #include "expr/node.h" #include "expr/node_traversal.h" -#include "expr/skolem_manager.h" #include "options/smt_options.h" #include "options/uf_options.h" -#include "preprocessing/assertion_pipeline.h" -#include "preprocessing/preprocessing_pass_context.h" #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h" +#include "preprocessing/assertion_pipeline.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/rewriter.h" -#include "util/bitvector.h" -#include "util/iand.h" -#include "util/rational.h" namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace cvc5::kind; using namespace cvc5::theory; using namespace cvc5::theory::bv; -namespace { - -Rational intpow2(uint64_t b) -{ - return Rational(Integer(2).pow(b), Integer(1)); -} - -} //end empty namespace - -Node BVToInt::mkRangeConstraint(Node newVar, uint64_t k) -{ - Node lower = d_nm->mkNode(kind::LEQ, d_zero, newVar); - Node upper = d_nm->mkNode(kind::LT, newVar, pow2(k)); - Node result = d_nm->mkNode(kind::AND, lower, upper); - return rewrite(result); -} - -Node BVToInt::maxInt(uint64_t k) -{ - Assert(k > 0); - Rational max_value = intpow2(k) - 1; - return d_nm->mkConst(CONST_RATIONAL, max_value); -} - -Node BVToInt::pow2(uint64_t k) -{ - Assert(k >= 0); - return d_nm->mkConst(CONST_RATIONAL, Rational(intpow2(k))); -} - -Node BVToInt::modpow2(Node n, uint64_t exponent) -{ - Node p2 = d_nm->mkConst(CONST_RATIONAL, Rational(intpow2(exponent))); - return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2); -} - -/** - * Binarizing n via post-order traversal. - */ -Node BVToInt::makeBinary(Node n) -{ - for (TNode current : NodeDfsIterable(n, - VisitOrder::POSTORDER, - // skip visited nodes - [this](TNode tn) { - return d_binarizeCache.find(tn) - != d_binarizeCache.end(); - })) - { - uint64_t numChildren = current.getNumChildren(); - /* - * We already visited the sub-dag rooted at the current node, - * and binarized all its children. - * Now we binarize the current node itself. - */ - kind::Kind_t k = current.getKind(); - if ((numChildren > 2) - && (k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT - || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR - || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT)) - { - // We only binarize bvadd, bvmul, bvand, bvor, bvxor, bvconcat - Assert(d_binarizeCache.find(current[0]) != d_binarizeCache.end()); - Node result = d_binarizeCache[current[0]]; - for (uint64_t i = 1; i < numChildren; i++) - { - Assert(d_binarizeCache.find(current[i]) != d_binarizeCache.end()); - Node child = d_binarizeCache[current[i]]; - result = d_nm->mkNode(current.getKind(), result, child); - } - d_binarizeCache[current] = result; - } - else if (numChildren > 0) - { - // current has children, but we do not binarize it - NodeBuilder builder(k); - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) - { - builder << current.getOperator(); - } - for (Node child : current) - { - builder << d_binarizeCache[child].get(); - } - d_binarizeCache[current] = builder.constructNode(); - } - else - { - // current has no children - d_binarizeCache[current] = current; - } - } - return d_binarizeCache[n]; -} - -/** - * We traverse n and perform rewrites both on the way down and on the way up. - * On the way down we rewrite the node but not it's children. - * On the way up, we update the node's children to the rewritten ones. - * For each sub-node, we perform rewrites to eliminate operators. - * Then, the original children are added to toVisit stack so that we rewrite - * them as well. - */ -Node BVToInt::eliminationPass(Node n) -{ - std::vector<Node> toVisit; - toVisit.push_back(n); - Node current; - while (!toVisit.empty()) - { - current = toVisit.back(); - // assert that the node is binarized - // The following variable is only used in assertions - CVC5_UNUSED kind::Kind_t k = current.getKind(); - uint64_t numChildren = current.getNumChildren(); - Assert((numChildren == 2) - || !(k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT - || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR - || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT)); - toVisit.pop_back(); - bool inEliminationCache = - (d_eliminationCache.find(current) != d_eliminationCache.end()); - bool inRebuildCache = - (d_rebuildCache.find(current) != d_rebuildCache.end()); - if (!inEliminationCache) - { - // current is not the elimination of any previously-visited node - // current hasn't been eliminated yet. - // eliminate operators from it using rewrite rules - Node currentEliminated = - FixpointRewriteStrategy<RewriteRule<UdivZero>, - RewriteRule<SdivEliminateFewerBitwiseOps>, - RewriteRule<SremEliminateFewerBitwiseOps>, - RewriteRule<SmodEliminateFewerBitwiseOps>, - RewriteRule<XnorEliminate>, - RewriteRule<NandEliminate>, - RewriteRule<NorEliminate>, - RewriteRule<NegEliminate>, - RewriteRule<XorEliminate>, - RewriteRule<OrEliminate>, - RewriteRule<SubEliminate>, - RewriteRule<RepeatEliminate>, - RewriteRule<RotateRightEliminate>, - RewriteRule<RotateLeftEliminate>, - RewriteRule<CompEliminate>, - RewriteRule<SleEliminate>, - RewriteRule<SltEliminate>, - RewriteRule<SgtEliminate>, - RewriteRule<SgeEliminate>>::apply(current); - - // save in the cache - d_eliminationCache[current] = currentEliminated; - // also assign the eliminated now to itself to avoid revisiting. - d_eliminationCache[currentEliminated] = currentEliminated; - // put the eliminated node in the rebuild cache, but mark that it hasn't - // yet been rebuilt by assigning null. - d_rebuildCache[currentEliminated] = Node(); - // Push the eliminated node to the stack - toVisit.push_back(currentEliminated); - // Add the children to the stack for future processing. - toVisit.insert( - toVisit.end(), currentEliminated.begin(), currentEliminated.end()); - } - if (inRebuildCache) - { - // current was already added to the rebuild cache. - if (d_rebuildCache[current].get().isNull()) - { - // current wasn't rebuilt yet. - numChildren = current.getNumChildren(); - if (numChildren == 0) - { - // We only eliminate operators that are not nullary. - d_rebuildCache[current] = current; - } - else - { - // The main operator is replaced, and the children - // are replaced with their eliminated counterparts. - NodeBuilder builder(current.getKind()); - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) - { - builder << current.getOperator(); - } - for (Node child : current) - { - Assert(d_eliminationCache.find(child) != d_eliminationCache.end()); - Node eliminatedChild = d_eliminationCache[child]; - Assert(d_rebuildCache.find(eliminatedChild) != d_eliminationCache.end()); - Assert(!d_rebuildCache[eliminatedChild].get().isNull()); - builder << d_rebuildCache[eliminatedChild].get(); - } - d_rebuildCache[current] = builder.constructNode(); - } - } - } - } - Assert(d_eliminationCache.find(n) != d_eliminationCache.end()); - Node eliminated = d_eliminationCache[n]; - Assert(d_rebuildCache.find(eliminated) != d_rebuildCache.end()); - Assert(!d_rebuildCache[eliminated].get().isNull()); - return d_rebuildCache[eliminated]; -} - -/** - * Translate n to Integers via post-order traversal. - */ -Node BVToInt::bvToInt(Node n) -{ - // make sure the node is re-written before processing it. - n = rewrite(n); - n = makeBinary(n); - n = eliminationPass(n); - // binarize again, in case the elimination pass introduced - // non-binary terms (as can happen by RepeatEliminate, for example). - n = makeBinary(n); - vector<Node> toVisit; - toVisit.push_back(n); - - while (!toVisit.empty()) - { - Node current = toVisit.back(); - uint64_t currentNumChildren = current.getNumChildren(); - if (d_bvToIntCache.find(current) == d_bvToIntCache.end()) - { - // This is the first time we visit this node and it is not in the cache. - // We mark this node as visited but not translated by assiging - // a null node to it. - d_bvToIntCache[current] = Node(); - // all the node's children are added to the stack to be visited - // before visiting this node again. - toVisit.insert(toVisit.end(), current.begin(), current.end()); - // If this is a UF applicatinon, we also add the function to - // toVisit. - if (current.getKind() == kind::APPLY_UF) - { - toVisit.push_back(current.getOperator()); - } - } - else - { - // We already visited and translated this node - if (!d_bvToIntCache[current].get().isNull()) - { - // We are done computing the translation for current - toVisit.pop_back(); - } - else - { - // We are now visiting current on the way back up. - // This is when we do the actual translation. - Node translation; - if (currentNumChildren == 0) - { - translation = translateNoChildren(current); - } - else - { - /** - * The current node has children. - * Since we are on the way back up, - * these children were already translated. - * We save their translation for easy access. - * If the node's kind is APPLY_UF, - * we also need to include the translated uninterpreted function in - * this list. - */ - vector<Node> translated_children; - if (current.getKind() == kind::APPLY_UF) - { - translated_children.push_back( - d_bvToIntCache[current.getOperator()]); - } - for (uint64_t i = 0; i < currentNumChildren; i++) - { - translated_children.push_back(d_bvToIntCache[current[i]]); - } - translation = translateWithChildren(current, translated_children); - } - // Map the current node to its translation in the cache. - d_bvToIntCache[current] = translation; - // Also map the translation to itself. - d_bvToIntCache[translation] = translation; - toVisit.pop_back(); - } - } - } - return d_bvToIntCache[n].get(); -} - -Node BVToInt::translateWithChildren(Node original, - const vector<Node>& translated_children) -{ - // The translation of the original node is determined by the kind of - // the node. - kind::Kind_t oldKind = original.getKind(); - // ultbv and sltbv were supposed to be eliminated before this point. - Assert(oldKind != kind::BITVECTOR_ULTBV); - Assert(oldKind != kind::BITVECTOR_SLTBV); - // The following variable will only be used in assertions. - CVC5_UNUSED uint64_t originalNumChildren = original.getNumChildren(); - Node returnNode; - switch (oldKind) - { - case kind::BITVECTOR_ADD: - { - Assert(originalNumChildren == 2); - uint64_t bvsize = original[0].getType().getBitVectorSize(); - Node plus = d_nm->mkNode(kind::PLUS, translated_children); - Node p2 = pow2(bvsize); - returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2); - break; - } - case kind::BITVECTOR_MULT: - { - Assert(originalNumChildren == 2); - uint64_t bvsize = original[0].getType().getBitVectorSize(); - Node mult = d_nm->mkNode(kind::MULT, translated_children); - Node p2 = pow2(bvsize); - returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, mult, p2); - break; - } - case kind::BITVECTOR_UDIV: - { - uint64_t bvsize = original[0].getType().getBitVectorSize(); - // we use an ITE for the case where the second operand is 0. - Node pow2BvSize = pow2(bvsize); - Node divNode = - d_nm->mkNode(kind::INTS_DIVISION_TOTAL, translated_children); - returnNode = d_nm->mkNode( - kind::ITE, - d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), - d_nm->mkNode(kind::MINUS, pow2BvSize, d_one), - divNode); - break; - } - case kind::BITVECTOR_UREM: - { - // we use an ITE for the case where the second operand is 0. - Node modNode = - d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children); - returnNode = d_nm->mkNode( - kind::ITE, - d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), - translated_children[0], - modNode); - break; - } - case kind::BITVECTOR_NOT: - { - uint64_t bvsize = original[0].getType().getBitVectorSize(); - // we use a specified function to generate the node. - returnNode = createBVNotNode(translated_children[0], bvsize); - break; - } - case kind::BITVECTOR_TO_NAT: - { - // In this case, we already translated the child to integer. - // So the result is the translated child. - returnNode = translated_children[0]; - break; - } - case kind::INT_TO_BITVECTOR: - { - // ((_ int2bv n) t) ---> (mod t 2^n) - size_t sz = original.getOperator().getConst<IntToBitVector>().d_size; - returnNode = d_nm->mkNode( - kind::INTS_MODULUS_TOTAL, translated_children[0], pow2(sz)); - } - break; - case kind::BITVECTOR_AND: - { - // We support three configurations: - // 1. translating to IAND - // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV - // operators) - // 3. translating into a sum - uint64_t bvsize = original[0].getType().getBitVectorSize(); - if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::IAND) - { - Node iAndOp = d_nm->mkConst(IntAnd(bvsize)); - returnNode = d_nm->mkNode( - kind::IAND, iAndOp, translated_children[0], translated_children[1]); - } - else if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BV) - { - // translate the children back to BV - Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize)); - Node x = translated_children[0]; - Node y = translated_children[1]; - Node bvx = d_nm->mkNode(intToBVOp, x); - Node bvy = d_nm->mkNode(intToBVOp, y); - // perform bvand on the bit-vectors - Node bvand = d_nm->mkNode(kind::BITVECTOR_AND, bvx, bvy); - // translate the result to integers - returnNode = d_nm->mkNode(kind::BITVECTOR_TO_NAT, bvand); - } - else - { - Assert(options().smt.solveBVAsInt == options::SolveBVAsIntMode::SUM); - // Construct a sum of ites, based on granularity. - Assert(translated_children.size() == 2); - returnNode = - d_iandUtils.createSumNode(translated_children[0], - translated_children[1], - bvsize, - options().smt.BVAndIntegerGranularity); - } - break; - } - case kind::BITVECTOR_SHL: - { - /** - * a << b is a*2^b. - * The exponentiation is simulated by an ite. - * Only cases where b <= bit width are considered. - * Otherwise, the result is 0. - */ - uint64_t bvsize = original[0].getType().getBitVectorSize(); - returnNode = createShiftNode(translated_children, bvsize, true); - break; - } - case kind::BITVECTOR_LSHR: - { - /** - * a >> b is a div 2^b. - * The exponentiation is simulated by an ite. - * Only cases where b <= bit width are considered. - * Otherwise, the result is 0. - */ - uint64_t bvsize = original[0].getType().getBitVectorSize(); - returnNode = createShiftNode(translated_children, bvsize, false); - break; - } - case kind::BITVECTOR_ASHR: - { - /* From SMT-LIB2: - * (bvashr s t) abbreviates - * (ite (= ((_ extract |m-1| |m-1|) s) #b0) - * (bvlshr s t) - * (bvnot (bvlshr (bvnot s) t))) - * - * Equivalently: - * (bvashr s t) abbreviates - * (ite (bvult s 100000...) - * (bvlshr s t) - * (bvnot (bvlshr (bvnot s) t))) - * - */ - uint64_t bvsize = original[0].getType().getBitVectorSize(); - // signed_min is 100000... - Node signed_min = pow2(bvsize - 1); - Node condition = - d_nm->mkNode(kind::LT, translated_children[0], signed_min); - Node thenNode = createShiftNode(translated_children, bvsize, false); - vector<Node> children = {createBVNotNode(translated_children[0], bvsize), - translated_children[1]}; - Node elseNode = - createBVNotNode(createShiftNode(children, bvsize, false), bvsize); - returnNode = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode); - break; - } - case kind::BITVECTOR_ITE: - { - // Lifted to a boolean ite. - Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one); - returnNode = d_nm->mkNode( - kind::ITE, cond, translated_children[1], translated_children[2]); - break; - } - case kind::BITVECTOR_ZERO_EXTEND: - { - returnNode = translated_children[0]; - break; - } - case kind::BITVECTOR_SIGN_EXTEND: - { - uint64_t bvsize = original[0].getType().getBitVectorSize(); - Node arg = translated_children[0]; - if (arg.isConst()) - { - Rational c(arg.getConst<Rational>()); - Rational twoToKMinusOne(intpow2(bvsize - 1)); - uint64_t amount = bv::utils::getSignExtendAmount(original); - /* if the msb is 0, this is like zero_extend. - * msb is 0 <-> the value is less than 2^{bvsize-1} - */ - if (c < twoToKMinusOne || amount == 0) - { - returnNode = arg; - } - else - { - /* otherwise, we add the integer equivalent of - * 11....1 `amount` times - */ - Rational max_of_amount = intpow2(amount) - 1; - Rational mul = max_of_amount * intpow2(bvsize); - Rational sum = mul + c; - returnNode = d_nm->mkConst(CONST_RATIONAL, sum); - } - } - else - { - uint64_t amount = bv::utils::getSignExtendAmount(original); - if (amount == 0) - { - returnNode = translated_children[0]; - } - else - { - Rational twoToKMinusOne(intpow2(bvsize - 1)); - Node minSigned = d_nm->mkConst(CONST_RATIONAL, twoToKMinusOne); - /* condition checks whether the msb is 1. - * This holds when the integer value is smaller than - * 100...0, which is 2^{bvsize-1}. - */ - Node condition = d_nm->mkNode(kind::LT, arg, minSigned); - Node thenResult = arg; - Node left = maxInt(amount); - Node mul = d_nm->mkNode(kind::MULT, left, pow2(bvsize)); - Node sum = d_nm->mkNode(kind::PLUS, mul, arg); - Node elseResult = sum; - Node ite = d_nm->mkNode(kind::ITE, condition, thenResult, elseResult); - returnNode = ite; - } - } - break; - } - case kind::BITVECTOR_CONCAT: - { - // (concat a b) translates to a*2^k+b, k being the bitwidth of b. - uint64_t bvsizeRight = original[1].getType().getBitVectorSize(); - Node pow2BvSizeRight = pow2(bvsizeRight); - Node a = - d_nm->mkNode(kind::MULT, translated_children[0], pow2BvSizeRight); - Node b = translated_children[1]; - returnNode = d_nm->mkNode(kind::PLUS, a, b); - break; - } - case kind::BITVECTOR_EXTRACT: - { - // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1} - // original = a[i:j] - uint64_t i = bv::utils::getExtractHigh(original); - uint64_t j = bv::utils::getExtractLow(original); - Assert(i >= j); - Node div = d_nm->mkNode( - kind::INTS_DIVISION_TOTAL, translated_children[0], pow2(j)); - returnNode = modpow2(div, i - j + 1); - break; - } - case kind::EQUAL: - { - returnNode = d_nm->mkNode(kind::EQUAL, translated_children); - break; - } - case kind::BITVECTOR_ULT: - { - returnNode = d_nm->mkNode(kind::LT, translated_children); - break; - } - case kind::BITVECTOR_ULE: - { - returnNode = d_nm->mkNode(kind::LEQ, translated_children); - break; - } - case kind::BITVECTOR_UGT: - { - returnNode = d_nm->mkNode(kind::GT, translated_children); - break; - } - case kind::BITVECTOR_UGE: - { - returnNode = d_nm->mkNode(kind::GEQ, translated_children); - break; - } - case kind::LT: - { - returnNode = d_nm->mkNode(kind::LT, translated_children); - break; - } - case kind::LEQ: - { - returnNode = d_nm->mkNode(kind::LEQ, translated_children); - break; - } - case kind::GT: - { - returnNode = d_nm->mkNode(kind::GT, translated_children); - break; - } - case kind::GEQ: - { - returnNode = d_nm->mkNode(kind::GEQ, translated_children); - break; - } - case kind::ITE: - { - returnNode = d_nm->mkNode(oldKind, translated_children); - break; - } - case kind::APPLY_UF: - { - /** - * higher order logic allows comparing between functions - * The translation does not support this, - * as the translated functions may be different outside - * of the bounds that were relevant for the original - * bit-vectors. - */ - if (childrenTypesChanged(original) && logicInfo().isHigherOrder()) - { - throw TypeCheckingExceptionPrivate( - original, - string("Cannot translate to Int: ") + original.toString()); - } - // Insert the translated application term to the cache - returnNode = d_nm->mkNode(kind::APPLY_UF, translated_children); - // Add range constraints if necessary. - // If the original range was a BV sort, the original application of - // the function Must be within the range determined by the - // bitwidth. - if (original.getType().isBitVector()) - { - d_rangeAssertions.insert(mkRangeConstraint( - returnNode, original.getType().getBitVectorSize())); - } - break; - } - case kind::BOUND_VAR_LIST: - { - returnNode = d_nm->mkNode(oldKind, translated_children); - break; - } - case kind::FORALL: - { - returnNode = translateQuantifiedFormula(original); - break; - } - default: - { - Assert(oldKind != kind::EXISTS); // Exists is eliminated by the rewriter. - // In the default case, we have reached an operator that we do not - // translate directly to integers. The children whose types have - // changed from bv to int should be adjusted back to bv and then - // this term is reconstructed. - TypeNode resultingType; - if (original.getType().isBitVector()) - { - resultingType = d_nm->integerType(); - } - else - { - resultingType = original.getType(); - } - Node reconstruction = - reconstructNode(original, resultingType, translated_children); - returnNode = reconstruction; - break; - } - } - Trace("bv-to-int-debug") << "original: " << original << endl; - Trace("bv-to-int-debug") << "returnNode: " << returnNode << endl; - return returnNode; -} - -Node BVToInt::translateNoChildren(Node original) -{ - SkolemManager* sm = d_nm->getSkolemManager(); - Node translation; - Assert(original.isVar() || original.isConst()); - if (original.isVar()) - { - 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 = sm->mkDummySkolem("__bvToInt_var", - d_nm->integerType(), - "Variable introduced in bvToInt " - "pass instead of original variable " - + original.toString()); - uint64_t bvsize = original.getType().getBitVectorSize(); - translation = newVar; - d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize)); - defineBVUFAsIntUF(original, newVar); - } - } - else if (original.getType().isFunction()) - { - translation = translateFunctionSymbol(original); - } - else - { - // variables other than bit-vector variables and function symbols - // are left intact - translation = original; - } - } - else - { - // original is a const - if (original.getKind() == kind::CONST_BITVECTOR) - { - // Bit-vector constants are transformed into their integer value. - BitVector constant(original.getConst<BitVector>()); - Integer c = constant.toInteger(); - translation = d_nm->mkConst(CONST_RATIONAL, Rational(c)); - } - else - { - // Other constants stay the same. - translation = original; - } - } - return translation; -} - -Node BVToInt::translateFunctionSymbol(Node bvUF) -{ - // construct the new function symbol. - Node intUF; - TypeNode tn = bvUF.getType(); - TypeNode bvRange = tn.getRangeType(); - // The function symbol has not been converted yet - vector<TypeNode> bvDomain = tn.getArgTypes(); - vector<TypeNode> intDomain; - /** - * if the original range is a bit-vector sort, - * the new range should be an integer sort. - * Otherwise, we keep the original range. - * Similarly for the domains. - */ - TypeNode intRange = bvRange.isBitVector() ? d_nm->integerType() : bvRange; - for (TypeNode d : bvDomain) - { - intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d); - } - SkolemManager* sm = d_nm->getSkolemManager(); - ostringstream os; - os << "__bvToInt_fun_" << bvUF << "_int"; - intUF = sm->mkDummySkolem( - os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function"); - // introduce a `define-fun` in the smt-engine to keep - // the correspondence between the original - // function symbol and the new one. - defineBVUFAsIntUF(bvUF, intUF); - return intUF; -} - -void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF) -{ - // The resulting term - Node result; - // The type of the resulting term - TypeNode resultType; - // symbolic arguments of original function - vector<Node> args; - if (!bvUF.getType().isFunction()) { - // bvUF is a variable. - // in this case, the result is just the original term - // (it will be casted later if needed) - result = intUF; - resultType = bvUF.getType(); - } else { - // bvUF is a function with arguments - // The arguments need to be casted as well. - TypeNode tn = bvUF.getType(); - resultType = tn.getRangeType(); - vector<TypeNode> bvDomain = tn.getArgTypes(); - // children of the new symbolic application - vector<Node> achildren; - achildren.push_back(intUF); - int i = 0; - for (const TypeNode& d : bvDomain) - { - // Each bit-vector argument is casted to a natural number - // Other arguments are left intact. - Node fresh_bound_var = d_nm->mkBoundVar(d); - args.push_back(fresh_bound_var); - Node castedArg = args[i]; - if (d.isBitVector()) - { - castedArg = castToType(castedArg, d_nm->integerType()); - } - achildren.push_back(castedArg); - i++; - } - result = d_nm->mkNode(kind::APPLY_UF, achildren); - } - // If the result is BV, it needs to be casted back. - result = castToType(result, resultType); - // add the substitution to the preprocessing context, which ensures the - // model for bvUF is correct, as well as substituting it in the input - // assertions when necessary. - if (!args.empty()) - { - result = d_nm->mkNode( - kind::LAMBDA, d_nm->mkNode(kind::BOUND_VAR_LIST, args), result); - } - d_preprocContext->addSubstitution(bvUF, result); -} - -bool BVToInt::childrenTypesChanged(Node n) -{ - bool result = false; - for (const Node& child : n) - { - TypeNode originalType = child.getType(); - TypeNode newType = d_bvToIntCache[child].get().getType(); - if (!newType.isSubtypeOf(originalType)) - { - result = true; - break; - } - } - return result; -} - -Node BVToInt::castToType(Node n, TypeNode tn) -{ - // If there is no reason to cast, return the - // original node. - if (n.getType().isSubtypeOf(tn)) - { - return n; - } - // We only case int to bv or vice verse. - Assert((n.getType().isBitVector() && tn.isInteger()) - || (n.getType().isInteger() && tn.isBitVector())); - if (n.getType().isInteger()) - { - Assert(tn.isBitVector()); - unsigned bvsize = tn.getBitVectorSize(); - Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize)); - return d_nm->mkNode(intToBVOp, n); - } - Assert(n.getType().isBitVector()); - Assert(tn.isInteger()); - return d_nm->mkNode(kind::BITVECTOR_TO_NAT, n); -} - -Node BVToInt::reconstructNode(Node originalNode, - TypeNode resultType, - const vector<Node>& translated_children) -{ - // first, we adjust the children of the node as needed. - // re-construct the term with the adjusted children. - kind::Kind_t oldKind = originalNode.getKind(); - NodeBuilder builder(oldKind); - if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED) - { - builder << originalNode.getOperator(); - } - for (size_t i = 0; i < originalNode.getNumChildren(); i++) - { - Node originalChild = originalNode[i]; - Node translatedChild = translated_children[i]; - Node adjustedChild = castToType(translatedChild, originalChild.getType()); - builder << adjustedChild; - } - Node reconstruction = builder.constructNode(); - // cast to tn in case the reconstruction is a bit-vector. - reconstruction = castToType(reconstruction, resultType); - return reconstruction; -} - BVToInt::BVToInt(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bv-to-int"), - d_binarizeCache(userContext()), - d_eliminationCache(userContext()), - d_rebuildCache(userContext()), - d_bvToIntCache(userContext()), - d_rangeAssertions(userContext()) -{ - d_nm = NodeManager::currentNM(); - d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1)); -}; + d_intBlaster(preprocContext->getEnv(), + options::solveBVAsInt(), + options::BVAndIntegerGranularity()) {} PreprocessingPassResult BVToInt::applyInternal( AssertionPipeline* assertionsToPreprocess) { + // vector of boolean nodes for additional constraints + // this will always contain range constraints + // and for options::SolveBVAsIntMode::BITWISE, it will + // also include bitwise assertion constraints + std::vector<Node> additionalConstraints; + std::map<Node, Node> skolems; for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i) { Node bvNode = (*assertionsToPreprocess)[i]; - Node intNode = bvToInt(bvNode); + Node intNode = + d_intBlaster.intBlast(bvNode, additionalConstraints, skolems); Node rwNode = rewrite(intNode); Trace("bv-to-int-debug") << "bv node: " << bvNode << std::endl; Trace("bv-to-int-debug") << "int node: " << intNode << std::endl; Trace("bv-to-int-debug") << "rw node: " << rwNode << std::endl; assertionsToPreprocess->replace(i, rwNode); } - addFinalizeRangeAssertions(assertionsToPreprocess); + addFinalizeAssertions(assertionsToPreprocess, additionalConstraints); + addSkolemDefinitions(skolems); return PreprocessingPassResult::NO_CONFLICT; } -void BVToInt::addFinalizeRangeAssertions( - AssertionPipeline* assertionsToPreprocess) -{ - // collect the range assertions from d_rangeAssertions - // (which is a context-dependent set) - // into a vector. - vector<Node> vec_range; - vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end()); - // conjoin all range assertions and add the conjunction - // as a new assertion - Node rangeAssertions = rewrite(d_nm->mkAnd(vec_range)); - assertionsToPreprocess->push_back(rangeAssertions); - Trace("bv-to-int-debug") << "range constraints: " - << rangeAssertions.toString() << std::endl; -} - -Node BVToInt::createShiftNode(vector<Node> children, - uint64_t bvsize, - bool isLeftShift) +void BVToInt::addSkolemDefinitions(const std::map<Node, Node>& skolems) { - /** - * from SMT-LIB: - * [[(bvshl s t)]] := nat2bv[m](bv2nat([[s]]) * 2^(bv2nat([[t]]))) - * [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]]))) - * Since we don't have exponentiation, we use an ite. - * Important note: below we use INTS_DIVISION_TOTAL, which is safe here - * because we divide by 2^... which is never 0. - */ - Node x = children[0]; - Node y = children[1]; - // shifting by const is eliminated by the theory rewriter - Assert(!y.isConst()); - Node ite = d_zero; - Node body; - for (uint64_t i = 0; i < bvsize; i++) + map<Node, Node>::const_iterator it; + for (it = skolems.begin(); it != skolems.end(); it++) { - if (isLeftShift) + Node originalSkolem = it->first; + Node definition = it->second; + std::vector<Node> args; + Node body; + if (definition.getType().isFunction()) { - body = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, - d_nm->mkNode(kind::MULT, x, pow2(i)), - pow2(bvsize)); + args.insert(args.end(), definition[0].begin(), definition[0].end()); + body = definition[1]; } else { - body = d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i)); + body = definition; } - ite = d_nm->mkNode( - kind::ITE, - d_nm->mkNode( - kind::EQUAL, y, d_nm->mkConst(CONST_RATIONAL, Rational(i))), - body, - ite); + Trace("bv-to-int-debug") << "adding substitution: " << "[" << originalSkolem << "] ----> [" << definition << "]" << std::endl; + d_preprocContext->addSubstitution(originalSkolem, definition); } - 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<Node> oldBoundVars; - vector<Node> newBoundVars; - vector<Node> 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 = d_nm->mkAnd(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::createBVNotNode(Node n, uint64_t bvsize) +void BVToInt::addFinalizeAssertions( + AssertionPipeline* assertionsToPreprocess, + const std::vector<Node>& additionalConstraints) { - return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n); + NodeManager* nm = NodeManager::currentNM(); + Node lemmas = nm->mkAnd(additionalConstraints); + assertionsToPreprocess->push_back(lemmas); + Trace("bv-to-int-debug") << "range constraints: " << lemmas.toString() + << std::endl; } } // namespace passes diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index d09f9e738..24fc185b5 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -1,6 +1,7 @@ + /****************************************************************************** * Top contributors (to current version): - * Yoni Zohar, Gereon Kremer, Makai Mann + * Yoni Zohar * * This file is part of the cvc5 project. * @@ -10,69 +11,18 @@ * directory for licensing information. * **************************************************************************** * - * The BVToInt preprocessing pass - * - * Converts bit-vector formulas to integer formulas. - * The conversion is implemented using a translation function Tr, - * roughly described as follows: - * - * Tr(x) = fresh_x for every bit-vector variable x, where fresh_x is a fresh - * integer variable. - * Tr(c) = the integer value of c, for any bit-vector constant c. - * Tr((bvadd s t)) = Tr(s) + Tr(t) mod 2^k, where k is the bit width of - * s and t. - * Similar transformations are done for bvmul, bvsub, bvudiv, bvurem, bvneg, - * bvnot, bvconcat, bvextract - * Tr((_ zero_extend m) x) = Tr(x) - * Tr((_ sign_extend m) x) = ite(msb(x)=0, x, 2^k*(2^m-1) + x)) - * explanation: if the msb is 0, this is the same as zero_extend, - * which does not change the integer value. - * If the msb is 1, then the result should correspond to - * concat(1...1, x), with m 1's. - * m 1's is 2^m-1, and multiplying it by x's width (k) moves it - * to the front. - * - * Tr((bvand s t)) depends on the granularity, which is provided by the user - * when enabling this preprocessing pass. - * We divide s and t to blocks. - * The size of each block is the granularity, and so the number of - * blocks is: - * bit width/granularity (rounded down). - * We create an ITE that represents an arbitrary block, - * and then create a sum by mutiplying each block by the - * appropriate power of two. - * More formally: - * Let g denote the granularity. - * Let k denote the bit width of s and t. - * Let b denote floor(k/g) if k >= g, or just k otherwise. - * Tr((bvand s t)) = - * Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g) - * - * Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor. - * - * Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of - * a and b, and ITE represents exponentiation up to k, that is: - * ITE = ite(Tr(b)=0, 1, ite(Tr(b)=1), 2, ite(Tr(b)=2, 4, ...)) - * Similar transformations are done for bvlshr. - * - * Tr(a=b) = Tr(a)=Tr(b) - * Tr((bvult a b)) = Tr(a) < Tr(b) - * Similar transformations are done for bvule, bvugt, and bvuge. - * - * Bit-vector operators that are not listed above are either eliminated using - * the function eliminationPass, or are not supported. - * + * The bv-to-int preprocessing pass. */ -#include "cvc5_private.h" - #ifndef __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H #define __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H #include "context/cdhashmap.h" -#include "context/cdhashset.h" +#include "context/cdo.h" +#include "context/context.h" #include "preprocessing/preprocessing_pass.h" -#include "theory/arith/nl/iand_utils.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/bv/int_blaster.h" namespace cvc5 { namespace preprocessing { @@ -88,200 +38,15 @@ class BVToInt : public PreprocessingPass protected: PreprocessingPassResult applyInternal( AssertionPipeline* assertionsToPreprocess) override; - /** - * A generic function that creates a logical shift node (either left or - * right). a << b gets translated to a * 2^b mod 2^k, where k is the bit - * width. a >> b gets translated to a div 2^b mod 2^k, where k is the bit - * width. The exponentiation operation is translated to an ite for possible - * values of the exponent, from 0 to k-1. - * If the right operand of the shift is greater than k-1, - * the result is 0. - * @param children the two operands for the shift - * @param bvsize the original bit widths of the operands - * (before translation to integers) - * @param isLeftShift true iff the desired operation is a left shift. - * @return a node representing the shift. - * - */ - Node createShiftNode(std::vector<Node> children, - uint64_t bvsize, - bool isLeftShift); - - /** - * Returns a node that represents the bitwise negation of n. - */ - Node createBVNotNode(Node n, uint64_t bvsize); - - /** - * The result is an integer term and is computed - * according to the translation specified above. - * @param n is a bit-vector term or formula to be translated. - * @return integer node that corresponds to n. - */ - Node bvToInt(Node n); - - /** - * Whenever we introduce an integer variable that represents a bit-vector - * variable, we need to guard the range of the newly introduced variable. - * For bit width k, the constraint is 0 <= newVar < 2^k. - * @param newVar the newly introduced integer variable - * @param k the bit width of the original bit-vector variable. - * @return a node representing the range constraint. - */ - Node mkRangeConstraint(Node newVar, uint64_t k); - - /** - * In the translation to integers, it is convenient to assume that certain - * bit-vector operators do not occur in the original formula (e.g., repeat). - * This function eliminates all these operators. - */ - Node eliminationPass(Node n); - - /** - * Some bit-vector operators (e.g., bvadd, bvand) are binary, but allow more - * than two arguments as a syntactic sugar. - * For example, we can have a node for (bvand x y z), - * that represents (bvand (x (bvand y z))). - * This function makes all such operators strictly binary. - */ - Node makeBinary(Node n); - - /** - * @param k A non-negative integer - * @return A node that represents the constant 2^k - */ - Node pow2(uint64_t k); - - /** - * @param k A positive integer k - * @return A node that represent the constant 2^k-1 - * For example, if k is 4, the result is a node representing the - * constant 15. - */ - Node maxInt(uint64_t k); - - /** - * @param n A node representing an integer term - * @param exponent A non-negative integer - * @return A node representing (n mod (2^exponent)) - */ - Node modpow2(Node n, uint64_t exponent); - - bool childrenTypesChanged(Node n); - - /** - * Add the range assertions collected in d_rangeAssertions - * (using mkRangeConstraint) to the assertion pipeline. - * If there are no range constraints, do nothing. - * If there is a single range constraint, add it to the pipeline. - * Otherwise, add all of them as a single conjunction - */ - 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. - * Reconstruction is done by casting to integers/bit-vectors - * as needed. - * For example, if node is (select A x) where A - * is a bit-vector array, we do not change A to be - * an integer array, even though x was translated - * to integers. - * In this case we cast x to (bv2nat x) during - * the reconstruction. - * - * @param originalNode the node that we are reconstructing - * @param resultType the desired type for the reconstruction - * @param translated_children the children of originalNode - * after their translation to integers. - * @return A node with originalNode's operator that has type resultType. - */ - Node reconstructNode(Node originalNode, - TypeNode resultType, - const std::vector<Node>& translated_children); - - /** - * A useful utility function. - * if n is an integer and tn is bit-vector, - * applies the IntToBitVector operator on n. - * if n is a vit-vector and tn is integer, - * applies BitVector_TO_NAT operator. - * Otherwise, keeps n intact. - */ - Node castToType(Node n, TypeNode tn); - - /** - * When a UF f is translated to a UF g, - * we add a define-fun command to the smt-engine - * to relate between f and g. - * We do the same when f and g are just variables. - * This is useful, for example, when asking - * for a model-value of a term that includes the - * original UF f. - * @param bvUF the original function or variable - * @param intUF the translated function or variable - */ - void defineBVUFAsIntUF(Node bvUF, Node intUF); - - /** - * @param bvUF is an uninterpreted function symbol from the original formula - * @return a fresh uninterpreted function symbol, obtained from bvUF - by replacing every argument of type BV to an argument of type Integer, - and the return type becomes integer in case it was BV. - */ - Node translateFunctionSymbol(Node bvUF); - - /** - * Performs the actual translation to integers for nodes - * that have children. - */ - Node translateWithChildren(Node original, - const std::vector<Node>& translated_children); - - /** - * Performs the actual translation to integers for nodes - * that don't have children (variables, constants, uninterpreted function - * symbols). - */ - Node translateNoChildren(Node original); - - /** - * Caches for the different functions - */ - CDNodeMap d_binarizeCache; - CDNodeMap d_eliminationCache; - CDNodeMap d_rebuildCache; - CDNodeMap d_bvToIntCache; - /** - * Node manager that is used throughout the pass - */ - NodeManager* d_nm; + // Add the lemmas in `additionalConstraints` to the assertions pipeline. + void addFinalizeAssertions(AssertionPipeline* assertionsToPreprocess, + const std::vector<Node>& additionalConstraints); - /** - * A set of constraints of the form 0 <= x < 2^k - * These are added for every new integer variable that we introduce. - */ - context::CDHashSet<Node> d_rangeAssertions; + // include the skolem map as substitutions + void addSkolemDefinitions(const std::map<Node, Node>& skolems); - /** - * Useful constants - */ - Node d_zero; - Node d_one; - - /** helper class for handeling bvand translation */ - theory::arith::nl::IAndUtils d_iandUtils; + IntBlaster d_intBlaster; }; } // namespace passes diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index e6b5a4bca..2ff45aef0 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -235,25 +235,19 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) } else if (current.isConst()) { - switch (current.getKind()) + if (current.getType().isInteger()) { - case kind::CONST_RATIONAL: + Rational constant = current.getConst<Rational>(); + Assert (constant.isIntegral()); + BitVector bv(size, constant.getNumerator()); + if (bv.toSignedInteger() != constant.getNumerator()) { - Rational constant = current.getConst<Rational>(); - if (constant.isIntegral()) { - BitVector bv(size, constant.getNumerator()); - if (bv.toSignedInteger() != constant.getNumerator()) - { - throw TypeCheckingExceptionPrivate( - current, - string("Not enough bits for constant in intToBV: ") - + current.toString()); - } - result = nm->mkConst(bv); - } - break; + throw TypeCheckingExceptionPrivate( + current, + string("Not enough bits for constant in intToBV: ") + + current.toString()); } - default: break; + result = nm->mkConst(bv); } } else diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp index 642a63aa4..3922525f2 100644 --- a/src/preprocessing/passes/learned_rewrite.cpp +++ b/src/preprocessing/passes/learned_rewrite.cpp @@ -61,7 +61,7 @@ PreprocessingPassResult LearnedRewrite::applyInternal( AssertionPipeline* assertionsToPreprocess) { NodeManager* nm = NodeManager::currentNM(); - arith::BoundInference binfer; + arith::BoundInference binfer(d_env); std::vector<Node> learnedLits = d_preprocContext->getLearnedLiterals(); std::unordered_set<Node> llrw; std::unordered_map<TNode, Node> visited; diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 66646b766..1be5ee81b 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -213,8 +213,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)), - one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = nm->mkConstInt(Rational(0)), one = nm->mkConstInt(Rational(1)); Node trueNode = nm->mkConst(true); unordered_map<TNode, Node> intVars; @@ -276,10 +275,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( break; } if ((*j1)[1].getKind() != kind::EQUAL - || !(((*j1)[1][0].isVar() - && (*j1)[1][1].getKind() == kind::CONST_RATIONAL) - || ((*j1)[1][0].getKind() == kind::CONST_RATIONAL - && (*j1)[1][1].isVar()))) + || !(((*j1)[1][0].isVar() && (*j1)[1][1].isConst()) + || ((*j1)[1][0].isConst() && (*j1)[1][1].isVar()))) { eligible = false; Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl; @@ -332,14 +329,11 @@ PreprocessingPassResult MipLibTrick::applyInternal( } sort(posv.begin(), posv.end()); const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv); - const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j1)[1][1] - : (*j1)[1][0]; + const TNode var = ((*j1)[1][0].isConst()) ? (*j1)[1][1] : (*j1)[1][0]; const pair<Node, Node> pos_var(pos, var); - const Rational& constant = - ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j1)[1][0].getConst<Rational>() - : (*j1)[1][1].getConst<Rational>(); + const Rational& constant = ((*j1)[1][0].isConst()) + ? (*j1)[1][0].getConst<Rational>() + : (*j1)[1][1].getConst<Rational>(); uint64_t mark = 0; unsigned countneg = 0, thepos = 0; for (unsigned ii = 0; ii < pos.getNumChildren(); ++ii) @@ -406,14 +400,11 @@ PreprocessingPassResult MipLibTrick::applyInternal( const bool xneg = (x.getKind() == kind::NOT); x = xneg ? x[0] : x; Debug("miplib") << " x:" << x << " " << xneg << endl; - const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j1)[1][1] - : (*j1)[1][0]; + const TNode var = ((*j1)[1][0].isConst()) ? (*j1)[1][1] : (*j1)[1][0]; const pair<Node, Node> x_var(x, var); - const Rational& constant = - ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j1)[1][0].getConst<Rational>() - : (*j1)[1][1].getConst<Rational>(); + const Rational& constant = ((*j1)[1][0].isConst()) + ? (*j1)[1][0].getConst<Rational>() + : (*j1)[1][1].getConst<Rational>(); unsigned mark = (xneg ? 0 : 1); if ((marks[x_var] & (1u << mark)) != 0) { @@ -573,17 +564,15 @@ PreprocessingPassResult MipLibTrick::applyInternal( NodeBuilder sumb(kind::PLUS); for (size_t jj = 0; jj < pos.getNumChildren(); ++jj) { - sumb << nm->mkNode(kind::MULT, - nm->mkConst(CONST_RATIONAL, coef[pos_var][jj]), - newVars[jj]); + sumb << nm->mkNode( + kind::MULT, nm->mkConstInt(coef[pos_var][jj]), newVars[jj]); } sum = sumb; } else { - sum = nm->mkNode(kind::MULT, - nm->mkConst(CONST_RATIONAL, coef[pos_var][0]), - newVars[0]); + sum = nm->mkNode( + kind::MULT, nm->mkConstInt(coef[pos_var][0]), newVars[0]); } Debug("miplib") << "vars[] " << var << endl << " eq " << rewrite(sum) << endl; diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 4bf29157e..247a8b72e 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -120,6 +120,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( << " learned literals." << std::endl; // No conflict, go through the literals and solve them context::Context* u = userContext(); + Rewriter* rw = d_env.getRewriter(); TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions(); CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get(); // constant propagations @@ -228,7 +229,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( c = learnedLiteral[1]; } Assert(!t.isConst()); - Assert(cps.apply(t, true) == t); + Assert(rewrite(cps.apply(t)) == t); Assert(top_level_substs.apply(t) == t); Assert(nss.apply(t) == t); // also add to learned literal @@ -293,7 +294,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { Node assertion = (*assertionsToPreprocess)[i]; - TrustNode assertionNew = newSubstitutions->applyTrusted(assertion); + TrustNode assertionNew = newSubstitutions->applyTrusted(assertion, rw); Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl; if (!assertionNew.isNull()) { @@ -305,7 +306,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } for (;;) { - assertionNew = constantPropagations->applyTrusted(assertion); + assertionNew = constantPropagations->applyTrusted(assertion, rw); if (assertionNew.isNull()) { break; @@ -340,7 +341,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( if (d_preprocContext->getSymsInAssertions().contains(lhs)) { // if it has, the substitution becomes an assertion - TrustNode trhs = newSubstitutions->applyTrusted(lhs); + TrustNode trhs = newSubstitutions->applyTrusted(lhs, rw); Assert(!trhs.isNull()); Trace("non-clausal-simplify") << "substitute: will notify SAT layer of substitution: " @@ -446,10 +447,11 @@ Node NonClausalSimp::processLearnedLit(Node lit, theory::TrustSubstitutionMap* subs, theory::TrustSubstitutionMap* cp) { + Rewriter* rw = d_env.getRewriter(); TrustNode tlit; if (subs != nullptr) { - tlit = subs->applyTrusted(lit); + tlit = subs->applyTrusted(lit, rw); if (!tlit.isNull()) { lit = processRewrittenLearnedLit(tlit); @@ -462,7 +464,7 @@ Node NonClausalSimp::processLearnedLit(Node lit, { for (;;) { - tlit = cp->applyTrusted(lit); + tlit = cp->applyTrusted(lit, rw); if (tlit.isNull()) { break; diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index 6c93eba15..0e7ac9c79 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -66,7 +66,7 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated) Node l = assertion[0]; Node r = assertion[1]; - if (r.getKind() != kind::CONST_RATIONAL) + if (!r.isConst()) { Debug("pbs::rewrites") << "not rhs constant" << assertion << std::endl; return false; @@ -216,7 +216,7 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, Node l = assertion[0]; Node r = assertion[1]; - if (r.getKind() == kind::CONST_RATIONAL) + if (r.isConst()) { const Rational& rc = r.getConst<Rational>(); if (isIntVar(l)) @@ -233,8 +233,7 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, else if (l.getKind() == kind::MULT && l.getNumChildren() == 2) { Node c = l[0], v = l[1]; - if (c.getKind() == kind::CONST_RATIONAL - && c.getConst<Rational>().isNegativeOne()) + if (c.isConst() && c.getConst<Rational>().isNegativeOne()) { if (isIntVar(v)) { diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 5c4539808..d2cde7b46 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -78,8 +78,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va if (!c.isNull()) { Assert(c.isConst()); - coeffs.push_back(NodeManager::currentNM()->mkConst( - CONST_RATIONAL, + coeffs.push_back(nm->mkConstInt( Rational(c.getConst<Rational>().getDenominator()))); } } @@ -134,15 +133,10 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va } Node sumt = sum.empty() - ? NodeManager::currentNM()->mkConst(CONST_RATIONAL, - Rational(0)) - : (sum.size() == 1 - ? sum[0] - : NodeManager::currentNM()->mkNode(kind::PLUS, sum)); - ret = NodeManager::currentNM()->mkNode( - ret_lit.getKind(), - sumt, - NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))); + ? nm->mkConstInt(Rational(0)) + : (sum.size() == 1 ? sum[0] : nm->mkNode(kind::PLUS, sum)); + ret = nm->mkNode( + ret_lit.getKind(), sumt, nm->mkConstInt(Rational(0))); if (!ret_pol) { ret = ret.negate(); diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 3da75beb2..cdbd6099e 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -301,14 +301,13 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, Trace("sygus-infer") << "*** Check sat..." << std::endl; Result r = rrSygus->checkSat(); Trace("sygus-infer") << "...result : " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + // get the synthesis solutions + std::map<Node, Node> synth_sols; + if (!rrSygus->getSubsolverSynthSolutions(synth_sols)) { // failed, conjecture was infeasible return false; } - // get the synthesis solutions - std::map<Node, Node> synth_sols; - rrSygus->getSynthSolutions(synth_sols); std::vector<Node> final_ff; std::vector<Node> final_ff_sol; diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index ae05d6b87..027be232b 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -515,9 +515,9 @@ void UnconstrainedSimplifier::processUnconstrained() if (current.getType().isInteger()) { // div/mult by 1 should have been simplified - Assert(other != nm->mkConst(CONST_RATIONAL, Rational(1))); + Assert(other != nm->mkConstInt(Rational(1))); // div by -1 should have been simplified - if (other != nm->mkConst(CONST_RATIONAL, Rational(-1))) + if (other != nm->mkConstInt(Rational(-1))) { break; } |