From 89ba584531115b7f6d47088d7614368ea05ab9d8 Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 1 Jun 2016 17:33:41 -0700 Subject: Merging proof branch --- src/theory/arrays/array_proof_reconstruction.cpp | 51 ++++ src/theory/arrays/theory_arrays.cpp | 5 +- src/theory/bv/abstraction.cpp | 352 +++++++++++------------ src/theory/bv/abstraction.h | 90 +++--- src/theory/bv/bv_subtheory_bitblast.cpp | 37 ++- src/theory/bv/bv_subtheory_bitblast.h | 6 +- src/theory/bv/theory_bv.cpp | 38 +-- src/theory/bv/theory_bv.h | 31 +- src/theory/theory_engine.cpp | 322 +++++++++++++++++++-- src/theory/theory_engine.h | 46 +-- src/theory/uf/equality_engine.cpp | 26 +- src/theory/uf/equality_engine.h | 8 +- src/theory/uf/theory_uf.cpp | 3 +- 13 files changed, 672 insertions(+), 343 deletions(-) (limited to 'src/theory') diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 11c3dc081..6dfd14157 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -101,8 +101,59 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, Debug("pf::ee") << "Getting explanation for ROW guard: " << indexOne << " != " << indexTwo << std::endl; + eq::EqProof* childProof = new eq::EqProof; d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof); + + // It could be that the guard condition is a constant disequality. In this case, + // we need to change it to a different format. + if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) { + // The proof has two children, explaining why each index is a (different) constant. + Assert(childProof->d_children.size() == 2); + + Node constantOne, constantTwo; + // Each subproof explains why one of the indices is constant. + + if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + constantOne = childProof->d_children[0]->d_node; + } else { + Assert(childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_EQUALITY); + if ((childProof->d_children[0]->d_node[0] == indexOne) || + (childProof->d_children[0]->d_node[0] == indexTwo)) { + constantOne = childProof->d_children[0]->d_node[1]; + } else { + constantOne = childProof->d_children[0]->d_node[0]; + } + } + + if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + constantTwo = childProof->d_children[1]->d_node; + } else { + Assert(childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_EQUALITY); + if ((childProof->d_children[1]->d_node[0] == indexOne) || + (childProof->d_children[1]->d_node[0] == indexTwo)) { + constantTwo = childProof->d_children[1]->d_node[1]; + } else { + constantTwo = childProof->d_children[1]->d_node[0]; + } + } + + eq::EqProof* constantDisequalityProof = new eq::EqProof; + constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS; + constantDisequalityProof->d_node = + NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate(); + + // Middle is where we need to insert the new disequality + std::vector::iterator middle = childProof->d_children.begin(); + ++middle; + + childProof->d_children.insert(middle, constantDisequalityProof); + + childProof->d_id = theory::eq::MERGED_THROUGH_TRANS; + childProof->d_node = + NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate(); + } + proof->d_children.push_back(childProof); } else { // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 6add1b55f..28a08630e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -829,7 +829,8 @@ void TheoryArrays::propagate(Effort e) Node TheoryArrays::explain(TNode literal) { - return explain(literal, NULL); + Node explanation = explain(literal, NULL); + return explanation; } Node TheoryArrays::explain(TNode literal, eq::EqProof *proof) @@ -1394,6 +1395,7 @@ void TheoryArrays::check(Effort e) { break; default: Unreachable(); + break; } } @@ -2231,6 +2233,7 @@ bool TheoryArrays::dischargeLemmas() void TheoryArrays::conflict(TNode a, TNode b) { Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl; eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL; + if (a.getKind() == kind::CONST_BOOLEAN) { d_conflictNode = explain(a.iffNode(b), proof); } else { 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& 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& assertions, st for (unsigned i = 0; i < assertions.size(); ++i) { if (assertions[i].getKind() == kind::OR && assertions[i][0].getKind() == kind::AND) { - std::vector new_children; + std::vector 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& 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& 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& assertions) { @@ -151,7 +151,7 @@ void AbstractionModule::skolemizeArguments(std::vector& 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& assertions) { NodeBuilder<> skolem_func (kind::APPLY_UF); skolem_func << func; std::vector 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 or_assignments; + std::vector 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(); + d_signatureSkolems[bitwidth] = vector(); } - + vector& 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_" <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& 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& t void AbstractionModule::collectArguments(TNode node, TNode signature, std::vector& 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 args; @@ -527,16 +527,16 @@ Node AbstractionModule::abstractSignatures(TNode assertion) { collectArguments(assertion, signature, args, seen); std::vector 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 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 >& instantiations, const std::vector 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 >& instant const std::vector& 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& lemmas) { - Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; + Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; std::vector functions; // collect abstract functions @@ -737,11 +737,11 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector& 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& 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 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& 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& 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& 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& 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& stack) { @@ -854,13 +854,13 @@ bool AbstractionModule::LemmaInstantiatior::accept(const vector& 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& stack) { if (!isConsistent(stack)) return; - + if (accept(stack)) { mkLemma(); return; @@ -871,7 +871,7 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector& 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& stack) { void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector& lemmas) { - Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; + Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; std::vector 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& 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& 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& 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& 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 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 d_data; - bool hasEntry(TNode signature) const; + bool hasEntry(TNode signature) const; public: typedef __gnu_cxx::hash_map::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 d_lemmas; - + void backtrack(std::vector& stack); int next(int val, int index); bool isConsistent(const std::vector& 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& lemmas); - + void generateInstantiations(std::vector& lemmas); + }; - + typedef __gnu_cxx::hash_map, NodeHashFunction> NodeVecMap; typedef __gnu_cxx::hash_map NodeTNodeMap; typedef __gnu_cxx::hash_map TNodeTNodeMap; typedef __gnu_cxx::hash_map NodeNodeMap; typedef __gnu_cxx::hash_map TNodeNodeMap; typedef __gnu_cxx::hash_set TNodeSet; - typedef __gnu_cxx::hash_map IntNodeMap; + typedef __gnu_cxx::hash_map IntNodeMap; typedef __gnu_cxx::hash_map IndexMap; typedef __gnu_cxx::hash_map > SkolemMap; typedef __gnu_cxx::hash_map 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& matches, + std::vector& matches, std::vector >& instantiations, std::vector >& new_instantiations); Node tryMatching(const std::vector& ss, const std::vector& tt, TNode conflict); void makeFreshArgs(TNode func, std::vector& fresh_args); void makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map); - + void skolemizeArguments(std::vector& 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& assertions, std::vector& 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& lemmas); void addInputAtom(TNode atom); bool isLemmaAtom(TNode node) const; 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/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index f5b2175f3..fec93e033 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -42,14 +42,16 @@ namespace CVC4 { namespace theory { 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), +TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + 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(), + d_statistics(getFullInstanceName()), d_staticLearnCache(), d_BVDivByZero(), d_BVRemByZero(), @@ -62,7 +64,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_literalsToPropagateIndex(c, 0), d_propagatedBy(c), d_eagerSolver(NULL), - d_abstractionModule(new AbstractionModule()), + d_abstractionModule(new AbstractionModule(getFullInstanceName())), d_isCoreTheory(false), d_calledPreregister(false) { @@ -119,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); @@ -234,7 +236,7 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector& assertions) { 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); @@ -276,9 +278,9 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { // 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 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; + // return node; // } else { Node divByZero = getBVDivByZero(node.getKind(), width); Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); @@ -327,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(); @@ -703,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; } @@ -723,7 +725,7 @@ 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); + 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); if (status != EQUALITY_UNKNOWN) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 7f0494dc1..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& assertions, std::vector& new_assertions); - + bool applyAbstraction(const std::vector& assertions, std::vector& 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 TNodeSet; + typedef __gnu_cxx::hash_set TNodeSet; void collectFunctionSymbols(TNode term, TNodeSet& seen); void storeFunction(TNode func, TNode term); typedef __gnu_cxx::hash_set NodeSet; NodeSet d_staticLearnCache; - + /** * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. @@ -142,7 +143,7 @@ private: CVC4::theory::SubstitutionMap d_funcToSkolem; context::CDO d_lemmasAdded; - + // Are we in conflict? context::CDO d_conflict; @@ -165,17 +166,17 @@ private: typedef context::CDHashMap 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; } @@ -191,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); @@ -212,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/theory_engine.cpp b/src/theory/theory_engine.cpp index 1ab4c228b..618fda4c0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -26,6 +26,8 @@ #include "options/bv_options.h" #include "options/options.h" #include "options/quantifiers_options.h" +#include "proof/cnf_proof.h" +#include "proof/lemma_proof.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" #include "smt/ite_removal.h" @@ -53,6 +55,104 @@ using namespace CVC4::theory; namespace CVC4 { +inline void flattenAnd(Node n, std::vector& out){ + Assert(n.getKind() == kind::AND); + for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){ + Node curr = *i; + if(curr.getKind() == kind::AND){ + flattenAnd(curr, out); + }else{ + out.push_back(curr); + } + } +} + +inline Node flattenAnd(Node n){ + std::vector out; + flattenAnd(n, out); + return NodeManager::currentNM()->mkNode(kind::AND, out); +} + +theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, + ProofRule rule, + bool removable, + bool preprocess, + bool sendAtoms) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << ", preprocess = " << preprocess << std::endl; + ++ d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + + LemmaProofRecipe* proofRecipe = NULL; + PROOF({ + // Theory lemmas have one step that proves the empty clause + proofRecipe = new LemmaProofRecipe; + + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode); + + Node rewritten; + if (lemma.getKind() == kind::OR) { + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { + rewritten = theory::Rewriter::rewrite(lemma[i]); + if (rewritten != lemma[i]) { + proofRecipe->addRewriteRule(lemma[i].negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma[i]); + proofRecipe->addBaseAssertion(rewritten); + } + } else { + rewritten = theory::Rewriter::rewrite(lemma); + if (rewritten != lemma) { + proofRecipe->addRewriteRule(lemma.negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma); + proofRecipe->addBaseAssertion(rewritten); + } + proofRecipe->addStep(proofStep); + }); + + theory::LemmaStatus result = d_engine->lemma(lemma, + rule, + false, + removable, + preprocess, + sendAtoms ? d_theory : theory::THEORY_LAST, + proofRecipe); + PROOF(delete proofRecipe;); + return result; +} + +theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; + ++ d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + + + LemmaProofRecipe* proofRecipe = NULL; + Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl; + theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, proofRecipe); + return result; +} + +bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) + throw(AssertionException, UnsafeInterruptException) { + Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; + ++ d_statistics.propagations; + d_engine->d_outputChannelUsed = true; + return d_engine->propagate(literal, d_theory); +} + +void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) + throw(AssertionException, UnsafeInterruptException) { + Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; + Assert (pf == NULL); // Theory shouldn't be producing proofs yet + ++ d_statistics.conflicts; + d_engine->d_outputChannelUsed = true; + d_engine->conflict(conflictNode, d_theory); +} + void TheoryEngine::finishInit() { // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); @@ -497,7 +597,10 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, carePair.theory); + + LemmaProofRecipe* proofRecipe = NULL; + lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe); + // This code is supposed to force preference to follow what the theory models already have // but it doesn't seem to make a big difference - need to explore more -Clark // if (true) { @@ -963,7 +1066,7 @@ bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, the void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { - Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl; + Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl; Assert(toTheoryId != fromTheoryId); if(toTheoryId != THEORY_SAT_SOLVER && @@ -1176,6 +1279,23 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory); } } else { + // We could be propagating a unit-clause lemma. In this case, we need to provide a + // recipe. + // TODO: Consider putting this someplace else? This is the only refence to the proof + // manager in this class. + + PROOF({ + LemmaProofRecipe proofRecipe; + proofRecipe.addBaseAssertion(literal); + + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theory, emptyNode); + proofStep.addAssertion(literal); + proofRecipe.addStep(proofStep); + + ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); + }); + // Just send off to the SAT solver Assert(d_propEngine->isSatLiteral(literal)); assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); @@ -1270,7 +1390,7 @@ static Node mkExplanation(const std::vector& explanation) { return conjunction; } -NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) { +Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl; bool polarity = node.getKind() != kind::NOT; @@ -1278,32 +1398,90 @@ NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) { // If we're not in shared mode, explanations are simple if (!d_logicInfo.isSharingEnabled()) { + Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. " + << " Responsible theory is: " + << theoryOf(atom)->getId() << std::endl; + Node explanation = theoryOf(atom)->explain(node); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; - return NodeTheoryPair(explanation, theoryOf(atom)->getId()); + PROOF({ + if(proofRecipe) { + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode); + proofStep.addAssertion(node); + proofRecipe->addBaseAssertion(node); + + if (explanation.getKind() == kind::AND) { + // If the explanation is a conjunction, the recipe for the corresponding lemma is + // the negation of its conjuncts. + Node flat = flattenAnd(explanation); + for (unsigned i = 0; i < flat.getNumChildren(); ++i) { + if (flat[i].isConst() && flat[i].getConst()) { + ++ i; + continue; + } + if (flat[i].getKind() == kind::NOT && + flat[i][0].isConst() && !flat[i][0].getConst()) { + ++ i; + continue; + } + Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: " + << flat[i].negate() << std::endl; + proofStep.addAssertion(flat[i].negate()); + proofRecipe->addBaseAssertion(flat[i].negate()); + } + } else { + // The recipe for proving it is by negating it. "True" is not an acceptable reason. + if (!((explanation.isConst() && explanation.getConst()) || + (explanation.getKind() == kind::NOT && + explanation[0].isConst() && !explanation[0].getConst()))) { + proofStep.addAssertion(explanation.negate()); + proofRecipe->addBaseAssertion(explanation.negate()); + } + } + + proofRecipe->addStep(proofStep); + } + }); + + return explanation; } + Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl; + // Initial thing to explain NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp); Assert(d_propagationMap.find(toExplain) != d_propagationMap.end()); NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain]; + Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node " + << nodeExplainerPair.node + << " is theory: " << nodeExplainerPair.theory << std::endl; TheoryId explainer = nodeExplainerPair.theory; // Create the workplace for explanations std::vector explanationVector; explanationVector.push_back(d_propagationMap[toExplain]); // Process the explanation - getExplanation(explanationVector); + if (proofRecipe) { + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode); + proofStep.addAssertion(node); + proofRecipe->addStep(proofStep); + proofRecipe->addBaseAssertion(node); + } + + getExplanation(explanationVector, proofRecipe); Node explanation = mkExplanation(explanationVector); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; - return NodeTheoryPair(explanation, explainer); + return explanation; } Node TheoryEngine::getExplanation(TNode node) { - return getExplanationAndExplainer(node).node; + LemmaProofRecipe *dontCareRecipe = NULL; + return getExplanationAndRecipe(node, dontCareRecipe); } struct AtomsCollect { @@ -1406,7 +1584,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool removable, bool preprocess, theory::TheoryId atomsTo, - theory::TheoryId ownerTheory) { + LemmaProofRecipe* proofRecipe) { // For resource-limiting (also does a time check). // spendResource(); @@ -1456,10 +1634,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, ownerTheory, node); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, ownerTheory, node); + d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. @@ -1493,22 +1671,69 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { << CheckSatCommand(conflict.toExpr()); } + LemmaProofRecipe* proofRecipe = NULL; + PROOF({ + proofRecipe = new LemmaProofRecipe; + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); + + if (conflict.getKind() == kind::AND) { + for (unsigned i = 0; i < conflict.getNumChildren(); ++i) { + proofStep.addAssertion(conflict[i].negate()); + } + } else { + proofStep.addAssertion(conflict.negate()); + } + + proofRecipe->addStep(proofStep); + }); + // In the multiple-theories case, we need to reconstruct the conflict if (d_logicInfo.isSharingEnabled()) { // Create the workplace for explanations std::vector explanationVector; explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); + // Process the explanation - getExplanation(explanationVector); + getExplanation(explanationVector, proofRecipe); Node fullConflict = mkExplanation(explanationVector); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId); + lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); + } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); - lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId); + PROOF({ + if (conflict.getKind() == kind::AND) { + // If the conflict is a conjunction, the corresponding lemma is derived by negating + // its conjuncts. + for (unsigned i = 0; i < conflict.getNumChildren(); ++i) { + if (conflict[i].isConst() && conflict[i].getConst()) { + ++ i; + continue; + } + if (conflict[i].getKind() == kind::NOT && + conflict[i][0].isConst() && !conflict[i][0].getConst()) { + ++ i; + continue; + } + proofRecipe->getStep(0)->addAssertion(conflict[i].negate()); + proofRecipe->addBaseAssertion(conflict[i].negate()); + } + } else { + proofRecipe->getStep(0)->addAssertion(conflict.negate()); + proofRecipe->addBaseAssertion(conflict.negate()); + } + }); + + lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); } + + PROOF({ + delete proofRecipe; + proofRecipe = NULL; + }); } void TheoryEngine::staticInitializeBVOptions(const std::vector& assertions) { @@ -1660,19 +1885,21 @@ bool TheoryEngine::donePPSimpITE(std::vector& assertions){ return result; } -void TheoryEngine::getExplanation(std::vector& explanationVector) -{ +void TheoryEngine::getExplanation(std::vector& explanationVector, LemmaProofRecipe* proofRecipe) { Assert(explanationVector.size() > 0); unsigned i = 0; // Index of the current literal we are processing unsigned j = 0; // Index of the last literal we are keeping - while (i < explanationVector.size()) { + std::set inputAssertions; + PROOF(inputAssertions = proofRecipe->getStep(0)->getAssertions();); + while (i < explanationVector.size()) { // Get the current literal to explain NodeTheoryPair toExplain = explanationVector[i]; - Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; + Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; + // If a true constant or a negation of a false constant we can ignore it if (toExplain.node.isConst() && toExplain.node.getConst()) { @@ -1686,6 +1913,7 @@ void TheoryEngine::getExplanation(std::vector& explanationVector // If from the SAT solver, keep it if (toExplain.theory == THEORY_SAT_SOLVER) { + Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; explanationVector[j++] = explanationVector[i++]; continue; } @@ -1704,10 +1932,26 @@ void TheoryEngine::getExplanation(std::vector& explanationVector // See if it was sent to the theory by another theory PropagationMap::const_iterator find = d_propagationMap.find(toExplain); if (find != d_propagationMap.end()) { + Debug("theory::explain") << "\tTerm was propagated by another theory (theory = " + << theoryOf((*find).second.theory)->getId() << ")" << std::endl; // There is some propagation, check if its a timely one if ((*find).second.timestamp < toExplain.timestamp) { + Debug("theory::explain") << "\tRelevant timetsamp, pushing " + << (*find).second.node << "to index = " << explanationVector.size() << std::endl; explanationVector.push_back((*find).second); - ++ i; + ++i; + + PROOF({ + if (toExplain.node != (*find).second.node) { + Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node + << ", toExplain = " << (*find).second.node << std::endl; + + if (proofRecipe) { + proofRecipe->addRewriteRule(toExplain.node, (*find).second.node); + } + } + }) + continue; } } @@ -1716,21 +1960,61 @@ void TheoryEngine::getExplanation(std::vector& explanationVector Node explanation; if (toExplain.theory == THEORY_BUILTIN) { explanation = d_sharedTerms.explain(toExplain.node); + Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl; } else { explanation = theoryOf(toExplain.theory)->explain(toExplain.node); + Debug("theory::explain") << "\tTerm was propagated by owner theory: " + << theoryOf(toExplain.theory)->getId() + << ". Explanation: " << explanation << std::endl; } + Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl; Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially"); // Mark the explanation NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); explanationVector.push_back(newExplain); + ++ i; + + PROOF({ + if (proofRecipe) { + // If we're expanding the target node of the explanation (this is the first expansion...), + // we don't want to add it as a separate proof step. It is already part of the assertions. + if (inputAssertions.find(toExplain.node) == inputAssertions.end()) { + LemmaProofRecipe::ProofStep proofStep(toExplain.theory, toExplain.node); + if (explanation.getKind() == kind::AND) { + Node flat = flattenAnd(explanation); + for (unsigned k = 0; k < flat.getNumChildren(); ++ k) { + // If a true constant or a negation of a false constant we can ignore it + if (! ((flat[k].isConst() && flat[k].getConst()) || + (flat[k].getKind() == kind::NOT && flat[k][0].isConst() && !flat[k][0].getConst()))) { + proofStep.addAssertion(flat[k].negate()); + } + } + } else { + if (! ((explanation.isConst() && explanation.getConst()) || + (explanation.getKind() == kind::NOT && explanation[0].isConst() && !explanation[0].getConst()))) { + proofStep.addAssertion(explanation.negate()); + } + } + proofRecipe->addStep(proofStep); + } + } + }); } // Keep only the relevant literals explanationVector.resize(j); -} + PROOF({ + if (proofRecipe) { + // The remaining literals are the base of the proof + for (unsigned k = 0; k < explanationVector.size(); ++k) { + proofRecipe->addBaseAssertion(explanationVector[k].node.negate()); + } + } + }); +} void TheoryEngine::ppUnconstrainedSimp(vector& assertions) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index db94edd7c..53c4aac77 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -50,6 +50,7 @@ namespace CVC4 { class ResourceManager; +class LemmaProofRecipe; /** * A pair of a theory and a node. This is used to mark the flow of @@ -270,46 +271,18 @@ class TheoryEngine { } } - void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) { - Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; - Assert(pf == NULL); // theory shouldn't be producing proofs yet - ++ d_statistics.conflicts; - d_engine->d_outputChannelUsed = true; - d_engine->conflict(conflictNode, d_theory); - } + void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException); - bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) { - Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; - ++ d_statistics.propagations; - d_engine->d_outputChannelUsed = true; - return d_engine->propagate(literal, d_theory); - } + bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException); theory::LemmaStatus lemma(TNode lemma, ProofRule rule, bool removable = false, bool preprocess = false, bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { - Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; - ++ d_statistics.lemmas; - d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST, d_theory); - } + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException); - /*theory::LemmaStatus preservedLemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) { - Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::preservedLemma(" << lemma << ")" << std::endl; - ++ d_statistics.lemmas; - d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, preprocess, d_theory); - }*/ - - theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { - Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::splitLemma(" << lemma << ")" << std::endl; - ++ d_statistics.lemmas; - d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, d_theory); - } + theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException); void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { NodeManager* curr = NodeManager::currentNM(); @@ -456,7 +429,7 @@ class TheoryEngine { bool removable, bool preprocess, theory::TheoryId atomsTo, - theory::TheoryId ownerTheory); + LemmaProofRecipe* proofRecipe); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); @@ -606,9 +579,10 @@ private: * asking relevant theories to explain the propagations. Initially * the explanation vector should contain only the element (node, theory) * where the node is the one to be explained, and the theory is the - * theory that sent the literal. + * theory that sent the literal. The lemmaProofRecipe will contain a list + * of the explanation steps required to produce the original node. */ - void getExplanation(std::vector& explanationVector); + void getExplanation(std::vector& explanationVector, LemmaProofRecipe* lemmaProofRecipe); public: @@ -730,7 +704,7 @@ public: * Returns an explanation of the node propagated to the SAT solver and the theory * that propagated it. */ - NodeTheoryPair getExplanationAndExplainer(TNode node); + Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe); /** * collect model info diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 9b429765e..25b12f75f 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -964,12 +964,9 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec std::vector orderedChildren; bool nullCongruenceFound = false; for (unsigned i = 0; i < eqpc->d_children.size(); ++i) { - if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) { - - // For now, assume there can only be one null congruence child - Assert(!nullCongruenceFound); + if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && + eqpc->d_children[i]->d_node.isNull()) { nullCongruenceFound = true; - Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl; orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]); orderedChildren.push_back(eqpc->d_children[i]->d_children[1]); @@ -1192,6 +1189,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc); if( eqpc ) { eqpc->d_children.push_back( eqpcc ); + + Debug("pf::ee") << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" << std::endl; + eqpc->debug_print("pf::ee", 1); } } @@ -1605,6 +1605,7 @@ void EqualityEngine::propagate() { } void EqualityEngine::debugPrintGraph() const { + Debug("equality::graph") << std::endl << "Dumping graph" << std::endl; for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) { Debug("equality::graph") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):"; @@ -1618,6 +1619,7 @@ void EqualityEngine::debugPrintGraph() const { Debug("equality::graph") << std::endl; } + Debug("equality::graph") << std::endl; } bool EqualityEngine::areEqual(TNode t1, TNode t2) const { @@ -2209,9 +2211,15 @@ bool EqClassIterator::isFinished() const { return d_current == null_id; } -void EqProof::debug_print( const char * c, unsigned tb ) const{ - for( unsigned i=0; iprintTag(d_id); + else + Debug( c ) << d_id; + + Debug( c ) << "("; if( !d_children.empty() || !d_node.isNull() ){ if( !d_node.isNull() ){ Debug( c ) << std::endl; @@ -2221,7 +2229,7 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{ for( unsigned i=0; i0 || !d_node.isNull() ) Debug( c ) << ","; Debug( c ) << std::endl; - d_children[i]->debug_print( c, tb+1 ); + d_children[i]->debug_print( c, tb+1, prettyPrinter ); } } Debug( c ) << ")" << std::endl; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f30f1e8a0..843e7ce7f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -902,11 +902,17 @@ public: class EqProof { public: + class PrettyPrinter { + public: + virtual ~PrettyPrinter() {} + virtual std::string printTag(unsigned tag) = 0; + }; + EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){} unsigned d_id; Node d_node; std::vector< EqProof * > d_children; - void debug_print( const char * c, unsigned tb = 0 ) const; + void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const; };/* class EqProof */ } // Namespace eq diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index d1685bdd1..9c461f57b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -502,7 +502,7 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg void TheoryUF::computeCareGraph() { if (d_sharedTerms.size() > 0) { - //use term indexing + //use term indexing Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl; std::map< Node, quantifiers::TermArgTrie > index; std::map< Node, unsigned > arity; @@ -533,6 +533,7 @@ void TheoryUF::computeCareGraph() { void TheoryUF::conflict(TNode a, TNode b) { eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; + if (a.getKind() == kind::CONST_BOOLEAN) { d_conflictNode = explain(a.iffNode(b),pf); } else { -- cgit v1.2.3