diff options
Diffstat (limited to 'src')
37 files changed, 1930 insertions, 1000 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 60f3bc7c2..c92078590 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -100,6 +100,12 @@ libcvc4_la_SOURCES = \ prop/sat_solver_types.h \ prop/sat_solver_factory.h \ prop/sat_solver_factory.cpp \ + prop/riss.h \ + prop/riss.cpp \ + prop/glucose.h \ + prop/glucose.cpp \ + prop/cryptominisat.h \ + prop/cryptominisat.cpp \ smt/smt_engine.cpp \ smt/smt_engine_check_proof.cpp \ smt/smt_engine.h \ diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h index 00f192d2f..2297d4492 100644 --- a/src/main/options_handlers.h +++ b/src/main/options_handlers.h @@ -25,51 +25,54 @@ namespace main { inline void showConfiguration(std::string option, SmtEngine* smt) { fputs(Configuration::about().c_str(), stdout); printf("\n"); - printf("version : %s\n", Configuration::getVersionString().c_str()); + printf("version : %s\n", Configuration::getVersionString().c_str()); if(Configuration::isGitBuild()) { const char* branchName = Configuration::getGitBranchName(); if(*branchName == '\0') { branchName = "-"; } - printf("scm : git [%s %s%s]\n", + printf("scm : git [%s %s%s]\n", branchName, std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), Configuration::hasGitModifications() ? " (with modifications)" : ""); } else if(Configuration::isSubversionBuild()) { - printf("scm : svn [%s r%u%s]\n", + printf("scm : svn [%s r%u%s]\n", Configuration::getSubversionBranchName(), Configuration::getSubversionRevision(), Configuration::hasSubversionModifications() ? " (with modifications)" : ""); } else { - printf("scm : no\n"); + printf("scm : no\n"); } printf("\n"); - printf("library : %u.%u.%u\n", + printf("library : %u.%u.%u\n", Configuration::getVersionMajor(), Configuration::getVersionMinor(), Configuration::getVersionRelease()); printf("\n"); - printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); - printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); - printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); - printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); - printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); - printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); - printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); - printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no"); - printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); - printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); - printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); + printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); + printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); + printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); + printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); + printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); + printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); + printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); + printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no"); + printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); + printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); + printf("competition : %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); printf("\n"); - printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); - printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); - printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); - printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); - printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); - printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); - printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); + printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); + printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); + printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); + printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); + printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); + printf("cryptominisat : %s\n", Configuration::isBuiltWithCryptominisat() ? "yes" : "no"); + printf("glucose : %s\n", Configuration::isBuiltWithGlucose() ? "yes" : "no"); + printf("riss : %s\n", Configuration::isBuiltWithRiss() ? "yes" : "no"); + printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); + printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); } diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index ab157844a..e83fa01e0 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -132,11 +132,11 @@ void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { } SatValue BVMinisatSatSolver::value(SatLiteral l){ - return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); + return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); } SatValue BVMinisatSatSolver::modelValue(SatLiteral l){ - return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); + return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); } void BVMinisatSatSolver::unregisterVar(SatLiteral lit) { diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 0bf4edf6a..3fe04899b 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -79,6 +79,9 @@ public: void setNotify(Notify* notify); void addClause(SatClause& clause, bool removable, uint64_t proof_id); + void addXorClause(SatClause& clause, bool rhs, bool removable, uint64_t proof_id) { + Unreachable("Minisat does not support native XOR reasoning"); + } SatValue propagate(); diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index c65189985..6e95543da 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -54,7 +54,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) : , use_rcheck (opt_use_rcheck) , use_elim (opt_use_elim && CVC4::options::bitblastMode() == CVC4::theory::bv::BITBLAST_MODE_EAGER && - !CVC4::options::produceModels()) + !CVC4::options::produceModels()) // FIXME: want to only freeze inputs , merges (0) , asymm_lits (0) , eliminated_vars (0) diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index b0b135b04..f11c041af 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -82,6 +82,36 @@ void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) { PROOF(ProofManager::currentPM()->setRegisteringFormula( Node::null(), RULE_INVALID ); ); } + void CnfStream::assertXorClause(TNode node, + bool rhs, + SatClause& c, + ProofRule proof_id) { + Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl; + if(Dump.isOn("clauses")) { + if(c.size() == 1) { + Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr())); + } else { + Assert(c.size() > 1); + NodeBuilder<> b(kind::XOR); + for(unsigned i = 0; i < c.size(); ++i) { + b << getNode(c[i]); + } + Node n = b; + NodeManager* nm = NodeManager::currentNM(); + Node assertion = nm->mkNode(kind::IFF, n, rhs ? nm->mkConst<bool>(true) : + nm->mkConst<bool>(false)); + Dump("clauses") << AssertCommand(assertion.toExpr()); + } + } + //store map between clause and original formula + // FIXME: no proofs for XOR solvers yet + // PROOF(ProofManager::currentPM()->setRegisteringFormula( node, proof_id ); ); + d_satSolver->addXorClause(c, rhs, d_removable, d_proofId); + // FIXME: no proofs for XOR solvers yet + // PROOF(ProofManager::currentPM()->setRegisteringFormula( Node::null(), RULE_INVALID ); ); +} + + void CnfStream::assertClause(TNode node, SatLiteral a, ProofRule proof_id) { SatClause clause(1); clause[0] = a; @@ -227,7 +257,9 @@ SatLiteral CnfStream::convertAtom(TNode node) { bool theoryLiteral = false; bool canEliminate = true; - bool preRegister = false; + // bool preRegister = false; + // FIXME: hacky and sketchy + bool preRegister = (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); // Is this a variable add it to the list if (node.isVar()) { @@ -263,6 +295,17 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { SatLiteral xorLit = newLiteral(xorNode); + if (d_satSolver->nativeXor() && + options::bvNativeXor()) { + SatClause clause(3); + clause[0] = a; + clause[1] = b; + clause[2] = xorLit; + // FIXME: no proofs yet for xor solvers + assertXorClause(xorNode, false, clause, RULE_INVALID); + return xorLit; + } + assertClause(xorNode.negate(), a, b, ~xorLit, RULE_TSEITIN); assertClause(xorNode.negate(), ~a, ~b, ~xorLit, RULE_TSEITIN); assertClause(xorNode, a, ~b, xorLit, RULE_TSEITIN); @@ -556,6 +599,17 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated, ProofRule pr } void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule proof_id) { + if (d_satSolver->nativeXor() && + options::bvNativeXor()) { + SatLiteral p = toCNF(node[0]); + SatLiteral q = toCNF(node[1]); + SatClause clause(2); + clause[0] = p; + clause[1] = q; + assertXorClause(node, !negated, clause, proof_id); + return; + } + if (!negated) { // p XOR q SatLiteral p = toCNF(node[0], false); diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index d5d01d126..66e956c69 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -134,6 +134,14 @@ protected: * @param clause the clause to assert */ void assertClause(TNode node, SatClause& clause, ProofRule proof_id); + /** + * Asserts the given xor clause to the sat solver. + * @param node the node giving rise to this clause + * @param rhs whether the xor of the literals in c is equal rhs + * @param c the clause to assert + */ + void assertXorClause(TNode node, bool rhs, SatClause& c, ProofRule proof_id); + /** * Asserts the unit clause to the sat solver. diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp new file mode 100644 index 000000000..2794bbfec --- /dev/null +++ b/src/prop/cryptominisat.cpp @@ -0,0 +1,218 @@ +/********************* */ +/*! \file cryptominisat.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the cryptominisat for cvc4 (bitvectors). + **/ + +#include "prop/cryptominisat.h" + +using namespace CVC4; +using namespace prop; + +#ifdef CVC4_USE_CRYPTOMINISAT + +CryptoMinisatSolver::CryptoMinisatSolver(const std::string& name) +: d_solver(new CMSat::SATSolver()) +, d_numVariables(0) +, d_okay(true) +, d_statistics(name) +{ + d_true = newVar(); + d_false = newVar(); + + std::vector<CMSat::Lit> clause(1); + clause[0] = CMSat::Lit(d_true, false); + d_solver->add_clause(clause); + + clause[0] = CMSat::Lit(d_false, true); + d_solver->add_clause(clause); +} + + +CryptoMinisatSolver::~CryptoMinisatSolver() throw(AssertionException) { + delete d_solver; +} + +void CryptoMinisatSolver::addXorClause(SatClause& clause, + bool rhs, + bool removable, + uint64_t proof_id) { + Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n"; + + if (!d_okay) { + Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n"; + return; + } + + ++(d_statistics.d_xorClausesAdded); + + // ensure all sat literals have positive polarity by pushing + // the negation on the result + std::vector<CMSat::Var> xor_clause; + for (unsigned i = 0; i < clause.size(); ++i) { + xor_clause.push_back(toInternalLit(clause[i]).var()); + rhs ^= clause[i].isNegated(); + } + bool res = d_solver->add_xor_clause(xor_clause, rhs); + d_okay &= res; +} + +void CryptoMinisatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { + Debug("sat::cryptominisat") << "Add clause " << clause <<"\n"; + + if (!d_okay) { + Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n"; + return; + } + + ++(d_statistics.d_clausesAdded); + + std::vector<CMSat::Lit> internal_clause; + toInternalClause(clause, internal_clause); + bool res = d_solver->add_clause(internal_clause); + d_okay &= res; +} + +SatVariable CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ + d_solver->new_var(); + ++d_numVariables; + Assert (d_numVariables == d_solver->nVars()); + return d_numVariables - 1; +} + +SatVariable CryptoMinisatSolver::trueVar() { + return d_true; +} + +SatVariable CryptoMinisatSolver::falseVar() { + return d_false; +} + +void CryptoMinisatSolver::markUnremovable(SatLiteral lit) { + // cryptominisat supports dynamically adding back variables (?) + // so this is a no-op + return; +} + +void CryptoMinisatSolver::interrupt(){ + d_solver->interrupt_asap(); +} + +SatValue CryptoMinisatSolver::solve(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + ++d_statistics.d_statCallsToSolve; + return toSatLiteralValue(d_solver->solve()); +} + +SatValue CryptoMinisatSolver::solve(long unsigned int& resource) { + // CMSat::SalverConf conf = d_solver->getConf(); + Unreachable("Not sure how to set different limits for calls to solve in Cryptominisat"); + return solve(); +} + +SatValue CryptoMinisatSolver::value(SatLiteral l){ + const std::vector<CMSat::lbool> model = d_solver->get_model(); + CMSat::Var var = l.getSatVariable(); + Assert (var < model.size()); + CMSat::lbool value = model[var]; + return toSatLiteralValue(value); +} + +SatValue CryptoMinisatSolver::modelValue(SatLiteral l){ + return value(l); +} + +unsigned CryptoMinisatSolver::getAssertionLevel() const { + Unreachable("No interface to get assertion level in Cryptominisat"); + return -1; +} + +// converting from internal sat solver representation + +SatVariable CryptoMinisatSolver::toSatVariable(CMSat::Var var) { + if (var == CMSat::var_Undef) { + return undefSatVariable; + } + return SatVariable(var); +} + +CMSat::Lit CryptoMinisatSolver::toInternalLit(SatLiteral lit) { + if (lit == undefSatLiteral) { + return CMSat::lit_Undef; + } + return CMSat::Lit(lit.getSatVariable(), lit.isNegated()); +} + +SatLiteral CryptoMinisatSolver::toSatLiteral(CMSat::Lit lit) { + Assert (lit != CMSat::lit_Error); + if (lit == CMSat::lit_Undef) { + return undefSatLiteral; + } + + return SatLiteral(SatVariable(lit.var()), + lit.sign()); +} + +SatValue CryptoMinisatSolver::toSatLiteralValue(CMSat::lbool res) { + if(res == CMSat::l_True) return SAT_VALUE_TRUE; + if(res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN; + Assert(res == CMSat::l_False); + return SAT_VALUE_FALSE; +} + +void CryptoMinisatSolver::toInternalClause(SatClause& clause, + std::vector<CMSat::Lit>& internal_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + internal_clause.push_back(toInternalLit(clause[i])); + } + Assert(clause.size() == internal_clause.size()); +} + +void CryptoMinisatSolver::toSatClause(std::vector<CMSat::Lit>& clause, + SatClause& sat_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + sat_clause.push_back(toSatLiteral(clause[i])); + } + Assert(clause.size() == sat_clause.size()); +} + + +// Satistics for CryptoMinisatSolver + +CryptoMinisatSolver::Statistics::Statistics(const std::string& prefix) : + d_statCallsToSolve("theory::bv::"+prefix+"::cryptominisat::calls_to_solve", 0), + d_xorClausesAdded("theory::bv::"+prefix+"::cryptominisat::xor_clauses", 0), + d_clausesAdded("theory::bv::"+prefix+"::cryptominisat::clauses", 0), + d_solveTime("theory::bv::"+prefix+"::cryptominisat::solve_time"), + d_registerStats(!prefix.empty()) +{ + if (!d_registerStats) + return; + + StatisticsRegistry::registerStat(&d_statCallsToSolve); + StatisticsRegistry::registerStat(&d_xorClausesAdded); + StatisticsRegistry::registerStat(&d_clausesAdded); + StatisticsRegistry::registerStat(&d_solveTime); +} + +CryptoMinisatSolver::Statistics::~Statistics() { + if (!d_registerStats) + return; + StatisticsRegistry::unregisterStat(&d_statCallsToSolve); + StatisticsRegistry::unregisterStat(&d_xorClausesAdded); + StatisticsRegistry::unregisterStat(&d_clausesAdded); + StatisticsRegistry::unregisterStat(&d_solveTime); +} +#endif diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h new file mode 100644 index 000000000..401510667 --- /dev/null +++ b/src/prop/cryptominisat.h @@ -0,0 +1,131 @@ +/********************* */ +/*! \file cryptominisat.h + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the cryptominisat sat solver for cvc4 (bitvectors). + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "prop/sat_solver.h" + +#ifdef CVC4_USE_CRYPTOMINISAT +#include <cryptominisat4/cryptominisat.h> +namespace CVC4 { +namespace prop { + +class CryptoMinisatSolver : public SatSolver { + +private: + CMSat::SATSolver* d_solver; + unsigned d_numVariables; + bool d_okay; + SatVariable d_true; + SatVariable d_false; +public: + CryptoMinisatSolver(const std::string& name = ""); + ~CryptoMinisatSolver() throw(AssertionException); + + void addClause(SatClause& clause, bool removable, uint64_t proof_id); + void addXorClause(SatClause& clause, bool rhs, bool removable, uint64_t proof_id); + + bool nativeXor() { return true; } + + SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); + + SatVariable trueVar(); + SatVariable falseVar(); + + void markUnremovable(SatLiteral lit); + + void interrupt(); + + SatValue solve(); + SatValue solve(long unsigned int&); + SatValue value(SatLiteral l); + SatValue modelValue(SatLiteral l); + + unsigned getAssertionLevel() const; + + + // helper methods for converting from the internal Minisat representation + + static SatVariable toSatVariable(CMSat::Var var); + static CMSat::Lit toInternalLit(SatLiteral lit); + static SatLiteral toSatLiteral(CMSat::Lit lit); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(CMSat::lbool res); + + static void toInternalClause(SatClause& clause, std::vector<CMSat::Lit>& internal_clause); + static void toSatClause (std::vector<CMSat::Lit>& clause, SatClause& sat_clause); + + class Statistics { + public: + IntStat d_statCallsToSolve; + IntStat d_xorClausesAdded; + IntStat d_clausesAdded; + TimerStat d_solveTime; + bool d_registerStats; + Statistics(const std::string& prefix); + ~Statistics(); + }; + + Statistics d_statistics; +}; +} // CVC4::prop +} // CVC4 + +#else // CVC4_USE_CRYPTOMINISAT + +namespace CVC4 { +namespace prop { + +class CryptoMinisatSolver : public SatSolver { + +public: + CryptoMinisatSolver(const std::string& name = "") { Unreachable(); } + /** Assert a clause in the solver. */ + void addClause(SatClause& clause, bool removable, uint64_t proof_id) { + Unreachable(); + } + + /** Return true if the solver supports native xor resoning */ + bool nativeXor() { Unreachable(); } + + /** Add a clause corresponding to rhs = l1 xor .. xor ln */ + void addXorClause(SatClause& clause, bool rhs, bool removable, uint64_t proof_id) { + Unreachable(); + } + + SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); } + SatVariable trueVar() { Unreachable(); } + SatVariable falseVar() { Unreachable(); } + SatValue solve() { Unreachable(); } + SatValue solve(long unsigned int&) { Unreachable(); } + void interrupt() { Unreachable(); } + SatValue value(SatLiteral l) { Unreachable(); } + SatValue modelValue(SatLiteral l) { Unreachable(); } + unsigned getAssertionLevel() const { Unreachable(); } + +};/* class CryptoMinisatSolver */ +} // CVC4::prop +} // CVC4 + +#endif // CVC4_USE_CRYPTOMINISAT + + + + diff --git a/src/prop/glucose.cpp b/src/prop/glucose.cpp new file mode 100644 index 000000000..1485e93aa --- /dev/null +++ b/src/prop/glucose.cpp @@ -0,0 +1,197 @@ +/********************* */ +/*! \file glucose.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the glucose sat solver for cvc4 (bitvectors). + **/ + +#include "prop/glucose.h" +#include "smt/options.h" + +#ifdef CVC4_USE_GLUCOSE + +using namespace CVC4; +using namespace prop; + +GlucoseSolver::GlucoseSolver(const std::string& name) +: d_solver(new Glucose::SimpSolver()) +, d_statistics(name) +{ + d_solver->verbosity = -1; + if (CVC4::options::produceModels()) { + // FIXME: we don't want to freeze everything + d_solver->use_elim = false; + } + d_true = newVar(); + d_false = newVar(); + d_solver->addClause(Glucose::mkLit(d_true, false)); + d_solver->addClause(Glucose::mkLit(d_false, true)); +} + + +GlucoseSolver::~GlucoseSolver() throw(AssertionException) { + delete d_solver; +} + +void GlucoseSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { + Debug("sat::glucose") << "Add clause " << clause <<"\n"; + + if (!d_solver->okay()) { + Debug("sat::glucose") << "Solver unsat: not adding clause.\n"; + return; + } + + ++(d_statistics.d_clausesAdded); + + Glucose::vec<Glucose::Lit> internal_clause; + toInternalClause(clause, internal_clause); + d_solver->addClause(internal_clause); // check return status? +} + +SatVariable GlucoseSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ + return d_solver->newVar(); +} + +SatVariable GlucoseSolver::trueVar() { + return d_true; +} + +SatVariable GlucoseSolver::falseVar() { + return d_false; +} + +void GlucoseSolver::markUnremovable(SatLiteral lit) { + d_solver->setFrozen(lit.getSatVariable(), true); + return; +} + +void GlucoseSolver::interrupt(){ + d_solver->interrupt(); +} + +SatValue GlucoseSolver::solve(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + ++d_statistics.d_statCallsToSolve; + return toSatLiteralValue(d_solver->solve()); +} + +SatValue GlucoseSolver::solve(long unsigned int& resource) { + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + if(resource == 0) { + d_solver->budgetOff(); + } else { + d_solver->setConfBudget(resource); + } + return solve(); +} + +SatValue GlucoseSolver::value(SatLiteral l){ + Assert (! d_solver->isEliminated(Glucose::var(toInternalLit(l)))); + // For some reason value returns unknown for glucose + return toSatLiteralValue(d_solver->modelValue(toInternalLit(l))); +} + +SatValue GlucoseSolver::modelValue(SatLiteral l){ + return toSatLiteralValue(d_solver->modelValue(toInternalLit(l))); +} + +unsigned GlucoseSolver::getAssertionLevel() const { + Unreachable("No interface to get assertion level in Glucose"); + return -1; +} + +// converting from internal sat solver representation + +SatVariable GlucoseSolver::toSatVariable(Glucose::Var var) { + if (var == Glucose::Var(-1)) { + return undefSatVariable; + } + return SatVariable(var); +} + +Glucose::Lit GlucoseSolver::toInternalLit(SatLiteral lit) { + if (lit == undefSatLiteral) { + return Glucose::lit_Undef; + } + return Glucose::mkLit(lit.getSatVariable(), lit.isNegated()); +} + +SatLiteral GlucoseSolver::toSatLiteral(Glucose::Lit lit) { + if (lit == Glucose::lit_Undef) { + return undefSatLiteral; + } + + return SatLiteral(SatVariable(Glucose::var(lit)), + Glucose::sign(lit)); +} + +SatValue GlucoseSolver::toSatLiteralValue(Glucose::lbool res) { + if(res == Glucose::lbool((uint8_t)0)/*Glucose::l_True*/) return SAT_VALUE_TRUE; + if(res == Glucose::lbool((uint8_t)2)/*Glucose::l_Undef*/) return SAT_VALUE_UNKNOWN; + Assert(res == Glucose::lbool((uint8_t)1)/*Glucose::l_False*/); + return SAT_VALUE_FALSE; +} + +SatValue GlucoseSolver::toSatLiteralValue(bool res) { + if(res) return SAT_VALUE_TRUE; + return SAT_VALUE_FALSE; +} + + +void GlucoseSolver::toInternalClause(SatClause& clause, + Glucose::vec<Glucose::Lit>& internal_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + internal_clause.push(toInternalLit(clause[i])); + } + Assert(clause.size() == (unsigned)internal_clause.size()); +} + +void GlucoseSolver::toSatClause(Glucose::vec<Glucose::Lit>& 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()); +} + + +// Satistics for GlucoseSolver + +GlucoseSolver::Statistics::Statistics(const std::string& prefix) : + d_statCallsToSolve("theory::bv::"+prefix+"::glucose::calls_to_solve", 0), + d_xorClausesAdded("theory::bv::"+prefix+"::glucose::xor_clauses", 0), + d_clausesAdded("theory::bv::"+prefix+"::glucose::clauses", 0), + d_solveTime("theory::bv::"+prefix+"::glucose::solve_time"), + d_registerStats(!prefix.empty()) +{ + if (!d_registerStats) + return; + + StatisticsRegistry::registerStat(&d_statCallsToSolve); + StatisticsRegistry::registerStat(&d_xorClausesAdded); + StatisticsRegistry::registerStat(&d_clausesAdded); + StatisticsRegistry::registerStat(&d_solveTime); +} + +GlucoseSolver::Statistics::~Statistics() { + if (!d_registerStats) + return; + StatisticsRegistry::unregisterStat(&d_statCallsToSolve); + StatisticsRegistry::unregisterStat(&d_xorClausesAdded); + StatisticsRegistry::unregisterStat(&d_clausesAdded); + StatisticsRegistry::unregisterStat(&d_solveTime); +} + + +#endif // CVC4_USE_GLUCOSE diff --git a/src/prop/glucose.h b/src/prop/glucose.h new file mode 100644 index 000000000..52665ed80 --- /dev/null +++ b/src/prop/glucose.h @@ -0,0 +1,133 @@ +/********************* */ +/*! \file glucose.h + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the glucose sat solver for cvc4 (bitvectors). + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "prop/sat_solver.h" + +#ifdef CVC4_USE_GLUCOSE + +#include <simp/SimpSolver.h> + +namespace CVC4 { +namespace prop { + +class GlucoseSolver : public SatSolver { + +private: + Glucose::SimpSolver* d_solver; + SatVariable d_true; + SatVariable d_false; + +public: + GlucoseSolver(const std::string& name = ""); + ~GlucoseSolver() throw(AssertionException); + + void addClause(SatClause& clause, bool removable, uint64_t proof_id); + void addXorClause(SatClause& clause, bool rhs, bool removable, uint64_t proof_id) { + Unreachable(); + } + + bool nativeXor() { return false; } + + SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); + + SatVariable trueVar(); + SatVariable falseVar(); + + void markUnremovable(SatLiteral lit); + + void interrupt(); + + SatValue solve(); + SatValue solve(long unsigned int&); + SatValue value(SatLiteral l); + SatValue modelValue(SatLiteral l); + unsigned getAssertionLevel() const; + + + // helper methods for converting from the internal representation + + static SatVariable toSatVariable(Glucose::Var var); + static Glucose::Lit toInternalLit(SatLiteral lit); + static SatLiteral toSatLiteral(Glucose::Lit lit); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(Glucose::lbool res); + + static void toInternalClause(SatClause& clause, Glucose::vec<Glucose::Lit>& internal_clause); + static void toSatClause (Glucose::vec<Glucose::Lit>& clause, SatClause& sat_clause); + + class Statistics { + public: + IntStat d_statCallsToSolve; + IntStat d_xorClausesAdded; + IntStat d_clausesAdded; + TimerStat d_solveTime; + bool d_registerStats; + Statistics(const std::string& prefix); + ~Statistics(); + }; + + Statistics d_statistics; +}; +} +} + +#else // CVC4_USE_GLUCOSE + +namespace CVC4 { +namespace prop { + +class GlucoseSolver : public SatSolver { + +public: + GlucoseSolver(const std::string& name = "") { Unreachable(); } + /** Assert a clause in the solver. */ + void addClause(SatClause& clause, bool removable, uint64_t proof_id) { + Unreachable(); + } + + /** Return true if the solver supports native xor resoning */ + bool nativeXor() { Unreachable(); } + + /** Add a clause corresponding to rhs = l1 xor .. xor ln */ + void addXorClause(SatClause& clause, bool rhs, bool removable, uint64_t proof_id) { + Unreachable(); + } + + SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); } + SatVariable trueVar() { Unreachable(); } + SatVariable falseVar() { Unreachable(); } + SatValue solve() { Unreachable(); } + SatValue solve(long unsigned int&) { Unreachable(); } + void interrupt() { Unreachable(); } + SatValue value(SatLiteral l) { Unreachable(); } + SatValue modelValue(SatLiteral l) { Unreachable(); } + unsigned getAssertionLevel() const { Unreachable(); } + +};/* class GlucoseSolver */ +} // CVC4::prop +} // CVC4 + +#endif // CVC4_USE_GLUCOSE + + + + diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 53ab2eccf..b2bbab37b 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -37,42 +37,42 @@ MinisatSatSolver::~MinisatSatSolver() throw() delete d_minisat; } -SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) { +SatVariable MinisatSatSolver::toSatVariable(CVC4::Minisat::Var var) { if (var == var_Undef) { return undefSatVariable; } return SatVariable(var); } -Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) { +CVC4::Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) { if (lit == undefSatLiteral) { - return Minisat::lit_Undef; + return CVC4::Minisat::lit_Undef; } - return Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); + return CVC4::Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); } -SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) { - if (lit == Minisat::lit_Undef) { +SatLiteral MinisatSatSolver::toSatLiteral(CVC4::Minisat::Lit lit) { + if (lit == CVC4::Minisat::lit_Undef) { return undefSatLiteral; } - return SatLiteral(SatVariable(Minisat::var(lit)), - Minisat::sign(lit)); + return SatLiteral(SatVariable(CVC4::Minisat::var(lit)), + CVC4::Minisat::sign(lit)); } -SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { - if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; - if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; - Assert(res == (Minisat::lbool((uint8_t)1))); +SatValue MinisatSatSolver::toSatLiteralValue(CVC4::Minisat::lbool res) { + if(res == (CVC4::Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; + if(res == (CVC4::Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; + Assert(res == (CVC4::Minisat::lbool((uint8_t)1))); return SAT_VALUE_FALSE; } -Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val) +CVC4::Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val) { - if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0); - if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2); + if(val == SAT_VALUE_TRUE) return CVC4::Minisat::lbool((uint8_t)0); + if(val == SAT_VALUE_UNKNOWN) return CVC4::Minisat::lbool((uint8_t)2); Assert(val == SAT_VALUE_FALSE); - return Minisat::lbool((uint8_t)1); + return CVC4::Minisat::lbool((uint8_t)1); } /*bool MinisatSatSolver::tobool(SatValue val) @@ -83,14 +83,14 @@ Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val) }*/ void MinisatSatSolver::toMinisatClause(SatClause& clause, - Minisat::vec<Minisat::Lit>& minisat_clause) { + CVC4::Minisat::vec<CVC4::Minisat::Lit>& minisat_clause) { for (unsigned i = 0; i < clause.size(); ++i) { minisat_clause.push(toMinisatLit(clause[i])); } Assert(clause.size() == (unsigned)minisat_clause.size()); } -void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, +void MinisatSatSolver::toSatClause(CVC4::Minisat::vec<CVC4::Minisat::Lit>& clause, SatClause& sat_clause) { for (int i = 0; i < clause.size(); ++i) { sat_clause.push_back(toSatLiteral(clause[i])); @@ -98,7 +98,7 @@ void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, Assert((unsigned)clause.size() == sat_clause.size()); } -void MinisatSatSolver::toSatClause(const Minisat::Clause& clause, +void MinisatSatSolver::toSatClause(const CVC4::Minisat::Clause& clause, SatClause& sat_clause) { for (int i = 0; i < clause.size(); ++i) { sat_clause.push_back(toSatLiteral(clause[i])); @@ -116,7 +116,7 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory } // Create the solver - d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, + d_minisat = new CVC4::Minisat::SimpSolver(theoryProxy, d_context, options::incrementalSolving() || options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ); @@ -146,7 +146,7 @@ void MinisatSatSolver::setupOptions() { } void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { - Minisat::vec<Minisat::Lit> minisat_clause; + CVC4::Minisat::vec<CVC4::Minisat::Lit> minisat_clause; toMinisatClause(clause, minisat_clause); d_minisat->addClause(minisat_clause, removable, proof_id); } @@ -163,7 +163,7 @@ SatValue MinisatSatSolver::solve(unsigned long& resource) { } else { d_minisat->setConfBudget(resource); } - Minisat::vec<Minisat::Lit> empty; + CVC4::Minisat::vec<CVC4::Minisat::Lit> empty; unsigned long conflictsBefore = d_minisat->conflicts + d_minisat->resources_consumed; SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); d_minisat->clearInterrupt(); @@ -259,7 +259,7 @@ MinisatSatSolver::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_statMaxLiterals); StatisticsRegistry::unregisterStat(&d_statTotLiterals); } -void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ +void MinisatSatSolver::Statistics::init(CVC4::Minisat::SimpSolver* d_minisat){ d_statStarts.setData(d_minisat->starts); d_statDecisions.setData(d_minisat->decisions); d_statRndDecisions.setData(d_minisat->rnd_decisions); diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 2564572c2..944acc590 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -27,7 +27,7 @@ namespace prop { class MinisatSatSolver : public DPLLSatSolverInterface { /** The SatSolver used */ - Minisat::SimpSolver* d_minisat; + CVC4::Minisat::SimpSolver* d_minisat; /** Context we will be using to synchronize the sat solver */ context::Context* d_context; @@ -40,20 +40,22 @@ public: ~MinisatSatSolver() throw(); ; - static SatVariable toSatVariable(Minisat::Var var); - static Minisat::Lit toMinisatLit(SatLiteral lit); - static SatLiteral toSatLiteral(Minisat::Lit lit); - static SatValue toSatLiteralValue(Minisat::lbool res); - static Minisat::lbool toMinisatlbool(SatValue val); + static SatVariable toSatVariable(CVC4::Minisat::Var var); + static CVC4::Minisat::Lit toMinisatLit(SatLiteral lit); + static SatLiteral toSatLiteral(CVC4::Minisat::Lit lit); + static SatValue toSatLiteralValue(CVC4::Minisat::lbool res); + static CVC4::Minisat::lbool toMinisatlbool(SatValue val); //(Commented because not in use) static bool tobool(SatValue val); - 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); + static void toMinisatClause(SatClause& clause, CVC4::Minisat::vec<CVC4::Minisat::Lit>& minisat_clause); + static void toSatClause (CVC4::Minisat::vec<CVC4::Minisat::Lit>& clause, SatClause& sat_clause); + static void toSatClause (const CVC4::Minisat::Clause& clause, SatClause& sat_clause); void initialize(context::Context* context, TheoryProxy* theoryProxy); void addClause(SatClause& clause, bool removable, uint64_t proof_id); - + void addXorClause(SatClause& clause, bool rhs, bool removable, uint64_t proof_id) { + Unreachable("Minisat does not support native XOR reasoning"); + } SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); SatVariable trueVar() { return d_minisat->trueVar(); } SatVariable falseVar() { return d_minisat->falseVar(); } @@ -93,7 +95,7 @@ public: public: Statistics(); ~Statistics(); - void init(Minisat::SimpSolver* d_minisat); + void init(CVC4::Minisat::SimpSolver* d_minisat); };/* class MinisatSatSolver::Statistics */ Statistics d_statistics; diff --git a/src/prop/riss.cpp b/src/prop/riss.cpp new file mode 100644 index 000000000..361caaa10 --- /dev/null +++ b/src/prop/riss.cpp @@ -0,0 +1,201 @@ +/********************* */ +/*! \file riss.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the riss sat solver for cvc4 (bitvectors). + **/ + +#include "prop/riss.h" +#include "smt/options.h" + +#ifdef CVC4_USE_RISS + +#include "theory/bv/options.h" + +using namespace CVC4; +using namespace prop; + +RissSolver::RissSolver(const std::string& name) + : d_config( CVC4::options::rissCommands() ) + , d_CP3Config(CVC4::options::rissCommands() ) + , d_solver(new Riss::Solver(&d_config)) + , d_statistics(name) +{ + // tell solver about preprocessor object + d_solver->setPreprocessor(&d_CP3Config); + + // if (CVC4::options::produceModels()) { + // // FIXME: we don't want to freeze everything + // d_solver->use_elim = false; + // } + d_true = newVar(); + d_false = newVar(); + d_solver->addClause(Riss::mkLit(d_true, false)); + d_solver->addClause(Riss::mkLit(d_false, true)); +} + + +RissSolver::~RissSolver() throw(AssertionException) { + delete d_solver; +} + +void RissSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { + Debug("sat::riss") << "Add clause " << clause <<"\n"; + + if (!d_solver->okay()) { + Debug("sat::riss") << "Solver unsat: not adding clause.\n"; + return; + } + + ++(d_statistics.d_clausesAdded); + + Riss::vec<Riss::Lit> internal_clause; + toInternalClause(clause, internal_clause); + d_solver->addClause(internal_clause); // check return status? +} + +SatVariable RissSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ + return d_solver->newVar(); +} + +SatVariable RissSolver::trueVar() { + return d_true; +} + +SatVariable RissSolver::falseVar() { + return d_false; +} + +void RissSolver::markUnremovable(SatLiteral lit) { + d_solver->freezeVariable(lit.getSatVariable(), true); + return; +} + +void RissSolver::interrupt(){ + d_solver->interrupt(); +} + +SatValue RissSolver::solve(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + ++d_statistics.d_statCallsToSolve; + return toSatLiteralValue(d_solver->solve()); +} + +SatValue RissSolver::solve(long unsigned int& resource) { + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + if(resource == 0) { + d_solver->budgetOff(); + } else { + d_solver->setConfBudget(resource); + } + return solve(); +} + +SatValue RissSolver::value(SatLiteral l){ + return toSatLiteralValue(d_solver->modelValue(toInternalLit(l))); +} + +SatValue RissSolver::modelValue(SatLiteral l){ + return toSatLiteralValue(d_solver->modelValue(toInternalLit(l))); +} + +unsigned RissSolver::getAssertionLevel() const { + Unreachable("No interface to get assertion level in Riss"); + return -1; +} + +// converting from internal sat solver representation + +SatVariable RissSolver::toSatVariable(Riss::Var var) { + if (var == Riss::Var(-1)) { + return undefSatVariable; + } + return SatVariable(var); +} + +Riss::Lit RissSolver::toInternalLit(SatLiteral lit) { + if (lit == undefSatLiteral) { + return Riss::lit_Undef; + } + return Riss::mkLit(lit.getSatVariable(), lit.isNegated()); +} + +SatLiteral RissSolver::toSatLiteral(Riss::Lit lit) { + if (lit == Riss::lit_Undef) { + return undefSatLiteral; + } + + return SatLiteral(SatVariable(Riss::var(lit)), + Riss::sign(lit)); +} + +SatValue RissSolver::toSatLiteralValue(Riss::lbool res) { + if(res == Riss::lbool((uint8_t)0)/*Riss::l_True*/) return SAT_VALUE_TRUE; + if(res == Riss::lbool((uint8_t)2)/*Riss::l_Undef*/) return SAT_VALUE_UNKNOWN; + Assert(res == Riss::lbool((uint8_t)1)/*Riss::l_False*/); + return SAT_VALUE_FALSE; +} + +SatValue RissSolver::toSatLiteralValue(bool res) { + if(res) return SAT_VALUE_TRUE; + return SAT_VALUE_FALSE; +} + + +void RissSolver::toInternalClause(SatClause& clause, + Riss::vec<Riss::Lit>& internal_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + internal_clause.push(toInternalLit(clause[i])); + } + Assert(clause.size() == (unsigned)internal_clause.size()); +} + +void RissSolver::toSatClause(Riss::vec<Riss::Lit>& 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()); +} + + +// Satistics for RissSolver + +RissSolver::Statistics::Statistics(const std::string& prefix) : + d_statCallsToSolve("theory::bv::"+prefix+"::riss::calls_to_solve", 0), + d_xorClausesAdded("theory::bv::"+prefix+"::riss::xor_clauses", 0), + d_clausesAdded("theory::bv::"+prefix+"::riss::clauses", 0), + d_solveTime("theory::bv::"+prefix+"::riss::solve_time"), + d_registerStats(!prefix.empty()) +{ + if (!d_registerStats) + return; + + StatisticsRegistry::registerStat(&d_statCallsToSolve); + StatisticsRegistry::registerStat(&d_xorClausesAdded); + StatisticsRegistry::registerStat(&d_clausesAdded); + StatisticsRegistry::registerStat(&d_solveTime); +} + +RissSolver::Statistics::~Statistics() { + if (!d_registerStats) + return; + + StatisticsRegistry::unregisterStat(&d_statCallsToSolve); + StatisticsRegistry::unregisterStat(&d_xorClausesAdded); + StatisticsRegistry::unregisterStat(&d_clausesAdded); + StatisticsRegistry::unregisterStat(&d_solveTime); +} + +#endif // CVC4_USE_RISS diff --git a/src/prop/riss.h b/src/prop/riss.h new file mode 100644 index 000000000..0e5a4593e --- /dev/null +++ b/src/prop/riss.h @@ -0,0 +1,136 @@ +/********************* */ +/*! \file glucose.h + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the glucose sat solver for cvc4 (bitvectors). + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "prop/sat_solver.h" + +#ifdef CVC4_USE_RISS + +#include <riss/core/Solver.h> +#include <coprocessor/Coprocessor.h> + +namespace CVC4 { +namespace prop { + +class RissSolver : public SatSolver { + +private: + Riss::CoreConfig d_config; + Coprocessor::CP3Config d_CP3Config; + Riss::Solver* d_solver; + SatVariable d_true; + SatVariable d_false; + +public: + RissSolver(const std::string& name = ""); + ~RissSolver() throw(AssertionException); + + void addClause(SatClause& clause, bool removable, uint64_t proof_id); + void addXorClause(SatClause& clause, bool rhs, bool removable, uint64_t proof_id) { + Unreachable(); + } + + bool nativeXor() { return false; } + + SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); + + SatVariable trueVar(); + SatVariable falseVar(); + + void markUnremovable(SatLiteral lit); + + void interrupt(); + + SatValue solve(); + SatValue solve(long unsigned int&); + SatValue value(SatLiteral l); + SatValue modelValue(SatLiteral l); + unsigned getAssertionLevel() const; + + + // helper methods for converting from the internal representation + + static SatVariable toSatVariable(Riss::Var var); + static Riss::Lit toInternalLit(SatLiteral lit); + static SatLiteral toSatLiteral(Riss::Lit lit); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(Riss::lbool res); + + static void toInternalClause(SatClause& clause, Riss::vec<Riss::Lit>& internal_clause); + static void toSatClause (Riss::vec<Riss::Lit>& clause, SatClause& sat_clause); + + class Statistics { + public: + IntStat d_statCallsToSolve; + IntStat d_xorClausesAdded; + IntStat d_clausesAdded; + TimerStat d_solveTime; + bool d_registerStats; + Statistics(const std::string& prefix); + ~Statistics(); + }; + + Statistics d_statistics; +}; + +} +} + +#else // CVC4_USE_RISS + +namespace CVC4 { +namespace prop { + +class RissSolver : public SatSolver { + +public: + RissSolver(const std::string& name = "") { Unreachable(); } + /** Assert a clause in the solver. */ + void addClause(SatClause& clause, bool removable, uint64_t proof_id) { + Unreachable(); + } + + /** Return true if the solver supports native xor resoning */ + bool nativeXor() { Unreachable(); } + + /** Add a clause corresponding to rhs = l1 xor .. xor ln */ + void addXorClause(SatClause& clause, bool rhs, bool removable, uint64_t proof_id) { + Unreachable(); + } + + SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); } + SatVariable trueVar() { Unreachable(); } + SatVariable falseVar() { Unreachable(); } + SatValue solve() { Unreachable(); } + SatValue solve(long unsigned int&) { Unreachable(); } + void interrupt() { Unreachable(); } + SatValue value(SatLiteral l) { Unreachable(); } + SatValue modelValue(SatLiteral l) { Unreachable(); } + unsigned getAssertionLevel() const { Unreachable(); } + +};/* class RissSolver */ +} // CVC4::prop +} // CVC4 + +#endif // CVC4_USE_RISS + + + diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 50d308541..e16832349 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -41,6 +41,12 @@ public: /** Assert a clause in the solver. */ virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0; + /** Return true if the solver supports native xor resoning */ + virtual bool nativeXor() { return false; } + + /** Add a clause corresponding to rhs = l1 xor .. xor ln */ + virtual void addXorClause(SatClause& clause, bool rhs, bool removable, uint64_t proof_id) = 0; + /** * Create a new boolean variable in the solver. * @param isTheoryAtom is this a theory atom that needs to be asserted to theory @@ -74,6 +80,7 @@ public: /** Get the current assertion level */ virtual unsigned getAssertionLevel() const = 0; + };/* class SatSolver */ @@ -177,4 +184,4 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) { }/* CVC4::prop namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PROP__SAT_MODULE_H */ +#endif /* __CVC4__PROP__SAT_SOLVER_H */ diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 98b8fce47..02efc69d6 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -14,20 +14,38 @@ ** SAT Solver. **/ +#include "prop/cryptominisat.h" +#include "prop/riss.h" +#include "prop/glucose.h" #include "prop/sat_solver_factory.h" #include "prop/minisat/minisat.h" #include "prop/bvminisat/bvminisat.h" + namespace CVC4 { namespace prop { - -BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, const std::string& name) { - return new BVMinisatSatSolver(mainSatContext, name); -} - -DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { - return new MinisatSatSolver(); -} - + + BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, + const std::string& name) { + return new BVMinisatSatSolver(mainSatContext, name); + } + + SatSolver* SatSolverFactory::createCryptoMinisat(const std::string& name) { + return new CryptoMinisatSolver(name); + } + + SatSolver* SatSolverFactory::createRiss(const std::string& name) { + return new RissSolver(name); + } + + SatSolver* SatSolverFactory::createGlucose(const std::string& name) { + return new GlucoseSolver(name); + } + + + DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { + return new MinisatSatSolver(); + } + } /* CVC4::prop namespace */ } /* CVC4 namespace */ diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 34776c245..a9fd71233 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -29,6 +29,10 @@ class SatSolverFactory { public: static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, const std::string& name = ""); + static SatSolver* createCryptoMinisat(const std::string& name = ""); + static SatSolver* createRiss(const std::string& name = ""); + static SatSolver* createGlucose(const std::string& name = ""); + static DPLLSatSolverInterface* createDPLLMinisat(); };/* class SatSolverFactory */ diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 9b2d3647e..cd0025fe2 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -192,7 +192,58 @@ void ArrayInfo::setConstArr(const TNode a, const TNode constArr) { } else { (*it).second->constArr = constArr; } - +} + +void ArrayInfo::setWeakEquivPointer(const TNode a, const TNode pointer) { + Assert(a.getType().isArray()); + Info* temp_info; + CNodeInfoMap::iterator it = info_map.find(a); + if(it == info_map.end()) { + temp_info = new Info(ct, bck); + temp_info->weakEquivPointer = pointer; + info_map[a] = temp_info; + } else { + (*it).second->weakEquivPointer = pointer; + } +} + +void ArrayInfo::setWeakEquivIndex(const TNode a, const TNode index) { + Assert(a.getType().isArray()); + Info* temp_info; + CNodeInfoMap::iterator it = info_map.find(a); + if(it == info_map.end()) { + temp_info = new Info(ct, bck); + temp_info->weakEquivIndex = index; + info_map[a] = temp_info; + } else { + (*it).second->weakEquivIndex = index; + } +} + +void ArrayInfo::setWeakEquivSecondary(const TNode a, const TNode secondary) { + Assert(a.getType().isArray()); + Info* temp_info; + CNodeInfoMap::iterator it = info_map.find(a); + if(it == info_map.end()) { + temp_info = new Info(ct, bck); + temp_info->weakEquivSecondary = secondary; + info_map[a] = temp_info; + } else { + (*it).second->weakEquivSecondary = secondary; + } +} + +void ArrayInfo::setWeakEquivSecondaryReason(const TNode a, const TNode reason) { + Assert(a.getType().isArray()); + Info* temp_info; + CNodeInfoMap::iterator it = info_map.find(a); + if(it == info_map.end()) { + temp_info = new Info(ct, bck); + temp_info->weakEquivSecondaryReason = reason; + info_map[a] = temp_info; + } else { + (*it).second->weakEquivSecondaryReason = reason; + } } /** @@ -248,6 +299,46 @@ const TNode ArrayInfo::getConstArr(const TNode a) const return TNode(); } +const TNode ArrayInfo::getWeakEquivPointer(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->weakEquivPointer; + } + return TNode(); +} + +const TNode ArrayInfo::getWeakEquivIndex(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->weakEquivIndex; + } + return TNode(); +} + +const TNode ArrayInfo::getWeakEquivSecondary(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->weakEquivSecondary; + } + return TNode(); +} + +const TNode ArrayInfo::getWeakEquivSecondaryReason(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->weakEquivSecondaryReason; + } + return TNode(); +} + const CTNodeList* ArrayInfo::getIndices(const TNode a) const{ CNodeInfoMap::const_iterator it = info_map.find(a); if(it!= info_map.end()) { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index f3c6385e5..ef49768b9 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -65,11 +65,23 @@ public: context::CDO<bool> rIntro1Applied; context::CDO<TNode> modelRep; context::CDO<TNode> constArr; + context::CDO<TNode> weakEquivPointer; + context::CDO<TNode> weakEquivIndex; + context::CDO<TNode> weakEquivSecondary; + context::CDO<TNode> weakEquivSecondaryReason; CTNodeList* indices; CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()), constArr(c,TNode()) { + Info(context::Context* c, Backtracker<TNode>* bck) + : isNonLinear(c, false), + rIntro1Applied(c, false), + modelRep(c,TNode()), + constArr(c,TNode()), + weakEquivPointer(c,TNode()), + weakEquivIndex(c,TNode()), + weakEquivSecondary(c,TNode()), + weakEquivSecondaryReason(c,TNode()) { indices = new(true)CTNodeList(c); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); @@ -212,6 +224,10 @@ public: void setModelRep(const TNode a, const TNode rep); void setConstArr(const TNode a, const TNode constArr); + void setWeakEquivPointer(const TNode a, const TNode pointer); + void setWeakEquivIndex(const TNode a, const TNode index); + void setWeakEquivSecondary(const TNode a, const TNode secondary); + void setWeakEquivSecondaryReason(const TNode a, const TNode reason); /** * Returns the information associated with TNode a */ @@ -225,6 +241,10 @@ public: const TNode getModelRep(const TNode a) const; const TNode getConstArr(const TNode a) const; + const TNode getWeakEquivPointer(const TNode a) const; + const TNode getWeakEquivIndex(const TNode a) const; + const TNode getWeakEquivSecondary(const TNode a) const; + const TNode getWeakEquivSecondaryReason(const TNode a) const; const CTNodeList* getIndices(const TNode a) const; diff --git a/src/theory/arrays/options b/src/theory/arrays/options index 8ed80c1f1..4a337e537 100644 --- a/src/theory/arrays/options +++ b/src/theory/arrays/options @@ -11,6 +11,9 @@ option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-wr option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination) +option arraysWeakEquivalence --arrays-weak-equiv bool :default false :read-write + use algorithm from Christ/Hoenicke (SMT 2014) + option arraysModelBased --arrays-model-based bool :default false :read-write turn on model-based array solver diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8bdf38ca3..587bb687f 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -30,6 +30,7 @@ using namespace std; namespace CVC4 { + namespace theory { namespace arrays { @@ -91,6 +92,8 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_modelConstraints(c), d_lemmasSaved(c), d_defValues(c), + d_readTableContext(new context::Context()), + d_arrayMerges(c), d_inCheckModel(false) { StatisticsRegistry::registerStat(&d_numRow); @@ -111,10 +114,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_ppEqualityEngine.addFunctionKind(kind::SELECT); d_ppEqualityEngine.addFunctionKind(kind::STORE); - // The mayequal congruence kinds - d_mayEqualEqualityEngine.addFunctionKind(kind::SELECT); - d_mayEqualEqualityEngine.addFunctionKind(kind::STORE); - // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::SELECT); if (d_ccStore) { @@ -126,9 +125,14 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC } TheoryArrays::~TheoryArrays() { - CNodeNListMap::iterator it = d_constReads.begin(); - for( ; it != d_constReads.end(); ++it ) { - (*it).second->deleteSelf(); + vector<CTNodeList*>::iterator it = d_readBucketAllocations.begin(), iend = d_readBucketAllocations.end(); + for (; it != iend; ++it) { + (*it)->deleteSelf(); + } + delete d_readTableContext; + CNodeNListMap::iterator it2 = d_constReads.begin(); + for( ; it2 != d_constReads.end(); ++it2 ) { + it2->second->deleteSelf(); } delete d_constReadsContext; StatisticsRegistry::unregisterStat(&d_numRow); @@ -392,6 +396,205 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) { } } +TNode TheoryArrays::weakEquivGetRep(TNode node) { + TNode pointer; + while (true) { + pointer = d_infoMap.getWeakEquivPointer(node); + if (pointer.isNull()) { + return node; + } + node = pointer; + } +} + +TNode TheoryArrays::weakEquivGetRepIndex(TNode node, TNode index) { + Assert(!index.isNull()); + TNode pointer, index2; + while (true) { + pointer = d_infoMap.getWeakEquivPointer(node); + if (pointer.isNull()) { + return node; + } + index2 = d_infoMap.getWeakEquivIndex(node); + if (index2.isNull() || !d_equalityEngine.areEqual(index, index2)) { + node = pointer; + } + else { + TNode secondary = d_infoMap.getWeakEquivSecondary(node); + if (secondary.isNull()) { + return node; + } + node = secondary; + } + } +} + +void TheoryArrays::visitAllLeaves(TNode reason, vector<TNode>& conjunctions) { + switch (reason.getKind()) { + case kind::AND: + Assert(reason.getNumChildren() == 2); + visitAllLeaves(reason[0], conjunctions); + visitAllLeaves(reason[1], conjunctions); + break; + case kind::NOT: + conjunctions.push_back(reason); + break; + case kind::EQUAL: + d_equalityEngine.explainEquality(reason[0], reason[1], true, conjunctions); + break; + default: + Unreachable(); + } +} + +void TheoryArrays::weakEquivBuildCond(TNode node, TNode index, vector<TNode>& conjunctions) { + Assert(!index.isNull()); + TNode pointer, index2; + while (true) { + pointer = d_infoMap.getWeakEquivPointer(node); + if (pointer.isNull()) { + return; + } + index2 = d_infoMap.getWeakEquivIndex(node); + if (index2.isNull()) { + // Null index means these two nodes became equal: explain the equality. + d_equalityEngine.explainEquality(node, pointer, true, conjunctions); + node = pointer; + } + else if (!d_equalityEngine.areEqual(index, index2)) { + // If indices are not equal in current context, need to add that to the lemma. + Node reason = index.eqNode(index2).notNode(); + d_permRef.push_back(reason); + conjunctions.push_back(reason); + node = pointer; + } + else { + TNode secondary = d_infoMap.getWeakEquivSecondary(node); + if (secondary.isNull()) { + return; + } + TNode reason = d_infoMap.getWeakEquivSecondaryReason(node); + Assert(!reason.isNull()); + visitAllLeaves(reason, conjunctions); + node = secondary; + } + } +} + +void TheoryArrays::weakEquivMakeRep(TNode node) { + TNode pointer = d_infoMap.getWeakEquivPointer(node); + if (pointer.isNull()) { + return; + } + weakEquivMakeRep(pointer); + d_infoMap.setWeakEquivPointer(pointer, node); + d_infoMap.setWeakEquivIndex(pointer, d_infoMap.getWeakEquivIndex(node)); + d_infoMap.setWeakEquivPointer(node, TNode()); + weakEquivMakeRepIndex(node); +} + +void TheoryArrays::weakEquivMakeRepIndex(TNode node) { + TNode secondary = d_infoMap.getWeakEquivSecondary(node); + if (secondary.isNull()) { + return; + } + TNode index = d_infoMap.getWeakEquivIndex(node); + Assert(!index.isNull()); + TNode index2 = d_infoMap.getWeakEquivIndex(secondary); + Node reason; + TNode next; + while (index2.isNull() || !d_equalityEngine.areEqual(index, index2)) { + next = d_infoMap.getWeakEquivPointer(secondary); + d_infoMap.setWeakEquivSecondary(node, next); + reason = d_infoMap.getWeakEquivSecondaryReason(node); + if (index2.isNull()) { + reason = reason.andNode(secondary.eqNode(next)); + } + else { + reason = reason.andNode(index.eqNode(index2).notNode()); + } + d_permRef.push_back(reason); + d_infoMap.setWeakEquivSecondaryReason(node, reason); + if (next.isNull()) { + return; + } + secondary = next; + index2 = d_infoMap.getWeakEquivIndex(secondary); + } + weakEquivMakeRepIndex(secondary); + d_infoMap.setWeakEquivSecondary(secondary, node); + d_infoMap.setWeakEquivSecondaryReason(secondary, d_infoMap.getWeakEquivSecondaryReason(node)); + d_infoMap.setWeakEquivSecondary(node, TNode()); + d_infoMap.setWeakEquivSecondaryReason(node, TNode()); +} + +void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) { + std::hash_set<TNode, TNodeHashFunction> marked; + vector<TNode> index_trail; + vector<TNode>::iterator it, iend; + Node equivalence_trail = reason; + Node current_reason; + TNode pointer, indexRep; + if (!index.isNull()) { + index_trail.push_back(index); + marked.insert(d_equalityEngine.getRepresentative(index)); + } + while (arrayFrom != arrayTo) { + index = d_infoMap.getWeakEquivIndex(arrayFrom); + pointer = d_infoMap.getWeakEquivPointer(arrayFrom); + if (!index.isNull()) { + indexRep = d_equalityEngine.getRepresentative(index); + if (marked.find(indexRep) == marked.end() && weakEquivGetRepIndex(arrayFrom, index) != arrayTo) { + weakEquivMakeRepIndex(arrayFrom); + d_infoMap.setWeakEquivSecondary(arrayFrom, arrayTo); + current_reason = equivalence_trail; + for (it = index_trail.begin(), iend = index_trail.end(); it != iend; ++it) { + current_reason = current_reason.andNode(index.eqNode(*it).notNode()); + } + d_permRef.push_back(current_reason); + d_infoMap.setWeakEquivSecondaryReason(arrayFrom, current_reason); + } + marked.insert(indexRep); + } + else { + equivalence_trail = equivalence_trail.andNode(arrayFrom.eqNode(pointer)); + } + arrayFrom = pointer; + } +} + +void TheoryArrays::checkWeakEquiv(bool arraysMerged) { + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_mayEqualEqualityEngine); + for (; !eqcs_i.isFinished(); ++eqcs_i) { + Node eqc = (*eqcs_i); + if (!eqc.getType().isArray()) { + continue; + } + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_mayEqualEqualityEngine); + TNode rep = d_mayEqualEqualityEngine.getRepresentative(*eqc_i); + TNode weakEquivRep = weakEquivGetRep(rep); + for (; !eqc_i.isFinished(); ++eqc_i) { + TNode n = *eqc_i; + Assert(!arraysMerged || weakEquivGetRep(n) == weakEquivRep); + TNode pointer = d_infoMap.getWeakEquivPointer(n); + TNode index = d_infoMap.getWeakEquivIndex(n); + TNode secondary = d_infoMap.getWeakEquivSecondary(n); + Assert(pointer.isNull() == (weakEquivGetRep(n) == n)); + Assert(!pointer.isNull() || secondary.isNull()); + Assert(!index.isNull() || secondary.isNull()); + Assert(d_infoMap.getWeakEquivSecondaryReason(n).isNull() || !secondary.isNull()); + if (!pointer.isNull()) { + if (index.isNull()) { + Assert(d_equalityEngine.areEqual(n, pointer)); + } + else { + Assert((n.getKind() == kind::STORE && n[0] == pointer && n[1] == index) || + (pointer.getKind() == kind::STORE && pointer[0] == n && pointer[1] == index)); + } + } + } + } +} /** * Stores in d_infoMap the following information for each term a of type array: @@ -432,7 +635,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) // The may equal needs the store d_mayEqualEqualityEngine.addTerm(store); - if (options::arraysLazyRIntro1()) { + if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) { // Apply RIntro1 rule to any stores equal to store if not done already const CTNodeList* stores = d_infoMap.getStores(store); CTNodeList::const_iterator it = stores->begin(); @@ -477,7 +680,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) // Record read in sharing data structure TNode index = d_equalityEngine.getRepresentative(node[1]); - if (index.isConst()) { + if (!options::arraysWeakEquivalence() && index.isConst()) { CTNodeList* temp; CNodeNListMap::iterator it = d_constReads.find(index); if (it == d_constReads.end()) { @@ -522,7 +725,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) Assert(d_mayEqualEqualityEngine.consistent()); } - if (!options::arraysLazyRIntro1()) { + if (!options::arraysLazyRIntro1() || options::arraysWeakEquivalence()) { TNode i = node[1]; TNode v = node[2]; NodeManager* nm = NodeManager::currentNM(); @@ -539,6 +742,17 @@ void TheoryArrays::preRegisterTermInternal(TNode node) d_infoMap.addInStore(a, node); d_infoMap.setModelRep(node, node); + //Add-Store for Weak Equivalence + if (options::arraysWeakEquivalence()) { + Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a)); + Assert(weakEquivGetRep(node) == node); + d_infoMap.setWeakEquivPointer(node, node[0]); + d_infoMap.setWeakEquivIndex(node, node[1]); +#ifdef CVC4_ASSERTIONS + checkWeakEquiv(false); +#endif + } + checkStore(node); break; } @@ -723,12 +937,7 @@ void TheoryArrays::computeCareGraph() } } } - if (options::arraysModelBased()) { - checkModel(EFFORT_COMBINATION); - return; - } if (d_sharedTerms) { - // Synchronize d_constReadsContext with SAT context Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) { @@ -1065,18 +1274,13 @@ void TheoryArrays::check(Effort e) { switch (fact.getKind()) { case kind::EQUAL: d_equalityEngine.assertEquality(fact, true, fact); - if (!fact[0].getType().isArray()) { - d_modelConstraints.push_back(fact); - } break; case kind::SELECT: d_equalityEngine.assertPredicate(fact, true, fact); - d_modelConstraints.push_back(fact); break; case kind::NOT: if (fact[0].getKind() == kind::SELECT) { d_equalityEngine.assertPredicate(fact[0], false, fact); - d_modelConstraints.push_back(fact); } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1], false)) { // Assert the dis-equality d_equalityEngine.assertEquality(fact[0], false, fact); @@ -1096,9 +1300,6 @@ void TheoryArrays::check(Effort e) { d_out->lemma(lemma); ++d_numExt; } - else { - d_modelConstraints.push_back(fact); - } } break; default: @@ -1106,746 +1307,97 @@ void TheoryArrays::check(Effort e) { } } - if (options::arraysModelBased() && !d_conflict && (options::arraysEagerIndexSplitting() || fullEffort(e))) { - checkModel(e); - } - - if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysModelBased()) { - // generate the lemmas on the worklist - Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n"; - while (d_RowQueue.size() > 0 && !d_conflict) { - if (dischargeLemmas()) { - break; - } - } - } - - Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; -} - - -void TheoryArrays::convertNodeToAssumptions(TNode node, vector<TNode>& assumptions, TNode nodeSkip) -{ - Assert(node.getKind() == kind::AND); - for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) { - if ((*child_it).getKind() == kind::AND) { - convertNodeToAssumptions(*child_it, assumptions, nodeSkip); - } - else if (*child_it != nodeSkip) { - assumptions.push_back(*child_it); - } - } -} - - -void TheoryArrays::preRegisterStores(TNode s) -{ - if (d_equalityEngine.hasTerm(s)) { - return; - } - if (s.getKind() == kind::STORE) { - preRegisterStores(s[0]); - preRegisterTermInternal(s); - } -} - - -void TheoryArrays::checkModel(Effort e) -{ - d_inCheckModel = true; - d_topLevel = getSatContext()->getLevel(); - Assert(d_skolemIndex == 0); - Assert(d_skolemAssertions.empty()); - Assert(d_lemmas.empty()); - - if (combination(e)) { - // Add constraints for shared terms - context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(), shared_it2; - Node modelVal, modelVal2, d; - vector<TNode> assumptions; - for (; shared_it != shared_it_end; ++shared_it) { - if ((*shared_it).getType().isArray()) { - continue; - } - if ((*shared_it).isConst()) { - modelVal = (*shared_it); - } - else { - modelVal = d_valuation.getModelValue(*shared_it); - if (modelVal.isNull()) { - continue; - } - } - Assert(modelVal.isConst()); - for (shared_it2 = shared_it, ++shared_it2; shared_it2 != shared_it_end; ++shared_it2) { - if ((*shared_it2).getType() != (*shared_it).getType()) { - continue; - } - if ((*shared_it2).isConst()) { - modelVal2 = (*shared_it2); - } - else { - modelVal2 = d_valuation.getModelValue(*shared_it2); - if (modelVal2.isNull()) { - continue; - } - } - Assert(modelVal2.isConst()); - d = (*shared_it).eqNode(*shared_it2); - if (modelVal != modelVal2) { - d = d.notNode(); - } - if (!setModelVal(d, d_true, false, true, assumptions)) { - assumptions.push_back(d); - d_lemmas.push_back(mkAnd(assumptions, true)); - goto finish; - } - assumptions.clear(); - } - } - } - { - // TODO: record and replay decisions - int baseLevel = getSatContext()->getLevel(); - unsigned constraintIdx; - Node assertion, assertionToCheck; - vector<TNode> assumptions; - int numrestarts = 0; - while (true || numrestarts < 1 || fullEffort(e) || combination(e)) { - ++numrestarts; - d_out->safePoint(1); - int level = getSatContext()->getLevel(); - d_getModelValCache.clear(); - for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) { - assertion = d_modelConstraints[constraintIdx]; - if (getModelValRec(assertion) != d_true) { - break; - } - } - getSatContext()->popto(level); - if (constraintIdx == d_modelConstraints.size()) { - break; - } - - if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) { - assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false); - if (assertionToCheck.getKind() == kind::AND && - assertionToCheck[assertionToCheck.getNumChildren()-1].getKind() == kind::EQUAL) { - TNode s = assertionToCheck[assertionToCheck.getNumChildren()-1][0]; - preRegisterStores(s); - } - } - else { - assertionToCheck = assertion; - } - // TODO: try not collecting assumptions the first time - while (!setModelVal(assertionToCheck, d_true, false, true, assumptions)) { - restart: - if (assertion.getKind() == kind::EQUAL) { - d_equalityEngine.explainEquality(assertion[0], assertion[1], true, assumptions); + if ((options::arraysEagerLemmas() || fullEffort(e)) && !d_conflict && options::arraysWeakEquivalence()) { + // Replay all array merges to update weak equivalence data structures + context::CDList<Node>::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end(); + TNode a, b, eq; + for (; it != iend; ++it) { + eq = *it; + a = eq[0]; + b = eq[1]; + weakEquivMakeRep(b); + if (weakEquivGetRep(a) == b) { + weakEquivAddSecondary(TNode(), a, b, eq); } else { - assumptions.push_back(assertion); + d_infoMap.setWeakEquivPointer(b, a); + d_infoMap.setWeakEquivIndex(b, TNode()); } #ifdef CVC4_ASSERTIONS - std::set<TNode> validAssumptions; - context::CDList<Assertion>::const_iterator assert_it2 = facts_begin(); - for (; assert_it2 != facts_end(); ++assert_it2) { - validAssumptions.insert(*assert_it2); - } - for (unsigned i = 0; i < d_decisions.size(); ++i) { - validAssumptions.insert(d_decisions[i]); - } + checkWeakEquiv(false); #endif - std::set<TNode> all; - std::set<TNode> explained; - unsigned i = 0; - TNode t; - for (; i < assumptions.size(); ++i) { - t = assumptions[i]; - if (t == d_true) { - continue; - } - if (t.getKind() == kind::AND) { - for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) { - Assert(validAssumptions.find(*child_it) != validAssumptions.end()); - all.insert(*child_it); - } - } - // Expand explanation resulting from propagating a ROW lemma - else if (t.getKind() == kind::OR) { - if ((explained.find(t) == explained.end())) { - Assert(t[1].getKind() == kind::EQUAL); - d_equalityEngine.explainEquality(t[1][0], t[1][1], false, assumptions); - explained.insert(t); - } - continue; - } - else { - Assert(validAssumptions.find(t) != validAssumptions.end()); - all.insert(t); - } - } - - bool eq = false; - Node decision, explanation; - while (!d_decisions.empty()) { - getSatContext()->pop(); - decision = d_decisions.back(); - d_decisions.pop_back(); - if (all.find(decision) != all.end()) { - if (getSatContext()->getLevel() < baseLevel) { - if (all.size() == 1) { - d_lemmas.push_back(decision.negate()); - } - else { - NodeBuilder<> disjunction(kind::OR); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - disjunction << (*it).negate(); - ++it; - } - d_lemmas.push_back(disjunction); - } - goto finish; - } - all.erase(decision); - eq = false; - if (decision.getKind() == kind::NOT) { - decision = decision[0]; - eq = true; - } - while (getSatContext()->getLevel() != baseLevel && all.find(d_decisions.back()) == all.end()) { - getSatContext()->pop(); - d_decisions.pop_back(); - } - break; - } - else { - decision = Node(); - } - } - if (all.size() == 0) { - explanation = d_true; - } - if (all.size() == 1) { - // All the same, or just one - explanation = *(all.begin()); - } - else { - NodeBuilder<> conjunction(kind::AND); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++it; - } - explanation = conjunction; - d_permRef.push_back(explanation); - } - if (decision.isNull()) { - // d_lemmas.pop_back(); - d_conflictNode = explanation; - d_conflict = true; - break; - } - { - // generate lemma - if (all.size() == 0) { - d_lemmas.push_back(decision.negate()); - } - else { - NodeBuilder<> disjunction(kind::OR); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - disjunction << (*it).negate(); - ++it; - } - disjunction << decision.negate(); - d_lemmas.push_back(disjunction); - } - } - d_equalityEngine.assertEquality(decision, eq, explanation); - if (!eq) decision = decision.notNode(); - Debug("arrays-model-based") << "Asserting learned literal " << decision << " with explanation " << explanation << endl; - if (d_conflict) { - assumptions.clear(); - convertNodeToAssumptions(d_conflictNode, assumptions, TNode()); - assertion = d_true; - goto restart; - } - assumptions.clear(); - - // Reassert skolems if necessary - Node d; - while (d_skolemIndex < d_skolemAssertions.size()) { - d = d_skolemAssertions[d_skolemIndex]; - Assert(isLeaf(d[0])); - if (!d_equalityEngine.hasTerm(d[0])) { - preRegisterTermInternal(d[0]); - } - if (d[0].getType().isArray()) { - Assert(d[1].getKind() == kind::STORE); - if (d[1][0].getKind() == kind::STORE) { - if (!d_equalityEngine.hasTerm(d[1][0][0])) { - preRegisterTermInternal(d[1][0][0]); - } - if (!d_equalityEngine.hasTerm(d[1][0][2])) { - preRegisterTermInternal(d[1][0][2]); - } - } - if (!d_equalityEngine.hasTerm(d[1][0])) { - preRegisterTermInternal(d[1][0]); - } - if (!d_equalityEngine.hasTerm(d[1][2])) { - preRegisterTermInternal(d[1][2]); - } - if (!d_equalityEngine.hasTerm(d[1])) { - preRegisterTermInternal(d[1]); - } - } - Debug("arrays-model-based") << "Re-asserting skolem equality " << d << endl; - d_equalityEngine.assertEquality(d, true, d_true); - Assert(!d_conflict); - if (!d[0].getType().isArray()) { - if (!setModelVal(d[1], d[0], false, true, assumptions)) { - assertion = d_true; - goto restart; - } - assumptions.clear(); - } - d_skolemIndex = d_skolemIndex + 1; - } - // Reregister stores - if (assertionToCheck != assertion && - assertionToCheck.getKind() == kind::AND && - assertionToCheck[assertionToCheck.getNumChildren()-1].getKind() == kind::EQUAL) { - TNode s = assertionToCheck[assertionToCheck.getNumChildren()-1][0]; - preRegisterStores(s); - } - } - if (d_conflict) { - break; } - // Assert(getModelVal(assertion) == d_true); - assumptions.clear(); - } #ifdef CVC4_ASSERTIONS - if (!d_conflict && fullEffort(e)) { - context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); - for (; assert_it != assert_it_end; ++assert_it) { - Assert(getModelVal(*assert_it) == d_true); - } - } + checkWeakEquiv(true); #endif - } - finish: - while (!d_decisions.empty()) { - Assert(!d_conflict); - getSatContext()->pop(); - d_decisions.pop_back(); - } - d_skolemAssertions.clear(); - d_skolemIndex = 0; - while (!d_lemmas.empty()) { - Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl; - d_out->splitLemma(d_lemmas.back()); -#ifdef CVC4_ASSERTIONS - // Assert(d_lemmasSaved.find(d_lemmas.back()) == d_lemmasSaved.end()); - // d_lemmasSaved.insert(d_lemmas.back()); -#endif - d_lemmas.pop_back(); - } - Assert(getSatContext()->getLevel() == d_topLevel); - if (d_conflict) { - Node tmp = d_conflictNode; - d_out->conflict(tmp); - } - d_inCheckModel = false; -} - -Node TheoryArrays::getModelVal(TNode node) -{ - int level = getSatContext()->getLevel(); - d_getModelValCache.clear(); - Node ret = getModelValRec(node); - getSatContext()->popto(level); - return ret; -} - - -Node TheoryArrays::getModelValRec(TNode node) -{ - if (node.isConst()) { - return node; - } - NodeMap::iterator it = d_getModelValCache.find(node); - if (it != d_getModelValCache.end()) { - return (*it).second; - } - Node val; - switch (node.getKind()) { - case kind::NOT: - val = getModelValRec(node[0]) == d_true ? d_false : d_true; - break; - case kind::AND: { - val = d_true; - for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) { - if (getModelValRec(*child_it) != d_true) { - val = d_false; - break; - } - } - break; - } - case kind::IMPLIES: - if (getModelValRec(node[0]) == d_false) { - val = d_true; - } - else { - val = getModelValRec(node[1]); - } - case kind::EQUAL: - val = getModelValRec(node[0]); - val = (val == getModelValRec(node[1])) ? d_true : d_false; - break; - case kind::SELECT: { - NodeManager* nm = NodeManager::currentNM(); - Node indexVal = getModelValRec(node[1]); - val = Rewriter::rewrite(nm->mkNode(kind::SELECT, node[0], indexVal)); - if (val.isConst()) { - break; - } - val = Rewriter::rewrite(nm->mkNode(kind::SELECT, getModelValRec(node[0]), indexVal)); - Assert(val.isConst()); - break; - } - case kind::STORE: { - NodeManager* nm = NodeManager::currentNM(); - val = getModelValRec(node[0]); - val = Rewriter::rewrite(nm->mkNode(kind::STORE, val, getModelValRec(node[1]), getModelValRec(node[2]))); - Assert(val.isConst()); - break; - } - default: { - Assert(isLeaf(node)); - TNode eRep = d_equalityEngine.getRepresentative(node); - if (eRep.isConst()) { - val = eRep; - break; - } - TNode rep = d_infoMap.getModelRep(eRep); - if (!rep.isNull()) { - // TODO: check for loop here - val = getModelValRec(rep); + d_readTableContext->push(); + TNode mayRep, iRep; + CTNodeList* bucketList = NULL; + CTNodeList::const_iterator i = d_reads.begin(), readsEnd = d_reads.end(); + for (; i != readsEnd; ++i) { + const TNode& r = *i; + + Debug("arrays::weak") << "TheoryArrays::check(): checking read " << r << std::endl; + + // Find the bucket for this read. + mayRep = d_mayEqualEqualityEngine.getRepresentative(r[0]); + iRep = d_equalityEngine.getRepresentative(r[1]); + std::pair<TNode, TNode> key(mayRep, iRep); + ReadBucketMap::iterator it = d_readBucketTable.find(key); + if (it == d_readBucketTable.end()) { + bucketList = new(true) CTNodeList(d_readTableContext); + d_readBucketAllocations.push_back(bucketList); + d_readBucketTable[key] = bucketList; } else { - NodeMap::iterator it = d_lastVal.find(eRep); - if (it != d_lastVal.end()) { - val = (*it).second; - if (!d_equalityEngine.hasTerm(val) || - !d_equalityEngine.areDisequal(eRep, val, true)) { - getSatContext()->push(); - ++d_numGetModelValSplits; - d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true); - if (!d_conflict) { - break; - } - ++d_numGetModelValConflicts; - getSatContext()->pop(); - } + bucketList = it->second; + } + CTNodeList::const_iterator it2 = bucketList->begin(), iend = bucketList->end(); + for (; it2 != iend; ++it2) { + const TNode& r2 = *it2; + Assert(r2.getKind() == kind::SELECT); + Assert(mayRep == d_mayEqualEqualityEngine.getRepresentative(r2[0])); + Assert(iRep == d_equalityEngine.getRepresentative(r2[1])); + if (d_equalityEngine.areEqual(r, r2)) { + continue; } - - TypeEnumerator te(eRep.getType()); - val = *te; - while (true) { - if (!d_equalityEngine.hasTerm(val) || - !d_equalityEngine.areDisequal(eRep, val, true)) { - getSatContext()->push(); - ++d_numGetModelValSplits; - d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true); - if (!d_conflict) { - d_lastVal[eRep] = val; - break; - } - ++d_numGetModelValConflicts; - getSatContext()->pop(); - } - ++te; - if (te.isFinished()) { - Assert(false); - // TODO: conflict - break; + if (weakEquivGetRepIndex(r[0], r[1]) == weakEquivGetRepIndex(r2[0], r[1])) { + // add lemma: r[1] = r2[1] /\ cond(r[0],r2[0]) => r = r2 + vector<TNode> conjunctions; + Assert(d_equalityEngine.areEqual(r, Rewriter::rewrite(r))); + Assert(d_equalityEngine.areEqual(r2, Rewriter::rewrite(r2))); + Node lemma = Rewriter::rewrite(r).eqNode(Rewriter::rewrite(r2)).negate(); + d_permRef.push_back(lemma); + conjunctions.push_back(lemma); + if (r[1] != r2[1]) { + d_equalityEngine.explainEquality(r[1], r2[1], true, conjunctions); } - val = *te; + // TODO: get smaller lemmas by eliminating shared parts of path + weakEquivBuildCond(r[0], r[1], conjunctions); + weakEquivBuildCond(r2[0], r[1], conjunctions); + lemma = mkAnd(conjunctions, true); + d_out->lemma(lemma, false, false, true); + d_readTableContext->pop(); + return; } } - break; - } - } - d_getModelValCache[node] = val; - return val; -} - - -bool TheoryArrays::hasLoop(TNode node, TNode target) -{ - if (node == target) { - return true; - } - - if (isLeaf(node)) { - TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node)); - if (!rep.isNull()) { - return hasLoop(rep, target); - } - return false; - } - - for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) { - if (hasLoop(*child_it, target)) { - return true; - } - } - - return false; -} - - -// Return true iff it we were able to modify model so that value of node has same value as val -bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, vector<TNode>& assumptions) -{ - Assert(!d_conflict); - if (node == val) { - return !invert; - } - if (node.isConst()) { - if (invert) { - return (val.isConst() && node != val); + bucketList->push_back(r); } - return val == node; + d_readTableContext->pop(); } - switch(node.getKind()) { - case kind::NOT: - Assert(val == d_true || val == d_false); - return setModelVal(node[0], val, !invert, explain, assumptions); - break; - case kind::AND: { - Assert(val == d_true || val == d_false); - if (val == d_false) { - invert = !invert; - } - int i; - for(i = node.getNumChildren()-1; i >=0; --i) { - if (setModelVal(node[i], d_true, invert, explain, assumptions) == invert) { - return invert; - } - } - return !invert; - } - case kind::IMPLIES: - Assert(val == d_true || val == d_false); - if (val == d_false) { - invert = !invert; - } - if (setModelVal(node[0], d_false, invert, explain, assumptions) == !invert) { - return !invert; - } - if (setModelVal(node[1], d_true, invert, explain, assumptions) == !invert) { - return !invert; - } - return invert; - case kind::EQUAL: - Assert(val == d_true || val == d_false); - if (val == d_false) { - invert = !invert; - } - if (node[0].isConst()) { - return setModelVal(node[1], node[0], invert, explain, assumptions); - } - else { - return setModelVal(node[0], node[1], invert, explain, assumptions); - } - case kind::SELECT: { - TNode s = node[0]; - Node index = node[1]; - - while (s.getKind() == kind::STORE) { - if (setModelVal(s[1].eqNode(index), d_true, false, explain, assumptions)) { - if (setModelVal(s[2].eqNode(val), d_true, invert, explain, assumptions)) { - return true; - } - // Now try to set the indices to be disequal - if (!setModelVal(s[1].eqNode(index), d_false, false, explain, assumptions)) { - return false; - } - Unreachable(); - } - s = s[0]; - } - TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(s)); - NodeManager* nm = NodeManager::currentNM(); - if (!rep.isNull()) { - // TODO: check for loop - if (explain) { - d_equalityEngine.explainEquality(s, rep, true, assumptions); - } - return setModelVal(nm->mkNode(kind::SELECT, rep, index), val, invert, explain, assumptions); - } - if (val.getKind() == kind::SELECT && val[0].getKind() == kind::STORE) { - return setModelVal(val, nm->mkNode(kind::SELECT, s, index), invert, explain, assumptions); - } - // Solve equation for s: select(s,index) op val --> s = store(s',i',v') /\ index = i' /\ v' op val - Node newVarArr = getSkolem(s, "array_model_arr_var", s.getType(), "a new array variable from the theory of arrays", false); - Assert(d_infoMap.getModelRep(d_equalityEngine.getRepresentative(newVarArr)).isNull()); - Node lookup; - bool checkIndex1 = false, checkIndex2 = false, checkIndex3 = false; - if (!isLeaf(index)) { - index = getSkolem(index, "array_model_index", index.getType(), "a new index variable from the theory of arrays"); - if (!index.getType().isArray()) { - checkIndex1 = true; - } - } - lookup = nm->mkNode(kind::SELECT, s, index); - Node newVarVal = getSkolem(lookup, "array_model_var", val.getType(), "a new value variable from the theory of arrays", false); - - Node newVarVal2; - Node index2; - TNode saveVal = val; - if (val.getKind() == kind::SELECT && val[0] == s) { - // Special case: select(s,index) = select(s,j): solution becomes s = store(store(s',j,v'),index,w') /\ v' = w' - index2 = val[1]; - if (!isLeaf(index2)) { - index2 = getSkolem(val, "array_model_index", index2.getType(), "a new index variable from the theory of arrays"); - if (!index2.getType().isArray()) { - checkIndex2 = true; - } - } - if (invert) { - checkIndex3 = true; - } - lookup = nm->mkNode(kind::SELECT, s, index2); - newVarVal2 = getSkolem(lookup, "array_model_var", val.getType(), "a new value variable from the theory of arrays", false); - newVarArr = nm->mkNode(kind::STORE, newVarArr, index2, newVarVal2); - preRegisterTermInternal(newVarArr); - val = newVarVal2; - } - - Node d = nm->mkNode(kind::STORE, newVarArr, index, newVarVal); - preRegisterTermInternal(d); - d = s.eqNode(d); - Debug("arrays-model-based") << "Asserting array skolem equality " << d << endl; - d_equalityEngine.assertEquality(d, true, d_true); - d_skolemAssertions.push_back(d); - d_skolemIndex = d_skolemIndex + 1; - Assert(!d_conflict); - if (checkIndex1) { - if (!setModelVal(node[1], index, false, explain, assumptions)) { - return false; - } - } - if (checkIndex2) { - if (!setModelVal(saveVal[1], index2, false, explain, assumptions)) { - return false; - } - } - if (checkIndex3) { - if (!setModelVal(index2, index, true, explain, assumptions)) { - return false; - } - } - return setModelVal(newVarVal, val, invert, explain, assumptions); - } - case kind::STORE: - if (val.getKind() != kind::STORE) { - return setModelVal(val, node, invert, explain, assumptions); - } - Unreachable(); - break; - default: { - Assert(isLeaf(node)); - TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node)); - if (!rep.isNull()) { - // Assume this array equation has already been dealt with - otherwise, it shouldn't have a rep - return true; - } - if (val.getKind() == kind::SELECT) { - return setModelVal(val, node, invert, explain, assumptions); - } - if (d_equalityEngine.hasTerm(node) && - d_equalityEngine.hasTerm(val)) { - if ((!invert && d_equalityEngine.areDisequal(node, val, true)) || - (invert && d_equalityEngine.areEqual(node, val))) { - if (explain) { - d_equalityEngine.explainEquality(node, val, invert, assumptions); - } - return false; - } - if ((!invert && d_equalityEngine.areEqual(node, val)) || - (invert && d_equalityEngine.areDisequal(node, val, true))) { - return true; - } - } - Node d = node.eqNode(val); - Node r = Rewriter::rewrite(d); - if (r.isConst()) { - d_equalityEngine.assertEquality(d, r == d_true, d_true); - return ((r == d_true) == (!invert)); - } - getSatContext()->push(); - d_decisions.push_back(invert ? d.negate() : d); - d_equalityEngine.assertEquality(d, !invert, d_decisions.back()); - Debug("arrays-model-based") << "Asserting " << d_decisions.back() << " with explanation " << d_decisions.back() << endl; - ++d_numSetModelValSplits; - if (d_conflict) { - ++d_numSetModelValConflicts; - Debug("arrays-model-based") << "...which results in a conflict!" << endl; - d = d_decisions.back(); - unsigned sz = assumptions.size(); - convertNodeToAssumptions(d_conflictNode, assumptions, d); - unsigned sz2 = assumptions.size(); - Assert(sz2 > sz); - Node explanation; - if (sz2 == sz+1) { - explanation = assumptions[sz]; - } - else { - NodeBuilder<> conjunction(kind::AND); - for (unsigned i = sz; i < sz2; ++i) { - conjunction << assumptions[i]; - } - explanation = conjunction; - } - // assumptions.push_back(d); - // d_lemmas.push_back(mkAnd(assumptions, true, sz)); - // while (assumptions.size() > sz2) { - // assumptions.pop_back(); - // } - getSatContext()->pop(); - d_decisions.pop_back(); - d_permRef.push_back(explanation); - d = d.negate(); - Debug("arrays-model-based") << "Asserting learned literal2 " << d << " with explanation " << explanation << endl; - bool eq = true; - if (d.getKind() == kind::NOT) { - d = d[0]; - eq = false; - } - d_equalityEngine.assertEquality(d, eq, explanation); - if (d_conflict) { - Assert(false); - } - return false; + if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysWeakEquivalence()) { + // generate the lemmas on the worklist + Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n"; + while (d_RowQueue.size() > 0 && !d_conflict) { + if (dischargeLemmas()) { + break; } - return true; } } - Unreachable(); - return false; + + Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; } @@ -1916,7 +1468,7 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned void TheoryArrays::setNonLinear(TNode a) { - if (options::arraysModelBased()) return; + if (options::arraysWeakEquivalence()) return; if (d_infoMap.isNonLinear(a)) return; Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; @@ -2029,84 +1581,6 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b) } -Node TheoryArrays::removeRepLoops(TNode a, TNode rep) -{ - if (rep.getKind() != kind::STORE) { - Assert(isLeaf(rep)); - TNode tmp = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(rep)); - if (!tmp.isNull()) { - Node tmp2 = removeRepLoops(a, tmp); - if (tmp != tmp2) { - return tmp2; - } - } - return rep; - } - - Node s = removeRepLoops(a, rep[0]); - bool changed = (s != rep[0]); - - Node index = rep[1]; - Node value = rep[2]; - Node lookup; - - // TODO: Change to hasLoop? - if (!isLeaf(index)) { - changed = true; - index = getSkolem(index, "array_model_index", index.getType(), "a new index variable from the theory of arrays", false); - if (!d_equalityEngine.hasTerm(index) || - !d_equalityEngine.hasTerm(rep[1]) || - !d_equalityEngine.areEqual(rep[1], index)) { - Node d = index.eqNode(rep[1]); - Debug("arrays-model-based") << "Asserting skolem equality " << d << endl; - d_equalityEngine.assertEquality(d, true, d_true); - d_modelConstraints.push_back(d); - } - } - if (!isLeaf(value)) { - changed = true; - value = getSkolem(value, "array_model_var", value.getType(), "a new value variable from the theory of arrays", false); - if (!d_equalityEngine.hasTerm(value) || - !d_equalityEngine.hasTerm(rep[2]) || - !d_equalityEngine.areEqual(rep[2], value)) { - Node d = value.eqNode(rep[2]); - Debug("arrays-model-based") << "Asserting skolem equality " << d << endl; - d_equalityEngine.assertEquality(d, true, d_true); - d_modelConstraints.push_back(d); - } - } - if (changed) { - NodeManager* nm = NodeManager::currentNM(); - return nm->mkNode(kind::STORE, s, index, value); - } - return rep; -} - - -Node TheoryArrays::expandStores(TNode s, vector<TNode>& assumptions, bool checkLoop, TNode a, TNode loopRep) -{ - if (s.getKind() != kind::STORE) { - Assert(isLeaf(s)); - TNode tmp = d_equalityEngine.getRepresentative(s); - if (checkLoop && tmp == a) { - // Loop detected - d_equalityEngine.explainEquality(s, loopRep, true, assumptions); - return loopRep; - } - tmp = d_infoMap.getModelRep(tmp); - if (!tmp.isNull()) { - d_equalityEngine.explainEquality(s, tmp, true, assumptions); - return expandStores(tmp, assumptions, checkLoop, a, loopRep); - } - return s; - } - Node tmp = expandStores(s[0], assumptions, checkLoop, a, loopRep); - if (tmp != s[0]) { - NodeManager* nm = NodeManager::currentNM(); - return nm->mkNode(kind::STORE, tmp, s[1], s[2]); - } - return s; -} void TheoryArrays::mergeArrays(TNode a, TNode b) @@ -2126,12 +1600,12 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) while (true) { Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n"; - if (options::arraysLazyRIntro1()) { + if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) { checkRIntro1(a, b); checkRIntro1(b, a); } - if (options::arraysOptimizeLinear() && !options::arraysModelBased()) { + if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) { bool aNL = d_infoMap.isNonLinear(a); bool bNL = d_infoMap.isNonLinear(b); if (aNL) { @@ -2202,77 +1676,13 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) checkRowLemmas(a,b); checkRowLemmas(b,a); - if (options::arraysModelBased()) { - TNode repA = d_infoMap.getModelRep(a); - Assert(repA.isNull() || d_equalityEngine.areEqual(a, repA)); - TNode repB = d_infoMap.getModelRep(b); - Assert(repB.isNull() || d_equalityEngine.areEqual(a, repB)); - Node rep; - bool done = false; - if (repA.isNull()) { - if (repB.isNull()) { - done = true; - } - else { - rep = repB; - } - } - else { - if (repB.isNull()) { - rep = repA; - } - else { - vector<TNode> assumptions; - rep = expandStores(repA, assumptions, true, a, repB); - if (rep != repA) { - Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl; - d_infoMap.setModelRep(a, rep); - Node reason = mkAnd(assumptions); - d_permRef.push_back(reason); - d_equalityEngine.assertEquality(repA.eqNode(rep), true, reason); - } - d_modelConstraints.push_back(rep.eqNode(repB)); - done = true; - } - } - if (!done) { - // 1. Check for store loop - TNode s = rep; - while (true) { - Assert(s.getKind() == kind::STORE); - while (s.getKind() == kind::STORE) { - s = s[0]; - } - Assert(isLeaf(s)); - TNode tmp = d_equalityEngine.getRepresentative(s); - if (tmp == a) { - d_modelConstraints.push_back(s.eqNode(rep)); - rep = TNode(); - break; - } - tmp = d_infoMap.getModelRep(tmp); - if (tmp.isNull()) { - break; - } - s = tmp; - } - if (!rep.isNull()) { - Node repOrig = rep; - rep = removeRepLoops(a, rep); - if (repOrig != rep) { - d_equalityEngine.assertEquality(repOrig.eqNode(rep), true, d_true); - } - } - if (rep != repA) { - Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl; - d_infoMap.setModelRep(a, rep); - } - } - } - // merge info adds the list of the 2nd argument to the first d_infoMap.mergeInfo(a, b); + if (options::arraysWeakEquivalence()) { + d_arrayMerges.push_back(a.eqNode(b)); + } + // If no more to do, break if (d_conflict || d_mergeQueue.empty()) { break; @@ -2289,7 +1699,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) void TheoryArrays::checkStore(TNode a) { - if (options::arraysModelBased()) return; + if (options::arraysWeakEquivalence()) return; Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n"; if(Trace.isOn("arrays-cri")) { @@ -2319,7 +1729,7 @@ void TheoryArrays::checkStore(TNode a) { void TheoryArrays::checkRowForIndex(TNode i, TNode a) { - if (options::arraysModelBased()) return; + if (options::arraysWeakEquivalence()) return; Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n"; Trace("arrays-cri")<<" index "<<i<<"\n"; @@ -2374,7 +1784,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) // look for new ROW lemmas void TheoryArrays::checkRowLemmas(TNode a, TNode b) { - if (options::arraysModelBased()) return; + if (options::arraysWeakEquivalence()) return; Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n"; if(Trace.isOn("arrays-crl")) d_infoMap.getInfo(a)->print(); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index b2e039912..20f1f57f3 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -257,6 +257,15 @@ class TheoryArrays : public Theory { private: + TNode weakEquivGetRep(TNode node); + TNode weakEquivGetRepIndex(TNode node, TNode index); + void visitAllLeaves(TNode reason, std::vector<TNode>& conjunctions); + void weakEquivBuildCond(TNode node, TNode index, std::vector<TNode>& conjunctions); + void weakEquivMakeRep(TNode node); + void weakEquivMakeRepIndex(TNode node); + void weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason); + void checkWeakEquiv(bool arraysMerged); + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module class NotifyClass : public eq::EqualityEngineNotify { TheoryArrays& d_arrays; @@ -394,6 +403,12 @@ class TheoryArrays : public Theory { typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap; DefValMap d_defValues; + typedef std::hash_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap; + ReadBucketMap d_readBucketTable; + context::Context* d_readTableContext; + context::CDList<Node> d_arrayMerges; + std::vector<CTNodeList*> d_readBucketAllocations; + Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); Node mkAnd(std::vector<TNode>& conjunctions, bool invert = false, unsigned startIndex = 0); void setNonLinear(TNode a); @@ -410,17 +425,6 @@ class TheoryArrays : public Theory { std::vector<Node> d_decisions; bool d_inCheckModel; int d_topLevel; - void convertNodeToAssumptions(TNode node, std::vector<TNode>& assumptions, TNode nodeSkip); - void preRegisterStores(TNode s); - void checkModel(Effort e); - bool hasLoop(TNode node, TNode target); - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; - NodeMap d_getModelValCache; - NodeMap d_lastVal; - Node getModelVal(TNode node); - Node getModelValRec(TNode node); - bool setModelVal(TNode node, TNode val, bool invert, - bool explain, std::vector<TNode>& assumptions); public: diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 6270995ef..4bd9903a8 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -136,14 +136,38 @@ Abc_Aig_t* AigBitblaster::currentAigM() { AigBitblaster::AigBitblaster() : TBitblaster<Abc_Obj_t*>() + , d_satSolver(NULL) , d_aigCache() , d_bbAtoms() , d_aigOutputNode(NULL) { - d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster"); - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - d_satSolver->setNotify(notify); + d_nullContext = new context::Context(); + + switch(options::bvSatSolver()) { + case SAT_SOLVER_MINISAT: { + prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext, + "AigBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + minisat->setNotify(notify); + d_satSolver = minisat; + break; + } + case SAT_SOLVER_CRYPTOMINISAT: + d_satSolver = prop::SatSolverFactory::createCryptoMinisat("AigBitblaster"); + break; + case SAT_SOLVER_RISS: + d_satSolver = prop::SatSolverFactory::createRiss("AigBitblaster"); + break; + case SAT_SOLVER_GLUCOSE: + d_satSolver = prop::SatSolverFactory::createGlucose("AigBitblaster"); + break; + default: + Unreachable("Unknown SAT solver type"); + } + + // d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster"); + // MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + // d_satSolver->setNotify(notify); } AigBitblaster::~AigBitblaster() { diff --git a/src/theory/bv/bitblast_mode.cpp b/src/theory/bv/bitblast_mode.cpp index 51c0290af..86b85f756 100644 --- a/src/theory/bv/bitblast_mode.cpp +++ b/src/theory/bv/bitblast_mode.cpp @@ -51,5 +51,26 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) { return out; } +std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode solver) { + switch(solver) { + case theory::bv::SAT_SOLVER_MINISAT: + out << "SAT_SOLVER_MINISAT"; + break; + case theory::bv::SAT_SOLVER_CRYPTOMINISAT: + out << "SAT_SOLVER_CRYPTOMINISAT"; + break; + case theory::bv::SAT_SOLVER_RISS: + out << "SAT_SOLVER_RISS"; + break; + case theory::bv::SAT_SOLVER_GLUCOSE: + out << "SAT_SOLVER_GLUCOSE"; + break; + default: + out << "SatSolverMode:UNKNOWN![" << unsigned(solver) << "]"; + } + + return out; +} + }/* CVC4 namespace */ diff --git a/src/theory/bv/bitblast_mode.h b/src/theory/bv/bitblast_mode.h index 89ecdc381..b6f4c4e96 100644 --- a/src/theory/bv/bitblast_mode.h +++ b/src/theory/bv/bitblast_mode.h @@ -60,12 +60,21 @@ enum BvSlicerMode { };/* enum BvSlicerMode */ +/** Enumeration of sat solvers that can be used. */ +enum SatSolverMode { + SAT_SOLVER_MINISAT, + SAT_SOLVER_CRYPTOMINISAT, + SAT_SOLVER_RISS, + SAT_SOLVER_GLUCOSE +};/* enum SatSolver */ + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode) CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index d42c4a8c9..6b82da79e 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -246,14 +246,15 @@ public: void safePoint(unsigned ammount) {} }; +class BitblastingRegistrar; class EagerBitblaster : public TBitblaster<Node> { typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; // sat solver used for bitblasting and associated CnfStream - prop::BVSatSolverInterface* d_satSolver; - BitblastingRegistrar* d_bitblastingRegistrar; - context::Context* d_nullContext; - prop::CnfStream* d_cnfStream; + prop::SatSolver* d_satSolver; + BitblastingRegistrar* d_bitblastingRegistrar; + context::Context* d_nullContext; + prop::CnfStream* d_cnfStream; theory::bv::TheoryBV* d_bv; TNodeSet d_bbAtoms; @@ -276,6 +277,7 @@ public: bool assertToSat(TNode node, bool propagate = true); bool solve(); void collectModelInfo(TheoryModel* m, bool fullModel); + friend class BitblastingRegistrar; }; class BitblastingRegistrar: public prop::Registrar { @@ -293,7 +295,7 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> { static Abc_Ntk_t* abcAigNetwork; context::Context* d_nullContext; - prop::BVSatSolverInterface* d_satSolver; + prop::SatSolver* d_satSolver; TNodeAigMap d_aigCache; NodeAigMap d_bbAtoms; diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index eca9f12ab..0327cef71 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -22,15 +22,26 @@ #include "theory/bv/theory_bv.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" - +#include "prop/sat_solver.h" using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; void BitblastingRegistrar::preRegister(Node n) { + // we treat Boolean variables differently + // since the bv solver is responsible for building a model + if (n.isVar() && n.getType().isBoolean()) { + if (d_bitblaster->hasBBTerm(n)) return; + std::vector<Node> bits(1); + bits[0] = n; + d_bitblaster->storeBBTerm(n, bits); + d_bitblaster->d_variables.insert(n); + return; + } + d_bitblaster->bbAtom(n); -}; +} EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) : TBitblaster<Node>() @@ -40,12 +51,29 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) { d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); + switch(options::bvSatSolver()) { + case SAT_SOLVER_MINISAT: { + prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext, + "EagerBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + minisat->setNotify(notify); + d_satSolver = minisat; + break; + } + case SAT_SOLVER_CRYPTOMINISAT: + d_satSolver = prop::SatSolverFactory::createCryptoMinisat("EagerBitblaster"); + break; + case SAT_SOLVER_RISS: + d_satSolver = prop::SatSolverFactory::createRiss("EagerBitblaster"); + break; + case SAT_SOLVER_GLUCOSE: + d_satSolver = prop::SatSolverFactory::createGlucose("EagerBitblaster"); + break; + default: + Unreachable("Unknown SAT solver type"); + } - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster"); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext); - - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - d_satSolver->setNotify(notify); } EagerBitblaster::~EagerBitblaster() { @@ -68,7 +96,12 @@ void EagerBitblaster::bbFormula(TNode node) { void EagerBitblaster::bbAtom(TNode node) { node = node.getKind() == kind::NOT? node[0] : node; if (node.getKind() == kind::BITVECTOR_BITOF) - return; + return; + + if (node.isVar() && node.getType().isBoolean()) { + d_variables.insert(node); + return; + } if (hasBBAtom(node)) { return; } @@ -169,7 +202,7 @@ Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { prop::SatValue bit_value; if (d_cnfStream->hasLiteral(bits[i])) { prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); - bit_value = d_satSolver->value(bit); + bit_value = d_satSolver->value(bit); Assert (bit_value != prop::SAT_VALUE_UNKNOWN); } else { if (!fullModel) return Node(); @@ -179,6 +212,15 @@ Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); value = value * 2 + bit_int; } + + if (a.getType().isBoolean()) { + Assert ( value == Integer(1) || + value == Integer(0)); + + Node res = (value == Integer(1) ? utils::mkTrue() : utils::mkFalse()); + return res; + } + return utils::mkConst(BitVector(bits.size(), value)); } @@ -197,7 +239,14 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= " << var << " " << const_value << "))\n"; - m->assertEquality(var, const_value, true); + // for eager bit-blasting we need to provide models for + // boolean variables too + if (var.getType().isBoolean()) { + m->assertPredicate(var, const_value == utils::mkTrue() ? true : false); + } + else { + m->assertEquality(var, const_value, true); + } } } } diff --git a/src/theory/bv/options b/src/theory/bv/options index eba4608d2..38e7eaed7 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -5,6 +5,18 @@ module BV "theory/bv/options.h" Bitvector theory +# Option to set SAT solver used + +expert-option bvSatSolver bv-sat-solver --bv-sat-solver=MODE CVC4::theory::bv::SatSolverMode :predicate CVC4::theory::bv::satSolverEnabledBuild :handler CVC4::theory::bv::stringToSatSolver :default CVC4::theory::bv::SAT_SOLVER_MINISAT :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h" :link --bv-native-xor + choose which sat solver to use, see --bv-sat-solver=help + +expert-option bvNativeXor --bv-native-xor bool :default false :read-write + use native xor reasoning in the SAT solver (if it supports it) + +expert-option rissCommands --riss-cmd=COMMAND std::string :default "" :read-write :link --bv-sat-solver=riss + simplification commands to pass to the Riss sat solver. + + # Option to set the bit-blasting mode (lazy, eager) option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::theory::bv::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h" diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h index a7a7101d2..e9812d9fc 100644 --- a/src/theory/bv/options_handlers.h +++ b/src/theory/bv/options_handlers.h @@ -46,6 +46,36 @@ inline void abcEnabledBuild(std::string option, std::string value, SmtEngine* sm #endif /* CVC4_USE_ABC */ } +inline void satSolverEnabledBuild(std::string option, + SatSolverMode solver, + SmtEngine* smt) throw(OptionException) { +#ifndef CVC4_USE_CRYPTOMINISAT + if(solver == SAT_SOLVER_CRYPTOMINISAT) { + std::stringstream ss; + ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_CRYPTOMINISAT */ + +#ifndef CVC4_USE_GLUCOSE + if(solver == SAT_SOLVER_GLUCOSE) { + std::stringstream ss; + ss << "option `" << option << "' requires an glucose-enabled build of CVC4; this binary was not built with glucose support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_GLUCOSE */ + +#ifndef CVC4_USE_RISS + if(solver == SAT_SOLVER_RISS) { + std::stringstream ss; + ss << "option `" << option << "' requires an riss-enabled build of CVC4; this binary was not built with riss support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_RISS */ + +} + + static const std::string bitblastingModeHelp = "\ Bit-blasting modes currently supported by the --bitblast option:\n\ \n\ @@ -153,6 +183,102 @@ inline void setBitblastAig(std::string option, bool arg, SmtEngine* smt) throw(O } } +static const std::string bvSatSolverHelp = "\ +Sat solvers currently supported by the --bv-sat-solver option:\n\ +\n\ +minisat (default)\n\ +\n\ +cryptominisat\n\ +\n\ +riss\n\ +\n\ +glucose\n\ +"; + +inline SatSolverMode stringToSatSolver(std::string option, + std::string optarg, + SmtEngine* smt) throw(OptionException) { + if(optarg == "minisat") { + return SAT_SOLVER_MINISAT; + } else if(optarg == "cryptominisat") { + + if (options::incrementalSolving() && + options::incrementalSolving.wasSetByUser()) { + throw OptionException(std::string("Cryptominsat does not support incremental mode. \n\ + Try --bv-sat-solver=minisat")); + } + + if (options::bitblastMode() == BITBLAST_MODE_LAZY && + options::bitblastMode.wasSetByUser()) { + throw OptionException(std::string("Cryptominsat does not support lazy bit-blsating. \n\ + Try --bv-sat-solver=minisat")); + } + if (!options::bitvectorToBool.wasSetByUser()) { + options::bitvectorToBool.set(true); + } + + if (!options::bvAbstraction.wasSetByUser() && + !options::skolemizeArguments.wasSetByUser()) { + options::bvAbstraction.set(true); + options::skolemizeArguments.set(true); + } + return SAT_SOLVER_CRYPTOMINISAT; + } else if(optarg == "riss") { + + if (options::incrementalSolving() && + options::incrementalSolving.wasSetByUser()) { + throw OptionException(std::string("Riss does not support incremental mode. \n\ + Try --bv-sat-solver=minisat")); + } + + if (options::bitblastMode() == BITBLAST_MODE_LAZY && + options::bitblastMode.wasSetByUser()) { + throw OptionException(std::string("Riss does not support lazy bit-blsating. \n\ + Try --bv-sat-solver=minisat")); + } + if (!options::bitvectorToBool.wasSetByUser()) { + options::bitvectorToBool.set(true); + } + + if (!options::bvAbstraction.wasSetByUser() && + !options::skolemizeArguments.wasSetByUser()) { + options::bvAbstraction.set(true); + options::skolemizeArguments.set(true); + } + return SAT_SOLVER_RISS; + }else if(optarg == "glucose") { + + if (options::incrementalSolving() && + options::incrementalSolving.wasSetByUser()) { + throw OptionException(std::string("Glucose does not support incremental mode. \n\ + Try --bv-sat-solver=minisat")); + } + + if (options::bitblastMode() == BITBLAST_MODE_LAZY && + options::bitblastMode.wasSetByUser()) { + throw OptionException(std::string("Glucose does not support lazy bit-blsating. \n\ + Try --bv-sat-solver=minisat")); + } + if (!options::bitvectorToBool.wasSetByUser()) { + options::bitvectorToBool.set(true); + } + + if (!options::bvAbstraction.wasSetByUser() && + !options::skolemizeArguments.wasSetByUser()) { + options::bvAbstraction.set(true); + options::skolemizeArguments.set(true); + } + return SAT_SOLVER_GLUCOSE; + } else if(optarg == "help") { + puts(bvSatSolverHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --bv-sat-solver: `") + + optarg + "'. Try --bv-sat-solver=help."); + } +} + + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 2da0f0467..b62f55a21 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -116,11 +116,12 @@ public: * @param n - a theory lemma valid at decision level 0 * @param removable - whether the lemma can be removed at any point * @param preprocess - whether to apply more aggressive preprocessing + * @param sendAtoms - whether to ensure atoms are sent to the theory * @return the "status" of the lemma, including user level at which * the lemma resides; the lemma will be removed when this user level pops */ virtual LemmaStatus lemma(TNode n, bool removable = false, - bool preprocess = false) + bool preprocess = false, bool sendAtoms = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) = 0; /** diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9b4815fd4..18aad4022 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1379,6 +1379,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The } } + theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) { // For resource-limiting (also does a time check). // spendResource(); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0c1a7c081..ab0c65759 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -303,11 +303,11 @@ class TheoryEngine { return d_engine->propagate(literal, d_theory); } - theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) { + theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false, bool sendAtoms = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST); + return d_engine->lemma(lemma, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST); } theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 6fe92eb6e..57fdc07f9 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -87,7 +87,7 @@ public: push(PROPAGATE_AS_DECISION, n); } - LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException, UnsafeInterruptException) { + LemmaStatus lemma(TNode n, bool removable, bool preprocess, bool sendAtoms) throw(AssertionException, UnsafeInterruptException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 5bd607d94..992826c2f 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -133,6 +133,18 @@ bool Configuration::isBuiltWithAbc() { return IS_ABC_BUILD; } +bool Configuration::isBuiltWithCryptominisat() { + return IS_CRYPTOMINISAT_BUILD; +} + +bool Configuration::isBuiltWithGlucose() { + return IS_GLUCOSE_BUILD; +} + +bool Configuration::isBuiltWithRiss() { + return IS_RISS_BUILD; +} + bool Configuration::isBuiltWithReadline() { return IS_READLINE_BUILD; } diff --git a/src/util/configuration.h b/src/util/configuration.h index c6562b3e6..0809d2644 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -93,6 +93,12 @@ public: static bool isBuiltWithAbc(); + static bool isBuiltWithCryptominisat(); + + static bool isBuiltWithGlucose(); + + static bool isBuiltWithRiss(); + static bool isBuiltWithReadline(); static bool isBuiltWithCudd(); diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 631a323d3..efa46cc0c 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -113,6 +113,24 @@ namespace CVC4 { # define IS_ABC_BUILD false #endif /* CVC4_USE_ABC */ +#if CVC4_USE_CRYPTOMINISAT +# define IS_CRYPTOMINISAT_BUILD true +#else /* CVC4_USE_CRYPTOMINISAT */ +# define IS_CRYPTOMINISAT_BUILD false +#endif /* CVC4_USE_CRYPTOMINISAT */ + +#if CVC4_USE_GLUCOSE +# define IS_GLUCOSE_BUILD true +#else /* CVC4_USE_GLUCOSE */ +# define IS_GLUCOSE_BUILD false +#endif /* CVC4_USE_GLUCOSE */ + +#if CVC4_USE_RISS +# define IS_RISS_BUILD true +#else /* CVC4_USE_RISS */ +# define IS_RISS_BUILD false +#endif /* CVC4_USE_RISS */ + #ifdef HAVE_LIBREADLINE # define IS_READLINE_BUILD true #else /* HAVE_LIBREADLINE */ |