From: Liana Hadarean Date: Fri, 28 Oct 2011 19:24:38 +0000 (+0000) Subject: merged the proofgen3 branch into trunk: X-Git-Tag: cvc5-1.0.0~8406 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b084a7efa9d65ec2f7475caa8486f8fd4cbafbd5;p=cvc5.git merged the proofgen3 branch into trunk: - can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof. --- diff --git a/config/build-type b/config/build-type index 91a88faa6..2f1b27cc2 100755 --- a/config/build-type +++ b/config/build-type @@ -22,6 +22,7 @@ # # staticbinary # optimized +# proof # debugsymbols # assertions # tracing @@ -52,7 +53,7 @@ while [ $# -gt 0 ]; do done build_type_suffix= -for arg in cln staticbinary optimized debugsymbols statistics replay assertions tracing muzzle coverage profiling; do +for arg in cln staticbinary optimized proof debugsymbols statistics replay assertions tracing muzzle coverage profiling; do if eval [ -n '"${'$arg'+set}"' ]; then if eval [ '"${'$arg'}"' -eq 0 ]; then build_type_suffix=$build_type_suffix-no$arg diff --git a/config/cvc4.m4 b/config/cvc4.m4 index b003884ed..58ab990b3 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -24,7 +24,7 @@ do ac_cvc4_build_profile_set=yes as_me=configure AC_MSG_NOTICE([CVC4: building profile $ac_option_build]) - for x in optimized statistics replay assertions tracing dumping muzzle coverage profiling; do + for x in optimized proof statistics replay assertions tracing dumping muzzle coverage profiling; do if expr "$ac_option" : '.*-no'$x'$' >/dev/null || expr "$ac_option" : '.*-no'$x'-' >/dev/null; then eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-$x\""' fi diff --git a/configure.ac b/configure.ac index cabb50706..922f65416 100644 --- a/configure.ac +++ b/configure.ac @@ -145,6 +145,13 @@ if test -n "${enable_assertions+set}"; then btargs="$btargs noassertions" fi fi +if test -n "${enable_proof+set}"; then + if test "$enable_proof" = yes; then + btargs="$btargs proof" + else + btargs="$btargs noproof" + fi +fi if test -n "${enable_tracing+set}"; then if test "$enable_tracing" = yes; then btargs="$btargs tracing" @@ -374,6 +381,7 @@ case "$with_build" in if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi if test -z "${enable_replay+set}" ; then enable_replay=no ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi + if test -z "${enable_proof+set}" ; then enable_proof=no ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi @@ -389,6 +397,7 @@ case "$with_build" in if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi + if test -z "${enable_proof+set}" ; then enable_proof=no ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi @@ -405,6 +414,7 @@ case "$with_build" in if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi + if test -z "${enable_proof+set}" ; then enable_proof=no ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi @@ -421,6 +431,7 @@ case "$with_build" in if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi if test -z "${enable_replay+set}" ; then enable_replay=no ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi + if test -z "${enable_proof+set}" ; then enable_proof=no ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi @@ -453,6 +464,21 @@ if test "$enable_static_binary" = yes -a "$enable_static" != yes; then AC_MSG_WARN([forcing static-library building, --enable-static-binary given]) fi +AC_MSG_CHECKING([whether to support proof in libcvc4]) + +AC_ARG_ENABLE([proof], + [AS_HELP_STRING([--enable-proof], + [support proof generation])]) +if test -z "${enable_proof+set}"; then + enable_proof=no +fi +AC_MSG_RESULT([$enable_proof]) + +if test "$enable_proof" = yes; then + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF" +fi + + AC_MSG_CHECKING([whether to optimize libcvc4]) AC_ARG_ENABLE([optimized], @@ -1026,6 +1052,7 @@ Build profile: $with_build Build ID : $build_type Optimized : $optimized Debug symbols: $enable_debug_symbols +Proof : $enable_proof Statistics : $enable_statistics Replay : $enable_replay Assertions : $enable_assertions diff --git a/src/Makefile.am b/src/Makefile.am index 63fcf590d..906a64a65 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -17,7 +17,7 @@ AM_CPPFLAGS = \ -I@srcdir@/include -I@srcdir@ -I@builddir@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = lib expr util context theory prop smt printer . parser compat bindings main +SUBDIRS = lib expr util context theory prop smt printer proof . parser compat bindings main lib_LTLIBRARIES = libcvc4.la if HAVE_CXXTESTGEN @@ -36,6 +36,7 @@ libcvc4_la_LIBADD = \ @builddir@/util/libutil.la \ @builddir@/expr/libexpr.la \ @builddir@/context/libcontext.la \ + @builddir@/proof/libproof.la \ @builddir@/prop/libprop.la \ @builddir@/prop/minisat/libminisat.la \ @builddir@/printer/libprinter.la \ @@ -46,6 +47,7 @@ libcvc4_noinst_la_LIBADD = \ @builddir@/util/libutil.la \ @builddir@/expr/libexpr.la \ @builddir@/context/libcontext.la \ + @builddir@/proof/libproof.la \ @builddir@/prop/libprop.la \ @builddir@/prop/minisat/libminisat.la \ @builddir@/printer/libprinter.la \ diff --git a/src/main/usage.h b/src/main/usage.h index c11a2b73e..f0c7c7f08 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -54,7 +54,8 @@ CVC4 options:\n\ --no-interactive do not run interactively\n\ --produce-models support the get-value command\n\ --produce-assignments support the get-assignment command\n\ - --lazy-definition-expansion expand define-fun lazily\n"; + --lazy-definition-expansion expand define-fun lazily\n + --proof\n"; }/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/proof/Makefile b/src/proof/Makefile new file mode 100644 index 000000000..b0985ba84 --- /dev/null +++ b/src/proof/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = src/proof + +include $(topdir)/Makefile.subdir diff --git a/src/proof/Makefile.am b/src/proof/Makefile.am new file mode 100644 index 000000000..d657dfa80 --- /dev/null +++ b/src/proof/Makefile.am @@ -0,0 +1,18 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -D __STDC_LIMIT_MACROS \ + -D __STDC_FORMAT_MACROS \ + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -I@srcdir@/../prop/minisat +AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libproof.la + +libproof_la_SOURCES = \ + proof.h \ + sat_proof.h \ + sat_proof.cpp \ + cnf_proof.h \ + cnf_proof.cpp \ + proof_manager.h \ + proof_manager.cpp + diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp new file mode 100644 index 000000000..2bf146661 --- /dev/null +++ b/src/proof/cnf_proof.cpp @@ -0,0 +1,9 @@ +#include "cnf_proof.h" +using namespace CVC4::prop; + +namespace CVC4 { +CnfProof::CnfProof(CnfStream* stream) : + d_cnfStream(stream) {} + + +} /* CVC4 namespace */ diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h new file mode 100644 index 000000000..c43c9fc62 --- /dev/null +++ b/src/proof/cnf_proof.h @@ -0,0 +1,35 @@ +/********************* */ +/*! \file cnf_proof.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 A manager for CnfProofs. + ** + ** A manager for CnfProofs. + ** + ** + **/ + +#ifndef __CVC4__CNF_PROOF_H +#define __CVC4__CNF_PROOF_H + +#include +namespace CVC4 { +namespace prop { +class CnfStream; +} +class CnfProof { + CVC4::prop::CnfStream* d_cnfStream; +public: + CnfProof(CVC4::prop::CnfStream* cnfStream); +}; + +} /* CVC4 namespace*/ +#endif /* __CVC4__CNF_PROOF_H */ diff --git a/src/proof/proof.h b/src/proof/proof.h new file mode 100644 index 000000000..f163a4ffd --- /dev/null +++ b/src/proof/proof.h @@ -0,0 +1,37 @@ +/********************* */ +/*! \file sat_proof.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 Proof manager + ** + ** Proof manager + **/ + +#ifndef __CVC4__PROOF_H +#define __CVC4__PROOF_H + +#include "util/options.h" +//#define CVC4_PROOFS + +#ifdef CVC4_PROOF +# define PROOF(x) if(Options::current()->proof) { x; } +# define NULLPROOF(x) (Options::current()->proof)? x : NULL +# define PROOF_ON() Options::current()->proof +#else /* CVC4_PROOF */ +# define PROOF(x) +# define NULLPROOF(x) NULL +# define PROOF_ON() false +#endif /* CVC4_PROOF */ + + + +#endif /* __CVC4__PROOF_H */ diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp new file mode 100644 index 000000000..d6dd7b73d --- /dev/null +++ b/src/proof/proof_manager.cpp @@ -0,0 +1,70 @@ +#include "proof/proof_manager.h" +#include "proof/sat_proof.h" +#include "proof/cnf_proof.h" +#include "util/Assert.h" + +namespace CVC4 { + +bool ProofManager::isInitialized = false; +ProofManager* ProofManager::proofManager = NULL; + +ProofManager::ProofManager(ProofFormat format = LFSC): + d_satProof(NULL), + d_cnfProof(NULL), + d_format(format) +{} + +ProofManager* ProofManager::currentPM() { + if (isInitialized) { + return proofManager; + } else { + proofManager = new ProofManager(); + isInitialized = true; + return proofManager; + } +} + +SatProof* ProofManager::getSatProof() { + Assert (currentPM()->d_satProof); + return currentPM()->d_satProof; +} + +CnfProof* ProofManager::getCnfProof() { + Assert (currentPM()->d_cnfProof); + return currentPM()->d_cnfProof; +} + +void ProofManager::initSatProof(Minisat::Solver* solver) { + Assert (currentPM()->d_satProof == NULL); + switch(currentPM()->d_format) { + case LFSC : + currentPM()->d_satProof = new LFSCSatProof(solver); + break; + case NATIVE : + currentPM()->d_satProof = new SatProof(solver); + break; + default: + Assert(false); + } + +} + +void ProofManager::initCnfProof(prop::CnfStream* cnfStream) { + Assert (currentPM()->d_cnfProof == NULL); + + switch(currentPM()->d_format) { + case LFSC : + currentPM()->d_cnfProof = new CnfProof(cnfStream); // FIXME + break; + case NATIVE : + currentPM()->d_cnfProof = new CnfProof(cnfStream); + break; + default: + Assert(false); + } + +} + + + +} /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h new file mode 100644 index 000000000..5d8b9d271 --- /dev/null +++ b/src/proof/proof_manager.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \file proof_manager.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 A manager for Proofs. + ** + ** A manager for Proofs. + ** + ** + **/ + +#ifndef __CVC4__PROOF_MANAGER_H +#define __CVC4__PROOF_MANAGER_H + +#include +#include "proof.h" + +// forward declarations +namespace Minisat { +class Solver; +} + +namespace CVC4 { +namespace prop { +class CnfStream; +} +class SatProof; +class CnfProof; + +// different proof modes +enum ProofFormat { + LFSC, + NATIVE +}; + +class ProofManager { + SatProof* d_satProof; + CnfProof* d_cnfProof; + ProofFormat d_format; + + static ProofManager* proofManager; + static bool isInitialized; + ProofManager(ProofFormat format); +public: + static ProofManager* currentPM(); + + static void initSatProof(Minisat::Solver* solver); + static void initCnfProof(CVC4::prop::CnfStream* cnfStream); + + static SatProof* getSatProof(); + static CnfProof* getCnfProof(); + +}; + +} /* CVC4 namespace*/ +#endif /* __CVC4__PROOF_MANAGER_H */ diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp new file mode 100644 index 000000000..095251da8 --- /dev/null +++ b/src/proof/sat_proof.cpp @@ -0,0 +1,711 @@ +#include "proof/sat_proof.h" +#include "prop/minisat/core/Solver.h" + +using namespace std; +using namespace Minisat; + +namespace CVC4 { + +/// some helper functions + +void printLit (Minisat::Lit l) { + Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1; +} + +void printClause (Minisat::Clause& c) { + for (int i = 0; i < c.size(); i++) { + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + } +} + +void printLitSet(const LitSet& s) { + for(LitSet::iterator it = s.begin(); it != s.end(); ++it) { + printLit(*it); + Debug("proof:sat") << " "; + } + Debug("proof:sat") << endl; +} + +// purely debugging functions +void printDebug (Minisat::Lit l) { + Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << endl; +} + +void printDebug (Minisat::Clause& c) { + for (int i = 0; i < c.size(); i++) { + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + } + Debug("proof:sat") << endl; +} + + +int SatProof::d_idCounter = 0; + +/** + * Converts the clause associated to id to a set of literals + * + * @param id the clause id + * @param set the clause converted to a set of literals + */ +void SatProof::createLitSet(ClauseId id, LitSet& set) { + Assert (set.empty()); + if(isUnit(id)) { + set.insert(getUnit(id)); + return; + } + if ( id == d_emptyClauseId) { + return; + } + CRef ref = getClauseRef(id); + Assert (ref != CRef_Undef); + Clause& c = d_solver->ca[ref]; + for (int i = 0; i < c.size(); i++) { + set.insert(c[i]); + } +} + + +/** + * Resolves clause1 and clause2 on variable var and stores the + * result in clause1 + * @param var + * @param clause1 + * @param clause2 + */ +bool resolve(const Lit v, LitSet& clause1, LitSet& clause2, bool s) { + Assert(!clause1.empty()); + Assert(!clause2.empty()); + Lit var = sign(v) ? ~v : v; + if (s) { + // literal appears positive in the first clause + if( !clause2.count(~var)) { + Debug("proof:sat") << "proof:resolve: Missing literal "; + printLit(var); + Debug("proof:sat") << endl; + return false; + } + clause1.erase(var); + clause2.erase(~var); + for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) { + clause1.insert(*it); + } + } else { + // literal appears negative in the first clause + if( !clause1.count(~var) || !clause2.count(var)) { + Debug("proof:sat") << "proof:resolve: Mising literal "; + printLit(var); + Debug("proof:sat") << endl; + return false; + } + clause1.erase(~var); + clause2.erase(var); + for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) { + clause1.insert(*it); + } + } + return true; +} + +/// ResChain + +ResChain::ResChain(ClauseId start) : + d_start(start), + d_steps(), + d_redundantLits(NULL) + {} + +void ResChain::addStep(Lit lit, ClauseId id, bool sign) { + ResStep step(lit, id, sign); + d_steps.push_back(step); +} + + +void ResChain::addRedundantLit(Lit lit) { + if (d_redundantLits) { + d_redundantLits->insert(lit); + } else { + d_redundantLits = new LitSet(); + d_redundantLits->insert(lit); + } +} + + +/// ProxyProof + +ProofProxy::ProofProxy(SatProof* proof): + d_proof(proof) +{} + +void ProofProxy::updateCRef(CRef oldref, CRef newref) { + d_proof->updateCRef(oldref, newref); +} + + +/// SatProof + +SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : + d_solver(solver), + d_idClause(), + d_clauseId(), + d_idUnit(), + d_deleted(), + d_inputClauses(), + d_resChains(), + d_resStack(), + d_checkRes(checkRes), + d_emptyClauseId(-1), + d_nullId(-2), + d_temp_clauseId(), + d_temp_idClause() + { + d_proxy = new ProofProxy(this); + } + + +/** + * Returns true if the resolution chain corresponding to id + * does resolve to the clause associated to id + * @param id + * + * @return + */ +bool SatProof::checkResolution(ClauseId id) { + if(d_checkRes) { + bool validRes = true; + Assert (d_resChains.find(id) != d_resChains.end()); + ResChain* res = d_resChains[id]; + LitSet clause1; + createLitSet(res->getStart(), clause1); + ResSteps& steps = res->getSteps(); + for (unsigned i = 0; i < steps.size(); i++) { + Lit var = steps[i].lit; + LitSet clause2; + createLitSet (steps[i].id, clause2); + bool res = resolve (var, clause1, clause2, steps[i].sign); + if(res == false) { + validRes = false; + break; + } + } + // compare clause we claimed to prove with the resolution result + if (isUnit(id)) { + // special case if it was a unit clause + Lit unit = getUnit(id); + validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); + return validRes; + } + if (id == d_emptyClauseId) { + return clause1.empty(); + } + CRef ref = getClauseRef(id); + Assert (ref != CRef_Undef); + Clause& c = d_solver->ca[ref]; + for (int i = 0; i < c.size(); ++i) { + int count = clause1.erase(c[i]); + if (count == 0) { + Debug("proof:sat") << "proof:checkResolution::literal not in computed result "; + printLit(c[i]); + Debug("proof:sat") << "\n"; + validRes = false; + } + } + validRes = clause1.empty(); + if (! validRes) { + Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n"; + printLitSet(clause1); + Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; + printClause(c); + } + return validRes; + + } else { + return true; + } +} + + + + +/// helper methods + +ClauseId SatProof::getClauseId(CRef ref) { + if(d_clauseId.find(ref) == d_clauseId.end()) { + Debug("proof:sat") << "Missing clause \n"; + } + Assert(d_clauseId.find(ref) != d_clauseId.end()); + return d_clauseId[ref]; +} + + +ClauseId SatProof::getClauseId(Lit lit) { + Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); + return d_unitId[toInt(lit)]; +} + +CRef SatProof::getClauseRef(ClauseId id) { + if (d_idClause.find(id) == d_idClause.end()) { + Debug("proof:sat") << "proof:getClauseRef cannot find clause "<ca[id]; +} +Lit SatProof::getUnit(ClauseId id) { + Assert (d_idUnit.find(id) != d_idUnit.end()); + return d_idUnit[id]; +} + +bool SatProof::isUnit(ClauseId id) { + return d_idUnit.find(id) != d_idUnit.end(); +} + +bool SatProof::isUnit(Lit lit) { + return d_unitId.find(toInt(lit)) != d_unitId.end(); +} + +ClauseId SatProof::getUnitId(Lit lit) { + Assert(isUnit(lit)); + return d_unitId[toInt(lit)]; +} + +bool SatProof::hasResolution(ClauseId id) { + return d_resChains.find(id) != d_resChains.end(); +} + +bool SatProof::isInputClause(ClauseId id) { + return (d_inputClauses.find(id) != d_inputClauses.end()); +} + + +void SatProof::print(ClauseId id) { + if (d_deleted.find(id) != d_deleted.end()) { + Debug("proof:sat") << "del"<ca[ref]); + } +} + +void SatProof::printRes(ClauseId id) { + Assert(hasResolution(id)); + Debug("proof:sat") << "id "<< id <<": "; + printRes(d_resChains[id]); +} + +void SatProof::printRes(ResChain* res) { + ClauseId start_id = res->getStart(); + + Debug("proof:sat") << "("; + print(start_id); + + ResSteps& steps = res->getSteps(); + for(unsigned i = 0; i < steps.size(); i++ ) { + Lit v = steps[i].lit; + ClauseId id = steps[i].id; + + Debug("proof:sat") << "["; + printLit(v); + Debug("proof:sat") << "] "; + print(id); + } + Debug("proof:sat") << ") \n"; +} + +/// registration methods + +ClauseId SatProof::registerClause(CRef clause, bool isInput) { + Assert(clause != CRef_Undef); + ClauseIdMap::iterator it = d_clauseId.find(clause); + if (it == d_clauseId.end()) { + ClauseId newId = d_idCounter++; + d_clauseId[clause]= newId; + d_idClause[newId] =clause; + if (isInput) { + Assert (d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); + } + } + return d_clauseId[clause]; +} + +ClauseId SatProof::registerUnitClause(Lit lit, bool isInput) { + UnitIdMap::iterator it = d_unitId.find(toInt(lit)); + if (it == d_unitId.end()) { + ClauseId newId = d_idCounter++; + d_unitId[toInt(lit)] = newId; + d_idUnit[newId] = lit; + if (isInput) { + Assert (d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); + } + } + return d_unitId[toInt(lit)]; +} + +void SatProof::removedDfs(Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen){ + // if we already added the literal return + if (seen.count(lit)) { + return; + } + + CRef reason_ref = d_solver->reason(var(lit)); + if (reason_ref == CRef_Undef) { + seen.insert(lit); + removeStack.push_back(lit); + return; + } + + Assert (reason_ref != CRef_Undef); + int size = d_solver->ca[reason_ref].size(); + for (int i = 1; i < size; i++ ) { + Lit v = d_solver->ca[reason_ref][i]; + if(inClause.count(v) == 0 && seen.count(v) == 0) { + removedDfs(v, removedSet, removeStack, inClause, seen); + } + } + if(seen.count(lit) == 0) { + seen.insert(lit); + removeStack.push_back(lit); + } +} + + +void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) { + LitSet* removed = res->getRedundant(); + if (removed == NULL) { + return; + } + + LitSet inClause; + createLitSet(id, inClause); + + LitVector removeStack; + LitSet seen; + for (LitSet::iterator it = removed->begin(); it != removed->end(); ++it) { + removedDfs(*it, removed, removeStack, inClause, seen); + } + + for (int i = removeStack.size()-1; i >= 0; --i) { + Lit lit = removeStack[i]; + CRef reason_ref = d_solver->reason(var(lit)); + ClauseId reason_id; + + if (reason_ref == CRef_Undef) { + Assert(isUnit(~lit)); + reason_id = getUnitId(~lit); + } else { + reason_id = registerClause(reason_ref); + } + res->addStep(lit, reason_id, !sign(lit)); + } + removed->clear(); +} + +void SatProof::registerResolution(ClauseId id, ResChain* res) { + Assert(res != NULL); + + removeRedundantFromRes(res, id); + Assert(res->redundantRemoved()); + + d_resChains[id] = res; + printRes(id); + if (d_checkRes) { + Assert(checkResolution(id)); + } +} + + +/// recording resolutions + +void SatProof::startResChain(CRef start) { + ClauseId id = getClauseId(start); + ResChain* res = new ResChain(id); + d_resStack.push_back(res); +} + +void SatProof::addResolutionStep(Lit lit, CRef clause, bool sign) { + ClauseId id = registerClause(clause); + ResChain* res = d_resStack.back(); + res->addStep(lit, id, sign); +} + +void SatProof::endResChain(CRef clause) { + Assert(d_resStack.size() > 0); + ClauseId id = registerClause(clause); + ResChain* res = d_resStack.back(); + registerResolution(id, res); + d_resStack.pop_back(); +} + + +void SatProof::endResChain(Lit lit) { + Assert(d_resStack.size() > 0); + ClauseId id = registerUnitClause(lit); + ResChain* res = d_resStack.back(); + + + registerResolution(id, res); + d_resStack.pop_back(); +} + +void SatProof::storeLitRedundant(Lit lit) { + Assert(d_resStack.size() > 0); + ResChain* res = d_resStack.back(); + res->addRedundantLit(lit); +} + +/// constructing resolutions + +void SatProof::resolveOutUnit(Lit lit) { + ClauseId id = resolveUnit(~lit); + ResChain* res = d_resStack.back(); + res->addStep(lit, id, !sign(lit)); +} + +void SatProof::storeUnitResolution(Lit lit) { + resolveUnit(lit); +} + +ClauseId SatProof::resolveUnit(Lit lit) { + // first check if we already have a resolution for lit + if(isUnit(lit)) { + ClauseId id = getClauseId(lit); + if(hasResolution(id) || isInputClause(id)) { + return id; + } + Assert (false); + } + CRef reason_ref = d_solver->reason(var(lit)); + Assert (reason_ref != CRef_Undef); + + ClauseId reason_id = registerClause(reason_ref); + + ResChain* res = new ResChain(reason_id); + Clause& reason = d_solver->ca[reason_ref]; + for (int i = 0; i < reason.size(); i++) { + Lit l = reason[i]; + if(lit != l) { + ClauseId res_id = resolveUnit(~l); + res->addStep(l, res_id, !sign(l)); + } + } + ClauseId unit_id = registerUnitClause(lit); + registerResolution(unit_id, res); + return unit_id; +} + +void SatProof::printProof() { + Debug("proof:sat") << "SatProof::printProof\n"; +} + +void SatProof::finalizeProof(CRef conflict_ref) { + Assert(d_resStack.size() == 0); + //ClauseId conflict_id = getClauseId(conflict_ref); + ClauseId conflict_id = registerClause(conflict_ref); //FIXME + Debug("proof:sat") << "proof::finalizeProof Final Conflict "; + print(conflict_id); + + ResChain* res = new ResChain(conflict_id); + Clause& conflict = d_solver->ca[conflict_ref] ; + for (int i = 0; i < conflict.size(); ++i) { + Lit lit = conflict[i]; + ClauseId res_id = resolveUnit(~lit); + res->addStep(lit, res_id, !sign(lit)); + } + registerResolution(d_emptyClauseId, res); + printProof(); +} + +/// CRef manager + +void SatProof::updateCRef(CRef oldref, CRef newref) { + if (d_clauseId.find(oldref) == d_clauseId.end()) { + return; + } + ClauseId id = getClauseId(oldref); + Assert (d_temp_clauseId.find(newref) == d_temp_clauseId.end()); + Assert (d_temp_idClause.find(id) == d_temp_idClause.end()); + d_temp_clauseId[newref] = id; + d_temp_idClause[id] = newref; +} + +void SatProof::finishUpdateCRef() { + d_clauseId.swap(d_temp_clauseId); + d_temp_clauseId.clear(); + + d_idClause.swap(d_temp_idClause); + d_temp_idClause.clear(); +} + +void SatProof::markDeleted(CRef clause) { + if (d_clauseId.find(clause) != d_clauseId.end()) { + ClauseId id = getClauseId(clause); + Assert (d_deleted.find(id) == d_deleted.end()); + d_deleted.insert(id); + } +} + +/// LFSCSatProof class + +string LFSCSatProof::varName(Lit lit) { + ostringstream os; + if (sign(lit)) { + os << "(neg v"<getStart(); + collectLemmas(start); + + ResSteps steps = res->getSteps(); + for(unsigned i = 0; i < steps.size(); i++) { + collectLemmas(steps[i].id); + } +} + + + +void LFSCSatProof::printResolution(ClauseId id) { + d_lemmaSS << "(satlem _ _ _ "; + + ResChain* res = d_resChains[id]; + ResSteps& steps = res->getSteps(); + + for (int i = steps.size()-1; i >= 0; i--) { + d_lemmaSS << "("; + d_lemmaSS << (steps[i].sign? "R" : "Q") << " _ _ "; + + } + + ClauseId start_id = res->getStart(); + if(isInputClause(start_id)) { + d_seenInput.insert(start_id); + } + d_lemmaSS << clauseName(start_id) << " "; + + for(unsigned i = 0; i < steps.size(); i++) { + d_lemmaSS << clauseName(steps[i].id) << " v" << var(steps[i].lit) <<")"; + } + + if (id == d_emptyClauseId) { + d_lemmaSS <<"(\\empty empty)"; + return; + } + + d_lemmaSS << "(\\" << clauseName(id) << "\n"; // bind to lemma name + d_paren << "))"; // closing parethesis for lemma binding and satlem +} + + +void LFSCSatProof::printInputClause(ClauseId id){ + ostringstream os; + CRef ref = getClauseRef(id); + Assert (ref != CRef_Undef); + Clause& c = getClause(ref); + + d_clauseSS << "(% " << clauseName(id) << " (holds "; + os << ")"; // closing paren for holds + d_paren << ")"; // closing paren for (% + + for(int i = 0; i < c.size(); i++) { + d_clauseSS << " (clc " << varName(c[i]) <<" "; + os <<")"; + d_seenVars.insert(var(c[i])); + } + d_clauseSS << "cln"; + d_clauseSS << os.str() << "\n"; +} + + +void LFSCSatProof::printClauses() { + for (IdHashSet::iterator it = d_seenInput.begin(); it!= d_seenInput.end(); ++it) { + printInputClause(*it); + } +} + +void LFSCSatProof::printVariables() { + for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) { + d_varSS << "(% v" << *it <<" var \n"; + d_paren << ")"; + } +} + + +void LFSCSatProof::flush() { + ostringstream out; + out << "(check \n"; + d_paren <<")"; + out << d_varSS.str(); + out << d_clauseSS.str(); + out << "(: (holds cln) \n"; + out << d_lemmaSS.str(); + d_paren << "))"; + out << d_paren.str(); + out << ";"; //to comment out the solver's answer + std::cout << out.str(); +} + +void LFSCSatProof::printProof() { + Debug("proof:sat") << " LFSCSatProof::printProof \n"; + + // first collect lemmas to print in reverse order + collectLemmas(d_emptyClauseId); + for(IdSet::iterator it = d_seenLemmas.begin(); it!= d_seenLemmas.end(); ++it) { + if(*it != d_emptyClauseId) { + printResolution(*it); + } + } + // last resolution to be printed is the empty clause + printResolution(d_emptyClauseId); + + printClauses(); + printVariables(); + flush(); + +} + +} /* CVC4 namespace */ + diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h new file mode 100644 index 000000000..4f9ba8e4a --- /dev/null +++ b/src/proof/sat_proof.h @@ -0,0 +1,256 @@ +/********************* */ +/*! \file sat_proof.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 Resolution proof + ** + ** Resolution proof + **/ + +#ifndef __CVC4__SAT__PROOF_H +#define __CVC4__SAT__PROOF_H + +#include +#include +#include +#include +#include +#include +#include +namespace Minisat { +class Solver; +typedef uint32_t CRef; +} + +#include "prop/minisat/core/SolverTypes.h" + +namespace std { +using namespace __gnu_cxx; +} + +namespace CVC4 { +/** + * Helper debugging functions + * + */ +void printDebug(::Minisat::Lit l); +void printDebug(::Minisat::Clause& c); + +typedef int ClauseId; +struct ResStep { + ::Minisat::Lit lit; + ClauseId id; + bool sign; + ResStep(::Minisat::Lit l, ClauseId i, bool s) : + lit(l), + id(i), + sign(s) + {} +}; + +typedef std::vector< ResStep > ResSteps; +typedef std::set < ::Minisat::Lit> LitSet; + +class ResChain { +private: + ClauseId d_start; + ResSteps d_steps; + LitSet* d_redundantLits; +public: + ResChain(ClauseId start); + void addStep(::Minisat::Lit, ClauseId, bool); + bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); } + void addRedundantLit(::Minisat::Lit lit); + ~ResChain(); + // accessor methods + ClauseId getStart() { return d_start; } + ResSteps& getSteps() { return d_steps; } + LitSet* getRedundant() { return d_redundantLits; } +}; + + +typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap; +typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap; +typedef std::hash_map < ClauseId, ::Minisat::Lit> IdUnitMap; +typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME +typedef std::hash_map < ClauseId, ResChain*> IdResMap; +typedef std::hash_set < ClauseId > IdHashSet; +typedef std::vector < ResChain* > ResStack; + +typedef std::hash_set < int > VarSet; +typedef std::set < ClauseId > IdSet; +typedef std::vector < ::Minisat::Lit > LitVector; +class SatProof; + +class ProofProxy : public ProofProxyAbstract { +private: + SatProof* d_proof; +public: + ProofProxy(SatProof* pf); + void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref); +}; + +class SatProof { +protected: + ::Minisat::Solver* d_solver; + // clauses + IdClauseMap d_idClause; + ClauseIdMap d_clauseId; + IdUnitMap d_idUnit; + UnitIdMap d_unitId; + IdHashSet d_deleted; + IdHashSet d_inputClauses; + + // resolutions + IdResMap d_resChains; + ResStack d_resStack; + bool d_checkRes; + + static ClauseId d_idCounter; + const ClauseId d_emptyClauseId; + const ClauseId d_nullId; + // proxy class to break circular dependencies + ProofProxy* d_proxy; + + // temporary map for updating CRefs + ClauseIdMap d_temp_clauseId; + IdClauseMap d_temp_idClause; +public: + SatProof(::Minisat::Solver* solver, bool checkRes = false); +protected: + void print(ClauseId id); + void printRes(ClauseId id); + void printRes(ResChain* res); + + bool isInputClause(ClauseId id); + bool isUnit(ClauseId id); + bool isUnit(::Minisat::Lit lit); + bool hasResolution(ClauseId id); + void createLitSet(ClauseId id, LitSet& set); + void registerResolution(ClauseId id, ResChain* res); + + ClauseId getClauseId(::Minisat::CRef clause); + ClauseId getClauseId(::Minisat::Lit lit); + ::Minisat::CRef getClauseRef(ClauseId id); + ::Minisat::Lit getUnit(ClauseId id); + ClauseId getUnitId(::Minisat::Lit lit); + ::Minisat::Clause& getClause(ClauseId id); + virtual void printProof(); + + bool checkResolution(ClauseId id); + /** + * Constructs a resolution tree that proves lit + * and returns the ClauseId for the unit clause lit + * @param lit the literal we are proving + * + * @return + */ + ClauseId resolveUnit(::Minisat::Lit lit); + /** + * Does a depth first search on removed literals and adds the literals + * to be removed in the proper order to the stack. + * + * @param lit the literal we are recusing on + * @param removedSet the previously computed set of redundantant literals + * @param removeStack the stack of literals in reverse order of resolution + */ + void removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen); + void removeRedundantFromRes(ResChain* res, ClauseId id); +public: + void startResChain(::Minisat::CRef start); + void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign); + /** + * Pops the current resolution of the stack and stores it + * in the resolution map. Also registers the @param clause. + * @param clause the clause the resolution is proving + */ + void endResChain(::Minisat::CRef clause); + void endResChain(::Minisat::Lit lit); + /** + * Stores in the current derivation the redundant literals that were + * eliminated from the conflict clause during conflict clause minimization. + * @param lit the eliminated literal + */ + void storeLitRedundant(::Minisat::Lit lit); + + /// update the CRef Id maps when Minisat does memory reallocation x + void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref); + void finishUpdateCRef(); + + /** + * Constructs the empty clause resolution from the final conflict + * + * @param conflict + */void finalizeProof(::Minisat::CRef conflict); + + /// clause registration methods + ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false); + ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false); + /** + * Marks the deleted clauses as deleted. Note we may still use them in the final + * resolution. + * @param clause + */ + void markDeleted(::Minisat::CRef clause); + /** + * Constructs the resolution of ~q and resolves it with the current + * resolution thus eliminating q from the current clause + * @param q the literal to be resolved out + */ + void resolveOutUnit(::Minisat::Lit q); + /** + * Constructs the resolution of the literal lit. Called when a clause + * containing lit becomes satisfied and is removed. + * @param lit + */ + void storeUnitResolution(::Minisat::Lit lit); + + ProofProxy* getProxy() {return d_proxy; } +}; + +class LFSCSatProof: public SatProof { +private: + VarSet d_seenVars; + std::ostringstream d_varSS; + std::ostringstream d_lemmaSS; + std::ostringstream d_clauseSS; + std::ostringstream d_paren; + IdSet d_seenLemmas; + IdHashSet d_seenInput; + + inline std::string varName(::Minisat::Lit lit); + inline std::string clauseName(ClauseId id); + + void collectLemmas(ClauseId id); + void printResolution(ClauseId id); + void printInputClause(ClauseId id); + + void printVariables(); + void printClauses(); + void flush(); + +public: + LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false): + SatProof(solver, checkRes), + d_seenVars(), + d_varSS(), + d_lemmaSS(), + d_paren(), + d_seenLemmas(), + d_seenInput() + {} + void printProof(); +}; + +} + +#endif diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 1c327c5a8..961ef85c5 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -28,6 +28,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/sat.h" #include "util/output.h" #include "expr/command.h" +#include "proof/proof_manager.h" +#include "proof/sat_proof.h" using namespace Minisat; using namespace CVC4; @@ -121,7 +123,9 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) -{} +{ + PROOF(ProofManager::initSatProof(this);) +} Solver::~Solver() @@ -233,6 +237,9 @@ bool Solver::addClause_(vec& ps, bool removable) } else if (ps.size() == 1) { if(assigns[var(ps[0])] == l_Undef) { uncheckedEnqueue(ps[0]); + + PROOF( ProofManager::getSatProof()->registerUnitClause(ps[0], true); ) + if(assertionLevel > 0) { // remember to unset it on user pop Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl; @@ -244,6 +251,8 @@ bool Solver::addClause_(vec& ps, bool removable) CRef cr = ca.alloc(assertionLevel, ps, false); clauses_persistent.push(cr); attachClause(cr); + + PROOF( ProofManager::getSatProof()->registerClause(cr, true); ) } } @@ -263,6 +272,8 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { + PROOF( ProofManager::getSatProof()->markDeleted(cr); ) + const Clause& c = ca[cr]; Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); @@ -401,10 +412,10 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) int max_level = 0; // Maximal level of the resolved clauses + PROOF( ProofManager::getSatProof()->startResChain(confl); ) do{ assert(confl != CRef_Undef); // (otherwise should be UIP) Clause& c = ca[confl]; - if (c.level() > max_level) { max_level = c.level(); } @@ -422,6 +433,11 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) pathC++; else out_learnt.push(q); + } else { + // FIXME: can we do it lazily if we actually need the proof? + if (level(var(q)) == 0) { + PROOF( ProofManager::getSatProof()->resolveOutUnit(q); ) + } } } @@ -431,6 +447,10 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) confl = reason(var(p)); seen[var(p)] = 0; pathC--; + + if ( pathC > 0 && confl != CRef_Undef ) { + PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); ) + } }while (pathC > 0); out_learnt[0] = ~p; @@ -442,7 +462,7 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) uint32_t abstract_level = 0; for (i = 1; i < out_learnt.size(); i++) abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) - + for (i = j = 1; i < out_learnt.size(); i++) { if (reason(var(out_learnt[i])) == CRef_Undef) { out_learnt[j++] = out_learnt[i]; @@ -453,6 +473,8 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) // Literal is not redundant out_learnt[j++] = out_learnt[i]; } else { + // + PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); ) // Literal is redundant, mark the level of the redundancy derivation if (max_level < red_level) { max_level = red_level; @@ -809,8 +831,13 @@ void Solver::removeSatisfied(vec& cs) int i, j; for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; - if (satisfied(c)) + if (satisfied(c)) { + if (locked(c)) { + // store a resolution of the literal c propagated + PROOF( ProofManager::getSatProof()->storeUnitResolution(c[0]); ) + } removeClause(cs[i]); + } else cs[j++] = cs[i]; } @@ -908,7 +935,10 @@ lbool Solver::search(int nof_conflicts) conflicts++; conflictC++; - if (decisionLevel() == 0) return l_False; + if (decisionLevel() == 0) { + PROOF( ProofManager::getSatProof()->finalizeProof(confl); ) + return l_False; + } // Analyze the conflict learnt_clause.clear(); @@ -918,12 +948,17 @@ lbool Solver::search(int nof_conflicts) // Assert the conflict clause and the asserting literal if (learnt_clause.size() == 1) { uncheckedEnqueue(learnt_clause[0]); - } else { + + PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); ) + + } else { CRef cr = ca.alloc(max_level, learnt_clause, true); clauses_removable.push(cr); attachClause(cr); claBumpActivity(ca[cr]); uncheckedEnqueue(learnt_clause[0], cr); + + PROOF( ProofManager::getSatProof()->endResChain(cr); ) } varDecayActivity(); @@ -1211,7 +1246,7 @@ void Solver::relocAll(ClauseAllocator& to) // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1); vec& ws = watches[p]; for (int j = 0; j < ws.size(); j++) - ca.reloc(ws[j].cref, to); + ca.reloc(ws[j].cref, to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); } // All reasons: @@ -1220,18 +1255,19 @@ void Solver::relocAll(ClauseAllocator& to) Var v = var(trail[i]); if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) - ca.reloc(vardata[v].reason, to); + ca.reloc(vardata[v].reason, to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); } - // All learnt: // for (int i = 0; i < clauses_removable.size(); i++) - ca.reloc(clauses_removable[i], to); + ca.reloc(clauses_removable[i], to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); // All original: // for (int i = 0; i < clauses_persistent.size(); i++) - ca.reloc(clauses_persistent[i], to); + ca.reloc(clauses_persistent[i], to, NULLPROOF( ProofManager::getSatProof()->getProxy() )); + + PROOF( ProofManager::getSatProof()->finishUpdateCRef(); ) } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index c5220997b..a3d449a36 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -37,9 +37,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "expr/command.h" namespace CVC4 { +class SatProof; + namespace prop { class SatSolver; }/* CVC4::prop namespace */ + }/* CVC4 namespace */ namespace Minisat { @@ -49,9 +52,9 @@ namespace Minisat { class Solver { - /** The only CVC4 entry point to the private solver data */ + /** The only two CVC4 entry points to the private solver data */ friend class CVC4::prop::SatSolver; - + friend class CVC4::SatProof; protected: /** The pointer to the proxy that provides interfaces to the SMT engine */ diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 1aff5094d..57ca95a41 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define Minisat_SolverTypes_h #include - +#include "util/output.h" #include "mtl/IntTypes.h" #include "mtl/Alg.h" #include "mtl/Vec.h" @@ -44,6 +44,7 @@ typedef int Var; #define var_Undef (-1) + struct Lit { int x; @@ -115,11 +116,26 @@ public: inline int toInt (lbool l) { return l.value; } inline lbool toLbool(int v) { return lbool((uint8_t)v); } -//================================================================================================= -// Clause -- a simple class for representing a clause: class Clause; typedef RegionAllocator::Ref CRef; +} /* Minisat */ + + + +namespace CVC4 { +class ProofProxyAbstract { +public: + virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; +}; +} + + + +namespace Minisat{ + +//================================================================================================= +// Clause -- a simple class for representing a clause: class Clause { struct { @@ -236,17 +252,21 @@ class ClauseAllocator : public RegionAllocator RegionAllocator::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, ClauseAllocator& to) + void reloc(CRef& cr, ClauseAllocator& to, CVC4::ProofProxyAbstract* proxy = NULL) { + + // FIXME what is this CRef_lazy if (cr == CRef_Lazy) return; + CRef old = cr; // save the old reference Clause& c = operator[](cr); - if (c.reloced()) { cr = c.relocation(); return; } cr = to.alloc(c.level(), c, c.removable()); c.relocate(cr); - + if (proxy) { + proxy->updateCRef(old, cr); + } // Copy extra data-fields: // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) to[cr].mark(c.mark()); diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 8c31dd377..6045fc881 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "mtl/Sort.h" #include "simp/SimpSolver.h" #include "utils/System.h" - +#include "proof/proof.h" using namespace Minisat; using namespace CVC4; @@ -57,7 +57,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con , asymm_lits (0) , eliminated_vars (0) , elimorder (1) - , use_simplification (!enableIncremental) + , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially , occurs (ClauseDeleted(ca)) , elim_heap (ElimLt(n_occ)) , bwdsub_assigns (0) @@ -702,10 +702,11 @@ void SimpSolver::relocAll(ClauseAllocator& to) // for (int i = 0; i < subsumption_queue.size(); i++) ca.reloc(subsumption_queue[i], to); - + // TODO reloc now takes the proof form the core solver // Temporary clause: // ca.reloc(bwdsub_tmpunit, to); + // TODO reloc now takes the proof form the core solver } @@ -723,4 +724,5 @@ void SimpSolver::garbageCollect() printf("| Garbage collection: %12d bytes => %12d bytes |\n", ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); + // TODO: proof.finalizeUpdateId(); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ecd61c0b4..96ee5b59b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -244,6 +244,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : if(Options::current()->cumulativeMillisecondLimit != 0) { setTimeLimit(Options::current()->cumulativeMillisecondLimit, true); } + } void SmtEngine::shutdown() { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f898ee76a..5d8f31d3c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -36,6 +36,7 @@ #include "util/result.h" #include "util/sexpr.h" #include "util/stats.h" +#include "proof/proof_manager.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -43,6 +44,7 @@ namespace CVC4 { + template class NodeTemplate; typedef NodeTemplate Node; typedef NodeTemplate TNode; diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 3164b75a5..211a1127b 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -69,6 +69,10 @@ bool Configuration::isAssertionBuild() { return IS_ASSERTIONS_BUILD; } +bool Configuration::isProofBuild() { + return IS_PROOFS_BUILD; +} + bool Configuration::isCoverageBuild() { return IS_COVERAGE_BUILD; } diff --git a/src/util/configuration.h b/src/util/configuration.h index c3040f3fb..1a57af62b 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -59,6 +59,8 @@ public: static bool isAssertionBuild(); + static bool isProofBuild(); + static bool isCoverageBuild(); static bool isProfilingBuild(); diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index abff15b3b..53b69ebfc 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -67,6 +67,12 @@ namespace CVC4 { # define IS_ASSERTIONS_BUILD false #endif /* CVC4_ASSERTIONS */ +#ifdef CVC4_PROOF +# define IS_PROOFS_BUILD true +#else /* CVC4_PROOF */ +# define IS_PROOFS_BUILD false +#endif /* CVC4_PROOF */ + #ifdef CVC4_COVERAGE # define IS_COVERAGE_BUILD true #else /* CVC4_COVERAGE */ diff --git a/src/util/options.cpp b/src/util/options.cpp index 64f1fe4d5..c69db62a3 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -80,6 +80,7 @@ Options::Options() : cumulativeMillisecondLimit(0), segvNoSpin(false), produceModels(false), + proof(false), produceAssignments(false), typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT), earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT), @@ -129,6 +130,7 @@ static const string optionsDescription = "\ --no-interactive do not run interactively\n\ --produce-models | -m support the get-value command\n\ --produce-assignments support the get-assignment command\n\ + --proof turn proof generation on\n\ --lazy-definition-expansion expand define-fun lazily\n\ --simplification=MODE choose simplification mode, see --simplification=help\n\ --no-static-learning turn off static learning (e.g. diamond-breaking)\n\ @@ -292,6 +294,7 @@ enum OptionValue { INTERACTIVE, NO_INTERACTIVE, PRODUCE_ASSIGNMENTS, + PROOF, NO_TYPE_CHECKING, LAZY_TYPE_CHECKING, EAGER_TYPE_CHECKING, @@ -369,6 +372,7 @@ static struct option cmdlineOptions[] = { { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { "produce-models", no_argument , NULL, 'm' }, { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS }, + { "proof", no_argument, NULL, PROOF }, { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING }, { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING }, { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING }, @@ -628,11 +632,15 @@ throw(OptionException) { case 'm': produceModels = true; break; - + case PRODUCE_ASSIGNMENTS: produceAssignments = true; break; - + + case PROOF: + proof = true; + break; + case NO_TYPE_CHECKING: typeChecking = false; earlyTypeChecking = false; @@ -828,6 +836,7 @@ throw(OptionException) { 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"); diff --git a/src/util/options.h b/src/util/options.h index f9dc042d1..699895c47 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -145,6 +145,9 @@ struct CVC4_PUBLIC Options { /** Whether we support SmtEngine::getValue() for this run. */ bool produceModels; + /** Whether we produce proofs. */ + bool proof; + /** Whether we support SmtEngine::getAssignment() for this run. */ bool produceAssignments;