Added a flag to enable/disbale this feature (enabled by default).
Also, added some infrastructure for proving rewrite rules.
# add support for more theories, just list them here in the same order
# you would to the LFSC proof-checker binary.
#
-CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_real.plf th_int.plf
+CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_bv_rewrites.plf th_real.plf th_int.plf
noinst_LTLIBRARIES = libsignatures.la
--- /dev/null
+;
+; Equality swap
+;
+
+(declare rr_bv_eq
+ (! n mpz
+ (! t1 (term (BitVec n))
+ (! t2 (term (BitVec n))
+ (th_holds (iff (= (BitVec n) t2 t1) (= (BitVec n) t1 t2)))))))
+
+;
+; Additional rules...
+;
+
+;
+; Default, if nothing else applied
+;
+
+(declare rr_bv_default
+ (! t1 formula
+ (! t2 formula
+ (th_holds (iff t1 t2))))))
module PROOF "options/proof_options.h" Proof
+option lfscLetification --lfsc-letification bool :default false
+ turns on global letification in LFSC proofs
+
endmodule
void ProofArith::toStream(std::ostream& out) {
Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl;
//AJR : carry this further?
- LetMap map;
+ ProofLetMap map;
toStreamLFSC(out, ProofManager::getArithProof(), d_proof, map);
}
-void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) {
+void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) {
Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl;
pf->debug_print("lfsc-arith");
Debug("lfsc-arith") << std::endl;
toStreamRecLFSC( out, tp, pf, 0, map );
}
-Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) {
+Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) {
Debug("pf::arith") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
pf->debug_print("pf::arith");
Debug("pf::arith") << std::endl;
}
}
-void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
Debug("pf::arith") << "Arith print term: " << term << ". Kind: " << term.getKind()
<< ". Type: " << term.getType()
<< ". Number of children: " << term.getNumChildren() << std::endl;
}
}
-void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
os << " ;; Arith Theory Lemma \n;;";
for (unsigned i = 0; i < lemma.size(); ++i) {
os << lemma[i] <<" ";
}
os <<"\n";
//os << " (clausify_false trust)";
- ArithProof::printTheoryLemmaProof( lemma, os, paren );
+ ArithProof::printTheoryLemmaProof(lemma, os, paren, map);
}
void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
//proof object outputted by TheoryArith
class ProofArith : public Proof {
private:
- static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map);
+ static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map);
public:
ProofArith( theory::eq::EqProof * pf ) : d_proof( pf ) {}
//it is simply an equality engine proof
theory::eq::EqProof * d_proof;
void toStream(std::ostream& out);
- static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map);
+ static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map);
};
LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine)
: ArithProof(arith, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+ virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
}
void ProofArray::toStream(std::ostream& out) {
+ ProofLetMap map;
+ toStream(out, map);
+}
+
+void ProofArray::toStream(std::ostream& out, const ProofLetMap& map) {
Trace("pf::array") << "; Print Array proof..." << std::endl;
- //AJR : carry this further?
- LetMap map;
toStreamLFSC(out, ProofManager::getArrayProof(), d_proof, map);
Debug("pf::array") << "; Print Array proof done!" << std::endl;
}
-void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map) {
+void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map) {
Debug("pf::array") << "Printing array proof in LFSC : " << std::endl;
pf->debug_print("pf::array", 0, &d_proofPrinter);
Debug("pf::array") << std::endl;
TheoryProof* tp,
theory::eq::EqProof* pf,
unsigned tb,
- const LetMap& map) {
+ const ProofLetMap& map) {
Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
pf->debug_print("pf::array", 0, &d_proofPrinter);
return d_skolemToLiteral[skolem];
}
-void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY);
if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) {
}
}
-void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
os << " ;; Array Theory Lemma \n;;";
for (unsigned i = 0; i < lemma.size(); ++i) {
os << lemma[i] <<" ";
}
os <<"\n";
//os << " (clausify_false trust)";
- ArrayProof::printTheoryLemmaProof(lemma, os, paren);
+ ArrayProof::printTheoryLemmaProof(lemma, os, paren, map);
}
void LFSCArrayProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
Node array_one = equality[0][0];
Node array_two = equality[0][1];
- LetMap map;
+ ProofLetMap map;
os << "(ext _ _ ";
printTerm(array_one.toExpr(), os, map);
os << " ";
Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
theory::eq::EqProof* pf,
unsigned tb,
- const LetMap& map);
+ const ProofLetMap& map);
/** Merge tag for ROW applications */
unsigned d_reasonRow;
//it is simply an equality engine proof
theory::eq::EqProof *d_proof;
void toStream(std::ostream& out);
- void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map);
+ void toStream(std::ostream& out, const ProofLetMap& map);
+ void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map);
void registerSkolem(Node equality, Node skolem);
: ArrayProof(arrays, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+ virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
#include "prop/bvminisat/bvminisat.h"
#include "theory/bv/bitblaster_template.h"
#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_rewrite_rules.h"
using namespace CVC4::theory;
using namespace CVC4::theory::bv;
}
}
-void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedTerm( " << term << " ), theory is: "
<< Theory::theoryOf(term) << std::endl;
}
}
-void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const ProofLetMap& map) {
Assert (term.getKind() == kind::BITVECTOR_BITOF);
unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex;
Expr var = term[0];
os << paren.str();
}
-void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) {
std::string op = utils::toLFSCKind(term.getKind());
std::ostringstream paren;
std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : "";
}
}
-void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) {
os <<"(";
os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" ";
os << " ";
os <<")";
}
-void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) {
os <<"(";
os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term[0]) <<" ";
os << " ";
os <<")";
}
-void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) {
os <<"(";
os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" ";
os <<" ";
os << "(BitVec "<<width<<")";
}
-void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" << std::endl;
Expr conflict = utils::mkSortedExpr(kind::OR, lemma);
Debug("pf::bv") << "\tconflict = " << conflict << std::endl;
os << "(trust_f ";
os << "(= (BitVec " << utils::getSize(it->first) << ") ";
os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") ";
- LetMap emptyMap;
+ ProofLetMap emptyMap;
d_proofEngine->printBoundTerm(it->first, os, emptyMap);
os << ")) ";
os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n";
}
}
-void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
- std::ostream& paren) {
- // collect the input clauses used
+void LFSCBitVectorProof::calculateAtomsInBitblastingProof() {
+ // Collect the input clauses used
IdToSatClause used_lemmas;
IdToSatClause used_inputs;
- d_resolutionProof->collectClausesUsed(used_inputs,
- used_lemmas);
- Assert (used_lemmas.empty());
-
- IdToSatClause::iterator it2;
- Debug("pf::bv") << std::endl << "BV Used inputs: " << std::endl;
- for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) {
- Debug("pf::bv") << "\t input = " << *(it2->second) << std::endl;
- }
- Debug("pf::bv") << std::endl;
+ d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
+ d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof);
+ Assert(used_lemmas.empty());
+}
+const std::set<Node>* LFSCBitVectorProof::getAtomsInBitblastingProof() {
+ return &d_atomsInBitblastingProof;
+}
+
+void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& letMap) {
// print mapping between theory atoms and internal SAT variables
os << std::endl << ";; BB atom mapping\n" << std::endl;
- std::set<Node> atoms;
- d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
-
std::set<Node>::iterator atomIt;
Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl;
- for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
+ for (atomIt = d_atomsInBitblastingProof.begin(); atomIt != d_atomsInBitblastingProof.end(); ++atomIt) {
Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl;
}
Debug("pf::bv") << std::endl;
printBitblasting(os, paren);
// print CNF conversion proof for bit-blasted facts
- d_cnfProof->printAtomMapping(atoms, os, paren);
+ IdToSatClause used_lemmas;
+ IdToSatClause used_inputs;
+ d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
+
+ d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl;
for (IdToSatClause::iterator it = used_inputs.begin();
it != used_inputs.end(); ++it) {
os << ")";
}
+void LFSCBitVectorProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) {
+ ProofLetMap emptyMap;
+ os << "(rr_bv_default ";
+ d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap);
+ os << " ";
+ d_proofEngine->printBoundTerm(n1.toExpr(), os, emptyMap);
+ os << ")";
+}
+
} /* namespace CVC4 */
virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0;
virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0;
- virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0;
-
+ virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0;
+ virtual const std::set<Node>* getAtomsInBitblastingProof() = 0;
+ virtual void calculateAtomsInBitblastingProof() = 0;
};
class LFSCBitVectorProof: public BitVectorProof {
void printConstant(Expr term, std::ostream& os);
- void printOperatorNary(Expr term, std::ostream& os, const LetMap& map);
- void printOperatorUnary(Expr term, std::ostream& os, const LetMap& map);
- void printPredicate(Expr term, std::ostream& os, const LetMap& map);
- void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map);
- void printBitOf(Expr term, std::ostream& os, const LetMap& map);
+ void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map);
+ void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map);
+ void printPredicate(Expr term, std::ostream& os, const ProofLetMap& map);
+ void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map);
+ void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map);
ExprToString d_exprToVariableName;
ExprToString d_assignedAliases;
std::map<std::string, std::string> d_aliasToBindDeclaration;
std::string assignAlias(Expr expr);
bool hasAlias(Expr expr);
+
+ std::set<Node> d_atomsInBitblastingProof;
+
public:
LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
:BitVectorProof(bv, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
virtual void printTermBitblasting(Expr term, std::ostream& os);
virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+ virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
virtual void printBitblasting(std::ostream& os, std::ostream& paren);
- virtual void printResolutionProof(std::ostream& os, std::ostream& paren);
+ virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap);
+ void calculateAtomsInBitblastingProof();
+ const std::set<Node>* getAtomsInBitblastingProof();
void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+ void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
};
}/* CVC4 namespace */
}
}
+void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
+ std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap &letMap) {
+ std::set<Node>::const_iterator it = atoms.begin();
+ std::set<Node>::const_iterator end = atoms.end();
+
+ for (;it != end; ++it) {
+ os << "(decl_atom ";
+ Node atom = *it;
+ prop::SatVariable var = getLiteral(atom).getSatVariable();
+ //FIXME hideous
+ LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
+ // pe->printLetTerm(atom.toExpr(), os);
+ pe->printBoundTerm(atom.toExpr(), os, letMap);
+
+ os << " (\\ " << ProofManager::getVarName(var, d_name);
+ os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
+ paren << ")))";
+ }
+}
+
// maps each expr to the position it had in the clause and the polarity it had
Node LFSCCnfProof::clauseToNode(const prop::SatClause& clause,
std::map<Node, unsigned>& childIndex,
virtual void printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren) = 0;
+ virtual void printAtomMapping(const std::set<Node>& atoms,
+ std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap &letMap) = 0;
virtual void printClause(const prop::SatClause& clause,
std::ostream& os,
std::ostream& os,
std::ostream& paren);
+ void printAtomMapping(const std::set<Node>& atoms,
+ std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap &letMap);
+
void printClause(const prop::SatClause& clause,
std::ostream& os,
std::ostream& paren);
#include "base/cvc4_assert.h"
#include "context/context.h"
#include "options/bv_options.h"
+#include "options/proof_options.h"
#include "proof/bitvector_proof.h"
#include "proof/clause_id.h"
#include "proof/cnf_proof.h"
, d_smtEngine(smtEngine)
{}
+void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) {
+ Unreachable();
+}
+
void LFSCProof::toStream(std::ostream& out) {
Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
out << " ;; Printing deferred declarations \n\n";
d_theoryProof->printDeferredDeclarations(out, paren);
+ d_theoryProof->finalizeBvConflicts(used_lemmas, out);
+ ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
+
+ out << "\n ;; Printing the global let map \n";
+
+ ProofLetMap globalLetMap;
+ if (options::lfscLetification()) {
+ ProofManager::currentPM()->printGlobalLetMap(atoms, globalLetMap, out, paren);
+ }
+
out << " ;; Printing aliasing declarations \n\n";
d_theoryProof->printAliasingDeclarations(out, paren);
d_theoryProof->printLemmaRewrites(rewrites, out, paren);
// print trust that input assertions are their preprocessed form
- printPreprocessedAssertions(used_assertions, out, paren);
+ printPreprocessedAssertions(used_assertions, out, paren, globalLetMap);
// print mapping between theory atoms and internal SAT variables
out << ";; Printing mapping from preprocessed assertions into atoms \n";
- d_cnfProof->printAtomMapping(atoms, out, paren);
+ d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap);
Debug("pf::pm") << std::endl << "Printing cnf proof for clauses" << std::endl;
Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
- d_theoryProof->printTheoryLemmas(used_lemmas, out, paren);
+ d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap);
Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
std::ostream& os,
- std::ostream& paren) {
+ std::ostream& paren,
+ ProofLetMap& globalLetMap) {
os << "\n ;; In the preprocessor we trust \n";
NodeSet::const_iterator it = assertions.begin();
NodeSet::const_iterator end = assertions.end();
//TODO
os << "(trust_f ";
- ProofManager::currentPM()->getTheoryProofEngine()->printLetTerm((*it).toExpr(), os);
+ ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
os << ") ";
os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
return out;
}
+void ProofManager::registerRewrite(unsigned ruleId, Node original, Node result){
+ Assert (currentPM()->d_theoryProof != NULL);
+ currentPM()->d_rewriteLog.push_back(RewriteLogEntry(ruleId, original, result));
+}
+
+void ProofManager::clearRewriteLog() {
+ Assert (currentPM()->d_theoryProof != NULL);
+ currentPM()->d_rewriteLog.clear();
+}
+
+std::vector<RewriteLogEntry> ProofManager::getRewriteLog() {
+ return currentPM()->d_rewriteLog;
+}
+
+void ProofManager::dumpRewriteLog() const {
+ Debug("pf::rr") << "Dumpign rewrite log:" << std::endl;
+
+ for (unsigned i = 0; i < d_rewriteLog.size(); ++i) {
+ Debug("pf::rr") << "\tRule " << d_rewriteLog[i].getRuleId()
+ << ": "
+ << d_rewriteLog[i].getOriginal()
+ << " --> "
+ << d_rewriteLog[i].getResult() << std::endl;
+ }
+}
+
+void bind(Expr term, ProofLetMap& map, Bindings& letOrder) {
+ ProofLetMap::iterator it = map.find(term);
+ if (it != map.end())
+ return;
+
+ for (unsigned i = 0; i < term.getNumChildren(); ++i)
+ bind(term[i], map, letOrder);
+
+ unsigned newId = ProofLetCount::newId();
+ ProofLetCount letCount(newId);
+ map[term] = letCount;
+ letOrder.push_back(LetOrderElement(term, newId));
+}
+
+void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
+ ProofLetMap& letMap,
+ std::ostream& out,
+ std::ostringstream& paren) {
+ Bindings letOrder;
+ std::set<Node>::const_iterator atom;
+ for (atom = atoms.begin(); atom != atoms.end(); ++atom) {
+ bind(atom->toExpr(), letMap, letOrder);
+ }
+
+ // TODO: give each theory a chance to add atoms. For now, just query BV directly...
+ const std::set<Node>* additionalAtoms = ProofManager::getBitVectorProof()->getAtomsInBitblastingProof();
+ for (atom = additionalAtoms->begin(); atom != additionalAtoms->end(); ++atom) {
+ Debug("gk::temp") << "Binding additional atom: " << *atom << std::endl;
+ bind(atom->toExpr(), letMap, letOrder);
+ }
+
+ for (unsigned i = 0; i < letOrder.size(); ++i) {
+ Expr currentExpr = letOrder[i].expr;
+ unsigned letId = letOrder[i].id;
+ ProofLetMap::iterator it = letMap.find(currentExpr);
+ Assert(it != letMap.end());
+ out << "\n(@ let" << letId << " ";
+ d_theoryProof->printBoundTerm(currentExpr, out, letMap);
+ paren << ")";
+ it->second.increment();
+ }
+
+ out << std::endl << std::endl;
+}
} /* CVC4 namespace */
#include <iosfwd>
#include <map>
#include "proof/proof.h"
+#include "proof/proof_utils.h"
#include "proof/skolemization_manager.h"
#include "util/proof.h"
#include "expr/node.h"
RULE_ARRAYS_ROW, /* arrays, read-over-write */
};/* enum ProofRules */
+class RewriteLogEntry {
+public:
+ RewriteLogEntry(unsigned ruleId, Node original, Node result)
+ : d_ruleId(ruleId), d_original(original), d_result(result) {
+ }
+
+ unsigned getRuleId() const {
+ return d_ruleId;
+ }
+
+ Node getOriginal() const {
+ return d_original;
+ }
+
+ Node getResult() const {
+ return d_result;
+ }
+
+private:
+ unsigned d_ruleId;
+ Node d_original;
+ Node d_result;
+};
+
class ProofManager {
CoreSatProof* d_satProof;
CnfProof* d_cnfProof;
std::map<std::string, std::string> d_rewriteFilters;
+ std::vector<RewriteLogEntry> d_rewriteLog;
+
protected:
LogicInfo d_logic;
void addRewriteFilter(const std::string &original, const std::string &substitute);
void clearRewriteFilters();
+ static void registerRewrite(unsigned ruleId, Node original, Node result);
+ static void clearRewriteLog();
+
+ std::vector<RewriteLogEntry> getRewriteLog();
+ void dumpRewriteLog() const;
+
+ void printGlobalLetMap(std::set<Node>& atoms,
+ ProofLetMap& letMap,
+ std::ostream& out,
+ std::ostringstream& paren);
};/* class ProofManager */
class LFSCProof : public Proof {
// FIXME: hack until we get preprocessing
void printPreprocessedAssertions(const NodeSet& assertions,
std::ostream& os,
- std::ostream& paren);
+ std::ostream& paren,
+ ProofLetMap& globalLetMap);
public:
LFSCProof(SmtEngine* smtEngine,
LFSCCoreSatProof* sat,
LFSCCnfProof* cnf,
LFSCTheoryProofEngine* theory);
virtual void toStream(std::ostream& out);
+ virtual void toStream(std::ostream& out, const ProofLetMap& map);
virtual ~LFSCProof() {}
};/* class LFSCProof */
typedef std::pair<Node, Node> NodePair;
typedef std::set<NodePair> NodePairSet;
+
+struct ProofLetCount {
+ static unsigned counter;
+ static void resetCounter() { counter = 0; }
+ static unsigned newId() { return ++counter; }
+
+ unsigned count;
+ unsigned id;
+ ProofLetCount()
+ : count(0)
+ , id(-1)
+ {}
+
+ void increment() { ++count; }
+ ProofLetCount(unsigned i)
+ : count(1)
+ , id(i)
+ {}
+
+ ProofLetCount(const ProofLetCount& other)
+ : count(other.count)
+ , id (other.id)
+ {}
+
+ bool operator==(const ProofLetCount &other) const {
+ return other.id == id && other.count == count;
+ }
+
+ ProofLetCount& operator=(const ProofLetCount &rhs) {
+ if (&rhs == this) return *this;
+ id = rhs.id;
+ count = rhs.count;
+ return *this;
+ }
+};
+
+struct LetOrderElement {
+ Expr expr;
+ unsigned id;
+ LetOrderElement(Expr e, unsigned i)
+ : expr(e)
+ , id(i)
+ {}
+
+ LetOrderElement()
+ : expr()
+ , id(-1)
+ {}
+};
+
+typedef std::vector<LetOrderElement> Bindings;
+
namespace utils {
std::string toLFSCKind(Kind kind);
namespace CVC4 {
-unsigned CVC4::LetCount::counter = 0;
+unsigned CVC4::ProofLetCount::counter = 0;
static unsigned LET_COUNT = 1;
TheoryProofEngine::TheoryProofEngine()
return pm->getCnfProof()->getProofRecipe(nodes).getTheory();
}
-void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) {
- LetMap::iterator it = map.find(term);
+void LFSCTheoryProofEngine::bind(Expr term, ProofLetMap& map, Bindings& let_order) {
+ ProofLetMap::iterator it = map.find(term);
if (it != map.end()) {
- LetCount& count = it->second;
+ ProofLetCount& count = it->second;
count.increment();
return;
}
for (unsigned i = 0; i < term.getNumChildren(); ++i) {
bind(term[i], map, let_order);
}
- unsigned new_id = LetCount::newId();
- map[term] = LetCount(new_id);
+ unsigned new_id = ProofLetCount::newId();
+ map[term] = ProofLetCount(new_id);
let_order.push_back(LetOrderElement(term, new_id));
}
void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) {
- LetMap map;
+ ProofLetMap map;
Bindings let_order;
bind(term, map, let_order);
std::ostringstream paren;
for (unsigned i = 0; i < let_order.size(); ++i) {
Expr current_expr = let_order[i].expr;
unsigned let_id = let_order[i].id;
- LetMap::const_iterator it = map.find(current_expr);
+ ProofLetMap::const_iterator it = map.find(current_expr);
Assert (it != map.end());
unsigned let_count = it->second.count;
Assert(let_count);
continue;
}
- os << "(@ let"<<let_id << " ";
+ os << "(@ let" <<let_id << " ";
printTheoryTerm(current_expr, os, map);
paren <<")";
}
printTheoryTerm(last, os, map);
}
else {
- os << " let"<< last_let_id;
+ os << " let" << last_let_id;
}
os << paren.str();
}
-
-void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
theory::TheoryId theory_id = theory::Theory::theoryOf(term);
// boolean terms and ITEs are special because they
std::ostringstream name;
name << "A" << counter++;
os << "(% " << name.str() << " (th_holds ";
- printLetTerm(*it, os);
+
+ // Assertions appear before the global let map, so we use a dummpMap to avoid letification here.
+ ProofLetMap dummyMap;
+ printBoundTerm(*it, os, dummyMap);
+
os << ")\n";
paren << ")";
}
Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl;
}
-void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren) {
+void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites,
+ std::ostream& os,
+ std::ostream& paren) {
Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites called" << std::endl << std::endl;
NodePairSet::const_iterator it;
for (it = rewrites.begin(); it != rewrites.end(); ++it) {
Debug("pf::tp") << "printLemmaRewrites: " << it->first << " --> " << it->second << std::endl;
+ Node n1 = it->first;
+ Node n2 = it->second;
+ Assert(theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2));
+
std::ostringstream rewriteRule;
rewriteRule << ".lrr" << d_assertionToRewrite.size();
- LetMap emptyMap;
- os << "(th_let_pf _ (trust_f (iff ";
- printBoundTerm(it->second.toExpr(), os, emptyMap);
- os << " ";
- printBoundTerm(it->first.toExpr(), os, emptyMap);
- os << ")) (\\ " << rewriteRule.str() << "\n";
+ os << "(th_let_pf _ ";
+ getTheoryProof(theory::Theory::theoryOf(n1))->printRewriteProof(os, n1, n2);
+ os << "(\\ " << rewriteRule.str() << "\n";
d_assertionToRewrite[it->first] = rewriteRule.str();
Debug("pf::tp") << "d_assertionToRewrite[" << it->first << "] = " << rewriteRule.str() << std::endl;
}
// TODO: this function should be moved into the BV prover.
-void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) {
+void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os) {
// BitVector theory is special case: must know all conflicts needed
// ahead of time for resolution proof lemmas
std::vector<Expr> bv_lemmas;
BitVectorProof* bv = ProofManager::getBitVectorProof();
bv->finalizeConflicts(bv_lemmas);
- bv->printResolutionProof(os, paren);
+ // bv->printResolutionProof(os, paren, letMap);
}
void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
std::ostream& os,
- std::ostream& paren) {
+ std::ostream& paren,
+ ProofLetMap& map) {
os << " ;; Theory Lemmas \n";
Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl;
dumpTheoryLemmas(lemmas);
}
- finalizeBvConflicts(lemmas, os, paren);
+ // finalizeBvConflicts(lemmas, os, paren, map);
+ ProofManager::getBitVectorProof()->printResolutionProof(os, paren, map);
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
Assert (lemmas.size() == 1);
// Query the appropriate theory for a proof of this clause
theory::TheoryId theory_id = getTheoryForLemma(clause);
Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
- getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren);
+ getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren, map);
// Turn rewrite filter OFF
pm->clearRewriteFilters();
pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
}
- getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren);
+ getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren, map);
// Turn rewrite filter OFF
pm->clearRewriteFilters();
}
}
-void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
- LetMap::const_iterator it = map.find(term);
+ ProofLetMap::const_iterator it = map.find(term);
if (it != map.end()) {
unsigned id = it->second.id;
unsigned count = it->second.count;
if (count > LET_COUNT) {
- os <<"let"<<id;
+ os << "let" << id;
return;
}
}
printTheoryTerm(term, os, map);
}
-void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
if (term.isVariable()) {
os << ProofManager::sanitize(term);
return;
}
-void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) {
// Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
Assert(d_theory!=NULL);
th->check(theory::Theory::EFFORT_FULL);
}
Debug("pf::tp") << "Calling oc.d_proof->toStream(os)" << std::endl;
- oc.d_proof->toStream(os);
+ oc.d_proof->toStream(os, map);
Debug("pf::tp") << "Calling oc.d_proof->toStream(os) -- DONE!" << std::endl;
Debug("pf::tp") << "About to delete the theory solver used for proving the lemma... " << std::endl;
}
}
-void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
Assert (term.getType().isBoolean());
if (term.isVariable()) {
if (d_treatBoolsAsFormulas)
void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
// By default, we just print a trust statement. Specific theories can implement
// better proofs.
- LetMap emptyMap;
+ ProofLetMap emptyMap;
os << "(trust_f (not (= _ ";
d_proofEngine->printBoundTerm(c1, os, emptyMap);
os << ")))";
}
+void TheoryProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) {
+ // This is the default for a rewrite proof: just a trust statement.
+ ProofLetMap emptyMap;
+ os << "(trust_f (iff ";
+ d_proofEngine->printBoundTerm(n1.toExpr(), os, emptyMap);
+ os << " ";
+ d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap);
+ os << "))";
+}
+
} /* namespace CVC4 */
class Theory;
} /* namespace CVC4::theory */
-struct LetCount {
- static unsigned counter;
- static void resetCounter() { counter = 0; }
- static unsigned newId() { return ++counter; }
-
- unsigned count;
- unsigned id;
- LetCount()
- : count(0)
- , id(-1)
- {}
-
- void increment() { ++count; }
- LetCount(unsigned i)
- : count(1)
- , id(i)
- {}
- LetCount(const LetCount& other)
- : count(other.count)
- , id (other.id)
- {}
- bool operator==(const LetCount &other) const {
- return other.id == id && other.count == count;
- }
- LetCount& operator=(const LetCount &rhs) {
- if (&rhs == this) return *this;
- id = rhs.id;
- count = rhs.count;
- return *this;
- }
-};
-
-struct LetOrderElement {
- Expr expr;
- unsigned id;
- LetOrderElement(Expr e, unsigned i)
- : expr(e)
- , id(i)
- {}
-
- LetOrderElement()
- : expr()
- , id(-1)
- {}
-};
-
typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
-typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap;
-typedef std::vector<LetOrderElement> Bindings;
-
class TheoryProof;
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
*/
virtual void printLetTerm(Expr term, std::ostream& os) = 0;
virtual void printBoundTerm(Expr term, std::ostream& os,
- const LetMap& map) = 0;
+ const ProofLetMap& map) = 0;
/**
* Print the proof representation of the given sort.
* @param paren
*/
virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os,
- std::ostream& paren) = 0;
+ std::ostream& paren, ProofLetMap& map) = 0;
/**
* Register theory atom (ensures all terms and atoms are declared).
void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
virtual void treatBoolsAsFormulas(bool value) {};
+
+ virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
};
class LFSCTheoryProofEngine : public TheoryProofEngine {
- LetMap d_letMap;
- void printTheoryTerm(Expr term, std::ostream& os, const LetMap& map);
- void bind(Expr term, LetMap& map, Bindings& let_order);
+ void bind(Expr term, ProofLetMap& map, Bindings& let_order);
public:
LFSCTheoryProofEngine()
: TheoryProofEngine() {}
+ void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map);
+
void registerTermsFromAssertions();
void printSortDeclarations(std::ostream& os, std::ostream& paren);
void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printCoreTerm(Expr term, std::ostream& os, const LetMap& map);
+ virtual void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map);
virtual void printLetTerm(Expr term, std::ostream& os);
- virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map);
+ virtual void printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map);
virtual void printAssertions(std::ostream& os, std::ostream& paren);
virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTheoryLemmas(const IdToSatClause& lemmas,
std::ostream& os,
- std::ostream& paren);
+ std::ostream& paren,
+ ProofLetMap& map);
virtual void printSort(Type type, std::ostream& os);
void performExtraRegistrations();
void treatBoolsAsFormulas(bool value);
+ void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os);
private:
static void dumpTheoryLemmas(const IdToSatClause& lemmas);
// TODO: this function should be moved into the BV prover.
- void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren);
std::map<Node, std::string> d_assertionToRewrite;
};
* @param term expresion representing term
* @param os output stream
*/
- void printTerm(Expr term, std::ostream& os, const LetMap& map) {
+ void printTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
d_proofEngine->printBoundTerm(term, os, map);
}
/**
* @param term expresion representing term
* @param os output stream
*/
- virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
/**
* Print the proof representation of the given type that belongs to some theory.
*
*
* @param os output stream
*/
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+ virtual void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map);
/**
* Print the sorts declarations for this theory.
*
* @param term
*/
virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+ /**
+ * Print a proof for the equivalence of n1 and n2.
+ *
+ * @param term
+ */
+ virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
virtual void treatBoolsAsFormulas(bool value) {}
};
virtual void registerTerm(Expr term);
- virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
virtual void printOwnedSort(Type type, std::ostream& os) = 0;
virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0;
LFSCBooleanProof(TheoryProofEngine* proofEngine)
: BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
void ProofUF::toStream(std::ostream& out) {
+ ProofLetMap map;
+ toStream(out, map);
+}
+
+void ProofUF::toStream(std::ostream& out, const ProofLetMap& map) {
Trace("theory-proof-debug") << "; Print UF proof..." << std::endl;
//AJR : carry this further?
- LetMap map;
toStreamLFSC(out, ProofManager::getUfProof(), d_proof, map);
}
-void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) {
+void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) {
Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl;
Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl;
pf->debug_print("lfsc-uf");
toStreamRecLFSC( out, tp, pf, 0, map );
}
-Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) {
+Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) {
Debug("pf::uf") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
pf->debug_print("pf::uf");
Debug("pf::uf") << std::endl;
}
}
-void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl;
Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF);
os << type <<" ";
}
-void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
os << " ;; UF Theory Lemma \n;;";
for (unsigned i = 0; i < lemma.size(); ++i) {
os << lemma[i] <<" ";
}
os <<"\n";
//os << " (clausify_false trust)";
- UFProof::printTheoryLemmaProof( lemma, os, paren );
+ UFProof::printTheoryLemmaProof(lemma, os, paren, map);
}
void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
//proof object outputted by TheoryUF
class ProofUF : public Proof {
private:
- static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map);
+ static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map);
public:
ProofUF( theory::eq::EqProof * pf ) : d_proof( pf ) {}
//it is simply an equality engine proof
theory::eq::EqProof * d_proof;
void toStream(std::ostream& out);
- static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map);
+ void toStream(std::ostream& out, const ProofLetMap& map);
+ static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map);
};
LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine)
: UFProof(uf, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+ virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
#define __CVC4__PROOF_H
#include <iosfwd>
+#include <ext/hash_map>
namespace CVC4 {
+class Expr;
+class ProofLetCount;
+struct ExprHashFunction;
+
+typedef __gnu_cxx::hash_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap;
+
class CVC4_PUBLIC Proof {
public:
virtual ~Proof() { }
virtual void toStream(std::ostream& out) = 0;
+ virtual void toStream(std::ostream& out, const ProofLetMap& map) = 0;
};/* class Proof */
}/* CVC4 namespace */
projects / cvc5.git / commitdiff