diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 16:59:28 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 17:58:14 -0400 |
commit | 2dbe1f150d30f0fb0c8522f891104270ce09db4c (patch) | |
tree | 1305f3de890f4353c3b5695a93ab7e2419760617 /src/proof | |
parent | 4ec2c8eb8b8a50dc743119100767e101f19305f6 (diff) |
Unsat core infrastruture and API (SMT-LIB compliance to come).
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/cnf_proof.cpp | 128 | ||||
-rw-r--r-- | src/proof/cnf_proof.h | 40 | ||||
-rw-r--r-- | src/proof/proof.h | 6 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 119 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 63 | ||||
-rw-r--r-- | src/proof/sat_proof.cpp | 77 | ||||
-rw-r--r-- | src/proof/sat_proof.h | 16 |
7 files changed, 300 insertions, 149 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 3dfb61428..22a40ff69 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -30,6 +30,8 @@ CnfProof::CnfProof(CnfStream* stream) : d_cnfStream(stream) {} +CnfProof::~CnfProof() { +} Expr CnfProof::getAtom(prop::SatVariable var) { prop::SatLiteral lit (var); @@ -38,34 +40,33 @@ Expr CnfProof::getAtom(prop::SatVariable var) { return atom; } -CnfProof::~CnfProof() { -} - -LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() { - return iterator(*this, ProofManager::currentPM()->begin_vars()); +prop::SatLiteral CnfProof::getLiteral(TNode atom) { + return d_cnfStream->getLiteral(atom); } -LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() { - return iterator(*this, ProofManager::currentPM()->end_vars()); +Expr CnfProof::getAssertion(uint64_t id) { + return d_cnfStream->getAssertion(id).toExpr(); } -void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) { - ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars(); - ProofManager::var_iterator end = ProofManager::currentPM()->end_vars(); - - for (;it != end; ++it) { - os << "(decl_atom "; - - if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { - Expr atom = getAtom(*it); - LFSCTheoryProof::printTerm(atom, os); - } else { - // print fake atoms for all other logics - os << "true "; +void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren) { + for (unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = clause->operator[](i); + if(d_atomsDeclared.find(lit.getSatVariable()) == d_atomsDeclared.end()) { + d_atomsDeclared.insert(lit.getSatVariable()); + os << "(decl_atom "; + if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0 || + ProofManager::currentPM()->getLogic().compare("QF_AX") == 0 || + ProofManager::currentPM()->getLogic().compare("QF_SAT") == 0) { + Expr atom = getAtom(lit.getSatVariable()); + LFSCTheoryProof::printTerm(atom, os); + } else { + // print fake atoms for all other logics (for now) + os << "true "; + } + + os << " (\\ " << ProofManager::getVarName(lit.getSatVariable()) << " (\\ " << ProofManager::getAtomName(lit.getSatVariable()) << "\n"; + paren << ")))"; } - - os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n"; - paren << ")))"; } } @@ -75,36 +76,93 @@ void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { } void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { - os << " ;; Input Clauses \n"; + os << " ;; Clauses\n"; ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses(); ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses(); for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; + printAtomMapping(clause, os, paren); os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); - os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getInputClauseName(id) << "\n"; + os << "(clausify_false trust)" << clause_paren.str() + << " (\\ " << ProofManager::getInputClauseName(id) << "\n"; paren << "))"; } } - void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) { - os << " ;; Theory Lemmas \n"; - ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas(); - ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas(); + os << " ;; Theory Lemmas\n"; + ProofManager::ordered_clause_iterator it = ProofManager::currentPM()->begin_lemmas(); + ProofManager::ordered_clause_iterator end = ProofManager::currentPM()->end_lemmas(); + + for(size_t n = 0; it != end; ++it, ++n) { + if(n % 100 == 0) { + Chat() << "proving theory conflicts...(" << n << "/" << ProofManager::currentPM()->num_lemmas() << ")" << std::endl; + } - for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; + NodeBuilder<> c(kind::AND); + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + prop::SatVariable var = lit.getSatVariable(); + if(lit.isNegated()) { + c << Node::fromExpr(getAtom(var)); + } else { + c << Node::fromExpr(getAtom(var)).notNode(); + } + } + Node cl = c; + if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) { + uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id]; + TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff); + if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) { + Debug("cores") << "; extensional lemma!" << std::endl; + Assert(cl.getKind() == kind::AND && cl.getNumChildren() == 2 && cl[0].getKind() == kind::EQUAL && cl[0][0].getKind() == kind::SELECT); + TNode myk = cl[0][0][1]; + Debug("cores") << "; so my skolemized k is " << myk << std::endl; + os << "(ext _ _ " << orig[0][0] << " " << orig[0][1] << " (\\ " << myk << " (\\ " << ProofManager::getLemmaName(id) << "\n"; + paren << ")))"; + } + } + printAtomMapping(clause, os, paren); os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); - os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n"; + + Debug("cores") << "\n;id is " << id << std::endl; + if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) { + uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id]; + Debug("cores") << ";getting id " << int32_t(proof_id & 0xffffffff) << std::endl; + Assert(int32_t(proof_id & 0xffffffff) != -1); + TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff); + Debug("cores") << "; ID is " << id << " and that's a lemma with " << ((proof_id >> 32) & 0xffffffff) << " / " << (proof_id & 0xffffffff) << std::endl; + Debug("cores") << "; that means the lemma was " << orig << std::endl; + if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) { + Debug("cores") << "; extensional" << std::endl; + os << "(clausify_false trust)\n"; + } else if(proof_id == 0) { + // theory propagation caused conflict + //ProofManager::currentPM()->printProof(os, cl); + os << "(clausify_false trust)\n"; + } else if(((proof_id >> 32) & 0xffffffff) == RULE_CONFLICT) { + os << "\n;; need to generate a (conflict) proof of " << cl << "\n"; + //ProofManager::currentPM()->printProof(os, cl); + os << "(clausify_false trust)\n"; + } else { + os << "\n;; need to generate a (lemma) proof of " << cl; + os << "\n;; DON'T KNOW HOW !!\n"; + os << "(clausify_false trust)\n"; + } + } else { + os << "\n;; need to generate a (conflict) proof of " << cl << "\n"; + ProofManager::currentPM()->printProof(os, cl); + } + os << clause_paren.str() + << " (\\ " << ProofManager::getLemmaClauseName(id) << "\n"; paren << "))"; } } @@ -114,10 +172,10 @@ void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, prop::SatLiteral lit = clause[i]; prop::SatVariable var = lit.getSatVariable(); if (lit.isNegated()) { - os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; + os << "(ast _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " "; paren << "))"; } else { - os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; + os << "(asf _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " "; paren << "))"; } } diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index b2c35c4f7..459815e60 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -30,62 +30,38 @@ namespace CVC4 { namespace prop { class CnfStream; -} +}/* CVC4::prop namespace */ class CnfProof; -class AtomIterator { - CnfProof& d_cnf; - ProofManager::var_iterator d_it; - -public: - AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it) - : d_cnf(cnf), d_it(it) - {} - inline Expr operator*(); - AtomIterator& operator++() { ++d_it; return *this; } - AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; } - bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; } - bool operator!=(const AtomIterator& it) const { return !(*this == it); } -};/* class AtomIterator */ - class CnfProof { protected: CVC4::prop::CnfStream* d_cnfStream; - Expr getAtom(prop::SatVariable var); - friend class AtomIterator; + VarSet d_atomsDeclared; public: CnfProof(CVC4::prop::CnfStream* cnfStream); - typedef AtomIterator iterator; - virtual iterator begin_atom_mapping() = 0; - virtual iterator end_atom_mapping() = 0; + Expr getAtom(prop::SatVariable var); + Expr getAssertion(uint64_t id); + prop::SatLiteral getLiteral(TNode atom); - virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; virtual ~CnfProof(); -}; +};/* class CnfProof */ class LFSCCnfProof : public CnfProof { void printInputClauses(std::ostream& os, std::ostream& paren); void printTheoryLemmas(std::ostream& os, std::ostream& paren); void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); + virtual void printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren); public: LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) : CnfProof(cnfStream) {} - virtual iterator begin_atom_mapping(); - virtual iterator end_atom_mapping(); - - virtual void printAtomMapping(std::ostream& os, std::ostream& paren); virtual void printClauses(std::ostream& os, std::ostream& paren); -}; - -inline Expr AtomIterator::operator*() { - return d_cnf.getAtom(*d_it); -} +};/* class LFSCCnfProof */ } /* CVC4 namespace */ diff --git a/src/proof/proof.h b/src/proof/proof.h index 174913755..440279dbc 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -22,9 +22,9 @@ #include "smt/options.h" #ifdef CVC4_PROOF -# define PROOF(x) if(options::proof()) { x; } -# define NULLPROOF(x) (options::proof()) ? x : NULL -# define PROOF_ON() options::proof() +# define PROOF(x) if(options::proof() || options::unsatCores()) { x; } +# define NULLPROOF(x) (options::proof() || options::unsatCores()) ? x : NULL +# define PROOF_ON() (options::proof() || options::unsatCores()) #else /* CVC4_PROOF */ # define PROOF(x) # define NULLPROOF(x) NULL diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 680e57d39..0cca16574 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -23,6 +23,15 @@ #include "util/cvc4_assert.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "theory/output_channel.h" +#include "theory/valuation.h" +#include "util/node_visitor.h" +#include "theory/term_registration_visitor.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/equality_engine.h" +#include "theory/arrays/theory_arrays.h" +#include "context/context.h" +#include "util/hash.h" namespace CVC4 { @@ -37,7 +46,8 @@ ProofManager::ProofManager(ProofFormat format): d_cnfProof(NULL), d_theoryProof(NULL), d_fullProof(NULL), - d_format(format) + d_format(format), + d_deps() { } @@ -53,7 +63,7 @@ ProofManager::~ProofManager() { delete it->second; } - for(IdToClause::iterator it = d_theoryLemmas.begin(); + for(OrderedIdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { delete it->second; @@ -91,11 +101,10 @@ CnfProof* ProofManager::getCnfProof() { } TheoryProof* ProofManager::getTheoryProof() { - Assert (currentPM()->d_theoryProof); + //Assert (currentPM()->d_theoryProof); return currentPM()->d_theoryProof; } - void ProofManager::initSatProof(Minisat::Solver* solver) { Assert (currentPM()->d_satProof == NULL); Assert(currentPM()->d_format == LFSC); @@ -114,35 +123,101 @@ void ProofManager::initTheoryProof() { currentPM()->d_theoryProof = new LFSCTheoryProof(); } - -std::string ProofManager::getInputClauseName(ClauseId id) {return append("pb", id); } -std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lem", id); } +std::string ProofManager::getInputClauseName(ClauseId id) { return append("pb", id); } +std::string ProofManager::getLemmaName(ClauseId id) { return append("lem", id); } +std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lemc", id); } std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); } -std::string ProofManager::getVarName(prop::SatVariable var) { return append("v", var); } -std::string ProofManager::getAtomName(prop::SatVariable var) { return append("a", var); } -std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); } +std::string ProofManager::getVarName(prop::SatVariable var) { return append("var", var); } +std::string ProofManager::getAtomName(prop::SatVariable var) { return append("atom", var); } +std::string ProofManager::getLitName(prop::SatLiteral lit) { return append("lit", lit.toInt()); } + +std::string ProofManager::getAtomName(TNode atom) { + prop::SatLiteral lit = currentPM()->d_cnfProof->getLiteral(atom); + Assert(!lit.isNegated()); + return getAtomName(lit.getSatVariable()); +} +std::string ProofManager::getLitName(TNode lit) { + return getLitName(currentPM()->d_cnfProof->getLiteral(lit)); +} + +void ProofManager::traceDeps(TNode n) { + Debug("cores") << "trace deps " << n << std::endl; + if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) { + // originating formula was in core set + Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl; + d_outputCoreFormulas.insert(n.toExpr()); + } else { + Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl; + if(d_deps.find(n) == d_deps.end()) { + InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str()); + } + Assert(d_deps.find(n) != d_deps.end()); + std::vector<Node> deps = (*d_deps.find(n)).second; + for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) { + Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl; + traceDeps(*i); + } + } +} void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { - for (unsigned i = 0; i < clause->size(); ++i) { + /*for (unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = clause->operator[](i); d_propVars.insert(lit.getSatVariable()); - } + }*/ if (kind == INPUT) { d_inputClauses.insert(std::make_pair(id, clause)); - return; + Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end()); + Debug("cores") << "core id is " << d_satProof->d_inputClauses[id] << std::endl; + if(d_satProof->d_inputClauses[id] == uint64_t(-1)) { + Debug("cores") << " + constant unit (true or false)" << std::endl; + } else if(options::unsatCores()) { + Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff); + Debug("cores") << "core input assertion from CnfStream is " << e << std::endl; + Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) << std::endl; + // Invalid proof rules are currently used for parts of CVC4 that don't + // support proofs (these are e.g. unproven theory lemmas) or don't need + // proofs (e.g. split lemmas). We can ignore these safely when + // constructing unsat cores. + if(((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) != RULE_INVALID) { + // trace dependences back to actual assertions + traceDeps(Node::fromExpr(e)); + } + } + } else { + Assert(kind == THEORY_LEMMA); + d_theoryLemmas.insert(std::make_pair(id, clause)); } - Assert (kind == THEORY_LEMMA); - d_theoryLemmas.insert(std::make_pair(id, clause)); } -void ProofManager::addAssertion(Expr formula) { +void ProofManager::addAssertion(Expr formula, bool inUnsatCore) { + Debug("cores") << "assert: " << formula << std::endl; d_inputFormulas.insert(formula); + d_deps[Node::fromExpr(formula)]; // empty vector of deps + if(inUnsatCore || options::dumpUnsatCores()) { + Debug("cores") << "adding to input core forms: " << formula << std::endl; + d_inputCoreFormulas.insert(formula); + } } -void ProofManager::setLogic(const std::string& logic_string) { - d_logic = logic_string; +void ProofManager::addDependence(TNode n, TNode dep) { + if(dep != n) { + Debug("cores") << "dep: " << n << " : " << dep << std::endl; + if(d_deps.find(dep) == d_deps.end()) { + Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl; + } + //Assert(d_deps.find(dep) != d_deps.end()); + d_deps[n].push_back(dep); + } +} + +void ProofManager::setLogic(const LogicInfo& logic) { + d_logic = logic; } +void ProofManager::printProof(std::ostream& os, TNode n) { + // no proofs here yet +} LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) : d_satProof(sat) @@ -157,17 +232,18 @@ void LFSCProof::toStream(std::ostream& out) { smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check\n"; + out << " ;; Declarations\n"; if (d_theoryProof == NULL) { d_theoryProof = new LFSCTheoryProof(); } - for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping(); + /*for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping(); i != d_cnfProof->end_atom_mapping(); ++i) { d_theoryProof->addDeclaration(*i); - } + }*/ d_theoryProof->printAssertions(out, paren); + out << " ;; Proof of empty clause follows\n"; out << "(: (holds cln)\n"; - d_cnfProof->printAtomMapping(out, paren); d_cnfProof->printClauses(out, paren); d_satProof->printResolutions(out, paren); paren <<")))\n;;"; @@ -175,5 +251,4 @@ void LFSCProof::toStream(std::ostream& out) { out << "\n"; } - } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index f428de36d..d60a3f6e3 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -20,9 +20,12 @@ #define __CVC4__PROOF_MANAGER_H #include <iostream> +#include <map> #include "proof/proof.h" #include "util/proof.h" - +#include "expr/node.h" +#include "theory/logic_info.h" +#include "theory/substitutions.h" // forward declarations namespace Minisat { @@ -63,6 +66,7 @@ enum ProofFormat { std::string append(const std::string& str, uint64_t num); typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; +typedef std::map < ClauseId, const prop::SatClause* > OrderedIdToClause; typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet; typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; @@ -74,6 +78,18 @@ enum ClauseKind { LEARNT };/* enum ClauseKind */ +enum ProofRule { + RULE_GIVEN, /* input assertion */ + RULE_DERIVED, /* a "macro" rule */ + RULE_RECONSTRUCT, /* prove equivalence using another method */ + RULE_TRUST, /* trust without evidence (escape hatch until proofs are fully supported) */ + RULE_INVALID, /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */ + RULE_CONFLICT, /* re-construct as a conflict */ + + RULE_ARRAYS_EXT, /* arrays, extensional */ + RULE_ARRAYS_ROW, /* arrays, read-over-write */ +};/* enum ProofRules */ + class ProofManager { SatProof* d_satProof; CnfProof* d_cnfProof; @@ -81,15 +97,25 @@ class ProofManager { // information that will need to be shared across proofs IdToClause d_inputClauses; - IdToClause d_theoryLemmas; + OrderedIdToClause d_theoryLemmas; + IdToClause d_theoryPropagations; ExprSet d_inputFormulas; - VarSet d_propVars; + ExprSet d_inputCoreFormulas; + ExprSet d_outputCoreFormulas; + //VarSet d_propVars; + + int d_nextId; Proof* d_fullProof; ProofFormat d_format; // used for now only in debug builds + __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction > d_deps; + + // trace dependences back to unsat core + void traceDeps(TNode n); + protected: - std::string d_logic; + LogicInfo d_logic; public: ProofManager(ProofFormat format = LFSC); @@ -109,35 +135,50 @@ public: // iterators over data shared by proofs typedef IdToClause::const_iterator clause_iterator; + typedef OrderedIdToClause::const_iterator ordered_clause_iterator; typedef ExprSet::const_iterator assertions_iterator; typedef VarSet::const_iterator var_iterator; clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); } clause_iterator end_input_clauses() const { return d_inputClauses.end(); } + size_t num_input_clauses() const { return d_inputClauses.size(); } - clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); } - clause_iterator end_lemmas() const { return d_theoryLemmas.end(); } + ordered_clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); } + ordered_clause_iterator end_lemmas() const { return d_theoryLemmas.end(); } + size_t num_lemmas() const { return d_theoryLemmas.size(); } assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); } assertions_iterator end_assertions() const { return d_inputFormulas.end(); } + size_t num_assertions() const { return d_inputFormulas.size(); } - var_iterator begin_vars() const { return d_propVars.begin(); } - var_iterator end_vars() const { return d_propVars.end(); } + void printProof(std::ostream& os, TNode n); - void addAssertion(Expr formula); + void addAssertion(Expr formula, bool inUnsatCore); void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); + // note that n depends on dep (for cores) + void addDependence(TNode n, TNode dep); + + assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); } + assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); } + size_t size_unsat_core() const { return d_outputCoreFormulas.size(); } + + int nextId() { return d_nextId++; } // variable prefixes static std::string getInputClauseName(ClauseId id); + static std::string getLemmaName(ClauseId id); static std::string getLemmaClauseName(ClauseId id); static std::string getLearntClauseName(ClauseId id); static std::string getVarName(prop::SatVariable var); static std::string getAtomName(prop::SatVariable var); + static std::string getAtomName(TNode atom); static std::string getLitName(prop::SatLiteral lit); + static std::string getLitName(TNode lit); + + void setLogic(const LogicInfo& logic); + const std::string getLogic() const { return d_logic.getLogicString(); } - void setLogic(const std::string& logic_string); - const std::string getLogic() const { return d_logic; } };/* class ProofManager */ class LFSCProof : public Proof { diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 0ace84b4d..f7b9c4889 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -57,9 +57,6 @@ void printDebug (Minisat::Clause& c) { Debug("proof:sat") << endl; } - -int SatProof::d_idCounter = 0; - /** * Converts the clause associated to id to a set of literals * @@ -274,7 +271,7 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) { Minisat::CRef SatProof::getClauseRef(ClauseId id) { if (d_idClause.find(id) == d_idClause.end()) { - Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" " + Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " " << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "") << (isUnit(id)? "Unit" : "") << endl; } @@ -318,16 +315,14 @@ bool SatProof::isLemmaClause(ClauseId id) { return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); } - void SatProof::print(ClauseId id) { if (d_deleted.find(id) != d_deleted.end()) { - Debug("proof:sat") << "del"<<id; + Debug("proof:sat") << "del" << id; } else if (isUnit(id)) { printLit(getUnit(id)); } else if (id == d_emptyClauseId) { - Debug("proof:sat") << "empty "<< endl; - } - else { + Debug("proof:sat") << "empty " << endl; + } else { CRef ref = getClauseRef(id); printClause(getClause(ref)); } @@ -335,7 +330,7 @@ void SatProof::print(ClauseId id) { void SatProof::printRes(ClauseId id) { Assert(hasResolution(id)); - Debug("proof:sat") << "id "<< id <<": "; + Debug("proof:sat") << "id " << id << ": "; printRes(d_resChains[id]); } @@ -364,42 +359,44 @@ void SatProof::printRes(ResChain* res) { /// registration methods -ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) { +ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) { + Debug("cores") << "registerClause " << proof_id << std::endl; Assert(clause != CRef_Undef); ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { - ClauseId newId = d_idCounter++; + ClauseId newId = ProofManager::currentPM()->nextId(); d_clauseId[clause] = newId; d_idClause[newId] = clause; if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses.insert(newId); + d_inputClauses[newId] = proof_id; } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses.insert(newId); + d_lemmaClauses[newId] = proof_id; } } - Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; + Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n"; return d_clauseId[clause]; } -ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) { +ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) { + Debug("cores") << "registerUnitClause " << kind << " " << proof_id << std::endl; UnitIdMap::iterator it = d_unitId.find(toInt(lit)); if (it == d_unitId.end()) { - ClauseId newId = d_idCounter++; + ClauseId newId = ProofManager::currentPM()->nextId(); d_unitId[toInt(lit)] = newId; d_idUnit[newId] = lit; if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses.insert(newId); + d_inputClauses[newId] = proof_id; } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses.insert(newId); + d_lemmaClauses[newId] = proof_id; } } - Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; + Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n"; return d_unitId[toInt(lit)]; } @@ -445,7 +442,7 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) { removedDfs(*it, removed, removeStack, inClause, seen); } - for (int i = removeStack.size()-1; i >= 0; --i) { + for (int i = removeStack.size() - 1; i >= 0; --i) { Lit lit = removeStack[i]; CRef reason_ref = d_solver->reason(var(lit)); ClauseId reason_id; @@ -454,7 +451,7 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) { Assert(isUnit(~lit)); reason_id = getUnitId(~lit); } else { - reason_id = registerClause(reason_ref); + reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1)); } res->addStep(lit, reason_id, !sign(lit)); } @@ -486,14 +483,14 @@ void SatProof::startResChain(::Minisat::CRef start) { } void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) { - ClauseId id = registerClause(clause); + ClauseId id = registerClause(clause, LEARNT, uint64_t(-1)); ResChain* res = d_resStack.back(); res->addStep(lit, id, sign); } void SatProof::endResChain(CRef clause) { Assert(d_resStack.size() > 0); - ClauseId id = registerClause(clause); + ClauseId id = registerClause(clause, LEARNT, uint64_t(-1)); ResChain* res = d_resStack.back(); registerResolution(id, res); d_resStack.pop_back(); @@ -502,7 +499,7 @@ void SatProof::endResChain(CRef clause) { void SatProof::endResChain(::Minisat::Lit lit) { Assert(d_resStack.size() > 0); - ClauseId id = registerUnitClause(lit); + ClauseId id = registerUnitClause(lit, LEARNT, uint64_t(-1)); ResChain* res = d_resStack.back(); registerResolution(id, res); d_resStack.pop_back(); @@ -523,6 +520,7 @@ void SatProof::resolveOutUnit(::Minisat::Lit lit) { } void SatProof::storeUnitResolution(::Minisat::Lit lit) { + Debug("cores") << "STORE UNIT RESOLUTION" << std::endl; resolveUnit(lit); } @@ -536,7 +534,7 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) { CRef reason_ref = d_solver->reason(var(lit)); Assert(reason_ref != CRef_Undef); - ClauseId reason_id = registerClause(reason_ref); + ClauseId reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1)); ResChain* res = new ResChain(reason_id); // Here, the call to resolveUnit() can reallocate memory in the @@ -551,7 +549,7 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) { res->addStep(l, res_id, !sign(l)); } } - ClauseId unit_id = registerUnitClause(lit); + ClauseId unit_id = registerUnitClause(lit, LEARNT, uint64_t(-1)); registerResolution(unit_id, res); return unit_id; } @@ -561,11 +559,12 @@ void SatProof::toStream(std::ostream& out) { Unimplemented("native proof printing not supported yet"); } -void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind) { +void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) { + Debug("cores") << "STORE UNIT CONFLICT" << std::endl; Assert(!d_storedUnitConflict); - d_unitConflictId = registerUnitClause(conflict_lit, kind); + d_unitConflictId = registerUnitClause(conflict_lit, kind, proof_id); d_storedUnitConflict = true; - Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; + Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId << "\n"; } void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { @@ -586,7 +585,7 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { return; } else { Assert(!d_storedUnitConflict); - conflict_id = registerClause(conflict_ref); //FIXME + conflict_id = registerClause(conflict_ref, LEARNT, uint64_t(-1)); //FIXME } if(Debug.isOn("proof:sat")) { @@ -652,11 +651,10 @@ std::string SatProof::clauseName(ClauseId id) { if (isInputClause(id)) { os << ProofManager::getInputClauseName(id); return os.str(); - } else - if (isLemmaClause(id)) { + } else if (isLemmaClause(id)) { os << ProofManager::getLemmaClauseName(id); return os.str(); - }else { + } else { os << ProofManager::getLearntClauseName(id); return os.str(); } @@ -728,10 +726,9 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& ResChain* res = d_resChains[id]; ResSteps& steps = res->getSteps(); - for (int i = steps.size()-1; i >= 0; i--) { + for (int i = steps.size() - 1; i >= 0; --i) { out << "("; out << (steps[i].sign? "R" : "Q") << " _ _ "; - } ClauseId start_id = res->getStart(); @@ -742,11 +739,13 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& out << clauseName(start_id) << " "; for(unsigned i = 0; i < steps.size(); i++) { - out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")"; + out << clauseName(steps[i].id) << " " + << ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) + << ") "; } if (id == d_emptyClauseId) { - out <<"(\\empty empty)"; + out << "(\\empty empty)"; return; } @@ -763,6 +762,4 @@ void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) { printResolution(d_emptyClauseId, out, paren); } - } /* CVC4 namespace */ - diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 7795dfa9c..ef4e7a5aa 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -86,6 +86,7 @@ typedef std::hash_map < ClauseId, ::Minisat::Lit> IdUnitMap; typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME typedef std::hash_map < ClauseId, ResChain*> IdResMap; typedef std::hash_set < ClauseId > IdHashSet; +typedef std::hash_map < ClauseId, uint64_t > IdProofRuleMap; typedef std::vector < ResChain* > ResStack; typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause; typedef std::set < ClauseId > IdSet; @@ -115,14 +116,15 @@ protected: UnitIdMap d_unitId; IdHashSet d_deleted; IdToSatClause d_deletedTheoryLemmas; - IdHashSet d_inputClauses; - IdHashSet d_lemmaClauses; +public: + IdProofRuleMap d_inputClauses; + IdProofRuleMap d_lemmaClauses; +protected: // resolutions IdResMap d_resChains; ResStack d_resStack; bool d_checkRes; - static ClauseId d_idCounter; const ClauseId d_emptyClauseId; const ClauseId d_nullId; // proxy class to break circular dependencies @@ -144,6 +146,7 @@ protected: void printRes(ResChain* res); bool isInputClause(ClauseId id); + bool isTheoryConflict(ClauseId id); bool isLemmaClause(ClauseId id); bool isUnit(ClauseId id); bool isUnit(::Minisat::Lit lit); @@ -207,10 +210,10 @@ public: void finalizeProof(::Minisat::CRef conflict); /// clause registration methods - ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT); - ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT); + ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id); + ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); - void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind = LEARNT); + void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); /** * Marks the deleted clauses as deleted. Note we may still use them in the final @@ -242,6 +245,7 @@ public: protected: IdSet d_seenLearnt; IdHashSet d_seenInput; + IdHashSet d_seenTheoryConflicts; IdHashSet d_seenLemmas; inline std::string varName(::Minisat::Lit lit); |