#
# staticbinary
# optimized
+# proof
# debugsymbols
# assertions
# tracing
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
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
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"
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
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
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
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
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],
Build ID : $build_type
Optimized : $optimized
Debug symbols: $enable_debug_symbols
+Proof : $enable_proof
Statistics : $enable_statistics
Replay : $enable_replay
Assertions : $enable_assertions
-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
@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 \
@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 \
--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 */
--- /dev/null
+topdir = ../..
+srcdir = src/proof
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+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
+
--- /dev/null
+#include "cnf_proof.h"
+using namespace CVC4::prop;
+
+namespace CVC4 {
+CnfProof::CnfProof(CnfStream* stream) :
+ d_cnfStream(stream) {}
+
+
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+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 */
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+#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 */
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+#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 */
--- /dev/null
+#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 "<<id<<" "
+ << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "")
+ << (isUnit(id)? "Unit" : "") << endl;
+ }
+ Assert(d_idClause.find(id) != d_idClause.end());
+ return d_idClause[id];
+}
+
+Clause& SatProof::getClause(ClauseId id) {
+ return d_solver->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"<<id;
+ } else if (isUnit(id)) {
+ printLit(getUnit(id));
+ } else if (id == d_emptyClauseId) {
+ Debug("proof:sat") << "empty "<< endl;
+ }
+ else {
+ CRef ref = getClauseRef(id);
+ Assert (ref != CRef_Undef);
+ printClause(d_solver->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"<<var(lit) << ")" ;
+ }
+ else {
+ os << "(pos v"<<var(lit) << ")";
+ }
+ return os.str();
+}
+
+
+string LFSCSatProof::clauseName(ClauseId id) {
+ ostringstream os;
+ if (isInputClause(id)) {
+ os << "p"<<id;
+ return os.str();
+ } else {
+ os << "l"<<id;
+ return os.str();
+ }
+}
+
+void LFSCSatProof::collectLemmas(ClauseId id) {
+ if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
+ return;
+ }
+ if (d_seenInput.find(id) != d_seenInput.end()) {
+ return;
+ }
+
+ if (isInputClause(id)) {
+ d_seenInput.insert(id);
+ return;
+ } else {
+ d_seenLemmas.insert(id);
+ }
+
+ ResChain* res = d_resChains[id];
+ ClauseId start = res->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 */
+
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+#include <stdint.h>
+#include <vector>
+#include <set>
+#include <ext/hash_map>
+#include <ext/hash_set>
+#include <sstream>
+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
#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;
, conflict_budget (-1)
, propagation_budget (-1)
, asynch_interrupt (false)
-{}
+{
+ PROOF(ProofManager::initSatProof(this);)
+}
Solver::~Solver()
} 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;
CRef cr = ca.alloc(assertionLevel, ps, false);
clauses_persistent.push(cr);
attachClause(cr);
+
+ PROOF( ProofManager::getSatProof()->registerClause(cr, true); )
}
}
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);
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();
}
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); )
+ }
}
}
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;
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];
// 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;
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];
}
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();
// 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();
// printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
vec<Watcher>& 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:
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(); )
}
#include "expr/command.h"
namespace CVC4 {
+class SatProof;
+
namespace prop {
class SatSolver;
}/* CVC4::prop namespace */
+
}/* CVC4 namespace */
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 */
#define Minisat_SolverTypes_h
#include <assert.h>
-
+#include "util/output.h"
#include "mtl/IntTypes.h"
#include "mtl/Alg.h"
#include "mtl/Vec.h"
#define var_Undef (-1)
+
struct Lit {
int x;
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<uint32_t>::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 {
RegionAllocator<uint32_t>::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());
#include "mtl/Sort.h"
#include "simp/SimpSolver.h"
#include "utils/System.h"
-
+#include "proof/proof.h"
using namespace Minisat;
using namespace CVC4;
, 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)
//
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
}
printf("| Garbage collection: %12d bytes => %12d bytes |\n",
ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
to.moveTo(ca);
+ // TODO: proof.finalizeUpdateId();
}
if(Options::current()->cumulativeMillisecondLimit != 0) {
setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
}
+
}
void SmtEngine::shutdown() {
#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)
namespace CVC4 {
+
template <bool ref_count> class NodeTemplate;
typedef NodeTemplate<true> Node;
typedef NodeTemplate<false> TNode;
return IS_ASSERTIONS_BUILD;
}
+bool Configuration::isProofBuild() {
+ return IS_PROOFS_BUILD;
+}
+
bool Configuration::isCoverageBuild() {
return IS_COVERAGE_BUILD;
}
static bool isAssertionBuild();
+ static bool isProofBuild();
+
static bool isCoverageBuild();
static bool isProfilingBuild();
# 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 */
cumulativeMillisecondLimit(0),
segvNoSpin(false),
produceModels(false),
+ proof(false),
produceAssignments(false),
typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
--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\
INTERACTIVE,
NO_INTERACTIVE,
PRODUCE_ASSIGNMENTS,
+ PROOF,
NO_TYPE_CHECKING,
LAZY_TYPE_CHECKING,
EAGER_TYPE_CHECKING,
{ "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 },
case 'm':
produceModels = true;
break;
-
+
case PRODUCE_ASSIGNMENTS:
produceAssignments = true;
break;
-
+
+ case PROOF:
+ proof = true;
+ break;
+
case NO_TYPE_CHECKING:
typeChecking = false;
earlyTypeChecking = false;
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");
/** 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;
projects / cvc5.git / commitdiff