Changes since 1.4
=================
-* nothing yet
+* Support for unsat cores.
+* Simplification mode "incremental" no longer supported.
Changes since 1.3
=================
/* class AssertCommand */
-AssertCommand::AssertCommand(const Expr& e) throw() :
- d_expr(e) {
+AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() :
+ d_expr(e), d_inUnsatCore(inUnsatCore) {
}
Expr AssertCommand::getExpr() const throw() {
void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
try {
- smtEngine->assertFormula(d_expr);
+ smtEngine->assertFormula(d_expr, d_inUnsatCore);
d_commandStatus = CommandSuccess::instance();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new AssertCommand(d_expr.exportTo(exprManager, variableMap));
+ return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
}
Command* AssertCommand::clone() const {
- return new AssertCommand(d_expr);
+ return new AssertCommand(d_expr, d_inUnsatCore);
}
std::string AssertCommand::getCommandName() const throw() {
return "assert";
}
-
/* class PushCommand */
void PushCommand::invoke(SmtEngine* smtEngine) throw() {
d_expr() {
}
-CheckSatCommand::CheckSatCommand(const Expr& expr) throw() :
- d_expr(expr) {
+CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() :
+ d_expr(expr), d_inUnsatCore(inUnsatCore) {
}
Expr CheckSatCommand::getExpr() const throw() {
}
Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap));
+ CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
c->d_result = d_result;
return c;
}
Command* CheckSatCommand::clone() const {
- CheckSatCommand* c = new CheckSatCommand(d_expr);
+ CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore);
c->d_result = d_result;
return c;
}
/* class QueryCommand */
-QueryCommand::QueryCommand(const Expr& e) throw() :
- d_expr(e) {
+QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() :
+ d_expr(e), d_inUnsatCore(inUnsatCore) {
}
Expr QueryCommand::getExpr() const throw() {
}
Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap));
+ QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
c->d_result = d_result;
return c;
}
Command* QueryCommand::clone() const {
- QueryCommand* c = new QueryCommand(d_expr);
+ QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore);
c->d_result = d_result;
return c;
}
}
void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
- /*
try {
d_result = smtEngine->getUnsatCore();
d_commandStatus = CommandSuccess::instance();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
- */
- d_commandStatus = new CommandUnsupported();
}
void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
- //do nothing -- unsat cores not yet supported
- // d_result->toStream(out);
+ d_result.toStream(out);
}
}
Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
GetUnsatCoreCommand* c = new GetUnsatCoreCommand();
- //c->d_result = d_result;
+ c->d_result = d_result;
return c;
}
Command* GetUnsatCoreCommand::clone() const {
GetUnsatCoreCommand* c = new GetUnsatCoreCommand();
- //c->d_result = d_result;
+ c->d_result = d_result;
return c;
}
#include "util/sexpr.h"
#include "util/datatype.h"
#include "util/proof.h"
+#include "util/unsat_core.h"
namespace CVC4 {
class CVC4_PUBLIC AssertCommand : public Command {
protected:
Expr d_expr;
+ bool d_inUnsatCore;
public:
- AssertCommand(const Expr& e) throw();
+ AssertCommand(const Expr& e, bool inUnsatCore = true) throw();
~AssertCommand() throw() {}
Expr getExpr() const throw();
void invoke(SmtEngine* smtEngine) throw();
protected:
Expr d_expr;
Result d_result;
+ bool d_inUnsatCore;
public:
CheckSatCommand() throw();
- CheckSatCommand(const Expr& expr) throw();
+ CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw();
~CheckSatCommand() throw() {}
Expr getExpr() const throw();
void invoke(SmtEngine* smtEngine) throw();
protected:
Expr d_expr;
Result d_result;
+ bool d_inUnsatCore;
public:
- QueryCommand(const Expr& e) throw();
+ QueryCommand(const Expr& e, bool inUnsatCore = true) throw();
~QueryCommand() throw() {}
Expr getExpr() const throw();
void invoke(SmtEngine* smtEngine) throw();
class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
protected:
- //UnsatCore* d_result;
+ UnsatCore d_result;
public:
GetUnsatCoreCommand() throw();
~GetUnsatCoreCommand() throw() {}
| /* assertion */
ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
term[expr, expr2]
- { cmd = new AssertCommand(expr); }
+ { cmd = new AssertCommand(expr, /* inUnsatCore */ PARSER_STATE->lastNamedTerm() == expr);
+ PARSER_STATE->setLastNamedTerm(Expr());
+ }
| /* check-sat */
CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( term[expr, expr2]
};
args.push_back(expr);
expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
- cmd = new AssertCommand(expr); }
+ cmd = new AssertCommand(expr, false); }
/* propagation rule */
| rewritePropaKind[kind]
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
};
args.push_back(expr);
expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
- cmd = new AssertCommand(expr); }
+ cmd = new AssertCommand(expr, false); }
;
rewritePropaKind[CVC4::Kind& kind]
/* attributed expressions */
| LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
- ( attribute[expr, attexpr,attr]
- { if( attr == ":pattern" && ! attexpr.isNull()) {
+ ( attribute[expr, attexpr, attr]
+ { if(attr == ":pattern" && ! attexpr.isNull()) {
patexprs.push_back( attexpr );
}
}
}
}
expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs);
- }else{
+ } else {
expr2 = f2;
}
}
PARSER_STATE->reserveSymbolAtAssertionLevel(name);
// define it
Expr func = PARSER_STATE->mkFunction(name, expr.getType());
+ // remember the last term to have been given a :named attribute
+ PARSER_STATE->setLastNamedTerm(expr);
// bind name to expr with define-fun
Command* c =
new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
bool d_logicSet;
LogicInfo d_logic;
std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap;
+ Expr d_lastNamedTerm;
protected:
Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
void includeFile(const std::string& filename);
+ void setLastNamedTerm(Expr e) {
+ d_lastNamedTerm = e;
+ }
+
+ Expr lastNamedTerm() {
+ return d_lastNamedTerm;
+ }
+
bool isAbstractValue(const std::string& name) {
return name.length() >= 2 && name[0] == '@' && name[1] != '0' &&
name.find_first_not_of("0123456789", 1) == std::string::npos;
tryToStream<GetAssignmentCommand>(out, c) ||
tryToStream<GetAssertionsCommand>(out, c) ||
tryToStream<GetProofCommand>(out, c) ||
+ tryToStream<GetUnsatCoreCommand>(out, c) ||
tryToStream<SetBenchmarkStatusCommand>(out, c) ||
tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) ||
tryToStream<SetInfoCommand>(out, c) ||
out << "(get-proof)";
}
+static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) throw() {
+ out << "(get-unsat-core)";
+}
+
static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
out << "(set-info :status " << c->getStatus() << ")";
}
: d_cnfStream(stream)
{}
+CnfProof::~CnfProof() {
+}
Expr CnfProof::getAtom(prop::SatVariable var) {
prop::SatLiteral lit (var);
return atom;
}
-CnfProof::~CnfProof() {
-}
-
-LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() {
- return iterator(*this, ProofManager::currentPM()->begin_vars());
+prop::SatLiteral CnfProof::getLiteral(TNode atom) {
+ return d_cnfStream->getLiteral(atom);
}
-LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() {
- return iterator(*this, ProofManager::currentPM()->end_vars());
+Expr CnfProof::getAssertion(uint64_t id) {
+ return d_cnfStream->getAssertion(id).toExpr();
}
-void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
- ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars();
- ProofManager::var_iterator end = ProofManager::currentPM()->end_vars();
-
- for (;it != end; ++it) {
- os << "(decl_atom ";
-
- if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
- Expr atom = getAtom(*it);
- LFSCTheoryProof::printTerm(atom, os);
- } else {
- // print fake atoms for all other logics
- os << "true ";
+void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren) {
+ for (unsigned i = 0; i < clause->size(); ++i) {
+ prop::SatLiteral lit = clause->operator[](i);
+ if(d_atomsDeclared.find(lit.getSatVariable()) == d_atomsDeclared.end()) {
+ d_atomsDeclared.insert(lit.getSatVariable());
+ os << "(decl_atom ";
+ if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0 ||
+ ProofManager::currentPM()->getLogic().compare("QF_AX") == 0 ||
+ ProofManager::currentPM()->getLogic().compare("QF_SAT") == 0) {
+ Expr atom = getAtom(lit.getSatVariable());
+ LFSCTheoryProof::printTerm(atom, os);
+ } else {
+ // print fake atoms for all other logics (for now)
+ os << "true ";
+ }
+
+ os << " (\\ " << ProofManager::getVarName(lit.getSatVariable()) << " (\\ " << ProofManager::getAtomName(lit.getSatVariable()) << "\n";
+ paren << ")))";
}
-
- os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n";
- paren << ")))";
}
}
}
void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
- os << " ;; Input Clauses \n";
+ os << " ;; Clauses\n";
ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses();
ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses();
for (; it != end; ++it) {
ClauseId id = it->first;
const prop::SatClause* clause = it->second;
+ printAtomMapping(clause, os, paren);
os << "(satlem _ _ ";
std::ostringstream clause_paren;
printClause(*clause, os, clause_paren);
- os << " (clausify_false trust)" << clause_paren.str();
- os << "( \\ " << ProofManager::getInputClauseName(id) << "\n";
+ os << "(clausify_false trust)" << clause_paren.str()
+ << " (\\ " << ProofManager::getInputClauseName(id) << "\n";
paren << "))";
}
}
-
void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
- os << " ;; Theory Lemmas \n";
- ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas();
- ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas();
+ os << " ;; Theory Lemmas\n";
+ ProofManager::ordered_clause_iterator it = ProofManager::currentPM()->begin_lemmas();
+ ProofManager::ordered_clause_iterator end = ProofManager::currentPM()->end_lemmas();
+
+ for(size_t n = 0; it != end; ++it, ++n) {
+ if(n % 100 == 0) {
+ Chat() << "proving theory conflicts...(" << n << "/" << ProofManager::currentPM()->num_lemmas() << ")" << std::endl;
+ }
- for (; it != end; ++it) {
ClauseId id = it->first;
const prop::SatClause* clause = it->second;
+ NodeBuilder<> c(kind::AND);
+ for(unsigned i = 0; i < clause->size(); ++i) {
+ prop::SatLiteral lit = (*clause)[i];
+ prop::SatVariable var = lit.getSatVariable();
+ if(lit.isNegated()) {
+ c << Node::fromExpr(getAtom(var));
+ } else {
+ c << Node::fromExpr(getAtom(var)).notNode();
+ }
+ }
+ Node cl = c;
+ if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) {
+ uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id];
+ TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff);
+ if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) {
+ Debug("cores") << "; extensional lemma!" << std::endl;
+ Assert(cl.getKind() == kind::AND && cl.getNumChildren() == 2 && cl[0].getKind() == kind::EQUAL && cl[0][0].getKind() == kind::SELECT);
+ TNode myk = cl[0][0][1];
+ Debug("cores") << "; so my skolemized k is " << myk << std::endl;
+ os << "(ext _ _ " << orig[0][0] << " " << orig[0][1] << " (\\ " << myk << " (\\ " << ProofManager::getLemmaName(id) << "\n";
+ paren << ")))";
+ }
+ }
+ printAtomMapping(clause, os, paren);
os << "(satlem _ _ ";
std::ostringstream clause_paren;
printClause(*clause, os, clause_paren);
- os << " (clausify_false trust)" << clause_paren.str();
- os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n";
+
+ Debug("cores") << "\n;id is " << id << std::endl;
+ if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) {
+ uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id];
+ Debug("cores") << ";getting id " << int32_t(proof_id & 0xffffffff) << std::endl;
+ Assert(int32_t(proof_id & 0xffffffff) != -1);
+ TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff);
+ Debug("cores") << "; ID is " << id << " and that's a lemma with " << ((proof_id >> 32) & 0xffffffff) << " / " << (proof_id & 0xffffffff) << std::endl;
+ Debug("cores") << "; that means the lemma was " << orig << std::endl;
+ if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) {
+ Debug("cores") << "; extensional" << std::endl;
+ os << "(clausify_false trust)\n";
+ } else if(proof_id == 0) {
+ // theory propagation caused conflict
+ //ProofManager::currentPM()->printProof(os, cl);
+ os << "(clausify_false trust)\n";
+ } else if(((proof_id >> 32) & 0xffffffff) == RULE_CONFLICT) {
+ os << "\n;; need to generate a (conflict) proof of " << cl << "\n";
+ //ProofManager::currentPM()->printProof(os, cl);
+ os << "(clausify_false trust)\n";
+ } else {
+ os << "\n;; need to generate a (lemma) proof of " << cl;
+ os << "\n;; DON'T KNOW HOW !!\n";
+ os << "(clausify_false trust)\n";
+ }
+ } else {
+ os << "\n;; need to generate a (conflict) proof of " << cl << "\n";
+ ProofManager::currentPM()->printProof(os, cl);
+ }
+ os << clause_paren.str()
+ << " (\\ " << ProofManager::getLemmaClauseName(id) << "\n";
paren << "))";
}
}
prop::SatLiteral lit = clause[i];
prop::SatVariable var = lit.getSatVariable();
if (lit.isNegated()) {
- os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
+ os << "(ast _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " ";
paren << "))";
} else {
- os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
+ os << "(asf _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " ";
paren << "))";
}
}
namespace CVC4 {
namespace prop {
class CnfStream;
-}
+}/* CVC4::prop namespace */
class CnfProof;
-class AtomIterator {
- CnfProof& d_cnf;
- ProofManager::var_iterator d_it;
-
-public:
- AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it)
- : d_cnf(cnf), d_it(it)
- {}
- inline Expr operator*();
- AtomIterator& operator++() { ++d_it; return *this; }
- AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; }
- bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; }
- bool operator!=(const AtomIterator& it) const { return !(*this == it); }
-};/* class AtomIterator */
-
class CnfProof {
protected:
CVC4::prop::CnfStream* d_cnfStream;
- Expr getAtom(prop::SatVariable var);
- friend class AtomIterator;
+ VarSet d_atomsDeclared;
public:
CnfProof(CVC4::prop::CnfStream* cnfStream);
- typedef AtomIterator iterator;
- virtual iterator begin_atom_mapping() = 0;
- virtual iterator end_atom_mapping() = 0;
+ Expr getAtom(prop::SatVariable var);
+ Expr getAssertion(uint64_t id);
+ prop::SatLiteral getLiteral(TNode atom);
- virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0;
virtual void printClauses(std::ostream& os, std::ostream& paren) = 0;
virtual ~CnfProof();
-};
+};/* class CnfProof */
class LFSCCnfProof : public CnfProof {
void printInputClauses(std::ostream& os, std::ostream& paren);
void printTheoryLemmas(std::ostream& os, std::ostream& paren);
void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren);
+ virtual void printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren);
public:
LFSCCnfProof(CVC4::prop::CnfStream* cnfStream)
: CnfProof(cnfStream)
{}
- virtual iterator begin_atom_mapping();
- virtual iterator end_atom_mapping();
-
- virtual void printAtomMapping(std::ostream& os, std::ostream& paren);
virtual void printClauses(std::ostream& os, std::ostream& paren);
-};
-
-inline Expr AtomIterator::operator*() {
- return d_cnf.getAtom(*d_it);
-}
+};/* class LFSCCnfProof */
} /* CVC4 namespace */
#include "smt/options.h"
#ifdef CVC4_PROOF
-# define PROOF(x) if(options::proof()) { x; }
-# define NULLPROOF(x) (options::proof()) ? x : NULL
-# define PROOF_ON() options::proof()
+# define PROOF(x) if(options::proof() || options::unsatCores()) { x; }
+# define NULLPROOF(x) (options::proof() || options::unsatCores()) ? x : NULL
+# define PROOF_ON() (options::proof() || options::unsatCores())
#else /* CVC4_PROOF */
# define PROOF(x)
# define NULLPROOF(x) NULL
#include "util/cvc4_assert.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
+#include "theory/output_channel.h"
+#include "theory/valuation.h"
+#include "util/node_visitor.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/arrays/theory_arrays.h"
+#include "context/context.h"
+#include "util/hash.h"
namespace CVC4 {
d_cnfProof(NULL),
d_theoryProof(NULL),
d_fullProof(NULL),
- d_format(format)
+ d_format(format),
+ d_deps()
{
}
delete it->second;
}
- for(IdToClause::iterator it = d_theoryLemmas.begin();
+ for(OrderedIdToClause::iterator it = d_theoryLemmas.begin();
it != d_theoryLemmas.end();
++it) {
delete it->second;
}
TheoryProof* ProofManager::getTheoryProof() {
- Assert (currentPM()->d_theoryProof);
+ //Assert (currentPM()->d_theoryProof);
return currentPM()->d_theoryProof;
}
-
void ProofManager::initSatProof(Minisat::Solver* solver) {
Assert (currentPM()->d_satProof == NULL);
Assert(currentPM()->d_format == LFSC);
currentPM()->d_theoryProof = new LFSCTheoryProof();
}
-
-std::string ProofManager::getInputClauseName(ClauseId id) {return append("pb", id); }
-std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lem", id); }
+std::string ProofManager::getInputClauseName(ClauseId id) { return append("pb", id); }
+std::string ProofManager::getLemmaName(ClauseId id) { return append("lem", id); }
+std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lemc", id); }
std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); }
-std::string ProofManager::getVarName(prop::SatVariable var) { return append("v", var); }
-std::string ProofManager::getAtomName(prop::SatVariable var) { return append("a", var); }
-std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); }
+std::string ProofManager::getVarName(prop::SatVariable var) { return append("var", var); }
+std::string ProofManager::getAtomName(prop::SatVariable var) { return append("atom", var); }
+std::string ProofManager::getLitName(prop::SatLiteral lit) { return append("lit", lit.toInt()); }
+
+std::string ProofManager::getAtomName(TNode atom) {
+ prop::SatLiteral lit = currentPM()->d_cnfProof->getLiteral(atom);
+ Assert(!lit.isNegated());
+ return getAtomName(lit.getSatVariable());
+}
+std::string ProofManager::getLitName(TNode lit) {
+ return getLitName(currentPM()->d_cnfProof->getLiteral(lit));
+}
+
+void ProofManager::traceDeps(TNode n) {
+ Debug("cores") << "trace deps " << n << std::endl;
+ if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
+ // originating formula was in core set
+ Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
+ d_outputCoreFormulas.insert(n.toExpr());
+ } else {
+ Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
+ if(d_deps.find(n) == d_deps.end()) {
+ InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str());
+ }
+ Assert(d_deps.find(n) != d_deps.end());
+ std::vector<Node> deps = (*d_deps.find(n)).second;
+ for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
+ Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
+ traceDeps(*i);
+ }
+ }
+}
void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) {
- for (unsigned i = 0; i < clause->size(); ++i) {
+ /*for (unsigned i = 0; i < clause->size(); ++i) {
prop::SatLiteral lit = clause->operator[](i);
d_propVars.insert(lit.getSatVariable());
- }
+ }*/
if (kind == INPUT) {
d_inputClauses.insert(std::make_pair(id, clause));
- return;
+ Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end());
+ Debug("cores") << "core id is " << d_satProof->d_inputClauses[id] << std::endl;
+ if(d_satProof->d_inputClauses[id] == uint64_t(-1)) {
+ Debug("cores") << " + constant unit (true or false)" << std::endl;
+ } else if(options::unsatCores()) {
+ Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff);
+ Debug("cores") << "core input assertion from CnfStream is " << e << std::endl;
+ Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) << std::endl;
+ // Invalid proof rules are currently used for parts of CVC4 that don't
+ // support proofs (these are e.g. unproven theory lemmas) or don't need
+ // proofs (e.g. split lemmas). We can ignore these safely when
+ // constructing unsat cores.
+ if(((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) != RULE_INVALID) {
+ // trace dependences back to actual assertions
+ traceDeps(Node::fromExpr(e));
+ }
+ }
+ } else {
+ Assert(kind == THEORY_LEMMA);
+ d_theoryLemmas.insert(std::make_pair(id, clause));
}
- Assert (kind == THEORY_LEMMA);
- d_theoryLemmas.insert(std::make_pair(id, clause));
}
-void ProofManager::addAssertion(Expr formula) {
+void ProofManager::addAssertion(Expr formula, bool inUnsatCore) {
+ Debug("cores") << "assert: " << formula << std::endl;
d_inputFormulas.insert(formula);
+ d_deps[Node::fromExpr(formula)]; // empty vector of deps
+ if(inUnsatCore || options::dumpUnsatCores()) {
+ Debug("cores") << "adding to input core forms: " << formula << std::endl;
+ d_inputCoreFormulas.insert(formula);
+ }
}
-void ProofManager::setLogic(const std::string& logic_string) {
- d_logic = logic_string;
+void ProofManager::addDependence(TNode n, TNode dep) {
+ if(dep != n) {
+ Debug("cores") << "dep: " << n << " : " << dep << std::endl;
+ if(d_deps.find(dep) == d_deps.end()) {
+ Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl;
+ }
+ //Assert(d_deps.find(dep) != d_deps.end());
+ d_deps[n].push_back(dep);
+ }
+}
+
+void ProofManager::setLogic(const LogicInfo& logic) {
+ d_logic = logic;
}
+void ProofManager::printProof(std::ostream& os, TNode n) {
+ // no proofs here yet
+}
LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
: d_satProof(sat)
smt::SmtScope scope(d_smtEngine);
std::ostringstream paren;
out << "(check\n";
+ out << " ;; Declarations\n";
if (d_theoryProof == NULL) {
d_theoryProof = new LFSCTheoryProof();
}
- for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
+ /*for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
i != d_cnfProof->end_atom_mapping();
++i) {
d_theoryProof->addDeclaration(*i);
- }
+ }*/
d_theoryProof->printAssertions(out, paren);
+ out << " ;; Proof of empty clause follows\n";
out << "(: (holds cln)\n";
- d_cnfProof->printAtomMapping(out, paren);
d_cnfProof->printClauses(out, paren);
d_satProof->printResolutions(out, paren);
paren <<")))\n;;";
out << "\n";
}
-
} /* CVC4 namespace */
#define __CVC4__PROOF_MANAGER_H
#include <iostream>
+#include <map>
#include "proof/proof.h"
#include "util/proof.h"
-
+#include "expr/node.h"
+#include "theory/logic_info.h"
+#include "theory/substitutions.h"
// forward declarations
namespace Minisat {
std::string append(const std::string& str, uint64_t num);
typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
+typedef std::map < ClauseId, const prop::SatClause* > OrderedIdToClause;
typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
LEARNT
};/* enum ClauseKind */
+enum ProofRule {
+ RULE_GIVEN, /* input assertion */
+ RULE_DERIVED, /* a "macro" rule */
+ RULE_RECONSTRUCT, /* prove equivalence using another method */
+ RULE_TRUST, /* trust without evidence (escape hatch until proofs are fully supported) */
+ RULE_INVALID, /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */
+ RULE_CONFLICT, /* re-construct as a conflict */
+
+ RULE_ARRAYS_EXT, /* arrays, extensional */
+ RULE_ARRAYS_ROW, /* arrays, read-over-write */
+};/* enum ProofRules */
+
class ProofManager {
SatProof* d_satProof;
CnfProof* d_cnfProof;
// information that will need to be shared across proofs
IdToClause d_inputClauses;
- IdToClause d_theoryLemmas;
+ OrderedIdToClause d_theoryLemmas;
+ IdToClause d_theoryPropagations;
ExprSet d_inputFormulas;
- VarSet d_propVars;
+ ExprSet d_inputCoreFormulas;
+ ExprSet d_outputCoreFormulas;
+ //VarSet d_propVars;
+
+ int d_nextId;
Proof* d_fullProof;
ProofFormat d_format; // used for now only in debug builds
+ __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction > d_deps;
+
+ // trace dependences back to unsat core
+ void traceDeps(TNode n);
+
protected:
- std::string d_logic;
+ LogicInfo d_logic;
public:
ProofManager(ProofFormat format = LFSC);
// iterators over data shared by proofs
typedef IdToClause::const_iterator clause_iterator;
+ typedef OrderedIdToClause::const_iterator ordered_clause_iterator;
typedef ExprSet::const_iterator assertions_iterator;
typedef VarSet::const_iterator var_iterator;
clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); }
clause_iterator end_input_clauses() const { return d_inputClauses.end(); }
+ size_t num_input_clauses() const { return d_inputClauses.size(); }
- clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
- clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+ ordered_clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
+ ordered_clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+ size_t num_lemmas() const { return d_theoryLemmas.size(); }
assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); }
assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
+ size_t num_assertions() const { return d_inputFormulas.size(); }
- var_iterator begin_vars() const { return d_propVars.begin(); }
- var_iterator end_vars() const { return d_propVars.end(); }
+ void printProof(std::ostream& os, TNode n);
- void addAssertion(Expr formula);
+ void addAssertion(Expr formula, bool inUnsatCore);
void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
+ // note that n depends on dep (for cores)
+ void addDependence(TNode n, TNode dep);
+
+ assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
+ assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
+ size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
+
+ int nextId() { return d_nextId++; }
// variable prefixes
static std::string getInputClauseName(ClauseId id);
+ static std::string getLemmaName(ClauseId id);
static std::string getLemmaClauseName(ClauseId id);
static std::string getLearntClauseName(ClauseId id);
static std::string getVarName(prop::SatVariable var);
static std::string getAtomName(prop::SatVariable var);
+ static std::string getAtomName(TNode atom);
static std::string getLitName(prop::SatLiteral lit);
+ static std::string getLitName(TNode lit);
+
+ void setLogic(const LogicInfo& logic);
+ const std::string getLogic() const { return d_logic.getLogicString(); }
- void setLogic(const std::string& logic_string);
- const std::string getLogic() const { return d_logic; }
};/* class ProofManager */
class LFSCProof : public Proof {
Debug("proof:sat") << endl;
}
-
-int SatProof::d_idCounter = 0;
-
/**
* Converts the clause associated to id to a set of literals
*
Minisat::CRef SatProof::getClauseRef(ClauseId id) {
if (d_idClause.find(id) == d_idClause.end()) {
- Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" "
+ Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " "
<< ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "")
<< (isUnit(id)? "Unit" : "") << endl;
}
return (d_lemmaClauses.find(id) != d_lemmaClauses.end());
}
-
void SatProof::print(ClauseId id) {
if (d_deleted.find(id) != d_deleted.end()) {
- Debug("proof:sat") << "del"<<id;
+ Debug("proof:sat") << "del" << id;
} else if (isUnit(id)) {
printLit(getUnit(id));
} else if (id == d_emptyClauseId) {
- Debug("proof:sat") << "empty "<< endl;
- }
- else {
+ Debug("proof:sat") << "empty " << endl;
+ } else {
CRef ref = getClauseRef(id);
printClause(getClause(ref));
}
void SatProof::printRes(ClauseId id) {
Assert(hasResolution(id));
- Debug("proof:sat") << "id "<< id <<": ";
+ Debug("proof:sat") << "id " << id << ": ";
printRes(d_resChains[id]);
}
/// registration methods
-ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) {
+ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) {
+ Debug("cores") << "registerClause " << proof_id << std::endl;
Assert(clause != CRef_Undef);
ClauseIdMap::iterator it = d_clauseId.find(clause);
if (it == d_clauseId.end()) {
- ClauseId newId = d_idCounter++;
+ ClauseId newId = ProofManager::currentPM()->nextId();
d_clauseId[clause] = newId;
d_idClause[newId] = clause;
if (kind == INPUT) {
Assert(d_inputClauses.find(newId) == d_inputClauses.end());
- d_inputClauses.insert(newId);
+ d_inputClauses[newId] = proof_id;
}
if (kind == THEORY_LEMMA) {
Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
- d_lemmaClauses.insert(newId);
+ d_lemmaClauses[newId] = proof_id;
}
}
- Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n";
+ Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n";
return d_clauseId[clause];
}
-ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
+ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) {
+ Debug("cores") << "registerUnitClause " << kind << " " << proof_id << std::endl;
UnitIdMap::iterator it = d_unitId.find(toInt(lit));
if (it == d_unitId.end()) {
- ClauseId newId = d_idCounter++;
+ ClauseId newId = ProofManager::currentPM()->nextId();
d_unitId[toInt(lit)] = newId;
d_idUnit[newId] = lit;
if (kind == INPUT) {
Assert(d_inputClauses.find(newId) == d_inputClauses.end());
- d_inputClauses.insert(newId);
+ d_inputClauses[newId] = proof_id;
}
if (kind == THEORY_LEMMA) {
Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
- d_lemmaClauses.insert(newId);
+ d_lemmaClauses[newId] = proof_id;
}
}
- Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n";
+ Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n";
return d_unitId[toInt(lit)];
}
removedDfs(*it, removed, removeStack, inClause, seen);
}
- for (int i = removeStack.size()-1; i >= 0; --i) {
+ for (int i = removeStack.size() - 1; i >= 0; --i) {
Lit lit = removeStack[i];
CRef reason_ref = d_solver->reason(var(lit));
ClauseId reason_id;
Assert(isUnit(~lit));
reason_id = getUnitId(~lit);
} else {
- reason_id = registerClause(reason_ref);
+ reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1));
}
res->addStep(lit, reason_id, !sign(lit));
}
}
void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) {
- ClauseId id = registerClause(clause);
+ ClauseId id = registerClause(clause, LEARNT, uint64_t(-1));
ResChain* res = d_resStack.back();
res->addStep(lit, id, sign);
}
void SatProof::endResChain(CRef clause) {
Assert(d_resStack.size() > 0);
- ClauseId id = registerClause(clause);
+ ClauseId id = registerClause(clause, LEARNT, uint64_t(-1));
ResChain* res = d_resStack.back();
registerResolution(id, res);
d_resStack.pop_back();
void SatProof::endResChain(::Minisat::Lit lit) {
Assert(d_resStack.size() > 0);
- ClauseId id = registerUnitClause(lit);
+ ClauseId id = registerUnitClause(lit, LEARNT, uint64_t(-1));
ResChain* res = d_resStack.back();
registerResolution(id, res);
d_resStack.pop_back();
}
void SatProof::storeUnitResolution(::Minisat::Lit lit) {
+ Debug("cores") << "STORE UNIT RESOLUTION" << std::endl;
resolveUnit(lit);
}
CRef reason_ref = d_solver->reason(var(lit));
Assert(reason_ref != CRef_Undef);
- ClauseId reason_id = registerClause(reason_ref);
+ ClauseId reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1));
ResChain* res = new ResChain(reason_id);
// Here, the call to resolveUnit() can reallocate memory in the
res->addStep(l, res_id, !sign(l));
}
}
- ClauseId unit_id = registerUnitClause(lit);
+ ClauseId unit_id = registerUnitClause(lit, LEARNT, uint64_t(-1));
registerResolution(unit_id, res);
return unit_id;
}
Unimplemented("native proof printing not supported yet");
}
-void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind) {
+void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) {
+ Debug("cores") << "STORE UNIT CONFLICT" << std::endl;
Assert(!d_storedUnitConflict);
- d_unitConflictId = registerUnitClause(conflict_lit, kind);
+ d_unitConflictId = registerUnitClause(conflict_lit, kind, proof_id);
d_storedUnitConflict = true;
- Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n";
+ Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId << "\n";
}
void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
return;
} else {
Assert(!d_storedUnitConflict);
- conflict_id = registerClause(conflict_ref); //FIXME
+ conflict_id = registerClause(conflict_ref, LEARNT, uint64_t(-1)); //FIXME
}
if(Debug.isOn("proof:sat")) {
if (isInputClause(id)) {
os << ProofManager::getInputClauseName(id);
return os.str();
- } else
- if (isLemmaClause(id)) {
+ } else if (isLemmaClause(id)) {
os << ProofManager::getLemmaClauseName(id);
return os.str();
- }else {
+ } else {
os << ProofManager::getLearntClauseName(id);
return os.str();
}
ResChain* res = d_resChains[id];
ResSteps& steps = res->getSteps();
- for (int i = steps.size()-1; i >= 0; i--) {
+ for (int i = steps.size() - 1; i >= 0; --i) {
out << "(";
out << (steps[i].sign? "R" : "Q") << " _ _ ";
-
}
ClauseId start_id = res->getStart();
out << clauseName(start_id) << " ";
for(unsigned i = 0; i < steps.size(); i++) {
- out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")";
+ out << clauseName(steps[i].id) << " "
+ << ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit)))
+ << ") ";
}
if (id == d_emptyClauseId) {
- out <<"(\\empty empty)";
+ out << "(\\empty empty)";
return;
}
printResolution(d_emptyClauseId, out, paren);
}
-
} /* CVC4 namespace */
-
typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME
typedef std::hash_map < ClauseId, ResChain*> IdResMap;
typedef std::hash_set < ClauseId > IdHashSet;
+typedef std::hash_map < ClauseId, uint64_t > IdProofRuleMap;
typedef std::vector < ResChain* > ResStack;
typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause;
typedef std::set < ClauseId > IdSet;
UnitIdMap d_unitId;
IdHashSet d_deleted;
IdToSatClause d_deletedTheoryLemmas;
- IdHashSet d_inputClauses;
- IdHashSet d_lemmaClauses;
+public:
+ IdProofRuleMap d_inputClauses;
+ IdProofRuleMap d_lemmaClauses;
+protected:
// resolutions
IdResMap d_resChains;
ResStack d_resStack;
bool d_checkRes;
- static ClauseId d_idCounter;
const ClauseId d_emptyClauseId;
const ClauseId d_nullId;
// proxy class to break circular dependencies
void printRes(ResChain* res);
bool isInputClause(ClauseId id);
+ bool isTheoryConflict(ClauseId id);
bool isLemmaClause(ClauseId id);
bool isUnit(ClauseId id);
bool isUnit(::Minisat::Lit lit);
void finalizeProof(::Minisat::CRef conflict);
/// clause registration methods
- ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT);
- ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT);
+ ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id);
+ ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
- void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind = LEARNT);
+ void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
/**
* Marks the deleted clauses as deleted. Note we may still use them in the final
protected:
IdSet d_seenLearnt;
IdHashSet d_seenInput;
+ IdHashSet d_seenTheoryConflicts;
IdHashSet d_seenLemmas;
inline std::string varName(::Minisat::Lit lit);
** Major contributors:
** Minor contributors (to current version):
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
d_minisat->setNotify(d_minisatNotify);
}
-void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void BVMinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
Debug("sat::minisat") << "Add clause " << clause <<"\n";
BVMinisat::vec<BVMinisat::Lit> minisat_clause;
toMinisatClause(clause, minisat_clause);
** Major contributors:
** Minor contributors (to current version):
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
void setNotify(Notify* notify);
- void addClause(SatClause& clause, bool removable);
+ void addClause(SatClause& clause, bool removable, uint64_t proof_id);
SatValue propagate();
namespace CVC4 {
namespace prop {
-
CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
d_satSolver(satSolver),
d_booleanVariables(context),
d_literalToNodeMap(context),
d_fullLitToNodeMap(fullLitToNodeMap),
d_registrar(registrar),
+ d_assertionTable(context),
d_removable(false) {
}
Dump("clauses") << AssertCommand(Expr(n.toExpr()));
}
}
- d_satSolver->addClause(c, d_removable);
+ d_satSolver->addClause(c, d_removable, d_proofId);
}
void CnfStream::assertClause(TNode node, SatLiteral a) {
}
void TseitinCnfStream::ensureLiteral(TNode n) {
-
- // These are not removable
+ // These are not removable and have no proof ID
d_removable = false;
+ d_proofId = uint64_t(-1);
Debug("cnf") << "ensureLiteral(" << n << ")" << endl;
if(hasLiteral(n)) {
// If a theory literal, we pre-register it
if (preRegister) {
- bool backup = d_removable;
+ // In case we are re-entered due to lemmas, save our state
+ bool backupRemovable = d_removable;
+ uint64_t backupProofId= d_proofId;
d_registrar->preRegister(node);
- d_removable = backup;
+ d_removable = backupRemovable;
+ d_proofId = backupProofId;
}
// Here, you can have it
// At the top level we must ensure that all clauses that are asserted are
// not unit, except for the direct assertions. This allows us to remove the
// clauses later when they are not needed anymore (lemmas for example).
-void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) {
+void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from) {
Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl;
d_removable = removable;
+ if(options::proof() || options::unsatCores()) {
+ // Encode the assertion ID in the proof_id to store with generated clauses.
+ uint64_t assertionTableIndex = d_assertionTable.size();
+ Assert((uint64_t(proof_id) & 0xffffffff00000000) == 0 && (assertionTableIndex & 0xffffffff00000000) == 0, "proof_id/table_index collision");
+ d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32);
+ d_assertionTable.push_back(from.isNull() ? node : from);
+ Debug("cores") << "cnf ix " << assertionTableIndex << " asst " << node << " proof_id " << proof_id << " from " << from << endl;
+ } else {
+ // We aren't producing proofs or unsat cores; use an invalid proof id.
+ d_proofId = uint64_t(-1);
+ }
convertAndAssert(node, negated);
}
#include "expr/node.h"
#include "prop/theory_proxy.h"
#include "prop/registrar.h"
+#include "proof/proof_manager.h"
#include "context/cdlist.h"
#include "context/cdinsert_hashmap.h"
namespace CVC4 {
namespace prop {
-
class PropEngine;
/**
/** The "registrar" for pre-registration of terms */
Registrar* d_registrar;
+ /** A table of assertions, used for regenerating proofs. */
+ context::CDList<Node> d_assertionTable;
+
/**
* How many literals were already mapped at the top-level when we
* tried to convertAndAssert() something. This
return node;
}
+ /**
+ * A reference into the assertion table, used to map clauses back to
+ * their "original" input assertion/lemma. This variable is manipulated
+ * by the top-level convertAndAssert(). This is needed in proofs-enabled
+ * runs, to justify where the SAT solver's clauses came from.
+ */
+ uint64_t d_proofId;
+
/**
* Are we asserting a removable clause (true) or a permanent clause (false).
* This is set at the beginning of convertAndAssert so that it doesn't
- * need to be passed on over the stack. Only pure clauses can be asserted as
- * removable.
+ * need to be passed on over the stack. Only pure clauses can be asserted
+ * as removable.
*/
bool d_removable;
* @param removable whether the sat solver can choose to remove the clauses
* @param negated whether we are asserting the node negated
*/
- virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0;
+ virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0;
/**
* Get the node that is represented by the given SatLiteral.
*/
SatLiteral getLiteral(TNode node);
+ /**
+ * Get the assertion with a given ID. (Used for reconstructing proofs.)
+ */
+ TNode getAssertion(uint64_t id) {
+ return d_assertionTable[id];
+ }
+
/**
* Returns the Boolean variables from the input problem.
*/
* @param removable is this something that can be erased
* @param negated true if negated
*/
- void convertAndAssert(TNode node, bool removable, bool negated);
+ void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null());
/**
* Constructs the stream to use the given sat solver.
// Assert the constants
uncheckedEnqueue(mkLit(varTrue, false));
uncheckedEnqueue(mkLit(varFalse, true));
- PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT); )
- PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT); )
+ PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT, uint64_t(-1)); )
+ PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); )
}
// Construct the reason
CRef real_reason = ca.alloc(explLevel, explanation, true);
- PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); );
+ PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); );
vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
clauses_removable.push(real_reason);
attachClause(real_reason);
return real_reason;
}
-bool Solver::addClause_(vec<Lit>& ps, bool removable)
+bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
{
if (!ok) return false;
lemmas.push();
ps.copyTo(lemmas.last());
lemmas_removable.push(removable);
+ Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
+ lemmas_proof_id.push(proof_id);
} else {
// If all false, we're in conflict
if (ps.size() == falseLiteralsCount) {
// construct the clause below to give to the proof manager
// as the final conflict.
if(falseLiteralsCount == 1) {
- PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); )
+ PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); )
PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
return ok = false;
}
attachClause(cr);
if(PROOF_ON()) {
- PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); )
+ PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); )
if(ps.size() == falseLiteralsCount) {
PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
return ok = false;
if(assigns[var(ps[0])] == l_Undef) {
assert(assigns[var(ps[0])] != l_False);
uncheckedEnqueue(ps[0], cr);
- PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } );
+ Debug("cores") << "i'm registering a unit clause, input, proof id " << proof_id << std::endl;
+ PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT, proof_id); } );
CRef confl = propagate(CHECK_WITHOUT_THEORY);
if(! (ok = (confl == CRef_Undef)) ) {
if(ca[confl].size() == 1) {
- PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); );
+ PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); );
PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
} else {
PROOF( ProofManager::getSatProof()->finalizeProof(confl); );
propagateTheory();
// If there are lemmas (or conflicts) update them
if (lemmas.size() > 0) {
- confl = updateLemmas();
+ confl = updateLemmas();
}
} else {
// Even though in conflict, we still need to discharge the lemmas
proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl);
vec<Lit> explanation;
MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
- addClause(explanation, true);
+ addClause(explanation, true, 0);
}
}
}
// The current lemma
vec<Lit>& lemma = lemmas[i];
bool removable = lemmas_removable[i];
+ uint64_t proof_id = lemmas_proof_id[i];
+ Debug("cores") << "pulled lemma proof id " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
// Attach it if non-unit
CRef lemma_ref = CRef_Undef;
}
lemma_ref = ca.alloc(clauseLevel, lemma, removable);
- PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); );
+ PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); );
if (removable) {
clauses_removable.push(lemma_ref);
} else {
}
attachClause(lemma_ref);
} else {
- PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); );
+ PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); );
}
// If the lemma is propagating enqueue its literal (or set the conflict)
} else {
Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
conflict = CRef_Lazy;
- PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0]); );
+ PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT, proof_id); );
}
} else {
Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
// Clear the lemmas
lemmas.clear();
lemmas_removable.clear();
+ lemmas_proof_id.clear();
if (conflict != CRef_Undef) {
theoryConflict = true;
#include "expr/command.h"
namespace CVC4 {
-class SatProof;
-
-namespace prop {
- class TheoryProxy;
-}/* CVC4::prop namespace */
+ class SatProof;
+ namespace prop {
+ class TheoryProxy;
+ }/* CVC4::prop namespace */
}/* CVC4 namespace */
namespace Minisat {
/** Is the lemma removable */
vec<bool> lemmas_removable;
+ /** Proof IDs for lemmas */
+ vec<uint64_t> lemmas_proof_id;
+
/** Do a another check if FULL_EFFORT was the last one */
bool recheck;
void push ();
void pop ();
- bool addClause (const vec<Lit>& ps, bool removable); // Add a clause to the solver.
+ // CVC4 adds the "proof_id" here to refer to the input assertion/lemma
+ // that produced this clause
+ bool addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id); // Add a clause to the solver.
bool addEmptyClause(bool removable); // Add the empty clause, making the solver contradictory.
- bool addClause (Lit p, bool removable); // Add a unit clause to the solver.
- bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver.
- bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver.
- bool addClause_( vec<Lit>& ps, bool removable); // Add a clause to the solver without making superflous internal copy. Will
+ bool addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver.
+ bool addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver.
+ bool addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver.
+ bool addClause_( vec<Lit>& ps, bool removable, uint64_t proof_id); // Add a clause to the solver without making superflous internal copy. Will
// change the passed vector 'ps'.
// Solving:
// NOTE: enqueue does not set the ok flag! (only public methods do)
inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
-inline bool Solver::addClause (const vec<Lit>& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
-inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); }
-inline bool Solver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
-inline bool Solver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
-inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
+inline bool Solver::addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id)
+ { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); }
+inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable, uint64_t(-1)); }
+inline bool Solver::addClause (Lit p, bool removable, uint64_t proof_id)
+ { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); }
+inline bool Solver::addClause (Lit p, Lit q, bool removable, uint64_t proof_id)
+ { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); }
+inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id)
+ { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); }
inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } }
d_minisat->restart_inc = options::satRestartInc();
}
-void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
Minisat::vec<Minisat::Lit> minisat_clause;
toMinisatClause(clause, minisat_clause);
- d_minisat->addClause(minisat_clause, removable);
+ d_minisat->addClause(minisat_clause, removable, proof_id);
}
SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
d_minisat->push();
}
-void MinisatSatSolver::pop(){
+void MinisatSatSolver::pop() {
d_minisat->pop();
}
static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause);
void initialize(context::Context* context, TheoryProxy* theoryProxy);
- void addClause(SatClause& clause, bool removable);
+ void addClause(SatClause& clause, bool removable, uint64_t proof_id);
SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
SatVariable trueVar() { return d_minisat->trueVar(); }
-bool SimpSolver::addClause_(vec<Lit>& ps, bool removable)
+bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
{
#ifndef NDEBUG
if (use_simplification) {
if (use_rcheck && implied(ps))
return true;
- if (!Solver::addClause_(ps, removable))
+ if (!Solver::addClause_(ps, removable, proof_id))
return false;
if (use_simplification && clauses_persistent.size() == nclauses + 1){
for (int i = 0; i < pos.size(); i++)
for (int j = 0; j < neg.size(); j++) {
bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
- if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable)) {
+ if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) {
return false;
}
}
removeClause(cls[i]);
- if (!addClause_(subst_clause, c.removable())) {
+ if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) {
return ok = false;
}
}
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
- bool addClause (const vec<Lit>& ps, bool removable);
- bool addEmptyClause(bool removable); // Add the empty clause to the solver.
- bool addClause (Lit p, bool removable); // Add a unit clause to the solver.
- bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver.
- bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver.
- bool addClause_(vec<Lit>& ps, bool removable);
+ bool addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id);
+ bool addEmptyClause(bool removable, uint64_t proof_id); // Add the empty clause to the solver.
+ bool addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver.
+ bool addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver.
+ bool addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver.
+ bool addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id);
bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
// Variable mode:
elim_heap.update(v); }
-inline bool SimpSolver::addClause (const vec<Lit>& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id)
+ { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addEmptyClause(bool removable, uint64_t proof_id) { add_tmp.clear(); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addClause (Lit p, bool removable, uint64_t proof_id)
+ { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, uint64_t proof_id)
+ { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id)
+ { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); }
inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
#include "decision/options.h"
#include "theory/theory_engine.h"
#include "theory/theory_registrar.h"
+#include "proof/proof_manager.h"
#include "util/cvc4_assert.h"
#include "options/options.h"
#include "smt/options.h"
Assert(!d_inCheckSat, "Sat solver in solve()!");
Debug("prop") << "assertFormula(" << node << ")" << endl;
// Assert as non-removable
- d_cnfStream->convertAndAssert(node, false, false);
+ d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN);
}
-void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
+void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from) {
//Assert(d_inCheckSat, "Sat solver should be in solve()!");
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
- // Assert as removable
- d_cnfStream->convertAndAssert(node, removable, negated);
+ // Assert as (possibly) removable
+ d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
}
void PropEngine::requirePhase(TNode n, bool phase) {
#include "options/options.h"
#include "util/result.h"
#include "smt/modal_exception.h"
+#include "proof/proof_manager.h"
#include <sys/time.h>
namespace CVC4 {
* @param removable whether this lemma can be quietly removed based
* on an activity heuristic (or not)
*/
- void assertLemma(TNode node, bool negated, bool removable);
+ void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null());
/**
* If ever n is decided upon, it must be in the given phase. This
#include "util/statistics_registry.h"
#include "context/cdlist.h"
#include "prop/sat_solver_types.h"
+#include "expr/node.h"
namespace CVC4 {
namespace prop {
virtual ~SatSolver() { }
/** Assert a clause in the solver. */
- virtual void addClause(SatClause& clause, bool removable) = 0;
+ virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0;
/**
* Create a new boolean variable in the solver.
if(lemmaCount % 1 == 0) {
Debug("shared") << "=) " << asNode << std::endl;
}
- d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true);
+ d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
} else {
Debug("shared") << "=(" << asNode << std::endl;
}
output proofs after every UNSAT/VALID response
option dumpInstantiations --dump-instantiations bool :default false
output instantiations of quantified formulas after every UNSAT/VALID response
-# this is just a placeholder for later; it doesn't show up in command-line options listings
-undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- turn on unsat core generation (NOT YET SUPPORTED)
+option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ turn on unsat core generation
+option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ output unsat cores after every UNSAT/VALID response
+
option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
support the get-assignment command
(MiniSat) propagation for all of them only after reaching a querying command\n\
(CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
\n\
-incremental\n\
-+ run nonclausal simplification and clausal propagation at each ASSERT\n\
- (and at CHECKSAT/QUERY/SUBTYPE)\n\
-\n\
none\n\
+ do not perform nonclausal simplification\n\
";
inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "batch") {
return SIMPLIFICATION_MODE_BATCH;
- } else if(optarg == "incremental") {
- return SIMPLIFICATION_MODE_INCREMENTAL;
} else if(optarg == "none") {
return SIMPLIFICATION_MODE_NONE;
} else if(optarg == "help") {
#endif /* CVC4_PROOF */
}
-inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
- if(value) {
- throw UnrecognizedOptionException("CVC4 does not yet have support for unsatisfiable cores");
- }
-}
-
// This macro is used for setting :regular-output-channel and :diagnostic-output-channel
// to redirect a stream. It maintains all attributes set on the stream.
#define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \
std::ostream& operator<<(std::ostream& out, SimplificationMode mode) {
switch(mode) {
- case SIMPLIFICATION_MODE_INCREMENTAL:
- out << "SIMPLIFICATION_MODE_INCREMENTAL";
- break;
case SIMPLIFICATION_MODE_BATCH:
out << "SIMPLIFICATION_MODE_BATCH";
break;
/** Enumeration of simplification modes (when to simplify). */
typedef enum {
- /** Simplify the assertions as they come in */
- SIMPLIFICATION_MODE_INCREMENTAL,
/** Simplify the assertions all together once a check is requested */
SIMPLIFICATION_MODE_BATCH,
/** Don't do simplification */
#include "theory/bv/theory_bv_rewriter.h"
#include "proof/proof_manager.h"
#include "main/options.h"
+#include "util/unsat_core.h"
#include "util/proof.h"
#include "proof/proof.h"
#include "proof/proof_manager.h"
Node getFormula() const { return d_formula; }
};/* class DefinedFunction */
+class AssertionPipeline {
+ vector<Node> d_nodes;
+
+public:
+
+ size_t size() const { return d_nodes.size(); }
+
+ void resize(size_t n) { d_nodes.resize(n); }
+ void clear() { d_nodes.clear(); }
+
+ Node& operator[](size_t i) { return d_nodes[i]; }
+ const Node& operator[](size_t i) const { return d_nodes[i]; }
+ void push_back(Node n) { d_nodes.push_back(n); }
+
+ vector<Node>& ref() { return d_nodes; }
+ const vector<Node>& ref() const { return d_nodes; }
+
+ void replace(size_t i, Node n) {
+ PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); );
+ d_nodes[i] = n;
+ }
+
+};/* class AssertionPipeline */
+
struct SmtEngineStatistics {
/** time spent in definition-expansion */
TimerStat d_definitionExpansionTime;
TimerStat d_iteRemovalTime;
/** time spent in theory preprocessing */
TimerStat d_theoryPreprocessTime;
+ /** time spent in theory preprocessing */
+ TimerStat d_rewriteApplyToConstTime;
/** time spent converting to CNF */
TimerStat d_cnfConversionTime;
/** Num of assertions before ite removal */
d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
+ d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
StatisticsRegistry::registerStat(&d_unconstrainedSimpTime);
StatisticsRegistry::registerStat(&d_iteRemovalTime);
StatisticsRegistry::registerStat(&d_theoryPreprocessTime);
+ StatisticsRegistry::registerStat(&d_rewriteApplyToConstTime);
StatisticsRegistry::registerStat(&d_cnfConversionTime);
StatisticsRegistry::registerStat(&d_numAssertionsPre);
StatisticsRegistry::registerStat(&d_numAssertionsPost);
StatisticsRegistry::registerStat(&d_checkModelTime);
+ StatisticsRegistry::registerStat(&d_checkProofTime);
StatisticsRegistry::registerStat(&d_solveTime);
StatisticsRegistry::registerStat(&d_pushPopTime);
StatisticsRegistry::registerStat(&d_processAssertionsTime);
StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime);
StatisticsRegistry::unregisterStat(&d_iteRemovalTime);
StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime);
+ StatisticsRegistry::unregisterStat(&d_rewriteApplyToConstTime);
StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
StatisticsRegistry::unregisterStat(&d_checkModelTime);
+ StatisticsRegistry::unregisterStat(&d_checkProofTime);
StatisticsRegistry::unregisterStat(&d_solveTime);
StatisticsRegistry::unregisterStat(&d_pushPopTime);
StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
class SmtEnginePrivate : public NodeManagerListener {
SmtEngine& d_smt;
- /** The assertions yet to be preprocessed */
- vector<Node> d_assertionsToPreprocess;
-
/** Learned literals */
vector<Node> d_nonClausalLearnedLiterals;
bool d_propagatorNeedsFinish;
std::vector<Node> d_boolVars;
- /** Assertions to push to sat */
- vector<Node> d_assertionsToCheck;
+ /** Assertions in the preprocessing pipeline */
+ AssertionPipeline d_assertions;
/** Whether any assertions have been processed */
CDO<bool> d_assertionsProcessed;
public:
/**
- * Map from skolem variables to index in d_assertionsToCheck containing
+ * Map from skolem variables to index in d_assertions containing
* corresponding introduced Boolean ite
*/
IteSkolemMap d_iteSkolemMap;
bool simpITE();
// Simplify based on unconstrained values
- void unconstrainedSimp(std::vector<Node>& assertions);
+ void unconstrainedSimp();
// Ensures the assertions asserted after before now
// effectively come before d_realAssertionsEnd
* (predicate subtype or integer subrange type) must be constrained
* to be in that type.
*/
- void constrainSubtypes(TNode n, std::vector<Node>& assertions)
+ void constrainSubtypes(TNode n, AssertionPipeline& assertions)
throw();
// trace nodes back to their assertions using CircuitPropagator's BackEdgesMap
SmtEnginePrivate(SmtEngine& smt) :
d_smt(smt),
- d_assertionsToPreprocess(),
d_nonClausalLearnedLiterals(),
d_realAssertionsEnd(0),
d_booleanTermConverter(NULL),
d_propagator(d_nonClausalLearnedLiterals, true, true),
d_propagatorNeedsFinish(false),
- d_assertionsToCheck(),
+ d_assertions(),
d_assertionsProcessed(smt.d_userContext, false),
d_substitutionsIndex(smt.d_userContext, 0),
d_fakeContext(),
* someone does a push-assert-pop without a check-sat.
*/
void notifyPop() {
- d_assertionsToPreprocess.clear();
+ d_assertions.clear();
d_nonClausalLearnedLiterals.clear();
- d_assertionsToCheck.clear();
d_realAssertionsEnd = 0;
d_iteSkolemMap.clear();
}
hash_map<Node, Node, NodeHashFunction> cache;
Node n = expandDefinitions(in, cache).toExpr();
// Make sure we've done all preprocessing, etc.
- Assert(d_assertionsToCheck.size() == 0 && d_assertionsToPreprocess.size() == 0);
+ Assert(d_assertions.size() == 0);
return applySubstitutions(n).toExpr();
}
}
}
+ if(options::unsatCores()) {
+ if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
+ if(options::simplificationMode.wasSetByUser()) {
+ throw OptionException("simplification not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off simplification to support unsat-cores" << endl;
+ options::simplificationMode.set(SIMPLIFICATION_MODE_NONE);
+ }
+
+ if(options::unconstrainedSimp()) {
+ if(options::unconstrainedSimp.wasSetByUser()) {
+ throw OptionException("unconstrained simplification not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl;
+ options::unconstrainedSimp.set(false);
+ }
+
+ if(options::pbRewrites()) {
+ if(options::pbRewrites.wasSetByUser()) {
+ throw OptionException("pseudoboolean rewrites not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl;
+ setOption("pb-rewrites", false);
+ }
+
+ if(options::sortInference()) {
+ if(options::sortInference.wasSetByUser()) {
+ throw OptionException("sort inference not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl;
+ options::sortInference.set(false);
+ }
+
+ if(options::preSkolemQuant()) {
+ if(options::preSkolemQuant.wasSetByUser()) {
+ throw OptionException("pre-skolemization not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl;
+ options::preSkolemQuant.set(false);
+ }
+
+ if(options::bitvectorToBool()) {
+ if(options::bitvectorToBool.wasSetByUser()) {
+ throw OptionException("bv-to-bool not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off bitvector-to-bool support unsat-cores" << endl;
+ options::bitvectorToBool.set(false);
+ }
+
+ if(options::bvIntroducePow2()) {
+ if(options::bvIntroducePow2.wasSetByUser()) {
+ throw OptionException("bv-intro-pow2 not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl;
+ setOption("bv-intro-pow2", false);
+ }
+ }
+
if(options::produceAssignments() && !options::produceModels()) {
Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl;
setOption("produce-models", SExpr("true"));
Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
// Remove all of the ITE occurrences and normalize
- d_iteRemover.run(d_assertionsToCheck, d_iteSkolemMap);
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- d_assertionsToCheck[i] = Rewriter::rewrite(d_assertionsToCheck[i]);
+ d_iteRemover.run(d_assertions.ref(), d_iteSkolemMap, true);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
}
-
}
void SmtEnginePrivate::staticLearning() {
Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl;
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
NodeBuilder<> learned(kind::AND);
- learned << d_assertionsToCheck[i];
- d_smt.d_theoryEngine->ppStaticLearn(d_assertionsToCheck[i], learned);
+ learned << d_assertions[i];
+ d_smt.d_theoryEngine->ppStaticLearn(d_assertions[i], learned);
if(learned.getNumChildren() == 1) {
learned.clear();
} else {
- d_assertionsToCheck[i] = learned;
+ d_assertions.replace(i, learned);
}
}
}
// do dumping (before/after any preprocessing pass)
-static void dumpAssertions(const char* key,
- const std::vector<Node>& assertionList) {
+static void dumpAssertions(const char* key, const AssertionPipeline& assertionList) {
if( Dump.isOn("assertions") &&
Dump.isOn(string("assertions:") + key) ) {
// Push the simplified assertions to the dump output stream
// Assert all the assertions to the propagator
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "asserting to propagator" << endl;
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- Assert(Rewriter::rewrite(d_assertionsToPreprocess[i]) == d_assertionsToPreprocess[i]);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
// Don't reprocess substitutions
if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) {
continue;
}
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << endl;
- d_propagator.assertTrue(d_assertionsToPreprocess[i]);
+ Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl;
+ Debug("cores") << "d_propagator assertTrue: " << d_assertions[i] << std::endl;
+ d_propagator.assertTrue(d_assertions[i]);
}
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
// If in conflict, just return false
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict in non-clausal propagation" << endl;
- d_assertionsToPreprocess.clear();
- d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ Node falseNode = NodeManager::currentNM()->mkConst<bool>(false);
+ Assert(!options::unsatCores());
+ d_assertions.clear();
+ d_assertions.push_back(falseNode);
d_propagatorNeedsFinish = true;
return false;
}
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict with "
<< d_nonClausalLearnedLiterals[i] << endl;
- d_assertionsToPreprocess.clear();
- d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ Assert(!options::unsatCores());
+ d_assertions.clear();
+ d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
d_propagatorNeedsFinish = true;
return false;
}
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict while solving "
<< learnedLiteral << endl;
- d_assertionsToPreprocess.clear();
- d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ Assert(!options::unsatCores());
+ d_assertions.clear();
+ d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
d_propagatorNeedsFinish = true;
return false;
default:
// constantPropagations.simplifyLHS(t, c, equations, true);
// if (!equations.empty()) {
// Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
- // d_assertionsToPreprocess.clear();
- // d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ // d_assertions.clear();
+ // d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
// return;
// }
// d_topLevelSubstitutions.simplifyRHS(constantPropagations);
hash_set<TNode, TNodeHashFunction> s;
Trace("debugging") << "NonClausal simplify pre-preprocess\n";
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- Node assertion = d_assertionsToPreprocess[i];
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Node assertion = d_assertions[i];
Node assertionNew = newSubstitutions.apply(assertion);
Trace("debugging") << "assertion = " << assertion << endl;
Trace("debugging") << "assertionNew = " << assertionNew << endl;
}
Trace("debugging") << "\n";
s.insert(assertion);
- d_assertionsToCheck.push_back(assertion);
+ d_assertions.replace(i, assertion);
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "non-clausal preprocessed: "
<< assertion << endl;
}
- d_assertionsToPreprocess.clear();
// If in incremental mode, add substitutions to the list of assertions
if (d_substitutionsIndex > 0) {
NodeBuilder<> substitutionsBuilder(kind::AND);
- substitutionsBuilder << d_assertionsToCheck[d_substitutionsIndex];
+ substitutionsBuilder << d_assertions[d_substitutionsIndex];
pos = newSubstitutions.begin();
for (; pos != newSubstitutions.end(); ++pos) {
// Add back this substitution as an assertion
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
}
if (substitutionsBuilder.getNumChildren() > 1) {
- d_assertionsToCheck[d_substitutionsIndex] =
- Rewriter::rewrite(Node(substitutionsBuilder));
+ d_assertions.replace(d_substitutionsIndex,
+ Rewriter::rewrite(Node(substitutionsBuilder)));
}
} else {
// If not in incremental mode, must add substitutions to model
}
NodeBuilder<> learnedBuilder(kind::AND);
- Assert(d_realAssertionsEnd <= d_assertionsToCheck.size());
- learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd - 1];
+ Assert(d_realAssertionsEnd <= d_assertions.size());
+ learnedBuilder << d_assertions[d_realAssertionsEnd - 1];
for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
Node learned = d_nonClausalLearnedLiterals[i];
}
d_nonClausalLearnedLiterals.clear();
-
for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
Node cProp = (*pos).first.eqNode((*pos).second);
Assert(d_topLevelSubstitutions.apply(cProp) == cProp);
d_topLevelSubstitutions.addSubstitutions(newSubstitutions);
if(learnedBuilder.getNumChildren() > 1) {
- d_assertionsToCheck[d_realAssertionsEnd - 1] =
- Rewriter::rewrite(Node(learnedBuilder));
+ d_assertions.replace(d_realAssertionsEnd - 1,
+ Rewriter::rewrite(Node(learnedBuilder)));
}
d_propagatorNeedsFinish = true;
void SmtEnginePrivate::bvAbstraction() {
Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl;
std::vector<Node> new_assertions;
- bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertionsToPreprocess, new_assertions);
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]);
+ bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertions.ref(), new_assertions);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
}
// if we are using the lazy solver and the abstraction
// applies, then UF symbols were introduced
void SmtEnginePrivate::bvToBool() {
Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
std::vector<Node> new_assertions;
- d_smt.d_theoryEngine->ppBvToBool(d_assertionsToPreprocess, new_assertions);
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]);
+ d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
}
}
Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
- unsigned numAssertionOnEntry = d_assertionsToCheck.size();
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
- Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
- d_assertionsToCheck[i] = result;
+ unsigned numAssertionOnEntry = d_assertions.size();
+ for (unsigned i = 0; i < d_assertions.size(); ++i) {
+ Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]);
+ d_assertions.replace(i, result);
if(result.isConst() && !result.getConst<bool>()){
return false;
}
}
- bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertionsToCheck);
- if(numAssertionOnEntry < d_assertionsToCheck.size()){
+ bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertions.ref());
+ if(numAssertionOnEntry < d_assertions.size()){
compressBeforeRealAssertions(numAssertionOnEntry);
}
return result;
}
void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
- size_t curr = d_assertionsToCheck.size();
+ size_t curr = d_assertions.size();
if(before >= curr ||
d_realAssertionsEnd <= 0 ||
d_realAssertionsEnd >= curr){
std::vector<Node> intoConjunction;
for(size_t i = before; i<curr; ++i){
- intoConjunction.push_back(d_assertionsToCheck[i]);
+ intoConjunction.push_back(d_assertions[i]);
}
- d_assertionsToCheck.resize(before);
+ d_assertions.resize(before);
size_t lastBeforeItes = d_realAssertionsEnd - 1;
- intoConjunction.push_back(d_assertionsToCheck[lastBeforeItes]);
+ intoConjunction.push_back(d_assertions[lastBeforeItes]);
Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
- d_assertionsToCheck[lastBeforeItes] = newLast;
- Assert(d_assertionsToCheck.size() == before);
+ d_assertions.replace(lastBeforeItes, newLast);
+ Assert(d_assertions.size() == before);
}
-void SmtEnginePrivate::unconstrainedSimp(std::vector<Node>& assertions) {
+void SmtEnginePrivate::unconstrainedSimp() {
TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
- d_smt.d_theoryEngine->ppUnconstrainedSimp(assertions);
+ d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
}
-void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
+void SmtEnginePrivate::constrainSubtypes(TNode top, AssertionPipeline& assertions)
throw() {
Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
}
void SmtEnginePrivate::doMiplibTrick() {
- Assert(d_assertionsToPreprocess.empty());
- Assert(d_realAssertionsEnd == d_assertionsToCheck.size());
+ Assert(d_realAssertionsEnd == d_assertions.size());
Assert(!options::incrementalSolving());
const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
Node newVar = nm->mkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME);
Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
- d_assertionsToCheck.push_back(Rewriter::rewrite(geq.andNode(leq)));
+ d_assertions.push_back(Rewriter::rewrite(geq.andNode(leq)));
SubstitutionMap nullMap(&d_fakeContext);
Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
status = d_smt.d_theoryEngine->solve(geq, nullMap);
}
newAssertion = Rewriter::rewrite(newAssertion);
Debug("miplib") << " " << newAssertion << endl;
- d_assertionsToCheck.push_back(newAssertion);
+ d_assertions.push_back(newAssertion);
Debug("miplib") << " assertions to remove: " << endl;
for(vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) {
Debug("miplib") << " " << *k << endl;
if(!removeAssertions.empty()) {
Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl;
for(size_t i = 0; i < d_realAssertionsEnd; ++i) {
- if(removeAssertions.find(d_assertionsToCheck[i].getId()) != removeAssertions.end()) {
- Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertionsToCheck[i] << endl;
- d_assertionsToCheck[i] = d_true;
+ if(removeAssertions.find(d_assertions[i].getId()) != removeAssertions.end()) {
+ Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions[i] << endl;
+ d_assertions[i] = d_true;
++d_smt.d_stats->d_numMiplibAssertionsRemoved;
- } else if(d_assertionsToCheck[i].getKind() == kind::AND) {
- size_t removals = removeFromConjunction(d_assertionsToCheck[i], removeAssertions);
+ } else if(d_assertions[i].getKind() == kind::AND) {
+ size_t removals = removeFromConjunction(d_assertions[i], removeAssertions);
if(removals > 0) {
- Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertionsToCheck[i] << endl;
+ Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions[i] << endl;
Debug("miplib") << "SmtEnginePrivate::simplify(): - by " << removals << " conjuncts" << endl;
d_smt.d_stats->d_numMiplibAssertionsRemoved += removals;
}
}
- Debug("miplib") << "had: " << d_assertionsToCheck[i] << endl;
- d_assertionsToCheck[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToCheck[i]));
- Debug("miplib") << "now: " << d_assertionsToCheck[i] << endl;
+ Debug("miplib") << "had: " << d_assertions[i] << endl;
+ d_assertions[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]));
+ Debug("miplib") << "now: " << d_assertions[i] << endl;
}
} else {
Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl;
}
- d_realAssertionsEnd = d_assertionsToCheck.size();
+ d_realAssertionsEnd = d_assertions.size();
}
// we add new assertions and need this (in practice, this
// restriction only disables miplib processing during
// re-simplification, which we don't expect to be useful anyway)
- d_realAssertionsEnd == d_assertionsToCheck.size() ) {
+ d_realAssertionsEnd == d_assertions.size() ) {
Chat() << "...fixing miplib encodings..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< "looking for miplib pseudobooleans..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl;
}
- } else {
- Assert(d_assertionsToCheck.empty());
- d_assertionsToCheck.swap(d_assertionsToPreprocess);
}
- dumpAssertions("post-nonclausal", d_assertionsToCheck);
+ dumpAssertions("post-nonclausal", d_assertions);
Trace("smt") << "POST nonClausalSimplify" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// before ppRewrite check if only core theory for BV theory
- d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertionsToCheck);
+ d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref());
+
+ dumpAssertions("pre-theorypp", d_assertions);
// Theory preprocessing
if (d_smt.d_earlyTheoryPP) {
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
// Call the theory preprocessors
d_smt.d_theoryEngine->preprocessStart();
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- Assert(Rewriter::rewrite(d_assertionsToCheck[i]) == d_assertionsToCheck[i]);
- d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
- Assert(Rewriter::rewrite(d_assertionsToCheck[i]) == d_assertionsToCheck[i]);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
+ d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
+ Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
}
}
- dumpAssertions("post-theorypp", d_assertionsToCheck);
+ dumpAssertions("post-theorypp", d_assertions);
Trace("smt") << "POST theoryPP" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// ITE simplification
if(options::doITESimp() &&
}
}
- dumpAssertions("post-itesimp", d_assertionsToCheck);
+ dumpAssertions("post-itesimp", d_assertions);
Trace("smt") << "POST iteSimp" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// Unconstrained simplification
if(options::unconstrainedSimp()) {
Chat() << "...doing unconstrained simplification..." << endl;
- unconstrainedSimp(d_assertionsToCheck);
+ unconstrainedSimp();
}
- dumpAssertions("post-unconstrained", d_assertionsToCheck);
+ dumpAssertions("post-unconstrained", d_assertions);
Trace("smt") << "POST unconstrainedSimp" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
Chat() << "...doing another round of nonclausal simplification..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< " doing repeated simplification" << endl;
- d_assertionsToCheck.swap(d_assertionsToPreprocess);
- Assert(d_assertionsToCheck.empty());
bool noConflict = nonClausalSimplify();
if(!noConflict) {
return false;
}
}
- dumpAssertions("post-repeatsimp", d_assertionsToCheck);
+ dumpAssertions("post-repeatsimp", d_assertions);
Trace("smt") << "POST repeatSimp" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
} catch(TypeCheckingExceptionPrivate& tcep) {
// Calls to this function should have already weeded out any
Assert(d_smt.d_pendingPops == 0);
// Dump the assertions
- dumpAssertions("pre-everything", d_assertionsToPreprocess);
+ dumpAssertions("pre-everything", d_assertions);
Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
-
- Assert(d_assertionsToCheck.size() == 0);
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- if (d_assertionsToPreprocess.size() == 0) {
+ if (d_assertions.size() == 0) {
// nothing to do
return;
}
- if (d_assertionsProcessed &&
- ( options::incrementalSolving() ||
- options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL )) {
+ if (d_assertionsProcessed && options::incrementalSolving()) {
// Placeholder for storing substitutions
- d_substitutionsIndex = d_assertionsToPreprocess.size();
- d_assertionsToPreprocess.push_back(NodeManager::currentNM()->mkConst<bool>(true));
+ d_substitutionsIndex = d_assertions.size();
+ d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
}
// Add dummy assertion in last position - to be used as a
// placeholder for any new assertions to get added
- d_assertionsToPreprocess.push_back(NodeManager::currentNM()->mkConst<bool>(true));
+ d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
// any assertions added beyond realAssertionsEnd must NOT affect the
// equisatisfiability
- d_realAssertionsEnd = d_assertionsToPreprocess.size();
+ d_realAssertionsEnd = d_assertions.size();
// Assertions are NOT guaranteed to be rewritten by this point
- dumpAssertions("pre-definition-expansion", d_assertionsToPreprocess);
+ dumpAssertions("pre-definition-expansion", d_assertions);
{
Chat() << "expanding definitions..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
hash_map<Node, Node, NodeHashFunction> cache;
- for(unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- d_assertionsToPreprocess[i] =
- expandDefinitions(d_assertionsToPreprocess[i], cache);
+ for(unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
}
}
- dumpAssertions("post-definition-expansion", d_assertionsToPreprocess);
+ dumpAssertions("post-definition-expansion", d_assertions);
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
!d_smt.d_logic.isPure(THEORY_BV)) {
}
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess);
+ d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertions.ref());
}
if ( options::bvAbstraction() &&
!options::incrementalSolving()) {
- dumpAssertions("pre-bv-abstraction", d_assertionsToPreprocess);
+ dumpAssertions("pre-bv-abstraction", d_assertions);
bvAbstraction();
- dumpAssertions("post-bv-abstraction", d_assertionsToPreprocess);
+ dumpAssertions("post-bv-abstraction", d_assertions);
}
- dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
+ dumpAssertions("pre-boolean-terms", d_assertions);
{
Chat() << "rewriting Boolean terms..." << endl;
- for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
- d_assertionsToPreprocess[i] = rewriteBooleanTerms(d_assertionsToPreprocess[i]);
+ for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
+ d_assertions.replace(i, rewriteBooleanTerms(d_assertions[i]));
}
}
- dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);
+ dumpAssertions("post-boolean-terms", d_assertions);
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- dumpAssertions("pre-constrain-subtypes", d_assertionsToPreprocess);
+ dumpAssertions("pre-constrain-subtypes", d_assertions);
{
// Any variables of subtype types need to be constrained properly.
// Careful, here: constrainSubtypes() adds to the back of
- // d_assertionsToPreprocess, but we don't need to reprocess those.
+ // d_assertions, but we don't need to reprocess those.
// We also can't use an iterator, because the vector may be moved in
// memory during this loop.
Chat() << "constraining subtypes..." << endl;
- for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
- constrainSubtypes(d_assertionsToPreprocess[i], d_assertionsToPreprocess);
+ for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
+ constrainSubtypes(d_assertions[i], d_assertions);
}
}
- dumpAssertions("post-constrain-subtypes", d_assertionsToPreprocess);
+ dumpAssertions("post-constrain-subtypes", d_assertions);
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
+ bool noConflict = true;
// Unconstrained simplification
if(options::unconstrainedSimp()) {
- dumpAssertions("pre-unconstrained-simp", d_assertionsToPreprocess);
+ dumpAssertions("pre-unconstrained-simp", d_assertions);
Chat() << "...doing unconstrained simplification..." << endl;
- unconstrainedSimp(d_assertionsToPreprocess);
- dumpAssertions("post-unconstrained-simp", d_assertionsToPreprocess);
+ unconstrainedSimp();
+ dumpAssertions("post-unconstrained-simp", d_assertions);
}
if(options::bvIntroducePow2()){
- theory::bv::BVIntroducePow2::pow2Rewrite(d_assertionsToPreprocess);
+ theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref());
}
- dumpAssertions("pre-substitution", d_assertionsToPreprocess);
+ dumpAssertions("pre-substitution", d_assertions);
- // Apply the substitutions we already have, and normalize
- Chat() << "applying substitutions..." << endl;
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "applying substitutions" << endl;
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << endl;
- d_assertionsToPreprocess[i] =
- Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
- Trace("simplify") << " got " << d_assertionsToPreprocess[i] << endl;
+ if(options::unsatCores()) {
+ // special rewriting pass for unsat cores, since many of the passes below are skipped
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
+ }
+ } else {
+ // Apply the substitutions we already have, and normalize
+ if(!options::unsatCores()) {
+ Chat() << "applying substitutions..." << endl;
+ Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+ << "applying substitutions" << endl;
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Trace("simplify") << "applying to " << d_assertions[i] << endl;
+ d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
+ Trace("simplify") << " got " << d_assertions[i] << endl;
+ }
+ }
}
- dumpAssertions("post-substitution", d_assertionsToPreprocess);
- // Assertions ARE guaranteed to be rewritten by this point
+ dumpAssertions("post-substitution", d_assertions);
+ // Assertions ARE guaranteed to be rewritten by this point
// Lift bit-vectors of size 1 to bool
if(options::bitvectorToBool()) {
- dumpAssertions("pre-bv-to-bool", d_assertionsToPreprocess);
+ dumpAssertions("pre-bv-to-bool", d_assertions);
Chat() << "...doing bvToBool..." << endl;
bvToBool();
- dumpAssertions("post-bv-to-bool", d_assertionsToPreprocess);
+ dumpAssertions("post-bv-to-bool", d_assertions);
}
if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
- dumpAssertions("pre-strings-pp", d_assertionsToPreprocess);
+ dumpAssertions("pre-strings-pp", d_assertions);
CVC4::theory::strings::StringsPreprocess sp;
std::vector<Node> newNodes;
- newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]);
- sp.simplify( d_assertionsToPreprocess, newNodes );
+ newNodes.push_back(d_assertions[d_realAssertionsEnd - 1]);
+ sp.simplify( d_assertions.ref(), newNodes );
if(newNodes.size() > 1) {
- d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
+ d_assertions[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
}
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions[i] = Rewriter::rewrite( d_assertions[i] );
}
- dumpAssertions("post-strings-pp", d_assertionsToPreprocess);
+ dumpAssertions("post-strings-pp", d_assertions);
}
if( d_smt.d_logic.isQuantified() ){
//remove rewrite rules
- for( unsigned i=0; i < d_assertionsToPreprocess.size(); i++ ) {
- if( d_assertionsToPreprocess[i].getKind() == kind::REWRITE_RULE ){
- Node prev = d_assertionsToPreprocess[i];
+ for( unsigned i=0; i < d_assertions.size(); i++ ) {
+ if( d_assertions[i].getKind() == kind::REWRITE_RULE ){
+ Node prev = d_assertions[i];
Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl;
- d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertionsToPreprocess[i] ) );
+ d_assertions[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) );
Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl;
- Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl;
+ Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl;
}
}
- dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
+ dumpAssertions("pre-skolem-quant", d_assertions);
if( options::preSkolemQuant() ){
//apply pre-skolemization to existential quantifiers
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- Node prev = d_assertionsToPreprocess[i];
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Node prev = d_assertions[i];
Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl;
vector< TypeNode > fvTypes;
vector< TNode > fvs;
- d_assertionsToPreprocess[i] = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
- if( prev!=d_assertionsToPreprocess[i] ){
- d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+ d_assertions.replace(i, quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ));
+ if( prev!=d_assertions[i] ){
+ d_assertions.replace(i, Rewriter::rewrite( d_assertions[i] ));
Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
- Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl;
+ Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl;
}
}
}
- dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
+ dumpAssertions("post-skolem-quant", d_assertions);
if( options::macrosQuant() ){
//quantifiers macro expansion
bool success;
do{
quantifiers::QuantifierMacros qm;
- success = qm.simplify( d_assertionsToPreprocess, true );
+ success = qm.simplify( d_assertions.ref(), true );
}while( success );
}
Trace("fo-rsn-enable") << std::endl;
if( options::foPropQuant() ){
quantifiers::FirstOrderPropagation fop;
- fop.simplify( d_assertionsToPreprocess );
+ fop.simplify( d_assertions.ref() );
}
}
if( options::sortInference() ){
//sort inference technique
SortInference * si = d_smt.d_theoryEngine->getSortInference();
- si->simplify( d_assertionsToPreprocess );
+ si->simplify( d_assertions.ref() );
for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){
d_smt.setPrintFuncInModel( it->first.toExpr(), false );
d_smt.setPrintFuncInModel( it->second.toExpr(), true );
}
//if( options::quantConflictFind() ){
- // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertionsToPreprocess );
+ // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertions );
//}
if( options::pbRewrites() ){
- d_pbsProcessor.learn(d_assertionsToPreprocess);
+ d_pbsProcessor.learn(d_assertions.ref());
if(d_pbsProcessor.likelyToHelp()){
- d_pbsProcessor.applyReplacements(d_assertionsToPreprocess);
+ d_pbsProcessor.applyReplacements(d_assertions.ref());
}
}
- dumpAssertions("pre-simplify", d_assertionsToPreprocess);
+ dumpAssertions("pre-simplify", d_assertions);
Chat() << "simplifying assertions..." << endl;
- bool noConflict = simplifyAssertions();
+ noConflict = simplifyAssertions();
if(!noConflict){
++(d_smt.d_stats->d_simplifiedToFalse);
}
- dumpAssertions("post-simplify", d_assertionsToCheck);
+ dumpAssertions("post-simplify", d_assertions);
- dumpAssertions("pre-static-learning", d_assertionsToCheck);
+ dumpAssertions("pre-static-learning", d_assertions);
if(options::doStaticLearning()) {
// Perform static learning
Chat() << "doing static learning..." << endl;
<< "performing static learning" << endl;
staticLearning();
}
- dumpAssertions("post-static-learning", d_assertionsToCheck);
+ dumpAssertions("post-static-learning", d_assertions);
Trace("smt") << "POST bvToBool" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- dumpAssertions("pre-ite-removal", d_assertionsToCheck);
+ dumpAssertions("pre-ite-removal", d_assertions);
{
Chat() << "removing term ITEs..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime);
// Remove ITEs, updating d_iteSkolemMap
- d_smt.d_stats->d_numAssertionsPre += d_assertionsToCheck.size();
+ d_smt.d_stats->d_numAssertionsPre += d_assertions.size();
removeITEs();
- d_smt.d_stats->d_numAssertionsPost += d_assertionsToCheck.size();
+ d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
}
- dumpAssertions("post-ite-removal", d_assertionsToCheck);
+ dumpAssertions("post-ite-removal", d_assertions);
- dumpAssertions("pre-repeat-simplify", d_assertionsToCheck);
+ dumpAssertions("pre-repeat-simplify", d_assertions);
if(options::repeatSimp()) {
- d_assertionsToCheck.swap(d_assertionsToPreprocess);
Chat() << "re-simplifying assertions..." << endl;
ScopeCounter depth(d_simplifyAssertionsDepth);
noConflict &= simplifyAssertions();
IteSkolemMap::iterator it = d_iteSkolemMap.begin();
IteSkolemMap::iterator iend = d_iteSkolemMap.end();
NodeBuilder<> builder(kind::AND);
- builder << d_assertionsToCheck[d_realAssertionsEnd - 1];
+ builder << d_assertions[d_realAssertionsEnd - 1];
vector<TNode> toErase;
for (; it != iend; ++it) {
if (skolemSet.find((*it).first) == skolemSet.end()) {
- TNode iteExpr = d_assertionsToCheck[(*it).second];
+ TNode iteExpr = d_assertions[(*it).second];
if (iteExpr.getKind() == kind::ITE &&
iteExpr[1].getKind() == kind::EQUAL &&
iteExpr[1][0] == (*it).first &&
}
}
// Move this iteExpr into the main assertions
- builder << d_assertionsToCheck[(*it).second];
- d_assertionsToCheck[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true);
+ builder << d_assertions[(*it).second];
+ d_assertions[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true);
toErase.push_back((*it).first);
}
if(builder.getNumChildren() > 1) {
d_iteSkolemMap.erase(toErase.back());
toErase.pop_back();
}
- d_assertionsToCheck[d_realAssertionsEnd - 1] =
+ d_assertions[d_realAssertionsEnd - 1] =
Rewriter::rewrite(Node(builder));
}
// For some reason this is needed for some benchmarks, such as
// http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
// Figure it out later
removeITEs();
- // Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
+ // Assert(iteRewriteAssertionsEnd == d_assertions.size());
}
}
- dumpAssertions("post-repeat-simplify", d_assertionsToCheck);
+ dumpAssertions("post-repeat-simplify", d_assertions);
- dumpAssertions("pre-rewrite-apply-to-const", d_assertionsToCheck);
+ dumpAssertions("pre-rewrite-apply-to-const", d_assertions);
if(options::rewriteApplyToConst()) {
Chat() << "Rewriting applies to constants..." << endl;
- TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- d_assertionsToCheck[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertionsToCheck[i]));
+ TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteApplyToConstTime);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertions[i]));
}
}
- dumpAssertions("post-rewrite-apply-to-const", d_assertionsToCheck);
+ dumpAssertions("post-rewrite-apply-to-const", d_assertions);
// begin: INVARIANT to maintain: no reordering of assertions or
// introducing new ones
#ifdef CVC4_ASSERTIONS
- unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size();
+ unsigned iteRewriteAssertionsEnd = d_assertions.size();
#endif
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- dumpAssertions("pre-theory-preprocessing", d_assertionsToCheck);
+ dumpAssertions("pre-theory-preprocessing", d_assertions);
{
Chat() << "theory preprocessing..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
// Call the theory preprocessors
d_smt.d_theoryEngine->preprocessStart();
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
}
}
- dumpAssertions("post-theory-preprocessing", d_assertionsToCheck);
+ dumpAssertions("post-theory-preprocessing", d_assertions);
// If we are using eager bit-blasting wrap assertions in fake atom so that
// everything gets bit-blasted to internal SAT solver
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
- TNode atom = d_assertionsToCheck[i];
+ for (unsigned i = 0; i < d_assertions.size(); ++i) {
+ TNode atom = d_assertions[i];
Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
- d_assertionsToCheck[i] = eager_atom;
+ d_assertions.replace(i, eager_atom);
TheoryModel* m = d_smt.d_theoryEngine->getModel();
m->addSubstitution(eager_atom, atom);
}
// Push the formula to decision engine
if(noConflict) {
Chat() << "pushing to decision engine..." << endl;
- Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
+ Assert(iteRewriteAssertionsEnd == d_assertions.size());
d_smt.d_decisionEngine->addAssertions
- (d_assertionsToCheck, d_realAssertionsEnd, d_iteSkolemMap);
+ (d_assertions.ref(), d_realAssertionsEnd, d_iteSkolemMap);
}
// end: INVARIANT to maintain: no reordering of assertions or
// introducing new ones
- dumpAssertions("post-everything", d_assertionsToCheck);
+ dumpAssertions("post-everything", d_assertions);
//set instantiation level of everything to zero
if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
- for( unsigned i=0; i < d_assertionsToCheck.size(); i++ ) {
- theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertionsToCheck[i], 0 );
+ for( unsigned i=0; i < d_assertions.size(); i++ ) {
+ theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertions[i], 0 );
}
}
-
// Push the formula to SAT
{
Chat() << "converting to CNF..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Chat() << "+ " << d_assertions[i] << std::endl;
+ d_smt.d_propEngine->assertFormula(d_assertions[i]);
}
}
d_assertionsProcessed = true;
- d_assertionsToCheck.clear();
+ d_assertions.clear();
d_iteSkolemMap.clear();
}
Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
// Add the normalized formula to the queue
- d_assertionsToPreprocess.push_back(n);
- //d_assertionsToPreprocess.push_back(Rewriter::rewrite(n));
-
- // If the mode of processing is incremental prepreocess and assert immediately
- if (options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL) {
- processAssertions();
- }
+ d_assertions.push_back(n);
+ //d_assertions.push_back(Rewriter::rewrite(n));
}
void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
}
}
-Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
+Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
// Ensure expr is type-checked at this point.
ensureBoolean(e);
// Give it to proof manager
- PROOF( ProofManager::currentPM()->addAssertion(e); );
+ PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); );
}
// check to see if a postsolve() is pending
return r;
}/* SmtEngine::checkSat() */
-Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
+Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
Assert(!ex.isNull());
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
// Ensure that the expression is type-checked at this point, and Boolean
ensureBoolean(e);
// Give it to proof manager
- PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); );
+ PROOF( ProofManager::currentPM()->addAssertion(e.notExpr(), inUnsatCore); );
// check to see if a postsolve() is pending
if(d_needPostsolve) {
return r;
}/* SmtEngine::query() */
-Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) {
+Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException) {
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
- PROOF( ProofManager::currentPM()->addAssertion(ex); );
+ PROOF( ProofManager::currentPM()->addAssertion(ex, inUnsatCore); );
Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
}
d_private->addFormula(e.getNode());
return quickCheck().asValidityResult();
-}
+}/* SmtEngine::assertFormula() */
Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
ModelPostprocessor mpost;
Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
}
+UnsatCore SmtEngine::getUnsatCore() throw(ModalException) {
+ Trace("smt") << "SMT getUnsatCore()" << endl;
+ SmtScope smts(this);
+ finalOptionsAreSet();
+ if(Dump.isOn("benchmark")) {
+ Dump("benchmark") << GetUnsatCoreCommand();
+ }
+#ifdef CVC4_PROOF
+ if(!options::unsatCores()) {
+ throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off.");
+ }
+ if(d_status.isNull() ||
+ d_status.asSatisfiabilityResult() != Result::UNSAT ||
+ d_problemExtended) {
+ throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.");
+ }
+
+ delete d_proofManager->getProof(this);// just to trigger core creation
+ return UnsatCore(d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core());
+#else /* CVC4_PROOF */
+ throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
+#endif /* CVC4_PROOF */
+}
+
Proof* SmtEngine::getProof() throw(ModalException) {
Trace("smt") << "SMT getProof()" << endl;
SmtScope smts(this);
}
#ifdef CVC4_PROOF
if(!options::proof()) {
- const char* msg =
- "Cannot get a proof when produce-proofs option is off.";
- throw ModalException(msg);
+ throw ModalException("Cannot get a proof when produce-proofs option is off.");
}
if(d_status.isNull() ||
d_status.asSatisfiabilityResult() != Result::UNSAT ||
d_problemExtended) {
- const char* msg =
- "Cannot get a proof unless immediately preceded by UNSAT/VALID response.";
- throw ModalException(msg);
+ throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response.");
}
return ProofManager::getProof(this);
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/proof.h"
+#include "util/unsat_core.h"
#include "smt/modal_exception.h"
#include "smt/logic_exception.h"
#include "options/options.h"
smt::SmtEnginePrivate* d_private;
/**
- * Check that a generated Proof (via getProof()) checks.
+ * Check that a generated proof (via getProof()) checks.
*/
void checkProof();
/**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
- * literals and conjunction of literals. Returns false iff
- * inconsistent.
+ * literals and conjunction of literals. Returns false if
+ * immediately determined to be inconsistent.
*/
void defineFunction(Expr func,
const std::vector<Expr>& formals,
/**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
- * literals and conjunction of literals. Returns false iff
- * inconsistent.
+ * literals and conjunction of literals. Returns false if
+ * immediately determined to be inconsistent. This version
+ * takes a Boolean flag to determine whether to include this asserted
+ * formula in an unsat core (if one is later requested).
*/
- Result assertFormula(const Expr& e) throw(TypeCheckingException, LogicException);
+ Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException);
/**
* Check validity of an expression with respect to the current set
* of assertions by asserting the query expression's negation and
* calling check(). Returns valid, invalid, or unknown result.
*/
- Result query(const Expr& e) throw(TypeCheckingException, ModalException, LogicException);
+ Result query(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
/**
* Assert a formula (if provided) to the current context and call
* check(). Returns sat, unsat, or unknown result.
*/
- Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException, LogicException);
+ Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
/**
* Simplify a formula without doing "much" work. Does not involve
*/
void printInstantiations( std::ostream& out );
+ /**
+ * Get an unsatisfiable core (only if immediately preceded by an
+ * UNSAT or VALID query). Only permitted if CVC4 was built with
+ * unsat-core support and produce-unsat-cores is on.
+ */
+ UnsatCore getUnsatCore() throw(ModalException);
+
/**
* Get the current set of assertions. Only permitted if the
* SmtEngine is set to operate interactively.
}
inline ProofManager* currentProofManager() {
- Assert(PROOF_ON());
+#ifdef CVC4_PROOF
+ Assert(options::proof() || options::unsatCores());
Assert(s_smtEngine_current != NULL);
return s_smtEngine_current->d_proofManager;
+#else /* CVC4_PROOF */
+ InternalError("proofs/unsat cores are not on, but ProofManager requested");
+ return NULL;
+#endif /* CVC4_PROOF */
}
class SmtScope : public NodeManagerScope {
}
}
- // Get the current assignement
+ // Get the current assignment
AssignmentStatus state = d_state[n];
if(state != UNASSIGNED) {
}
void EagerBitblaster::bbFormula(TNode node) {
- d_cnfStream->convertAndAssert(node, false, false);
+ d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, TNode::null());
}
/**
AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
storeBBAtom(node, atom_definition);
- d_cnfStream->convertAndAssert(atom_definition, false, false);
+ d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
}
void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
Assert (!atom_bb.isNull());
Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
storeBBAtom(node, atom_bb);
- d_cnfStream->convertAndAssert(atom_definition, false, false);
+ d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
return;
}
// asserting that the atom is true iff the definition holds
Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
storeBBAtom(node, atom_bb);
- d_cnfStream->convertAndAssert(atom_definition, false, false);
+ d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
}
void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
#include "smt/logic_exception.h"
+#include "proof/proof_manager.h"
+
#include "util/node_visitor.h"
#include "util/ite_removal.h"
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
- PROOF (ProofManager::currentPM()->initTheoryProof(); );
+ PROOF (ProofManager::initTheoryProof(); );
d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
}
// assert to prop engine
- d_propEngine->assertLemma(additionalLemmas[0], negated, removable);
+ d_propEngine->assertLemma(additionalLemmas[0], negated, removable, RULE_INVALID, node);
for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
- d_propEngine->assertLemma(additionalLemmas[i], false, removable);
+ d_propEngine->assertLemma(additionalLemmas[i], false, removable, RULE_INVALID, node);
}
// WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
regexp.cpp \
bin_heap.h \
didyoumean.h \
- didyoumean.cpp
+ didyoumean.cpp \
+ unsat_core.h \
+ unsat_core.cpp
libstatistics_la_SOURCES = \
statistics_registry.h \
uninterpreted_constant.i \
chain.i \
regexp.i \
- proof.i
+ proof.i \
+ unsat_core.i
DISTCLEANFILES = \
integer.h.tmp \
#include "util/ite_removal.h"
#include "expr/command.h"
#include "theory/ite_utilities.h"
+#include "proof/proof_manager.h"
using namespace CVC4;
using namespace std;
return d_containsVisitor->cache_size() + d_iteCache.size();
}
-void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
+void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
{
+ size_t n = output.size();
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
// Do this in two steps to avoid Node problems(?)
// Appears related to bug 512, splitting this into two lines
// fixes the bug on clang on Mac OS
Node itesRemoved = run(output[i], output, iteSkolemMap, false);
+ // In some calling contexts, not necessary to report dependence information.
+ if(reportDeps && options::unsatCores()) {
+ // new assertions have a dependence on the node
+ PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
+ while(n < output.size()) {
+ PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
+ ++n;
+ }
+ }
output[i] = itesRemoved;
}
}
* contains a map from introduced skolem variables to the index in
* assertions containing the new Boolean ite created in conjunction
* with that skolem variable.
+ *
+ * With reportDeps true, report reasoning dependences to the proof
+ * manager (for unsat cores).
*/
- void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap);
+ void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
/**
* Removes the ITE from the node by introducing skolem
--- /dev/null
+/********************* */
+/*! \file unsat_core.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of unsat cores
+ **
+ ** Representation of unsat cores.
+ **/
+
+#include "util/unsat_core.h"
+#include "expr/command.h"
+
+namespace CVC4 {
+
+UnsatCore::const_iterator UnsatCore::begin() const {
+ return d_core.begin();
+}
+
+UnsatCore::const_iterator UnsatCore::end() const {
+ return d_core.end();
+}
+
+void UnsatCore::toStream(std::ostream& out) const {
+ for(UnsatCore::const_iterator i = begin(); i != end(); ++i) {
+ out << AssertCommand(*i) << std::endl;
+ }
+}
+
+std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
+ core.toStream(out);
+ return out;
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file unsat_core.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__UNSAT_CORE_H
+#define __CVC4__UNSAT_CORE_H
+
+#include <iostream>
+#include <vector>
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC UnsatCore {
+ std::vector<Expr> d_core;
+
+public:
+ UnsatCore() {}
+
+ template <class T>
+ UnsatCore(T begin, T end) : d_core(begin, end) {}
+
+ ~UnsatCore() {}
+
+ typedef std::vector<Expr>::const_iterator iterator;
+ typedef std::vector<Expr>::const_iterator const_iterator;
+
+ const_iterator begin() const;
+ const_iterator end() const;
+
+ void toStream(std::ostream& out) const;
+
+};/* class UnsatCore */
+
+std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UNSAT_CORE_H */
--- /dev/null
+%{
+#include "util/unsat_core.h"
+%}
+
+%include "util/unsat_core.h"
wiki.19.cvc \
wiki.20.cvc \
wiki.21.cvc \
- simplification_bug3.cvc \
queries0.cvc \
print_lambda.cvc
+++ /dev/null
-% COMMAND-LINE: --simplification=incremental
-x, y: BOOLEAN;
-ASSERT x OR y;
-ASSERT NOT x;
-ASSERT NOT y;
-% EXPECT: unsat
-CHECKSAT;
projects / cvc5.git / commitdiff