diff options
30 files changed, 970 insertions, 304 deletions
diff --git a/src/proof/Makefile.am b/src/proof/Makefile.am index 75588ceb8..e996ddb60 100644 --- a/src/proof/Makefile.am +++ b/src/proof/Makefile.am @@ -13,6 +13,8 @@ libproof_la_SOURCES = \ sat_proof.cpp \ cnf_proof.h \ cnf_proof.cpp \ + theory_proof.h \ + theory_proof.cpp \ proof_manager.h \ proof_manager.cpp diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 5f03ef5cf..8e9c4cd21 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -16,11 +16,105 @@ **/ #include "proof/cnf_proof.h" +#include "proof/theory_proof.h" +#include "proof/proof_manager.h" +#include "prop/sat_solver_types.h" +#include "prop/minisat/minisat.h" +#include "prop/cnf_stream.h" + using namespace CVC4::prop; namespace CVC4 { -CnfProof::CnfProof(CnfStream* stream) : - d_cnfStream(stream) {} +CnfProof::CnfProof(CnfStream* stream) + : d_cnfStream(stream) +{} + + +Expr CnfProof::getAtom(prop::SatVariable var) { + prop::SatLiteral lit (var); + Node node = d_cnfStream->getNode(lit); + Expr atom = node.toExpr(); + return atom; +} + +CnfProof::~CnfProof() { +} + +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::printFormula(atom, os); + } else { + // print fake atoms for all other logics + os << "true "; + } + + os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n"; + paren << ")))"; + } +} + +void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { + printInputClauses(os, paren); + printTheoryLemmas(os, paren); +} + +void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { + os << " ;; Input 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; + os << "(satlem _ _ "; + std::ostringstream clause_paren; + printClause(*clause, os, clause_paren); + os << " (clausify_false trust)" << clause_paren.str(); + os << "( \\ " << 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(); + + for (; it != end; ++it) { + ClauseId id = it->first; + const prop::SatClause* clause = it->second; + os << "(satlem _ _ "; + std::ostringstream clause_paren; + printClause(*clause, os, clause_paren); + os << " (clausify_false trust)" << clause_paren.str(); + os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n"; + paren << "))"; + } +} + +void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) { + for (unsigned i = 0; i < clause.size(); ++i) { + prop::SatLiteral lit = clause[i]; + prop::SatVariable var = lit.getSatVariable(); + if (lit.isNegated()) { + os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; + paren << "))"; + } else { + os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; + paren << "))"; + } + } +} + } /* CVC4 namespace */ + diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 984dc76c6..a550f274a 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -16,20 +16,44 @@ ** **/ -#include "cvc4_private.h" -#include "util/proof.h" #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H +#include "cvc4_private.h" +#include "util/proof.h" +#include "proof/sat_proof.h" + +#include <ext/hash_set> +#include <ext/hash_map> #include <iostream> + namespace CVC4 { namespace prop { class CnfStream; } + class CnfProof { +protected: CVC4::prop::CnfStream* d_cnfStream; + Expr getAtom(prop::SatVariable var); public: CnfProof(CVC4::prop::CnfStream* cnfStream); + + virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; + virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; + virtual ~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); +public: + LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) + : CnfProof(cnfStream) + {} + virtual void printAtomMapping(std::ostream& os, std::ostream& paren); + virtual void printClauses(std::ostream& os, std::ostream& paren); }; } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index e03e9058b..110e6b79a 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -19,18 +19,46 @@ #include "util/proof.h" #include "proof/sat_proof.h" #include "proof/cnf_proof.h" +#include "proof/theory_proof.h" #include "util/cvc4_assert.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" namespace CVC4 { +std::string append(const std::string& str, uint64_t num) { + std::ostringstream os; + os << str << num; + return os.str(); +} + + bool ProofManager::isInitialized = false; ProofManager* ProofManager::proofManager = NULL; ProofManager::ProofManager(ProofFormat format): d_satProof(NULL), d_cnfProof(NULL), + d_theoryProof(NULL), + d_fullProof(NULL), d_format(format) -{} +{ +} + +ProofManager::~ProofManager() { + delete d_satProof; + delete d_cnfProof; + delete d_theoryProof; + delete d_fullProof; + for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { + delete it->second; + } + for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { + delete it->second; + } + // FIXME: memory leak because there are deleted theory lemmas that were not used in the + // SatProof +} ProofManager* ProofManager::currentPM() { if (isInitialized) { @@ -42,9 +70,16 @@ ProofManager* ProofManager::currentPM() { } } -Proof* ProofManager::getProof() { - // for now, this is just the SAT proof - return getSatProof(); +Proof* ProofManager::getProof(SmtEngine* smt) { + if (currentPM()->d_fullProof != NULL) + return currentPM()->d_fullProof; + Assert (currentPM()->d_format == LFSC); + + currentPM()->d_fullProof = new LFSCProof(smt, + (LFSCSatProof*)getSatProof(), + (LFSCCnfProof*)getCnfProof(), + (LFSCTheoryProof*)getTheoryProof()); + return currentPM()->d_fullProof; } SatProof* ProofManager::getSatProof() { @@ -57,37 +92,83 @@ CnfProof* ProofManager::getCnfProof() { return currentPM()->d_cnfProof; } +TheoryProof* ProofManager::getTheoryProof() { + Assert (currentPM()->d_theoryProof); + return currentPM()->d_theoryProof; +} + + void ProofManager::initSatProof(Minisat::Solver* solver) { Assert (currentPM()->d_satProof == NULL); - switch(currentPM()->d_format) { - case LFSC : - currentPM()->d_satProof = new LFSCSatProof(solver); - break; - case NATIVE : - currentPM()->d_satProof = new SatProof(solver); - break; - default: - Assert(false); - } - + Assert(currentPM()->d_format == LFSC); + currentPM()->d_satProof = new LFSCSatProof(solver); } void ProofManager::initCnfProof(prop::CnfStream* cnfStream) { Assert (currentPM()->d_cnfProof == NULL); + Assert (currentPM()->d_format == LFSC); + currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); +} - switch(currentPM()->d_format) { - case LFSC : - currentPM()->d_cnfProof = new CnfProof(cnfStream); // FIXME - break; - case NATIVE : - currentPM()->d_cnfProof = new CnfProof(cnfStream); - break; - default: - Assert(false); +void ProofManager::initTheoryProof() { + Assert (currentPM()->d_theoryProof == NULL); + Assert (currentPM()->d_format == LFSC); + 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::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()); } + +void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { + 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 (kind == THEORY_LEMMA); + d_theoryLemmas.insert(std::make_pair(id, clause)); +} +void ProofManager::addAssertion(Expr formula) { + d_inputFormulas.insert(formula); } +void ProofManager::setLogic(const std::string& logic_string) { + d_logic = logic_string; +} + + +LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) + : d_satProof(sat) + , d_cnfProof(cnf) + , d_theoryProof(theory) + , d_smtEngine(smtEngine) +{ + d_satProof->constructProof(); +} + +void LFSCProof::toStream(std::ostream& out) { + smt::SmtScope scope(d_smtEngine); + std::ostringstream paren; + out << "(check \n"; + if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { + d_theoryProof->printAssertions(out, paren); + } + out << "(: (holds cln) \n"; + d_cnfProof->printAtomMapping(out, paren); + d_cnfProof->printClauses(out, paren); + d_satProof->printResolutions(out, paren); + paren <<")))\n;;"; + out << paren.str(); +} } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index efd39a118..82a1bd6be 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -23,6 +23,8 @@ #include <iostream> #include "proof/proof.h" +#include "util/proof.h" + // forward declarations namespace Minisat { @@ -35,9 +37,24 @@ namespace prop { class CnfStream; } +class SmtEngine; + +typedef int ClauseId; + class Proof; class SatProof; class CnfProof; +class TheoryProof; + +class LFSCSatProof; +class LFSCCnfProof; +class LFSCTheoryProof; + +namespace prop { +typedef uint64_t SatVariable; +class SatLiteral; +typedef std::vector<SatLiteral> SatClause; +} // different proof modes enum ProofFormat { @@ -45,26 +62,96 @@ enum ProofFormat { NATIVE };/* enum ProofFormat */ +std::string append(const std::string& str, uint64_t num); + +typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; +typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet; +typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; + +typedef int ClauseId; + +enum ClauseKind { + INPUT, + THEORY_LEMMA, + LEARNT +}; + class ProofManager { - SatProof* d_satProof; - CnfProof* d_cnfProof; + SatProof* d_satProof; + CnfProof* d_cnfProof; + TheoryProof* d_theoryProof; + + // information that will need to be shared across proofs + IdToClause d_inputClauses; + IdToClause d_theoryLemmas; + ExprSet d_inputFormulas; + VarSet d_propVars; + + Proof* d_fullProof; ProofFormat d_format; static ProofManager* proofManager; static bool isInitialized; ProofManager(ProofFormat format = LFSC); + ~ProofManager(); +protected: + std::string d_logic; public: static ProofManager* currentPM(); + // initialization + static void initSatProof(Minisat::Solver* solver); + static void initCnfProof(CVC4::prop::CnfStream* cnfStream); + static void initTheoryProof(); + + static Proof* getProof(SmtEngine* smt); + static SatProof* getSatProof(); + static CnfProof* getCnfProof(); + static TheoryProof* getTheoryProof(); - static void initSatProof(Minisat::Solver* solver); - static void initCnfProof(CVC4::prop::CnfStream* cnfStream); + // iterators over data shared by proofs + typedef IdToClause::const_iterator 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(); } + + clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); } + clause_iterator end_lemmas() const { return d_theoryLemmas.end(); } - static Proof* getProof(); - static SatProof* getSatProof(); - static CnfProof* getCnfProof(); + assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); } + assertions_iterator end_assertions() const { return d_inputFormulas.end(); } + var_iterator begin_vars() const { return d_propVars.begin(); } + var_iterator end_vars() const { return d_propVars.end(); } + + void addAssertion(Expr formula); + void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); + + // variable prefixes + static std::string getInputClauseName(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 getLitName(prop::SatLiteral lit); + + void setLogic(const std::string& logic_string); + const std::string getLogic() const { return d_logic; } };/* class ProofManager */ +class LFSCProof : public Proof { + LFSCSatProof* d_satProof; + LFSCCnfProof* d_cnfProof; + LFSCTheoryProof* d_theoryProof; + SmtEngine* d_smtEngine; +public: + LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); + virtual void toStream(std::ostream& out); + virtual ~LFSCProof() {} +}; + }/* CVC4 namespace */ #endif /* __CVC4__PROOF_MANAGER_H */ diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index d9b57f87e..da9df0d42 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -16,11 +16,13 @@ **/ #include "proof/sat_proof.h" +#include "proof/proof_manager.h" #include "prop/minisat/core/Solver.h" +#include "prop/minisat/minisat.h" using namespace std; using namespace Minisat; - +using namespace CVC4::prop; namespace CVC4 { /// some helper functions @@ -166,7 +168,8 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_clauseId(), d_idUnit(), d_deleted(), - d_inputClauses(), + d_inputClauses(), + d_lemmaClauses(), d_resChains(), d_resStack(), d_checkRes(checkRes), @@ -176,12 +179,13 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_temp_idClause(), d_unitConflictId(), d_storedUnitConflict(false), - d_atomToVar() + d_seenLearnt(), + d_seenInput(), + d_seenLemmas() { d_proxy = new ProofProxy(this); } - /** * Returns true if the resolution chain corresponding to id * does resolve to the clause associated to id @@ -262,7 +266,7 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) { return d_unitId[toInt(lit)]; } -::Minisat::CRef SatProof::getClauseRef(ClauseId id) { +Minisat::CRef SatProof::getClauseRef(ClauseId id) { if (d_idClause.find(id) == d_idClause.end()) { Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" " << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "") @@ -272,10 +276,10 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) { return d_idClause[id]; } -Clause& SatProof::getClause(ClauseId id) { - return d_solver->ca[id]; +Clause& SatProof::getClause(CRef ref) { + return d_solver->ca[ref]; } -::Minisat::Lit SatProof::getUnit(ClauseId id) { +Minisat::Lit SatProof::getUnit(ClauseId id) { Assert (d_idUnit.find(id) != d_idUnit.end()); return d_idUnit[id]; } @@ -301,6 +305,10 @@ bool SatProof::isInputClause(ClauseId id) { return (d_inputClauses.find(id) != d_inputClauses.end()); } +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()) { @@ -344,34 +352,43 @@ void SatProof::printRes(ResChain* res) { /// registration methods -ClauseId SatProof::registerClause(::Minisat::CRef clause, bool isInput) { +ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) { Assert(clause != CRef_Undef); ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { ClauseId newId = d_idCounter++; d_clauseId[clause]= newId; d_idClause[newId] =clause; - if (isInput) { + if (kind == INPUT) { Assert (d_inputClauses.find(newId) == d_inputClauses.end()); d_inputClauses.insert(newId); } + if (kind == THEORY_LEMMA) { + Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); + } } - Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " <<isInput << "\n"; + Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; return d_clauseId[clause]; } -ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, bool isInput) { +ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) { UnitIdMap::iterator it = d_unitId.find(toInt(lit)); if (it == d_unitId.end()) { ClauseId newId = d_idCounter++; d_unitId[toInt(lit)] = newId; d_idUnit[newId] = lit; - if (isInput) { + if (kind == INPUT) { Assert (d_inputClauses.find(newId) == d_inputClauses.end()); d_inputClauses.insert(newId); } + if (kind == THEORY_LEMMA) { + Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); + } + } - Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << isInput <<"\n"; + Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; return d_unitId[toInt(lit)]; } @@ -547,7 +564,7 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { Assert (d_storedUnitConflict); conflict_id = d_unitConflictId; } else { - Assert (!d_storedUnitConflict); + Assert (!d_storedUnitConflict); conflict_id = registerClause(conflict_ref); //FIXME } @@ -562,6 +579,9 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { res->addStep(lit, res_id, !sign(lit)); } registerResolution(d_emptyClauseId, res); + // // FIXME: massive hack + // Proof* proof = ProofManager::getProof(); + // proof->toStream(std::cout); } /// CRef manager @@ -589,182 +609,136 @@ void SatProof::markDeleted(CRef clause) { if (d_clauseId.find(clause) != d_clauseId.end()) { ClauseId id = getClauseId(clause); Assert (d_deleted.find(id) == d_deleted.end()); - d_deleted.insert(id); + d_deleted.insert(id); + if (isLemmaClause(id)) { + const Clause& minisat_cl = getClause(clause); + SatClause* sat_cl = new SatClause(); + MinisatSatSolver::toSatClause(minisat_cl, *sat_cl); + d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); + } } } -/// store mapping from theory atoms to new variables -void SatProof::storeAtom(::Minisat::Lit literal, Expr atom) { - Assert(d_atomToVar.find(atom) == d_atomToVar.end()); - d_atomToVar[atom] = literal; -} - - - -/// LFSCSatProof class - -std::string LFSCSatProof::varName(::Minisat::Lit lit) { - ostringstream os; - if (sign(lit)) { - os << "(neg v"<<var(lit) << ")" ; - } - else { - os << "(pos v"<<var(lit) << ")"; - } - return os.str(); +void SatProof::constructProof() { + collectClauses(d_emptyClauseId); } - -std::string LFSCSatProof::clauseName(ClauseId id) { +std::string SatProof::clauseName(ClauseId id) { ostringstream os; if (isInputClause(id)) { - os << "p"<<id; + os << ProofManager::getInputClauseName(id); return os.str(); - } else { - os << "l"<<id; + } else + if (isLemmaClause(id)) { + os << ProofManager::getLemmaClauseName(id); + return os.str(); + }else { + os << ProofManager::getLearntClauseName(id); return os.str(); } } -void LFSCSatProof::collectLemmas(ClauseId id) { - if (d_seenLemmas.find(id) != d_seenLemmas.end()) { +void SatProof::addToProofManager(ClauseId id, ClauseKind kind) { + if (isUnit(id)) { + Minisat::Lit lit = getUnit(id); + prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit); + prop::SatClause* clause = new SatClause(); + clause->push_back(sat_lit); + ProofManager::currentPM()->addClause(id, clause, kind); + return; + } + + if (isDeleted(id)) { + Assert (kind == THEORY_LEMMA); + SatClause* clause = d_deletedTheoryLemmas.find(id)->second; + ProofManager::currentPM()->addClause(id, clause, kind); + return; + } + + CRef ref = getClauseRef(id); + const Clause& minisat_cl = getClause(ref); + SatClause* clause = new SatClause(); + MinisatSatSolver::toSatClause(minisat_cl, *clause); + ProofManager::currentPM()->addClause(id, clause, kind); +} + +void SatProof::collectClauses(ClauseId id) { + if (d_seenLearnt.find(id) != d_seenLearnt.end()) { return; } if (d_seenInput.find(id) != d_seenInput.end()) { return; } + if (d_seenLemmas.find(id) != d_seenLemmas.end()) { + return; + } if (isInputClause(id)) { + addToProofManager(id, INPUT); d_seenInput.insert(id); return; - } else { - d_seenLemmas.insert(id); + } + else if (isLemmaClause(id)) { + addToProofManager(id, THEORY_LEMMA); + d_seenLemmas.insert(id); + return; + } + else { + d_seenLearnt.insert(id); } Assert (d_resChains.find(id) != d_resChains.end()); ResChain* res = d_resChains[id]; ClauseId start = res->getStart(); - collectLemmas(start); + collectClauses(start); ResSteps steps = res->getSteps(); for(unsigned i = 0; i < steps.size(); i++) { - collectLemmas(steps[i].id); + collectClauses(steps[i].id); } } +/// LFSCSatProof class - -void LFSCSatProof::printResolution(ClauseId id) { - d_lemmaSS << "(satlem _ _ _ "; +void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { + out << "(satlem_simplify _ _ _ "; ResChain* res = d_resChains[id]; ResSteps& steps = res->getSteps(); for (int i = steps.size()-1; i >= 0; i--) { - d_lemmaSS << "("; - d_lemmaSS << (steps[i].sign? "R" : "Q") << " _ _ "; + out << "("; + out << (steps[i].sign? "R" : "Q") << " _ _ "; } ClauseId start_id = res->getStart(); - if(isInputClause(start_id)) { - d_seenInput.insert(start_id); - } - d_lemmaSS << clauseName(start_id) << " "; + // WHY DID WE NEED THIS? + // if(isInputClause(start_id)) { + // d_seenInput.insert(start_id); + // } + out << clauseName(start_id) << " "; for(unsigned i = 0; i < steps.size(); i++) { - d_lemmaSS << clauseName(steps[i].id) << " v" << var(steps[i].lit) <<")"; + out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")"; } if (id == d_emptyClauseId) { - d_lemmaSS <<"(\\empty empty)"; + out <<"(\\empty empty)"; return; } - d_lemmaSS << "(\\" << clauseName(id) << "\n"; // bind to lemma name - d_paren << "))"; // closing parethesis for lemma binding and satlem -} - - -void LFSCSatProof::printInputClause(ClauseId id) { - if (isUnit(id)) { - ::Minisat::Lit lit = getUnit(id); - d_clauseSS << "(% " << clauseName(id) << " (holds (clc "; - d_clauseSS << varName(lit) << "cln ))"; - d_paren << ")"; - return; - } - - ostringstream os; - CRef ref = getClauseRef(id); - Assert (ref != CRef_Undef); - Clause& c = getClause(ref); - - d_clauseSS << "(% " << clauseName(id) << " (holds "; - os << ")"; // closing paren for holds - d_paren << ")"; // closing paren for (% - - for(int i = 0; i < c.size(); i++) { - d_clauseSS << " (clc " << varName(c[i]) <<" "; - os <<")"; - d_seenVars.insert(var(c[i])); - } - d_clauseSS << "cln"; - d_clauseSS << os.str() << "\n"; -} - - -void LFSCSatProof::printClauses() { - for (IdHashSet::iterator it = d_seenInput.begin(); it!= d_seenInput.end(); ++it) { - printInputClause(*it); - } -} - -void LFSCSatProof::printVariables() { - for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) { - d_varSS << "(% v" << *it <<" var \n"; - d_paren << ")"; - } + out << "(\\" << clauseName(id) << "\n"; // bind to lemma name + paren << "))"; // closing parethesis for lemma binding and satlem } - -void LFSCSatProof::flush(std::ostream& out) { - out << d_atomsSS.str(); - out << "(check \n"; - d_paren <<")"; - out << d_varSS.str(); - out << d_clauseSS.str(); - out << "(: (holds cln) \n"; - out << d_lemmaSS.str(); - d_paren << "))"; - out << d_paren.str(); - out << "\n"; -} - -void LFSCSatProof::toStream(std::ostream& out) { - Debug("proof:sat") << " LFSCSatProof::printProof \n"; - - // first collect lemmas to print in reverse order - collectLemmas(d_emptyClauseId); - for(IdSet::iterator it = d_seenLemmas.begin(); it!= d_seenLemmas.end(); ++it) { +void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) { + for(IdSet::iterator it = d_seenLearnt.begin(); it!= d_seenLearnt.end(); ++it) { if(*it != d_emptyClauseId) { - printResolution(*it); + printResolution(*it, out, paren); } } - printAtoms(); - // last resolution to be printed is the empty clause - printResolution(d_emptyClauseId); - - printClauses(); - printVariables(); - flush(out); -} - -void LFSCSatProof::printAtoms() { - d_atomsSS << "; Mapping between boolean variables and theory atoms \n"; - for (AtomToVar::iterator it = d_atomToVar.begin(); it != d_atomToVar.end(); ++it) { - d_atomsSS << "; " << it->first << " => v" << var(it->second) << "\n"; - } + printResolution(d_emptyClauseId, out, paren); } diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index fb8966400..362a9fb90 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -27,7 +27,7 @@ #include <ext/hash_set> #include <sstream> #include "expr/expr.h" - +#include "proof/proof_manager.h" namespace Minisat { class Solver; @@ -36,7 +36,7 @@ namespace Minisat { #include "prop/minisat/core/SolverTypes.h" #include "util/proof.h" - +#include "prop/sat_solver_types.h" namespace std { using namespace __gnu_cxx; }/* std namespace */ @@ -49,7 +49,6 @@ namespace CVC4 { void printDebug(::Minisat::Lit l); void printDebug(::Minisat::Clause& c); -typedef int ClauseId; struct ResStep { ::Minisat::Lit lit; ClauseId id; @@ -81,18 +80,17 @@ public: LitSet* getRedundant() { return d_redundantLits; } };/* class ResChain */ -typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap; +typedef std::hash_map < ClauseId, ::Minisat::CRef > IdCRefMap; typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap; 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::vector < ResChain* > ResStack; - -typedef std::hash_set < int > VarSet; +typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause; typedef std::set < ClauseId > IdSet; typedef std::vector < ::Minisat::Lit > LitVector; -typedef __gnu_cxx::hash_map<Expr, ::Minisat::Lit, ExprHashFunction > AtomToVar; +typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause; class SatProof; @@ -104,17 +102,21 @@ public: void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref); };/* class ProofProxy */ -class SatProof : public Proof { + +class CnfProof; + +class SatProof { protected: ::Minisat::Solver* d_solver; // clauses - IdClauseMap d_idClause; + IdCRefMap d_idClause; ClauseIdMap d_clauseId; IdUnitMap d_idUnit; UnitIdMap d_unitId; IdHashSet d_deleted; + IdToSatClause d_deletedTheoryLemmas; IdHashSet d_inputClauses; - + IdHashSet d_lemmaClauses; // resolutions IdResMap d_resChains; ResStack d_resStack; @@ -128,14 +130,11 @@ protected: // temporary map for updating CRefs ClauseIdMap d_temp_clauseId; - IdClauseMap d_temp_idClause; + IdCRefMap d_temp_idClause; // unit conflict ClauseId d_unitConflictId; bool d_storedUnitConflict; - - // atom mapping - AtomToVar d_atomToVar; public: SatProof(::Minisat::Solver* solver, bool checkRes = false); protected: @@ -143,7 +142,8 @@ protected: void printRes(ClauseId id); void printRes(ResChain* res); - bool isInputClause(ClauseId id); + bool isInputClause(ClauseId id); + bool isLemmaClause(ClauseId id); bool isUnit(ClauseId id); bool isUnit(::Minisat::Lit lit); bool hasResolution(ClauseId id); @@ -155,7 +155,7 @@ protected: ::Minisat::CRef getClauseRef(ClauseId id); ::Minisat::Lit getUnit(ClauseId id); ClauseId getUnitId(::Minisat::Lit lit); - ::Minisat::Clause& getClause(ClauseId id); + ::Minisat::Clause& getClause(::Minisat::CRef ref); virtual void toStream(std::ostream& out); bool checkResolution(ClauseId id); @@ -206,8 +206,8 @@ public: void finalizeProof(::Minisat::CRef conflict); /// clause registration methods - ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false); - ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false); + ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT); + ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT); void storeUnitConflict(::Minisat::Lit lit); @@ -217,6 +217,7 @@ public: * @param clause */ void markDeleted(::Minisat::CRef clause); + bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); } /** * Constructs the resolution of ~q and resolves it with the current * resolution thus eliminating q from the current clause @@ -231,49 +232,34 @@ public: void storeUnitResolution(::Minisat::Lit lit); ProofProxy* getProxy() {return d_proxy; } - /** - * At mapping between literal and theory-atom it represents - * - * @param literal - * @param atom - */ - void storeAtom(::Minisat::Lit literal, Expr atom); -};/* class SatProof */ - -class LFSCSatProof: public SatProof { -private: - VarSet d_seenVars; - std::ostringstream d_atomsSS; - std::ostringstream d_varSS; - std::ostringstream d_lemmaSS; - std::ostringstream d_clauseSS; - std::ostringstream d_paren; - IdSet d_seenLemmas; - IdHashSet d_seenInput; + /** + Constructs the SAT proof identifying the needed lemmas + */ + void constructProof(); + +protected: + IdSet d_seenLearnt; + IdHashSet d_seenInput; + IdHashSet d_seenLemmas; + inline std::string varName(::Minisat::Lit lit); inline std::string clauseName(ClauseId id); - void collectLemmas(ClauseId id); - void printResolution(ClauseId id); - void printInputClause(ClauseId id); + void collectClauses(ClauseId id); + void addToProofManager(ClauseId id, ClauseKind kind); +public: + virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; +};/* class SatProof */ - void printVariables(); - void printClauses(); - void flush(std::ostream& out); - void printAtoms(); +class LFSCSatProof: public SatProof { +private: + void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); public: - LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false): - SatProof(solver, checkRes), - d_seenVars(), - d_atomsSS(), - d_varSS(), - d_lemmaSS(), - d_paren(), - d_seenLemmas(), - d_seenInput() - {} - virtual void toStream(std::ostream& out); + LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false) + : SatProof(solver, checkRes) + {} + virtual void printResolutions(std::ostream& out, std::ostream& paren); };/* class LFSCSatProof */ }/* CVC4 namespace */ diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp new file mode 100644 index 000000000..696bd8309 --- /dev/null +++ b/src/proof/theory_proof.cpp @@ -0,0 +1,197 @@ +/********************* */ +/*! \file theory_proof.cpp + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "proof/theory_proof.h" +#include "proof/proof_manager.h" +using namespace CVC4; + +TheoryProof::TheoryProof() + : d_termDeclarations() + , d_sortDeclarations() + , d_declarationCache() +{} + +void TheoryProof::addDeclaration(Expr term) { + if (d_declarationCache.count(term)) + return; + + Type type = term.getType(); + if (type.isSort()) + d_sortDeclarations.insert(type); + if (term.getKind() == kind::APPLY_UF) { + Expr function = term.getOperator(); + d_termDeclarations.insert(function); + } else if (term.isVariable()) { + Assert (type.isSort()); + d_termDeclarations.insert(term); + } + // recursively declare all other terms + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + addDeclaration(term[i]); + } + d_declarationCache.insert(term); +} + +void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { + if (term.isVariable()) { + os << term; + return; + } + + Assert (term.getKind() == kind::APPLY_UF); + Expr func = term.getOperator(); + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + os<< "(apply _ _ "; + } + os << func << " "; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + printTerm(term[i], os); + os << ")"; + } +} + +std::string toLFSCKind(Kind kind) { + switch(kind) { + case kind::OR : return "or"; + case kind::AND: return "and"; + case kind::XOR: return "xor"; + case kind::EQUAL: return "="; + case kind::IMPLIES: return "impl"; + case kind::NOT: return "not"; + default: + Unreachable(); + } +} + +void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { + // should make this more general and overall sane + Assert (atom.getType().isBoolean() && "Only printing booleans." ); + Kind kind = atom.getKind(); + // this is the only predicate we have + if (kind == kind::EQUAL) { + os << "("; + os <<"= "; + os << atom[0].getType() <<" "; + printTerm(atom[0], os); + os <<" "; + printTerm(atom[1], os); + os <<")"; + } else if ( kind == kind::DISTINCT) { + os <<"(not (= "; + os << atom[0].getType() <<" "; + printTerm(atom[0], os); + os <<" "; + printTerm(atom[1], os); + os <<"))"; + } else if ( kind == kind::OR || + kind == kind::AND || + kind == kind::XOR || + kind == kind::IMPLIES || + kind == kind::NOT) { + // print the boolean operators + os << "("; + os << toLFSCKind(kind); + if (atom.getNumChildren() > 2) { + std::ostringstream paren; + os << " "; + for (unsigned i =0; i < atom.getNumChildren(); ++i) { + printFormula(atom[i], os); + os << " "; + if (i < atom.getNumChildren() - 2) { + os << "("<< toLFSCKind(kind) << " "; + paren << ")"; + } + } + os << paren.str() <<")"; + } else { + // this is for binary and unary operators + for (unsigned i = 0; i < atom.getNumChildren(); ++i) { + os <<" "; + printFormula(atom[i], os); + } + os <<")"; + } + } else if (kind == kind::CONST_BOOLEAN) { + if (atom.getConst<bool>()) + os << "true"; + else + os << "false"; + } + else { + std::cout << kind << "\n"; + Assert (false && "Unsupported kind"); + } +} + +void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) { + unsigned counter = 0; + ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); + ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); + + // collect declarations first + for(; it != end; ++it) { + addDeclaration(*it); + } + printDeclarations(os, paren); + + it = ProofManager::currentPM()->begin_assertions(); + for (; it != end; ++it) { + os << "(% A" << counter++ << " (th_holds "; + printFormula(*it, os); + os << ")\n"; + paren <<")"; + } +} + +void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { + // declaring the sorts + for (SortSet::const_iterator it = d_sortDeclarations.begin(); it != d_sortDeclarations.end(); ++it) { + os << "(% " << *it << " sort \n"; + paren << ")"; + } + + // declaring the terms + for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { + Expr term = *it; + + os << "(% " << term << " (term "; + paren <<")"; + + Type type = term.getType(); + if (type.isFunction()) { + std::ostringstream fparen; + FunctionType ftype = (FunctionType)type; + std::vector<Type> args = ftype.getArgTypes(); + args.push_back(ftype.getRangeType()); + os << "(arrow "; + for (unsigned i = 0; i < args.size(); i++) { + Type arg_type = args[i]; + Assert (arg_type.isSort()); + os << arg_type << " "; + if (i < args.size() - 2) { + os << "(arrow "; + fparen <<")"; + } + } + os << fparen.str() << "))\n"; + } else { + Assert (term.isVariable()); + Assert (type.isSort()); + os << type << ")\n"; + } + } +} diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h new file mode 100644 index 000000000..773428633 --- /dev/null +++ b/src/proof/theory_proof.h @@ -0,0 +1,54 @@ +/********************* */ +/*! \file theory_proof.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A manager for UfProofs. + ** + ** A manager for UfProofs. + ** + ** + **/ + + +#ifndef __CVC4__THEORY_PROOF_H +#define __CVC4__THEORY_PROOF_H + +#include "cvc4_private.h" +#include "util/proof.h" +#include "expr/expr.h" +#include <ext/hash_set> +#include <iostream> + +namespace CVC4 { + + + typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; + typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; + class TheoryProof { + protected: + ExprSet d_termDeclarations; + SortSet d_sortDeclarations; + ExprSet d_declarationCache; + + void addDeclaration(Expr atom); + public: + TheoryProof(); + virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; + }; + + class LFSCTheoryProof: public TheoryProof { + static void printTerm(Expr term, std::ostream& os); + void printDeclarations(std::ostream& os, std::ostream& paren); + public: + static void printFormula(Expr atom, std::ostream& os); + virtual void printAssertions(std::ostream& os, std::ostream& paren); + }; +} /* CVC4 namespace */ +#endif /* __CVC4__THEORY_PROOF_H */ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 8ebb461e5..47d352949 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -238,7 +238,6 @@ SatLiteral CnfStream::convertAtom(TNode node) { // Make a new literal (variables are not considered theory literals) SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate); - PROOF (ProofManager::getSatProof()->storeAtom(MinisatSatSolver::toMinisatLit(lit), node.toExpr()); ); // Return the resulting literal return lit; } diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 36e196821..16fa3ba60 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -135,8 +135,8 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, // Assert the constants uncheckedEnqueue(mkLit(varTrue, false)); uncheckedEnqueue(mkLit(varFalse, true)); - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), true); ) - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), true); ) + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT); ) + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT); ) } @@ -263,7 +263,7 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - PROOF (ProofManager::getSatProof()->registerClause(real_reason, true); ); + PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -339,7 +339,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) clauses_persistent.push(cr); attachClause(cr); - PROOF( ProofManager::getSatProof()->registerClause(cr, true); ) + PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); ) } // Check if it propagates @@ -347,7 +347,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) if(assigns[var(ps[0])] == l_Undef) { assert(assigns[var(ps[0])] != l_False); uncheckedEnqueue(ps[0], cr); - PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], true); } ) + PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } ) return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef); } else return ok; } @@ -369,9 +369,8 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { - PROOF( ProofManager::getSatProof()->markDeleted(cr); ) - const Clause& c = ca[cr]; + PROOF( ProofManager::getSatProof()->markDeleted(cr); ) Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); @@ -1631,7 +1630,7 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, true); ); + PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ); if (removable) { clauses_removable.push(lemma_ref); } else { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 960f2ad62..98e43aaf0 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -103,6 +103,13 @@ void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, Assert((unsigned)clause.size() == sat_clause.size()); } +void MinisatSatSolver::toSatClause(const Minisat::Clause& clause, + SatClause& sat_clause) { + for (int i = 0; i < clause.size(); ++i) { + sat_clause.push_back(toSatLiteral(clause[i])); + } + Assert((unsigned)clause.size() == sat_clause.size()); +} void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) { diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index ec49b5f71..27258b3c2 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -51,7 +51,7 @@ public: static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause); static void toSatClause (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause); - + static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); void initialize(context::Context* context, TheoryProxy* theoryProxy); void addClause(SatClause& clause, bool removable); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index a169d31e6..036877b6a 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -19,6 +19,7 @@ #include "prop/theory_proxy.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" +#include "proof/proof_manager.h" #include "decision/decision_engine.h" #include "decision/options.h" @@ -90,6 +91,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); + PROOF (ProofManager::currentPM()->initCnfProof(d_cnfStream); ); } PropEngine::~PropEngine() { diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index ab2bcda47..8fee0d11e 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -135,6 +135,10 @@ public: return (size_t)d_value; } + uint64_t toInt() const { + return d_value; + } + /** * Returns true if the literal is undefined. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index be6acd09c..0cfb674cf 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -38,6 +38,7 @@ #include "expr/node.h" #include "expr/node_self_iterator.h" #include "prop/prop_engine.h" +#include "proof/theory_proof.h" #include "smt/modal_exception.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -46,6 +47,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" #include "util/proof.h" +#include "proof/proof.h" #include "util/boolean_simplification.h" #include "util/node_visitor.h" #include "util/configuration.h" @@ -678,6 +680,7 @@ void SmtEngine::finishInit() { if(options::cumulativeMillisecondLimit() != 0) { setTimeLimit(options::cumulativeMillisecondLimit(), true); } + PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); } void SmtEngine::finalOptionsAreSet() { @@ -881,16 +884,16 @@ void SmtEngine::setLogicInternal() throw() { } } // Turn on model-based arrays for QF_AX (unless models are enabled) - if(! options::arraysModelBased.wasSetByUser()) { - if (not d_logic.isQuantified() && - d_logic.isTheoryEnabled(THEORY_ARRAY) && - d_logic.isPure(THEORY_ARRAY) && - !options::produceModels() && - !options::checkModels()) { - Trace("smt") << "turning on model-based array solver" << endl; - options::arraysModelBased.set(true); - } - } + // if(! options::arraysModelBased.wasSetByUser()) { + // if (not d_logic.isQuantified() && + // d_logic.isTheoryEnabled(THEORY_ARRAY) && + // d_logic.isPure(THEORY_ARRAY) && + // !options::produceModels() && + // !options::checkModels()) { + // Trace("smt") << "turning on model-based array solver" << endl; + // options::arraysModelBased.set(true); + // } + // } // Turn on multiple-pass non-clausal simplification for QF_AUFBV if(! options::repeatSimp.wasSetByUser()) { bool repeatSimp = !d_logic.isQuantified() && @@ -3106,6 +3109,10 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); + + + PROOF( ProofManager::currentPM()->addAssertion(ex); ); + Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { @@ -3249,6 +3256,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); + PROOF( ProofManager::currentPM()->addAssertion(ex);); Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; // Substitute out any abstract values in ex @@ -3706,7 +3714,7 @@ Proof* SmtEngine::getProof() throw(ModalException) { throw ModalException(msg); } - return ProofManager::getProof(); + return ProofManager::getProof(this); #else /* CVC4_PROOF */ throw ModalException("This build of CVC4 doesn't have proof support."); #endif /* CVC4_PROOF */ diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index bc7da8786..19c6a9248 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -18,6 +18,7 @@ #include "bitblaster.h" #include "prop/sat_solver.h" #include "theory/booleans/theory_bool_rewriter.h" +#include <cmath> using namespace CVC4::prop; using namespace CVC4::theory::bv::utils; @@ -717,10 +718,18 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) { bb->bbTerm(node[0], a); bb->bbTerm(node[1], b); - res = a; - Bits prev_res; + // check for b < log2(n) + unsigned size = utils::getSize(node); + unsigned log2_size = std::ceil(log2((double)size)); + Node a_size = utils::mkConst(BitVector(size, size)); + Node b_ult_a_size = utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size); + // ensure that the inequality is bit-blasted + bb->bbAtom(b_ult_a_size); - for(unsigned s = 0; s < b.size(); ++s) { + Bits prev_res; + res = a; + // we only need to look at the bits bellow log2_a_size + for(unsigned s = 0; s < log2_size; ++s) { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched prev_res = res; @@ -733,10 +742,16 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) { } else { // if b[s]= 0, use previous value, otherwise shift by threshold bits Assert(i >= threshold); - res[i] = mkNode(kind::ITE, mkNot(b[s]), prev_res[i], prev_res[i-threshold]); + res[i] = mkNode(kind::ITE, b[s], prev_res[i-threshold], prev_res[i]); } } } + prev_res = res; + for (unsigned i = 0; i < b.size(); ++i) { + // this is fine because b_ult_a_size has been bit-blasted + res[i] = utils::mkNode(kind::ITE, b_ult_a_size, prev_res[i], utils::mkFalse()); + } + if(Debug.isOn("bitvector-bb")) { Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } @@ -750,10 +765,18 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { bb->bbTerm(node[0], a); bb->bbTerm(node[1], b); + // check for b < log2(n) + unsigned size = utils::getSize(node); + unsigned log2_size = std::ceil(log2((double)size)); + Node a_size = utils::mkConst(BitVector(size, size)); + Node b_ult_a_size = utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size); + // ensure that the inequality is bit-blasted + bb->bbAtom(b_ult_a_size); + res = a; Bits prev_res; - for(unsigned s = 0; s < b.size(); ++s) { + for(unsigned s = 0; s < log2_size; ++s) { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched prev_res = res; @@ -770,6 +793,13 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { } } } + + prev_res = res; + for (unsigned i = 0; i < b.size(); ++i) { + // this is fine because b_ult_a_size has been bit-blasted + res[i] = utils::mkNode(kind::ITE, b_ult_a_size, prev_res[i], utils::mkFalse()); + } + if(Debug.isOn("bitvector-bb")) { Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } @@ -784,11 +814,19 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { bb->bbTerm(node[0], a); bb->bbTerm(node[1], b); + // check for b < n + unsigned size = utils::getSize(node); + unsigned log2_size = std::ceil(log2((double)size)); + Node a_size = utils::mkConst(BitVector(size, size)); + Node b_ult_a_size = utils::mkNode(kind::BITVECTOR_ULT, node[1], a_size); + // ensure that the inequality is bit-blasted + bb->bbAtom(b_ult_a_size); + res = a; TNode sign_bit = a.back(); Bits prev_res; - for(unsigned s = 0; s < b.size(); ++s) { + for(unsigned s = 0; s < log2_size; ++s) { // barrel shift stage: at each stage you can either shift by 2^s bits // or leave the previous stage untouched prev_res = res; @@ -805,6 +843,13 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { } } } + + prev_res = res; + for (unsigned i = 0; i < b.size(); ++i) { + // this is fine because b_ult_a_size has been bit-blasted + res[i] = utils::mkNode(kind::ITE, b_ult_a_size, prev_res[i], sign_bit); + } + if(Debug.isOn("bitvector-bb")) { Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d7a7f358a..a2de951aa 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -177,7 +177,8 @@ void TheoryBV::check(Effort e) while (!done()) { TNode fact = get().assertion; - checkForLemma(fact); + checkForLemma(fact); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->assertFact(fact); } diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 8426afb59..db48a1d05 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -152,6 +152,7 @@ enum RewriteRuleId { PlusCombineLikeTerms, MultSimplify, MultDistribConst, + MultDistribVariable, SolveEq, BitwiseEq, AndSimplify, @@ -265,6 +266,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out; case MultSimplify: out << "MultSimplify"; return out; case MultDistribConst: out << "MultDistribConst"; return out; + case MultDistribVariable: out << "MultDistribConst"; return out; case SolveEq : out << "SolveEq"; return out; case BitwiseEq : out << "BitwiseEq"; return out; case NegMult : out << "NegMult"; return out; @@ -498,6 +500,7 @@ struct AllRewriteRules { RewriteRule<SltZero> rule115; RewriteRule<BVToNatEliminate> rule116; RewriteRule<IntToBVEliminate> rule117; + RewriteRule<MultDistribVariable> rule118; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 2da4dfa6a..bb5c94b1e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -432,6 +432,36 @@ Node RewriteRule<MultSimplify>::apply(TNode node) { } template<> inline +bool RewriteRule<MultDistribVariable>::applies(TNode node) { + if (node.getKind() != kind::BITVECTOR_MULT || + node.getNumChildren() != 2) { + return false; + } + Assert(!node[0].isConst()); + if (!node[1].getNumChildren() == 0) { + return false; + } + TNode factor = node[0]; + return (factor.getKind() == kind::BITVECTOR_PLUS || + factor.getKind() == kind::BITVECTOR_SUB); +} + +template<> inline +Node RewriteRule<MultDistribVariable>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<MultDistrib>(" << node << ")" << std::endl; + TNode var = node[1]; + TNode factor = node[0]; + + std::vector<Node> children; + for(unsigned i = 0; i < factor.getNumChildren(); ++i) { + children.push_back(utils::mkNode(kind::BITVECTOR_MULT, factor[i], var)); + } + + return utils::mkNode(factor.getKind(), children); +} + + +template<> inline bool RewriteRule<MultDistribConst>::applies(TNode node) { if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 2467ae3f1..76eb97b39 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -332,6 +332,12 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) { // creating new terms that might simplify further return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + if(RewriteRule<MultDistribVariable>::applies(resultNode)) { + resultNode = RewriteRule<MultDistribVariable>::run<false>(resultNode); + // creating new terms that might simplify further + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + } if(resultNode == node) { diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 840c8bc3a..393f3883c 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -28,17 +28,22 @@ using namespace CVC4::context; using namespace CVC4::theory; TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) : - d_substitutions(c, false), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) + d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); + + d_eeContext = new context::Context(); + d_equalityEngine = new eq::EqualityEngine(d_eeContext, name); + // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::APPLY_UF); - d_equalityEngine.addFunctionKind(kind::SELECT); - // d_equalityEngine.addFunctionKind(kind::STORE); - d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); + d_equalityEngine->addFunctionKind(kind::APPLY_UF); + d_equalityEngine->addFunctionKind(kind::SELECT); + // d_equalityEngine->addFunctionKind(kind::STORE); + d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); + d_eeContext->push(); } void TheoryModel::reset(){ @@ -46,6 +51,8 @@ void TheoryModel::reset(){ d_rep_set.clear(); d_uf_terms.clear(); d_uf_models.clear(); + d_eeContext->pop(); + d_eeContext->push(); } Node TheoryModel::getValue(TNode n) const { @@ -98,7 +105,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // no good. Instead, return the quantifier itself. If we're in // checkModel(), and the quantifier actually matters, we'll get an // assert-fail since the quantifier isn't a constant. - if(!d_equalityEngine.hasTerm(Rewriter::rewrite(n))) { + if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) { return n; } else { n = Rewriter::rewrite(n); @@ -158,13 +165,13 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const return val; } - if (!d_equalityEngine.hasTerm(n)) { + if (!d_equalityEngine->hasTerm(n)) { // Unknown term - return first enumerated value for this type TypeEnumerator te(n.getType()); return *te; } } - Node val = d_equalityEngine.getRepresentative(n); + Node val = d_equalityEngine->getRepresentative(n); Assert(d_reps.find(val) != d_reps.end()); std::map< Node, Node >::const_iterator it = d_reps.find( val ); if( it!=d_reps.end() ){ @@ -237,7 +244,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ /** add term */ void TheoryModel::addTerm(TNode n ){ - Assert(d_equalityEngine.hasTerm(n)); + Assert(d_equalityEngine->hasTerm(n)); //must collect UF terms if (n.getKind()==APPLY_UF) { Node op = n.getOperator(); @@ -254,8 +261,8 @@ void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){ return; } Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl; - d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() ); - Assert(d_equalityEngine.consistent()); + d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() ); + Assert(d_equalityEngine->consistent()); } /** assert predicate */ @@ -266,11 +273,11 @@ void TheoryModel::assertPredicate(TNode a, bool polarity ){ } if (a.getKind() == EQUAL) { Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl; - d_equalityEngine.assertEquality( a, polarity, Node::null() ); + d_equalityEngine->assertEquality( a, polarity, Node::null() ); } else { Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl; - d_equalityEngine.assertPredicate( a, polarity, Node::null() ); - Assert(d_equalityEngine.consistent()); + d_equalityEngine->assertPredicate( a, polarity, Node::null() ); + Assert(d_equalityEngine->consistent()); } } @@ -309,8 +316,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* } else { Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl; - d_equalityEngine.mergePredicates(*eqc_i, rep, Node::null()); - Assert(d_equalityEngine.consistent()); + d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null()); + Assert(d_equalityEngine->consistent()); } } } else { @@ -334,13 +341,13 @@ void TheoryModel::assertRepresentative(TNode n ) bool TheoryModel::hasTerm(TNode a) { - return d_equalityEngine.hasTerm( a ); + return d_equalityEngine->hasTerm( a ); } Node TheoryModel::getRepresentative(TNode a) { - if( d_equalityEngine.hasTerm( a ) ){ - Node r = d_equalityEngine.getRepresentative( a ); + if( d_equalityEngine->hasTerm( a ) ){ + Node r = d_equalityEngine->getRepresentative( a ); if( d_reps.find( r )!=d_reps.end() ){ return d_reps[ r ]; }else{ @@ -355,8 +362,8 @@ bool TheoryModel::areEqual(TNode a, TNode b) { if( a==b ){ return true; - }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ - return d_equalityEngine.areEqual( a, b ); + }else if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){ + return d_equalityEngine->areEqual( a, b ); }else{ return false; } @@ -364,8 +371,8 @@ bool TheoryModel::areEqual(TNode a, TNode b) bool TheoryModel::areDisequal(TNode a, TNode b) { - if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ - return d_equalityEngine.areDisequal( a, b, false ); + if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){ + return d_equalityEngine->areDisequal( a, b, false ); }else{ return false; } @@ -422,7 +429,7 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac return; } if (isAssignable(n)) { - tm->d_equalityEngine.addTerm(n); + tm->d_equalityEngine->addTerm(n); } for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { checkTerms(*child_it, tm, cache); @@ -448,11 +455,11 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) d_te->collectModelInfo(tm, fullModel); // Loop through all terms and make sure that assignable sub-terms are in the equality engine - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine ); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine ); { NodeSet cache; for ( ; !eqcs_i.isFinished(); ++eqcs_i) { - eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i),tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { checkTerms(*eqc_i, tm, cache); } @@ -465,20 +472,20 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) std::map< Node, Node > assertedReps, constantReps; TypeSet typeConstSet, typeRepSet, typeNoRepSet; std::set< TypeNode > allTypes; - eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); + eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); for ( ; !eqcs_i.isFinished(); ++eqcs_i) { // eqc is the equivalence class representative Node eqc = (*eqcs_i); Trace("model-builder") << "Processing EC: " << eqc << endl; - Assert(tm->d_equalityEngine.getRepresentative(eqc) == eqc); + Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc); TypeNode eqct = eqc.getType(); Assert(assertedReps.find(eqc) == assertedReps.end()); Assert(constantReps.find(eqc) == constantReps.end()); // Loop through terms in this EC Node rep, const_rep; - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; Trace("model-builder") << " Processing Term: " << n << endl; @@ -556,7 +563,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) assignable = false; evaluable = false; evaluated = false; - eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; if (isAssignable(n)) { @@ -653,7 +660,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) for (i = noRepSet.begin(); i != noRepSet.end(); ) { i2 = i; ++i; - eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine); assignable = false; evaluable = false; for ( ; !eqc_i.isFinished(); ++eqc_i) { @@ -744,7 +751,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) #ifdef CVC4_ASSERTIONS if (fullModel) { // Check that every term evaluates to its representative in the model - for (eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { + for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { // eqc is the equivalence class representative Node eqc = (*eqcs_i); Node rep; @@ -757,7 +764,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Assert(itMap != constantReps.end()); rep = itMap->second; } - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; static int repCheckInstance = 0; @@ -795,18 +802,19 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node bool childrenConst = true; for (size_t i=0; i < r.getNumChildren(); ++i) { Node ri = r[i]; + bool recurse = true; if (!ri.isConst()) { - if (m->d_equalityEngine.hasTerm(ri)) { - ri = m->d_equalityEngine.getRepresentative(ri); - itMap = constantReps.find(ri); + if (m->d_equalityEngine->hasTerm(ri)) { + itMap = constantReps.find(m->d_equalityEngine->getRepresentative(ri)); if (itMap != constantReps.end()) { ri = (*itMap).second; + recurse = false; } - else if (evalOnly) { - ri = normalize(m, r[i], constantReps, evalOnly); - } + else if (!evalOnly) { + recurse = false; + } } - else { + if (recurse) { ri = normalize(m, ri, constantReps, evalOnly); } if (!ri.isConst()) { diff --git a/src/theory/model.h b/src/theory/model.h index 03a641df4..a18d66ab0 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -42,8 +42,11 @@ protected: public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel(){} + + /** special local context for our equalityEngine so we can clear it independently of search context */ + context::Context* d_eeContext; /** equality engine containing all known equalities/disequalities */ - eq::EqualityEngine d_equalityEngine; + eq::EqualityEngine* d_equalityEngine; /** map of representatives of equality engine to used representatives in representative set */ std::map< Node, Node > d_reps; /** stores set of representatives for each type */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 78710e4b9..84bbbc179 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -46,6 +46,8 @@ #include "theory/rewriterules/efficient_e_matching.h" +#include "proof/proof_manager.h" + using namespace std; using namespace CVC4; @@ -138,6 +140,7 @@ TheoryEngine::TheoryEngine(context::Context* context, StatisticsRegistry::registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); + PROOF (ProofManager::currentPM()->initTheoryProof(); ); } TheoryEngine::~TheoryEngine() { diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 8c85e4dd2..8aa7d625d 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1382,7 +1382,7 @@ void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){ void StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){ if( Trace.isOn("uf-ss-warn") ){ std::vector< Node > eqcs; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine ); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); if( eqc.getType()==d_type ){ diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 601d65799..bfbc851ef 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -19,6 +19,7 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ + array_card.smt2 \ agree466.smt2 \ ALG008-1.smt2 \ german169.smt2 \ @@ -29,7 +30,7 @@ TESTS = \ german73.smt2 \ PUZ001+1.smt2 \ refcount24.cvc.smt2 \ - bug0909.smt2 + bug0909.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/array_card.smt2 b/test/regress/regress0/fmf/array_card.smt2 new file mode 100644 index 000000000..9ee00d13a --- /dev/null +++ b/test/regress/regress0/fmf/array_card.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +; EXIT: 10 +(set-logic AUFLIA) +(set-option :produce-models true) +(declare-sort U 0) +(declare-fun f () (Array U U)) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) + +(assert (distinct a b c)) + +(assert (distinct (select f a) (select f b))) + +(assert (forall ((x U)) (or (= (select f x) c) (= (select f x) b)))) + +(check-sat) diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index bf9a36df1..19e673fea 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -42,7 +42,8 @@ TESTS = \ simple.01.cvc \ simple.02.cvc \ simple.03.cvc \ - simple.04.cvc + simple.04.cvc \ + proof00.smt2 EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/proof00.smt2 b/test/regress/regress0/uf/proof00.smt2 new file mode 100644 index 000000000..1b7e7b8dd --- /dev/null +++ b/test/regress/regress0/uf/proof00.smt2 @@ -0,0 +1,21 @@ +; PROOF +(set-logic QF_UF) +(set-info :source | +CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC + for more information. + +This benchmark was obtained by trying to find a finite model of a first-order +formula (Albert Oliveras). +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort U 0) +(declare-fun c3 () U) +(declare-fun f1 (U U) U) +(declare-fun f4 (U) U) +(declare-fun c2 () U) +(declare-fun c_0 () U) +(declare-fun c_1 () U) +(assert (let ((?v_1 (f1 c3 c_0))) (let ((?v_0 (f1 ?v_1 c_0)) (?v_2 (f1 c_0 c_0)) (?v_4 (f1 c_0 c_1)) (?v_3 (f1 ?v_1 c_1)) (?v_6 (f1 c3 c_1))) (let ((?v_5 (f1 ?v_6 c_0)) (?v_7 (f1 c_1 c_0)) (?v_9 (f1 c_1 c_1)) (?v_8 (f1 ?v_6 c_1)) (?v_10 (f4 c_0))) (let ((?v_11 (f1 c_0 ?v_10)) (?v_12 (f4 c_1))) (let ((?v_13 (f1 c_1 ?v_12)) (?v_15 (f1 c2 c_0))) (let ((?v_14 (f1 ?v_15 c_0)) (?v_16 (f1 ?v_15 c_1)) (?v_18 (f1 c2 c_1))) (let ((?v_17 (f1 ?v_18 c_0)) (?v_19 (f1 ?v_18 c_1))) (and (distinct c_0 c_1) (= (f1 ?v_0 c_0) (f1 c_0 ?v_2)) (= (f1 ?v_0 c_1) (f1 c_0 ?v_4)) (= (f1 ?v_3 c_0) (f1 c_1 ?v_2)) (= (f1 ?v_3 c_1) (f1 c_1 ?v_4)) (= (f1 ?v_5 c_0) (f1 c_0 ?v_7)) (= (f1 ?v_5 c_1) (f1 c_0 ?v_9)) (= (f1 ?v_8 c_0) (f1 c_1 ?v_7)) (= (f1 ?v_8 c_1) (f1 c_1 ?v_9)) (not (= ?v_11 (f1 ?v_10 ?v_11))) (not (= ?v_13 (f1 ?v_12 ?v_13))) (= (f1 ?v_14 c_0) (f1 (f1 ?v_2 c_0) c_0)) (= (f1 ?v_14 c_1) (f1 (f1 ?v_4 c_0) c_1)) (= (f1 ?v_16 c_0) (f1 (f1 ?v_2 c_1) c_0)) (= (f1 ?v_16 c_1) (f1 (f1 ?v_4 c_1) c_1)) (= (f1 ?v_17 c_0) (f1 (f1 ?v_7 c_0) c_0)) (= (f1 ?v_17 c_1) (f1 (f1 ?v_9 c_0) c_1)) (= (f1 ?v_19 c_0) (f1 (f1 ?v_7 c_1) c_0)) (= (f1 ?v_19 c_1) (f1 (f1 ?v_9 c_1) c_1)) (or (= ?v_2 c_0) (= ?v_2 c_1)) (or (= ?v_4 c_0) (= ?v_4 c_1)) (or (= ?v_7 c_0) (= ?v_7 c_1)) (or (= ?v_9 c_0) (= ?v_9 c_1)) (or (= ?v_10 c_0) (= ?v_10 c_1)) (or (= ?v_12 c_0) (= ?v_12 c_1)) (or (= c3 c_0) (= c3 c_1)) (or (= c2 c_0) (= c2 c_1))))))))))) +(check-sat) diff --git a/test/regress/run_regression b/test/regress/run_regression index e9c17a3af..44517cc0c 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -112,7 +112,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then proof_command='(get-proof)' lang=smt2 if test -e "$benchmark.expect"; then - expected_proof=`grep '^% PROOF' "$benchmark.expect" &>/dev/null && echo yes` + expected_proof=`grep '^[%;] PROOF' "$benchmark.expect" &>/dev/null && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -140,7 +140,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_exit_status=10 command_line= elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_proof= + expected_proof=`grep '^; PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=unsat expected_exit_status=20 command_line= @@ -276,8 +276,15 @@ fi if [ "$proof" = yes -a "$expected_proof" = yes ]; then gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX - cp "$benchmark" "$pfbenchmark"; - echo "$proof_command" >>"$pfbenchmark"; + # remove exit command to add proof command for smt2 benchmarks + if expr "$benchmark" : '.*\.smt2$' &>/dev/null; then + head -n -0 "$benchmark" > "$pfbenchmark"; + echo "$proof_command" >>"$pfbenchmark"; + echo "(exit)" >> "$pfbenchmark"; + else + cp $benchmark $pfbenchmark + echo "$proof_command" >>"$pfbenchmark"; + fi echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`] time ( :; \ ( cd `dirname "$pfbenchmark"`; @@ -286,6 +293,7 @@ if [ "$proof" = yes -a "$expected_proof" = yes ]; then ) > "$outfile" 2> "$errfile" ) gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX + diff --unchanged-group-format='' \ --old-group-format='' \ --new-group-format='%>' \ |