diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/abstraction.cpp | 352 | ||||
-rw-r--r-- | src/theory/bv/abstraction.h | 90 | ||||
-rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 26 | ||||
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 37 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 6 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 25 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 184 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 47 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 4 |
12 files changed, 407 insertions, 377 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index fdc36ce72..dc5520411 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -41,7 +41,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st continue; } Node signature = computeSignature(assertions[i][j]); - storeSignature(signature, assertions[i][j]); + storeSignature(signature, assertions[i][j]); Debug("bv-abstraction") << " assertion: " << assertions[i][j] <<"\n"; Debug("bv-abstraction") << " signature: " << signature <<"\n"; } @@ -52,7 +52,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st for (unsigned i = 0; i < assertions.size(); ++i) { if (assertions[i].getKind() == kind::OR && assertions[i][0].getKind() == kind::AND) { - std::vector<Node> new_children; + std::vector<Node> new_children; for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) { if (hasSignature(assertions[i][j])) { new_children.push_back(abstractSignatures(assertions[i][j])); @@ -60,10 +60,10 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st new_children.push_back(assertions[i][j]); } } - new_assertions.push_back(utils::mkNode(kind::OR, new_children)); + new_assertions.push_back(utils::mkNode(kind::OR, new_children)); } else { // assertions that are not changed - new_assertions.push_back(assertions[i]); + new_assertions.push_back(assertions[i]); } } @@ -71,21 +71,21 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st skolemizeArguments(new_assertions); } - + // if we are using the eager solver reverse the abstraction if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { if (d_funcToSignature.size() == 0) { // we did not change anything return false; } - NodeNodeMap seen; + NodeNodeMap seen; for (unsigned i = 0; i < new_assertions.size(); ++i) { - new_assertions[i] = reverseAbstraction(new_assertions[i], seen); + new_assertions[i] = reverseAbstraction(new_assertions[i], seen); } // we undo the abstraction functions so the logic is QF_BV still - return true; + return true; } - + // return true if we have created new function symbols for the problem return d_funcToSignature.size() != 0; } @@ -99,7 +99,7 @@ bool AbstractionModule::isConjunctionOfAtoms(TNode node) { bool AbstractionModule::isConjunctionOfAtomsRec(TNode node, TNodeSet& seen) { if (seen.find(node)!= seen.end()) return true; - + if (!node.getType().isBitVector()) { return (node.getKind() == kind::AND || utils::isBVPredicate(node)); } @@ -120,30 +120,30 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) { if (seen.find(assertion) != seen.end()) return seen[assertion]; - + if (isAbstraction(assertion)) { Node interp = getInterpretation(assertion); seen[assertion] = interp; - Assert (interp.getType() == assertion.getType()); + Assert (interp.getType() == assertion.getType()); return interp; } if (assertion.getNumChildren() == 0) { seen[assertion] = assertion; - return assertion; + return assertion; } - + NodeBuilder<> result(assertion.getKind()); if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) { - result << assertion.getOperator(); + result << assertion.getOperator(); } for (unsigned i = 0; i < assertion.getNumChildren(); ++i) { - result << reverseAbstraction(assertion[i], seen); + result << reverseAbstraction(assertion[i], seen); } Node res = result; seen[assertion] = res; - return res; + return res; } void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) { @@ -151,7 +151,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) { TNode assertion = assertions[i]; if (assertion.getKind() != kind::OR) continue; - + bool is_skolemizable = true; for (unsigned k = 0; k < assertion.getNumChildren(); ++k) { if (assertion[k].getKind() != kind::EQUAL || @@ -191,54 +191,54 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) { NodeBuilder<> skolem_func (kind::APPLY_UF); skolem_func << func; std::vector<Node> skolem_args; - + for (unsigned j = 0; j < args.getArity(); ++j) { bool all_same = true; for (unsigned k = 1; k < args.getNumEntries(); ++k) { if ( args.getEntry(k)[j] != args.getEntry(0)[j]) - all_same = false; + all_same = false; } - Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j])); + Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j])); skolem_args.push_back(new_arg); - skolem_func << new_arg; + skolem_func << new_arg; } - - Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); - + + Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); + // enumerate arguments assignments - std::vector<Node> or_assignments; + std::vector<Node> or_assignments; for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) { NodeBuilder<> arg_assignment(kind::AND); ArgsVec& args = *it; for (unsigned k = 0; k < args.size(); ++k) { Node eq = utils::mkNode(kind::EQUAL, args[k], skolem_args[k]); - arg_assignment << eq; + arg_assignment << eq; } or_assignments.push_back(arg_assignment); } - + Node new_func_def = utils::mkNode(kind::AND, skolem_func_eq1, utils::mkNode(kind::OR, or_assignments)); - assertion_builder << new_func_def; + assertion_builder << new_func_def; } Node new_assertion = assertion_builder; Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " << assertions[i] << " => \n"; - Debug("bv-abstraction-dbg") << " " << new_assertion; + Debug("bv-abstraction-dbg") << " " << new_assertion; assertions[i] = new_assertion; } } void AbstractionModule::storeSignature(Node signature, TNode assertion) { if(d_signatures.find(signature) == d_signatures.end()) { - d_signatures[signature] = 0; + d_signatures[signature] = 0; } - d_signatures[signature] = d_signatures[signature] + 1; - d_assertionToSignature[assertion] = signature; + d_signatures[signature] = d_signatures[signature] + 1; + d_assertionToSignature[assertion] = signature; } Node AbstractionModule::computeSignature(TNode node) { - resetSignatureIndex(); - NodeNodeMap cache; + resetSignatureIndex(); + NodeNodeMap cache; Node sig = computeSignatureRec(node, cache); return sig; } @@ -247,17 +247,17 @@ Node AbstractionModule::getSignatureSkolem(TNode node) { Assert (node.getKind() == kind::VARIABLE); unsigned bitwidth = utils::getSize(node); if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) { - d_signatureSkolems[bitwidth] = vector<Node>(); + d_signatureSkolems[bitwidth] = vector<Node>(); } - + vector<Node>& skolems = d_signatureSkolems[bitwidth]; // get the index of bv variables of this size - unsigned index = getBitwidthIndex(bitwidth); + unsigned index = getBitwidthIndex(bitwidth); Assert (skolems.size() + 1 >= index ); if (skolems.size() == index) { ostringstream os; os << "sig_" <<bitwidth <<"_" << index; - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); skolems.push_back(nm->mkSkolem(os.str(), nm->mkBitVectorType(bitwidth), "skolem for computing signatures")); } ++(d_signatureIndices[bitwidth]); @@ -268,12 +268,12 @@ unsigned AbstractionModule::getBitwidthIndex(unsigned bitwidth) { if (d_signatureIndices.find(bitwidth) == d_signatureIndices.end()) { d_signatureIndices[bitwidth] = 0; } - return d_signatureIndices[bitwidth]; + return d_signatureIndices[bitwidth]; } void AbstractionModule::resetSignatureIndex() { for (IndexMap::iterator it = d_signatureIndices.begin(); it != d_signatureIndices.end(); ++it) { - it->second = 0; + it->second = 0; } } @@ -282,24 +282,24 @@ bool AbstractionModule::hasSignature(Node node) { } Node AbstractionModule::getGeneralizedSignature(Node node) { - NodeNodeMap::const_iterator it = d_assertionToSignature.find(node); + NodeNodeMap::const_iterator it = d_assertionToSignature.find(node); Assert (it != d_assertionToSignature.end()); - Node generalized_signature = getGeneralization(it->second); - return generalized_signature; + Node generalized_signature = getGeneralization(it->second); + return generalized_signature; } Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) { if (cache.find(node) != cache.end()) { - return cache.find(node)->second; + return cache.find(node)->second; } - + if (node.getNumChildren() == 0) { if (node.getKind() == kind::CONST_BITVECTOR) return node; Node sig = getSignatureSkolem(node); - cache[node] = sig; - return sig; + cache[node] = sig; + return sig; } NodeBuilder<> builder(node.getKind()); @@ -308,30 +308,30 @@ Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) { } for (unsigned i = 0; i < node.getNumChildren(); ++i) { Node converted = computeSignatureRec(node[i], cache); - builder << converted; + builder << converted; } Node result = builder; cache[node] = result; - return result; + return result; } -/** +/** * Returns 0, if the two are equal, * 1 if s is a generalization of t * 2 if t is a generalization of s * -1 if the two cannot be unified * - * @param s - * @param t - * - * @return + * @param s + * @param t + * + * @return */ int AbstractionModule::comparePatterns(TNode s, TNode t) { if (s.getKind() == kind::SKOLEM && t.getKind() == kind::SKOLEM) { return 0; } - + if (s.getKind() == kind::CONST_BITVECTOR && t.getKind() == kind::CONST_BITVECTOR) { if (s == t) { @@ -350,7 +350,7 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) { t.getKind() == kind::SKOLEM) { return 2; } - + if (s.getNumChildren() != t.getNumChildren() || s.getKind() != t.getKind()) return -1; @@ -370,26 +370,26 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) { } TNode AbstractionModule::getGeneralization(TNode term) { - NodeNodeMap::iterator it = d_sigToGeneralization.find(term); + NodeNodeMap::iterator it = d_sigToGeneralization.find(term); // if not in the map we add it if (it == d_sigToGeneralization.end()) { d_sigToGeneralization[term] = term; - return term; + return term; } - // doesn't have a generalization + // doesn't have a generalization if (it->second == term) return term; - + TNode generalization = getGeneralization(it->second); Assert (generalization != term); d_sigToGeneralization[term] = generalization; - return generalization; + return generalization; } void AbstractionModule::storeGeneralization(TNode s, TNode t) { Assert (s == getGeneralization(s)); Assert (t == getGeneralization(t)); - d_sigToGeneralization[s] = t; + d_sigToGeneralization[s] = t; } void AbstractionModule::finalizeSignatures() { @@ -402,29 +402,29 @@ void AbstractionModule::finalizeSignatures() { for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) { TNode t = getGeneralization(tt->first); TNode s = getGeneralization(ss->first); - + if (t != s) { int status = comparePatterns(s, t); - Assert (status); + Assert (status); if (status < 0) continue; if (status == 1) { - storeGeneralization(t, s); + storeGeneralization(t, s); } else { - storeGeneralization(s, t); + storeGeneralization(s, t); } } } } // keep only most general signatures for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) { - TNode sig = it->first; + TNode sig = it->first; TNode gen = getGeneralization(sig); if (sig != gen) { - Assert (d_signatures.find(gen) != d_signatures.end()); + Assert (d_signatures.find(gen) != d_signatures.end()); // update the count d_signatures[gen]+= d_signatures[sig]; - d_signatures.erase(it++); + d_signatures.erase(it++); } else { ++it; } @@ -434,12 +434,12 @@ void AbstractionModule::finalizeSignatures() { // remove signatures that are not frequent enough for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) { if (it->second <= 7) { - d_signatures.erase(it++); + d_signatures.erase(it++); } else { ++it; } } - + for (SignatureMap::const_iterator it = d_signatures.begin(); it != d_signatures.end(); ++it) { TNode signature = it->first; // we already processed this signature @@ -451,31 +451,31 @@ void AbstractionModule::finalizeSignatures() { collectArgumentTypes(signature, arg_types, seen); Assert (signature.getType().isBoolean()); // make function return a bitvector of size 1 - //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u)); + //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u)); TypeNode range = NodeManager::currentNM()->mkBitVectorType(1); - + TypeNode abs_type = nm->mkFunctionType(arg_types, range); Node abs_func = nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory"); Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n"; // NOTE: signature expression type is BOOLEAN d_signatureToFunc[signature] = abs_func; - d_funcToSignature[abs_func] = signature; + d_funcToSignature[abs_func] = signature; } d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size()); - + Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " << d_signatureToFunc.size() << " signatures. \n"; } void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen) { if (seen.find(sig) != seen.end()) return; - + if (sig.getKind() == kind::SKOLEM) { types.push_back(sig.getType()); - seen.insert(sig); - return; + seen.insert(sig); + return; } for (unsigned i = 0; i < sig.getNumChildren(); ++i) { @@ -487,36 +487,36 @@ void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& t void AbstractionModule::collectArguments(TNode node, TNode signature, std::vector<Node>& args, TNodeSet& seen) { if (seen.find(node)!= seen.end()) return; - + if (node.getKind() == kind::VARIABLE || node.getKind() == kind::CONST_BITVECTOR) { // a constant in the node can either map to an argument of the abstraction - // or can be hard-coded and part of the abstraction + // or can be hard-coded and part of the abstraction if (signature.getKind() == kind::SKOLEM) { args.push_back(node); seen.insert(node); } else { - Assert (signature.getKind() == kind::CONST_BITVECTOR); + Assert (signature.getKind() == kind::CONST_BITVECTOR); } - // - return; + // + return; } Assert (node.getKind() == signature.getKind() && - node.getNumChildren() == signature.getNumChildren()); + node.getNumChildren() == signature.getNumChildren()); for (unsigned i = 0; i < node.getNumChildren(); ++i) { - collectArguments(node[i], signature[i], args, seen); - seen.insert(node); + collectArguments(node[i], signature[i], args, seen); + seen.insert(node); } } Node AbstractionModule::abstractSignatures(TNode assertion) { - Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n"; + Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n"; // assume the assertion has been fully abstracted Node signature = getGeneralizedSignature(assertion); - - Debug("bv-abstraction") << " with sig "<< signature <<"\n"; + + Debug("bv-abstraction") << " with sig "<< signature <<"\n"; NodeNodeMap::iterator it = d_signatureToFunc.find(signature); if (it!= d_signatureToFunc.end()) { std::vector<Node> args; @@ -527,16 +527,16 @@ Node AbstractionModule::abstractSignatures(TNode assertion) { collectArguments(assertion, signature, args, seen); std::vector<TNode> real_args; for (unsigned i = 1; i < args.size(); ++i) { - real_args.push_back(args[i]); + real_args.push_back(args[i]); } - d_argsTable.addEntry(func, real_args); - Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args), + d_argsTable.addEntry(func, real_args); + Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args), utils::mkConst(1, 1u)); - Debug("bv-abstraction") << "=> "<< result << "\n"; - Assert (result.getType() == assertion.getType()); - return result; + Debug("bv-abstraction") << "=> "<< result << "\n"; + Assert (result.getType() == assertion.getType()); + return result; } - return assertion; + return assertion; } bool AbstractionModule::isAbstraction(TNode node) { @@ -557,11 +557,11 @@ bool AbstractionModule::isAbstraction(TNode node) { if (constant != utils::mkConst(1, 1u)) return false; - TNode func_symbol = func.getOperator(); + TNode func_symbol = func.getOperator(); if (d_funcToSignature.find(func_symbol) == d_funcToSignature.end()) return false; - return true; + return true; } Node AbstractionModule::getInterpretation(TNode node) { @@ -571,51 +571,51 @@ Node AbstractionModule::getInterpretation(TNode node) { Assert (constant.getKind() == kind::CONST_BITVECTOR && apply.getKind() == kind::APPLY_UF); - Node func = apply.getOperator(); + Node func = apply.getOperator(); Assert (d_funcToSignature.find(func) != d_funcToSignature.end()); - + Node sig = d_funcToSignature[func]; - + // substitute arguments in signature TNodeTNodeMap seen; unsigned index = 0; Node result = substituteArguments(sig, apply, index, seen); - Assert (result.getType().isBoolean()); + Assert (result.getType().isBoolean()); Assert (index == apply.getNumChildren()); // Debug("bv-abstraction") << "AbstractionModule::getInterpretation " << node << "\n"; // Debug("bv-abstraction") << " => " << result << "\n"; - return result; + return result; } Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsigned& index, TNodeTNodeMap& seen) { if (seen.find(signature) != seen.end()) { - return seen[signature]; + return seen[signature]; } - + if (signature.getKind() == kind::SKOLEM) { // return corresponding argument and increment counter seen[signature] = apply[index]; - return apply[index++]; + return apply[index++]; } if (signature.getNumChildren() == 0) { Assert (signature.getKind() != kind::VARIABLE && - signature.getKind() != kind::SKOLEM); + signature.getKind() != kind::SKOLEM); seen[signature] = signature; - return signature; + return signature; } - + NodeBuilder<> builder(signature.getKind()); if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << signature.getOperator(); } - + for (unsigned i = 0; i < signature.getNumChildren(); ++i) { Node child = substituteArguments(signature[i], apply, index, seen); - builder << child; + builder << child; } - Node result = builder; + Node result = builder; seen[signature]= result; return result; @@ -625,20 +625,20 @@ Node AbstractionModule::simplifyConflict(TNode conflict) { if (Dump.isOn("bv-abstraction")) { NodeNodeMap seen; Node c = reverseAbstraction(conflict, seen); - Dump("bv-abstraction") << PushCommand(); + Dump("bv-abstraction") << PushCommand(); Dump("bv-abstraction") << AssertCommand(c.toExpr()); Dump("bv-abstraction") << CheckSatCommand(); - Dump("bv-abstraction") << PopCommand(); + Dump("bv-abstraction") << PopCommand(); } - Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n"; + Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n"; if (conflict.getKind() != kind::AND) - return conflict; + return conflict; std::vector<Node> conjuncts; for (unsigned i = 0; i < conflict.getNumChildren(); ++i) conjuncts.push_back(conflict[i]); - + theory::SubstitutionMap subst(new context::Context()); for (unsigned i = 0; i < conjuncts.size(); ++i) { TNode conjunct = conjuncts[i]; @@ -658,12 +658,12 @@ Node AbstractionModule::simplifyConflict(TNode conflict) { } else { continue; } - + Assert (!subst.hasSubstitution(s)); Assert (!t.isNull() && !s.isNull() && s!= t); - subst.addSubstitution(s, t); + subst.addSubstitution(s, t); for (unsigned k = 0; k < conjuncts.size(); k++) { conjuncts[k] = subst.apply(conjuncts[k]); @@ -671,28 +671,28 @@ Node AbstractionModule::simplifyConflict(TNode conflict) { } } Node new_conflict = Rewriter::rewrite(utils::mkAnd(conjuncts)); - + Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n"; Debug("bv-abstraction") << " => " << new_conflict <<"\n"; if (Dump.isOn("bv-abstraction")) { - + NodeNodeMap seen; Node nc = reverseAbstraction(new_conflict, seen); - Dump("bv-abstraction") << PushCommand(); + Dump("bv-abstraction") << PushCommand(); Dump("bv-abstraction") << AssertCommand(nc.toExpr()); Dump("bv-abstraction") << CheckSatCommand(); - Dump("bv-abstraction") << PopCommand(); + Dump("bv-abstraction") << PopCommand(); } - - return new_conflict; + + return new_conflict; } void DebugPrintInstantiations(const std::vector< std::vector<ArgsVec> >& instantiations, const std::vector<TNode> functions) { // print header - Debug("bv-abstraction-dbg") <<"[ "; + Debug("bv-abstraction-dbg") <<"[ "; for (unsigned i = 0; i < functions.size(); ++i) { for (unsigned j = 1; j < functions[i].getNumChildren(); ++j) { Debug("bv-abstraction-dgb") << functions[i][j] <<" "; @@ -706,16 +706,16 @@ void DebugPrintInstantiations(const std::vector< std::vector<ArgsVec> >& instant const std::vector<ArgsVec>& inst = instantiations[i]; for (unsigned j = 0; j < inst.size(); ++j) { for (unsigned k = 0; k < inst[j].size(); ++k) { - Debug("bv-abstraction-dbg") << inst[j][k] << " "; + Debug("bv-abstraction-dbg") << inst[j][k] << " "; } - Debug("bv-abstraction-dbg") << " || "; + Debug("bv-abstraction-dbg") << " || "; } Debug("bv-abstraction-dbg") <<"]\n"; } } void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& lemmas) { - Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; + Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; std::vector<TNode> functions; // collect abstract functions @@ -737,11 +737,11 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le // if (functions.size() >= 3) { // // dump conflict // NodeNodeMap seen; - // Node reversed = reverseAbstraction(conflict, seen); - // std::cout << "CONFLICT " << reversed << "\n"; + // Node reversed = reverseAbstraction(conflict, seen); + // std::cout << "CONFLICT " << reversed << "\n"; // } - + if (functions.size() == 0 || functions.size() > options::bvNumFunc()) { return; } @@ -751,31 +751,31 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le SubstitutionMap skolem_subst(new context::Context()); SubstitutionMap reverse_skolem(new context::Context()); makeFreshSkolems(conflict, skolem_subst, reverse_skolem); - + Node skolemized_conflict = skolem_subst.apply(conflict); for (unsigned i = 0; i < functions.size(); ++i) { functions[i] = skolem_subst.apply(functions[i]); } - conflict = skolem_subst.apply(conflict); + conflict = skolem_subst.apply(conflict); LemmaInstantiatior inst(functions, d_argsTable, conflict); std::vector<Node> new_lemmas; - inst.generateInstantiations(new_lemmas); + inst.generateInstantiations(new_lemmas); for (unsigned i = 0; i < new_lemmas.size(); ++i) { TNode lemma = reverse_skolem.apply(new_lemmas[i]); if (d_addedLemmas.find(lemma) == d_addedLemmas.end()) { lemmas.push_back(lemma); - Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n"; + Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n"; storeLemma(lemma); if (Dump.isOn("bv-abstraction")) { NodeNodeMap seen; Node l = reverseAbstraction(lemma, seen); - Dump("bv-abstraction") << PushCommand(); + Dump("bv-abstraction") << PushCommand(); Dump("bv-abstraction") << AssertCommand(l.toExpr()); Dump("bv-abstraction") << CheckSatCommand(); - Dump("bv-abstraction") << PopCommand(); + Dump("bv-abstraction") << PopCommand(); } } } @@ -787,18 +787,18 @@ int AbstractionModule::LemmaInstantiatior::next(int val, int index) { return -1; } -/** +/** * Assumes the stack without top is consistent, and checks that the * full stack is consistent - * - * @param stack - * - * @return + * + * @param stack + * + * @return */ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stack) { if (stack.empty()) return true; - + unsigned current = stack.size() - 1; TNode func = d_functions[current]; ArgsTableEntry& matches = d_argsTable.getEntry(func.getOperator()); @@ -807,12 +807,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac for (unsigned k = 0; k < args.size(); ++k) { TNode s = func[k]; TNode t = args[k]; - + TNode s0 = s; while (d_subst.hasSubstitution(s0)) { s0 = d_subst.getSubstitution(s0); } - + TNode t0 = t; while (d_subst.hasSubstitution(t0)) { t0 = d_subst.getSubstitution(t0); @@ -824,7 +824,7 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac else continue; } - + if(s0.getMetaKind() == kind::metakind::VARIABLE && t0.isConst()) { d_subst.addSubstitution(s0, t0); @@ -839,12 +839,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac Assert (s0.getMetaKind() == kind::metakind::VARIABLE && t0.getMetaKind() == kind::metakind::VARIABLE); - + if (s0 != t0) { d_subst.addSubstitution(s0, t0); } } - return true; + return true; } bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) { @@ -854,13 +854,13 @@ bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) { void AbstractionModule::LemmaInstantiatior::mkLemma() { Node lemma = d_subst.apply(d_conflict); // Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::mkLemma " << lemma <<"\n"; - d_lemmas.push_back(lemma); + d_lemmas.push_back(lemma); } void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) { if (!isConsistent(stack)) return; - + if (accept(stack)) { mkLemma(); return; @@ -871,7 +871,7 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) { d_ctx->push(); stack.push_back(x); backtrack(stack); - + d_ctx->pop(); stack.pop_back(); x = next(x, stack.size()); @@ -880,13 +880,13 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) { void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector<Node>& lemmas) { - Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; + Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; std::vector<int> stack; backtrack(stack); - Assert (d_ctx->getLevel() == 0); - Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n"; - lemmas.swap(d_lemmas); + Assert (d_ctx->getLevel() == 0); + Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n"; + lemmas.swap(d_lemmas); } void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map) { @@ -910,7 +910,7 @@ void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, Subst void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args) { Assert (fresh_args.size() == 0); Assert (func.getKind() == kind::APPLY_UF); - TNodeNodeMap d_map; + TNodeNodeMap d_map; for (unsigned i = 0; i < func.getNumChildren(); ++i) { TNode arg = func[i]; if (arg.isConst()) { @@ -918,9 +918,9 @@ void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args) continue; } Assert (arg.getMetaKind() == kind::metakind::VARIABLE); - TNodeNodeMap::iterator it = d_map.find(arg); + TNodeNodeMap::iterator it = d_map.find(arg); if (it != d_map.end()) { - fresh_args.push_back(it->second); + fresh_args.push_back(it->second); } else { Node skolem = utils::mkVar(utils::getSize(arg)); d_map[arg] = skolem; @@ -947,7 +947,7 @@ Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vect Debug("bv-abstraction-dbg") <<"\n"; } - + SubstitutionMap subst(new context::Context()); for (unsigned i = 0; i < ss.size(); ++i) { @@ -982,10 +982,10 @@ Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vect Assert (s0 != t0); subst.addSubstitution(s0, t0); } - + Node res = subst.apply(conflict); - Debug("bv-abstraction-dbg") << " Lemma: " << res <<"\n"; - return res; + Debug("bv-abstraction-dbg") << " Lemma: " << res <<"\n"; + return res; } void AbstractionModule::storeLemma(TNode lemma) { @@ -996,7 +996,7 @@ void AbstractionModule::storeLemma(TNode lemma) { atom = atom.getKind() == kind::NOT ? atom[0] : atom; Assert (atom.getKind() != kind::NOT); Assert (utils::isBVPredicate(atom)); - d_lemmaAtoms.insert(atom); + d_lemmaAtoms.insert(atom); } } else { lemma = lemma.getKind() == kind::NOT? lemma[0] : lemma; @@ -1009,9 +1009,9 @@ void AbstractionModule::storeLemma(TNode lemma) { bool AbstractionModule::isLemmaAtom(TNode node) const { Assert (node.getType().isBoolean()); node = node.getKind() == kind::NOT? node[0] : node; - + return d_inputAtoms.find(node) == d_inputAtoms.end() && - d_lemmaAtoms.find(node) != d_lemmaAtoms.end(); + d_lemmaAtoms.find(node) != d_lemmaAtoms.end(); } void AbstractionModule::addInputAtom(TNode atom) { @@ -1022,31 +1022,31 @@ void AbstractionModule::addInputAtom(TNode atom) { void AbstractionModule::ArgsTableEntry::addArguments(const ArgsVec& args) { Assert (args.size() == d_arity); - d_data.push_back(args); + d_data.push_back(args); } void AbstractionModule::ArgsTable::addEntry(TNode signature, const ArgsVec& args) { if (d_data.find(signature) == d_data.end()) { - d_data[signature] = ArgsTableEntry(args.size()); + d_data[signature] = ArgsTableEntry(args.size()); } ArgsTableEntry& entry = d_data[signature]; - entry.addArguments(args); + entry.addArguments(args); } bool AbstractionModule::ArgsTable::hasEntry(TNode signature) const { - return d_data.find(signature) != d_data.end(); + return d_data.find(signature) != d_data.end(); } AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode signature) { Assert (hasEntry(signature)); - return d_data.find(signature)->second; + return d_data.find(signature)->second; } -AbstractionModule::Statistics::Statistics() - : d_numFunctionsAbstracted("theory::bv::AbstractioModule::NumFunctionsAbstracted", 0) - , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0) - , d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime") +AbstractionModule::Statistics::Statistics(const std::string& name) + : d_numFunctionsAbstracted(name + "theory::bv::AbstractioModule::NumFunctionsAbstracted", 0) + , d_numArgsSkolemized(name + "theory::bv::AbstractioModule::NumArgsSkolemized", 0) + , d_abstractionTime(name + "theory::bv::AbstractioModule::AbstractionTime") { smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted); smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized); diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 5d580f6ce..5d48b926e 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -38,11 +38,11 @@ class AbstractionModule { IntStat d_numFunctionsAbstracted; IntStat d_numArgsSkolemized; TimerStat d_abstractionTime; - Statistics(); + Statistics(const std::string& name); ~Statistics(); }; - + class ArgsTableEntry { std::vector<ArgsVec> d_data; unsigned d_arity; @@ -61,11 +61,11 @@ class AbstractionModule { unsigned getArity() { return d_arity; } unsigned getNumEntries() { return d_data.size(); } ArgsVec& getEntry(unsigned i ) { Assert (i < d_data.size()); return d_data[i]; } - }; + }; class ArgsTable { __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; - bool hasEntry(TNode signature) const; + bool hasEntry(TNode signature) const; public: typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; ArgsTable() {} @@ -75,12 +75,12 @@ class AbstractionModule { iterator end() { return d_data.end(); } }; - /** + /** * Checks if one pattern is a generalization of the other - * - * @param s - * @param t - * + * + * @param s + * @param t + * * @return 1 if s :> t, 2 if s <: t, 0 if they equivalent and -1 if they are incomparable */ static int comparePatterns(TNode s, TNode t); @@ -93,7 +93,7 @@ class AbstractionModule { theory::SubstitutionMap d_subst; TNode d_conflict; std::vector<Node> d_lemmas; - + void backtrack(std::vector<int>& stack); int next(int val, int index); bool isConsistent(const std::vector<int>& stack); @@ -108,7 +108,7 @@ class AbstractionModule { , d_conflict(conflict) , d_lemmas() { - Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n"; + Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n"; // initializing the search space for (unsigned i = 0; i < functions.size(); ++i) { TNode func_op = functions[i].getOperator(); @@ -118,31 +118,31 @@ class AbstractionModule { } } - void generateInstantiations(std::vector<Node>& lemmas); - + void generateInstantiations(std::vector<Node>& lemmas); + }; - + typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap; typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap; typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap; typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap; typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap; + typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap; typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap; typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap; typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap; - - ArgsTable d_argsTable; + + ArgsTable d_argsTable; // mapping between signature and uninterpreted function symbol used to // abstract the signature NodeNodeMap d_signatureToFunc; - NodeNodeMap d_funcToSignature; + NodeNodeMap d_funcToSignature; - NodeNodeMap d_assertionToSignature; + NodeNodeMap d_assertionToSignature; SignatureMap d_signatures; - NodeNodeMap d_sigToGeneralization; + NodeNodeMap d_sigToGeneralization; TNodeSet d_skolems; // skolems maps @@ -165,7 +165,7 @@ class AbstractionModule { Node getGeneralizedSignature(Node node); Node getSignatureSkolem(TNode node); - unsigned getBitwidthIndex(unsigned bitwidth); + unsigned getBitwidthIndex(unsigned bitwidth); void resetSignatureIndex(); Node computeSignatureRec(TNode, NodeNodeMap&); void storeSignature(Node signature, TNode assertion); @@ -175,14 +175,14 @@ class AbstractionModule { // crazy instantiation methods void generateInstantiations(unsigned current, - std::vector<ArgsTableEntry>& matches, + std::vector<ArgsTableEntry>& matches, std::vector<std::vector<ArgsVec> >& instantiations, std::vector<std::vector<ArgsVec> >& new_instantiations); Node tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict); void makeFreshArgs(TNode func, std::vector<Node>& fresh_args); void makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map); - + void skolemizeArguments(std::vector<Node>& assertions); Node reverseAbstraction(Node assertion, NodeNodeMap& seen); @@ -192,9 +192,9 @@ class AbstractionModule { void storeLemma(TNode lemma); Statistics d_statistics; - + public: - AbstractionModule() + AbstractionModule(const std::string& name) : d_argsTable() , d_signatureToFunc() , d_funcToSignature() @@ -207,34 +207,34 @@ public: , d_addedLemmas() , d_lemmaAtoms() , d_inputAtoms() - , d_statistics() + , d_statistics(name) {} - /** + /** * returns true if there are new uninterepreted functions symbols in the output - * - * @param assertions - * @param new_assertions - * - * @return + * + * @param assertions + * @param new_assertions + * + * @return */ bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); - /** - * Returns true if the node represents an abstraction predicate. - * - * @param node - * - * @return + /** + * Returns true if the node represents an abstraction predicate. + * + * @param node + * + * @return */ bool isAbstraction(TNode node); - /** - * Returns the interpretation of the abstraction predicate. - * - * @param node - * - * @return + /** + * Returns the interpretation of the abstraction predicate. + * + * @param node + * + * @return */ Node getInterpretation(TNode node); - Node simplifyConflict(TNode conflict); + Node simplifyConflict(TNode conflict); void generalizeConflict(TNode conflict, std::vector<Node>& lemmas); void addInputAtom(TNode atom); bool isLemmaAtom(TNode node) const; diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 887daa1bd..37e9f4476 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -19,7 +19,7 @@ #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" - +#include "smt/smt_statistics_registry.h" #ifdef CVC4_USE_ABC // Function is defined as static in ABC. Not sure how else to do this. @@ -140,10 +140,24 @@ AigBitblaster::AigBitblaster() , d_bbAtoms() , d_aigOutputNode(NULL) { - d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster"); - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - d_satSolver->setNotify(notify); + d_nullContext = new context::Context(); + switch(options::bvSatSolver()) { + case SAT_SOLVER_MINISAT: { + prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext, + smtStatisticsRegistry(), + "AigBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + minisat->setNotify(notify); + d_satSolver = minisat; + break; + } + case SAT_SOLVER_CRYPTOMINISAT: + d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), + "AigBitblaster"); + break; + default: + Unreachable("Unknown SAT solver type"); + } } AigBitblaster::~AigBitblaster() { @@ -402,7 +416,7 @@ void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) { prop::SatLiteral lit(sat_variables[index-1], int_lit < 0); clause.push_back(lit); } - d_satSolver->addClause(clause, false, RULE_INVALID); + d_satSolver->addClause(clause, false); } } diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index cfbadbf32..c6c0d6def 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -257,7 +257,7 @@ public: class EagerBitblaster : public TBitblaster<Node> { typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; // sat solver used for bitblasting and associated CnfStream - prop::BVSatSolverInterface* d_satSolver; + prop::SatSolver* d_satSolver; BitblastingRegistrar* d_bitblastingRegistrar; context::Context* d_nullContext; prop::CnfStream* d_cnfStream; @@ -268,6 +268,8 @@ class EagerBitblaster : public TBitblaster<Node> { MinisatEmptyNotify d_notify; + MinisatEmptyNotify d_notify; + Node getModelFromSatSolver(TNode a, bool fullModel); bool isSharedTerm(TNode node); @@ -306,7 +308,7 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> { static Abc_Ntk_t* abcAigNetwork; context::Context* d_nullContext; - prop::BVSatSolverInterface* d_satSolver; + prop::SatSolver* d_satSolver; TNodeAigMap d_aigCache; NodeAigMap d_bbAtoms; @@ -459,7 +461,7 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) { if (Theory::isLeafOf(node, theory::THEORY_BV)) { // if it is a leaf may ask for fullModel - value = getModelFromSatSolver(node, fullModel); + value = getModelFromSatSolver(node, true); Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n"; Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel); if (!value.isNull()) { diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 00d337395..b7e973928 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -714,7 +714,8 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) { Assert (!value.isNull() || !fullModel); // may be a shared term that did not appear in the current assertions - if (!value.isNull()) { + // AJR: need to check whether already in map for cases where collectModelInfo is called multiple times in the same context + if (!value.isNull() && !d_modelMap->hasSubstitution(var)) { Debug("bitvector-model") << " " << var << " => " << value << "\n"; Assert (value.getKind() == kind::CONST_BITVECTOR); d_modelMap->addSubstitution(var, value); diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index b7619c4bb..6c6c13ee8 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -37,9 +37,9 @@ namespace bv { BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), - d_bitblaster(new TLazyBitblaster(c, bv, "lazy")), + d_bitblaster(new TLazyBitblaster(c, bv, bv->getFullInstanceName() + "lazy")), d_bitblastQueue(c), - d_statistics(), + d_statistics(bv->getFullInstanceName()), d_validModelCache(c, true), d_lemmaAtomsQueue(c), d_useSatPropagation(options::bitvectorPropagate()), @@ -55,9 +55,9 @@ BitblastSolver::~BitblastSolver() { delete d_bitblaster; } -BitblastSolver::Statistics::Statistics() - : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0) - , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0) +BitblastSolver::Statistics::Statistics(const std::string &instanceName) + : d_numCallstoCheck(instanceName + "theory::bv::BitblastSolver::NumCallsToCheck", 0) + , d_numBBLemmas(instanceName + "theory::bv::BitblastSolver::NumTimesLemmasBB", 0) { smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); smtStatisticsRegistry()->registerStat(&d_numBBLemmas); @@ -68,8 +68,8 @@ BitblastSolver::Statistics::~Statistics() { } void BitblastSolver::setAbstraction(AbstractionModule* abs) { - d_abstractionModule = abs; - d_bitblaster->setAbstraction(abs); + d_abstractionModule = abs; + d_bitblaster->setAbstraction(abs); } void BitblastSolver::preRegister(TNode node) { @@ -117,7 +117,7 @@ void BitblastSolver::bitblastQueue() { bool BitblastSolver::check(Theory::Effort e) { Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); ++(d_statistics.d_numCallstoCheck); @@ -135,10 +135,10 @@ bool BitblastSolver::check(Theory::Effort e) { // skip atoms that are the result of abstraction lemmas if (d_abstractionModule->isLemmaAtom(fact)) { d_lemmaAtomsQueue.push_back(fact); - continue; + continue; } } - + if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) { // Some atoms have not been bit-blasted yet @@ -183,7 +183,7 @@ bool BitblastSolver::check(Theory::Effort e) { if (options::bvAbstraction() && e == Theory::EFFORT_FULL && d_lemmaAtomsQueue.size()) { - + // bit-blast lemma atoms while(!d_lemmaAtomsQueue.empty()) { TNode lemma_atom = d_lemmaAtomsQueue.front(); @@ -199,7 +199,7 @@ bool BitblastSolver::check(Theory::Effort e) { return false; } } - + Assert(!d_bv->inConflict()); bool ok = d_bitblaster->solve(); if (!ok) { @@ -210,9 +210,9 @@ bool BitblastSolver::check(Theory::Effort e) { ++(d_statistics.d_numBBLemmas); return false; } - + } - + return true; } @@ -228,9 +228,9 @@ void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { Node BitblastSolver::getModelValue(TNode node) { if (d_bv->d_invalidateModelCache.get()) { - d_bitblaster->invalidateModelCache(); + d_bitblaster->invalidateModelCache(); } - d_bv->d_invalidateModelCache.set(false); + d_bv->d_invalidateModelCache.set(false); Node val = d_bitblaster->getTermModel(node, true); return val; } @@ -241,9 +241,9 @@ void BitblastSolver::setConflict(TNode conflict) { Node final_conflict = conflict; if (options::bitvectorQuickXplain() && conflict.getKind() == kind::AND) { - // std::cout << "Original conflict " << conflict.getNumChildren() << "\n"; + // std::cout << "Original conflict " << conflict.getNumChildren() << "\n"; final_conflict = d_quickXplain->minimizeConflict(conflict); - //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n"; + //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n"; } d_bv->setConflict(final_conflict); } @@ -256,4 +256,3 @@ void BitblastSolver::setProofLog( BitVectorProof * bvp ) { }/* namespace CVC4::theory::bv */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ - diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index e9300138b..fe16d2702 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -37,7 +37,7 @@ class BitblastSolver : public SubtheorySolver { struct Statistics { IntStat d_numCallstoCheck; IntStat d_numBBLemmas; - Statistics(); + Statistics(const std::string &instanceName); ~Statistics(); }; /** Bitblaster */ @@ -71,8 +71,8 @@ public: Node getModelValue(TNode node); bool isComplete() { return true; } void bitblastQueue(); - void setAbstraction(AbstractionModule* module); - uint64_t computeAtomWeight(TNode atom); + void setAbstraction(AbstractionModule* module); + uint64_t computeAtomWeight(TNode atom); void setProofLog( BitVectorProof * bvp ); }; diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 3b54e3794..53fb4f94b 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -47,15 +47,30 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) { d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); - - d_satSolver = prop::SatSolverFactory::createMinisat( - d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); + + switch(options::bvSatSolver()) { + case SAT_SOLVER_MINISAT: { + prop::BVSatSolverInterface* minisat = + prop::SatSolverFactory::createMinisat(d_nullContext, + smtStatisticsRegistry(), + "EagerBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + minisat->setNotify(notify); + d_satSolver = minisat; + break; + } + case SAT_SOLVER_CRYPTOMINISAT: + d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), + "EagerBitblaster"); + break; + default: + Unreachable("Unknown SAT solver type"); + } d_cnfStream = new prop::TseitinCnfStream( d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(), "EagerBitblaster"); - d_satSolver->setNotify(&d_notify); d_bvp = NULL; } @@ -216,7 +231,7 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { // only shared terms could not have been bit-blasted Assert (hasBBTerm(var) || isSharedTerm(var)); - Node const_value = getModelFromSatSolver(var, fullModel); + Node const_value = getModelFromSatSolver(var, true); if(const_value != Node()) { Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= " diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index c821b50cd..b549c329a 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -491,7 +491,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { // only shared terms could not have been bit-blasted Assert (hasBBTerm(var) || isSharedTerm(var)); - Node const_value = getModelFromSatSolver(var, fullModel); + Node const_value = getModelFromSatSolver(var, true); Assert (const_value.isNull() || const_value.isConst()); if(const_value != Node()) { Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 2edadce72..fec93e033 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -44,25 +44,29 @@ namespace bv { TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo), - d_context(c), - d_alreadyPropagatedSet(c), - d_sharedTermsSet(c), - d_subtheories(), - d_subtheoryMap(), - d_statistics(), - d_staticLearnCache(), - d_lemmasAdded(c, false), - d_conflict(c, false), - d_invalidateModelCache(c, true), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_propagatedBy(c), - d_eagerSolver(NULL), - d_abstractionModule(new AbstractionModule()), - d_isCoreTheory(false), - d_calledPreregister(false) + const LogicInfo& logicInfo, std::string name) + : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name), + d_context(c), + d_alreadyPropagatedSet(c), + d_sharedTermsSet(c), + d_subtheories(), + d_subtheoryMap(), + d_statistics(getFullInstanceName()), + d_staticLearnCache(), + d_BVDivByZero(), + d_BVRemByZero(), + d_funcToArgs(), + d_funcToSkolem(u), + d_lemmasAdded(c, false), + d_conflict(c, false), + d_invalidateModelCache(c, true), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_propagatedBy(c), + d_eagerSolver(NULL), + d_abstractionModule(new AbstractionModule(getFullInstanceName())), + d_isCoreTheory(false), + d_calledPreregister(false) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { @@ -117,14 +121,14 @@ void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) { getOutputChannel().spendResource(ammount); } -TheoryBV::Statistics::Statistics(): - d_avgConflictSize("theory::bv::AvgBVConflictSize"), - d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0), - d_solveTimer("theory::bv::solveTimer"), - d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0), - d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0), - d_weightComputationTimer("theory::bv::weightComputationTimer"), - d_numMultSlice("theory::bv::NumMultSliceApplied", 0) +TheoryBV::Statistics::Statistics(const std::string &name): + d_avgConflictSize(name + "theory::bv::AvgBVConflictSize"), + d_solveSubstitutions(name + "theory::bv::NumberOfSolveSubstitutions", 0), + d_solveTimer(name + "theory::bv::solveTimer"), + d_numCallsToCheckFullEffort(name + "theory::bv::NumberOfFullCheckCalls", 0), + d_numCallsToCheckStandardEffort(name + "theory::bv::NumberOfStandardCheckCalls", 0), + d_weightComputationTimer(name + "theory::bv::weightComputationTimer"), + d_numMultSlice(name + "theory::bv::NumMultSliceApplied", 0) { smtStatisticsRegistry()->registerStat(&d_avgConflictSize); smtStatisticsRegistry()->registerStat(&d_solveSubstitutions); @@ -175,30 +179,31 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { } -void TheoryBV::collectNumerators(TNode term, TNodeSet& seen) { +void TheoryBV::collectFunctionSymbols(TNode term, TNodeSet& seen) { if (seen.find(term) != seen.end()) return; - if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UDIV) { - unsigned size = utils::getSize(term[0]); - if (d_BVDivByZeroAckerman.find(size) == d_BVDivByZeroAckerman.end()) { - d_BVDivByZeroAckerman[size] = TNodeSet(); - } - d_BVDivByZeroAckerman[size].insert(term[0]); - seen.insert(term); - } else if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UREM) { - unsigned size = utils::getSize(term[0]); - if (d_BVRemByZeroAckerman.find(size) == d_BVRemByZeroAckerman.end()) { - d_BVRemByZeroAckerman[size] = TNodeSet(); - } - d_BVRemByZeroAckerman[size].insert(term[0]); - seen.insert(term); + if (term.getKind() == kind::APPLY_UF) { + TNode func = term.getOperator(); + storeFunction(func, term); } for (unsigned i = 0; i < term.getNumChildren(); ++i) { - collectNumerators(term[i], seen); + collectFunctionSymbols(term[i], seen); } seen.insert(term); } +void TheoryBV::storeFunction(TNode func, TNode term) { + if (d_funcToArgs.find(func) == d_funcToArgs.end()) { + d_funcToArgs.insert(make_pair(func, NodeSet())); + } + NodeSet& set = d_funcToArgs[func]; + if (set.find(term) == set.end()) { + set.insert(term); + Node skolem = utils::mkVar(utils::getSize(term)); + d_funcToSkolem.addSubstitution(term, skolem); + } +} + void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) { Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n"; @@ -206,51 +211,44 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) { AlwaysAssert(!options::incrementalSolving()); TNodeSet seen; for (unsigned i = 0; i < assertions.size(); ++i) { - collectNumerators(assertions[i], seen); - } - - // process division UF - Debug("bv-ackermanize") << "Process division UF...\n"; - for (WidthToNumerators::const_iterator it = d_BVDivByZeroAckerman.begin(); it != d_BVDivByZeroAckerman.end(); ++it) { - const TNodeSet& numerators= it->second; - for (TNodeSet::const_iterator i = numerators.begin(); i != numerators.end(); ++i) { - TNodeSet::const_iterator j = i; - j++; - for (; j != numerators.end(); ++j) { - TNode arg1 = *i; - TNode arg2 = *j; - TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg1); - TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2); - - Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2); - Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2); - Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq); - Debug("bv-ackermanize") << " " << lemma << "\n"; - assertions.push_back(lemma); - } - } + collectFunctionSymbols(assertions[i], seen); } - // process remainder UF - Debug("bv-ackermanize") << "Process remainder UF...\n"; - for (WidthToNumerators::const_iterator it = d_BVRemByZeroAckerman.begin(); it != d_BVRemByZeroAckerman.end(); ++it) { - const TNodeSet& numerators= it->second; - for (TNodeSet::const_iterator i = numerators.begin(); i != numerators.end(); ++i) { - TNodeSet::const_iterator j = i; - j++; - for (; j != numerators.end(); ++j) { - TNode arg1 = *i; - TNode arg2 = *j; - TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg1); - TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2); - - Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2); - Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2); - Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq); - Debug("bv-ackermanize") << " " << lemma << "\n"; + + FunctionToArgs::const_iterator it = d_funcToArgs.begin(); + NodeManager* nm = NodeManager::currentNM(); + for (; it!= d_funcToArgs.end(); ++it) { + TNode func = it->first; + const NodeSet& args = it->second; + NodeSet::const_iterator it1 = args.begin(); + for ( ; it1 != args.end(); ++it1) { + for(NodeSet::const_iterator it2 = it1; it2 != args.end(); ++it2) { + TNode args1 = *it1; + TNode args2 = *it2; + + AlwaysAssert (args1.getKind() == kind::APPLY_UF && + args1.getOperator() == func); + AlwaysAssert (args2.getKind() == kind::APPLY_UF && + args2.getOperator() == func); + AlwaysAssert (args1.getNumChildren() == args2.getNumChildren()); + + std::vector<Node> eqs(args1.getNumChildren()); + + for (unsigned i = 0; i < args1.getNumChildren(); ++i) { + eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); + } + + Node args_eq = eqs.size() == 1 ? eqs[0] : nm->mkNode(kind::AND, eqs); + Node func_eq = nm->mkNode(kind::EQUAL, args1, args2); + Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq); assertions.push_back(lemma); } } } + + // replace applications of UF by skolems (FIXME for model building) + for(unsigned i = 0; i < assertions.size(); ++i) { + assertions[i] = d_funcToSkolem.apply(assertions[i]); + } } Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { @@ -278,18 +276,18 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL, num, den); - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - // Ackermanize UF if using eager bit-blasting - Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); - node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen); - return node; - } else { + // if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + // // Ackermanize UF if using eager bit-blasting + // Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); + // node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen); + // return node; + // } else { Node divByZero = getBVDivByZero(node.getKind(), width); Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); logicRequest.widenLogic(THEORY_UF); return node; - } + //} } break; @@ -331,7 +329,7 @@ void TheoryBV::sendConflict() { if (d_conflictNode.isNull()) { return; } else { - Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; + Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; d_out->conflict(d_conflictNode); d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); d_conflictNode = Node::null(); @@ -707,7 +705,7 @@ Node TheoryBV::explain(TNode node) { // return the explanation Node explanation = utils::mkAnd(assumptions); Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl; - Debug("bitvector::explain") << "TheoryBV::explain done. \n"; + Debug("bitvector::explain") << "TheoryBV::explain done. \n"; return explanation; } @@ -725,6 +723,8 @@ void TheoryBV::addSharedTerm(TNode t) { EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + return EQUALITY_UNKNOWN; Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); for (unsigned i = 0; i < d_subtheories.size(); ++i) { EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 0bbcba9b0..ba2a4fc2a 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -56,7 +56,8 @@ class TheoryBV : public Theory { public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); + Valuation valuation, const LogicInfo& logicInfo, + std::string name = ""); ~TheoryBV(); @@ -88,8 +89,8 @@ public: void presolve(); - bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); - + bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + void setProofLog( BitVectorProof * bvp ); private: @@ -100,10 +101,10 @@ private: IntStat d_solveSubstitutions; TimerStat d_solveTimer; IntStat d_numCallsToCheckFullEffort; - IntStat d_numCallsToCheckStandardEffort; + IntStat d_numCallsToCheckStandardEffort; TimerStat d_weightComputationTimer; IntStat d_numMultSlice; - Statistics(); + Statistics(const std::string &name); ~Statistics(); }; @@ -121,12 +122,12 @@ private: */ Node getBVDivByZero(Kind k, unsigned width); - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - void collectNumerators(TNode term, TNodeSet& seen); - + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + void collectFunctionSymbols(TNode term, TNodeSet& seen); + void storeFunction(TNode func, TNode term); typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; NodeSet d_staticLearnCache; - + /** * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. @@ -134,17 +135,15 @@ private: __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero; __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero; - /** - * Maps from bit-vector width to numerators - * of uninterpreted function symbol - */ - typedef __gnu_cxx::hash_map<unsigned, TNodeSet > WidthToNumerators; - WidthToNumerators d_BVDivByZeroAckerman; - WidthToNumerators d_BVRemByZeroAckerman; + typedef __gnu_cxx::hash_map<Node, NodeSet, NodeHashFunction> FunctionToArgs; + typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode; + // for ackermanization + FunctionToArgs d_funcToArgs; + CVC4::theory::SubstitutionMap d_funcToSkolem; context::CDO<bool> d_lemmasAdded; - + // Are we in conflict? context::CDO<bool> d_conflict; @@ -167,17 +166,17 @@ private: typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap; PropagatedMap d_propagatedBy; - EagerBitblastSolver* d_eagerSolver; + EagerBitblastSolver* d_eagerSolver; AbstractionModule* d_abstractionModule; bool d_isCoreTheory; bool d_calledPreregister; - + bool wasPropagatedBySubtheory(TNode literal) const { - return d_propagatedBy.find(literal) != d_propagatedBy.end(); + return d_propagatedBy.find(literal) != d_propagatedBy.end(); } - + SubTheory getPropagatingSubtheory(TNode literal) const { - Assert(wasPropagatedBySubtheory(literal)); + Assert(wasPropagatedBySubtheory(literal)); PropagatedMap::const_iterator find = d_propagatedBy.find(literal); return (*find).second; } @@ -193,7 +192,7 @@ private: void addSharedTerm(TNode t); bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } - + EqualityStatus getEqualityStatus(TNode a, TNode b); Node getModelValue(TNode var); @@ -214,7 +213,7 @@ private: void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; } - void checkForLemma(TNode node); + void checkForLemma(TNode node); friend class LazyBitblaster; friend class TLazyBitblaster; diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 152a335a5..2bcb6ca1b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -349,7 +349,7 @@ Node RewriteRule<SdivEliminate>::apply(TNode node) { Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); - Node a_udiv_b = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); + Node a_udiv_b = utils::mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UDIV, abs_a, abs_b); Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b); Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0); @@ -377,7 +377,7 @@ Node RewriteRule<SremEliminate>::apply(TNode node) { Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); - Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); + Node a_urem_b = utils::mkNode( options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL : kind::BITVECTOR_UREM, abs_a, abs_b); Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b); Node result = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); |