CnfStream(satSolver) {
}
-void CnfStream::assertClause(SatClause& c) {
+void CnfStream::assertClause(TNode node, SatClause& c) {
Debug("cnf") << "Inserting into stream " << c << endl;
- d_satSolver->addClause(c);
+ d_satSolver->addClause(c, d_assertingLemma);
}
-void CnfStream::assertClause(SatLiteral a) {
+void CnfStream::assertClause(TNode node, SatLiteral a) {
SatClause clause(1);
clause[0] = a;
- assertClause(clause);
+ assertClause(node, clause);
}
-void CnfStream::assertClause(SatLiteral a, SatLiteral b) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) {
SatClause clause(2);
clause[0] = a;
clause[1] = b;
- assertClause(clause);
+ assertClause(node, clause);
}
-void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) {
SatClause clause(3);
clause[0] = a;
clause[1] = b;
clause[2] = c;
- assertClause(clause);
+ assertClause(node, clause);
}
bool CnfStream::isCached(TNode n) const {
void CnfStream::cacheTranslation(TNode node, SatLiteral lit) {
Debug("cnf") << "caching translation " << node << " to " << lit << endl;
- // We always cash bot the node and the negation at the same time
+ // We always cash both the node and the negation at the same time
d_translationCache[node] = lit;
d_translationCache[node.notNode()] = ~lit;
}
if(node.getKind() == kind::CONST_BOOLEAN) {
if(node.getConst<bool>()) {
- assertClause(lit);
+ assertClause(node, lit);
} else {
- assertClause(~lit);
+ assertClause(node, ~lit);
}
}
SatLiteral xorLit = newLiteral(xorNode);
- assertClause(a, b, ~xorLit);
- assertClause(~a, ~b, ~xorLit);
- assertClause(a, ~b, xorLit);
- assertClause(~a, b, xorLit);
+ assertClause(xorNode, a, b, ~xorLit);
+ assertClause(xorNode, ~a, ~b, ~xorLit);
+ assertClause(xorNode, a, ~b, xorLit);
+ assertClause(xorNode, ~a, b, xorLit);
return xorLit;
}
// lit | ~(a_1 | a_2 | a_3 | ... | a_n)
// (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
for(unsigned i = 0; i < n_children; ++i) {
- assertClause(orLit, ~clause[i]);
+ assertClause(orNode, orLit, ~clause[i]);
}
// lit -> (a_1 | a_2 | a_3 | ... | a_n)
// ~lit | a_1 | a_2 | a_3 | ... | a_n
clause[n_children] = ~orLit;
// This needs to go last, as the clause might get modified by the SAT solver
- assertClause(clause);
+ assertClause(orNode, clause);
// Return the literal
return orLit;
// ~lit | (a_1 & a_2 & a_3 & ... & a_n)
// (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
for(unsigned i = 0; i < n_children; ++i) {
- assertClause(~andLit, ~clause[i]);
+ assertClause(andNode, ~andLit, ~clause[i]);
}
// lit <- (a_1 & a_2 & a_3 & ... a_n)
// lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
clause[n_children] = andLit;
// This needs to go last, as the clause might get modified by the SAT solver
- assertClause(clause);
+ assertClause(andNode, clause);
return andLit;
}
// lit -> (a->b)
// ~lit | ~ a | b
- assertClause(~impliesLit, ~a, b);
+ assertClause(impliesNode, ~impliesLit, ~a, b);
// (a->b) -> lit
// ~(~a | b) | lit
// (a | l) & (~b | l)
- assertClause(a, impliesLit);
- assertClause(~b, impliesLit);
+ assertClause(impliesNode, a, impliesLit);
+ assertClause(impliesNode, ~b, impliesLit);
return impliesLit;
}
// lit -> ((a-> b) & (b->a))
// ~lit | ((~a | b) & (~b | a))
// (~a | b | ~lit) & (~b | a | ~lit)
- assertClause(~a, b, ~iffLit);
- assertClause(a, ~b, ~iffLit);
+ assertClause(iffNode, ~a, b, ~iffLit);
+ assertClause(iffNode, a, ~b, ~iffLit);
// (a<->b) -> lit
// ~((a & b) | (~a & ~b)) | lit
// (~(a & b)) & (~(~a & ~b)) | lit
// ((~a | ~b) & (a | b)) | lit
// (~a | ~b | lit) & (a | b | lit)
- assertClause(~a, ~b, iffLit);
- assertClause(a, b, iffLit);
+ assertClause(iffNode, ~a, ~b, iffLit);
+ assertClause(iffNode, a, b, iffLit);
return iffLit;
}
// lit -> (t | e) & (b -> t) & (!b -> e)
// lit -> (t | e) & (!b | t) & (b | e)
// (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
- assertClause(~iteLit, thenLit, elseLit);
- assertClause(~iteLit, ~condLit, thenLit);
- assertClause(~iteLit, condLit, elseLit);
+ assertClause(iteNode, ~iteLit, thenLit, elseLit);
+ assertClause(iteNode, ~iteLit, ~condLit, thenLit);
+ assertClause(iteNode, ~iteLit, condLit, elseLit);
// If ITE is false then one of the branches is false and the condition
// implies which one
// !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
// !lit -> (!t | !e) & (!b | !t) & (b | !e)
// (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
- assertClause(iteLit, ~thenLit, ~elseLit);
- assertClause(iteLit, ~condLit, ~thenLit);
- assertClause(iteLit, condLit, ~elseLit);
+ assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
+ assertClause(iteNode, iteLit, ~condLit, ~thenLit);
+ assertClause(iteNode, iteLit, condLit, ~elseLit);
return iteLit;
}
nodeManager->mkNode(EQUAL, skolem, node[1]),
nodeManager->mkNode(EQUAL, skolem, node[2]));
nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
- convertAndAssert( newAssertion );
+ convertAndAssert(newAssertion, d_assertingLemma);
return skolem;
} else {
std::vector<Node> newChildren;
}
}
-void TseitinCnfStream::convertAndAssert(TNode node) {
+void TseitinCnfStream::convertAndAssert(TNode node, bool lemma) {
Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
+ d_assertingLemma = lemma;
if(node.getKind() == AND) {
// If the node is a conjunction, we handle each conjunct separately
for( TNode::const_iterator conjunct = node.begin(),
node_end = node.end();
conjunct != node_end;
++conjunct ) {
- convertAndAssert(*conjunct);
+ convertAndAssert(*conjunct, lemma);
}
} else if(node.getKind() == OR) {
// If the node is a disjunction, we construct a clause and assert it
clause[i] = toCNF(*disjunct);
}
Assert( disjunct == node.end() );
- assertClause(clause);
+ assertClause(node, clause);
} else {
// Otherwise, we just convert using the definitional transformation
- assertClause(toCNF(node));
+ assertClause(node, toCNF(node));
}
}
* @author Tim King <taking@cs.nyu.edu>
*/
class CnfStream {
+
public:
+
/** Cache of what nodes have been registered to a literal. */
typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache;
protected:
+ /**
+ * Are we asserting a lemma (true) or a permanent clause (false).
+ * This is set at the begining of convertAndAssert so that it doesn't
+ * need to be passed on over the stack.
+ */
+ bool d_assertingLemma;
+
/**
* Asserts the given clause to the sat solver.
* @param clause the clasue to assert
*/
- void assertClause(SatClause& clause);
+ void assertClause(TNode node, SatClause& clause);
/**
* Asserts the unit clause to the sat solver.
* @param a the unit literal of the clause
*/
- void assertClause(SatLiteral a);
+ void assertClause(TNode node, SatLiteral a);
/**
* Asserts the binary clause to the sat solver.
* @param a the first literal in the clause
* @param b the second literal in the clause
*/
- void assertClause(SatLiteral a, SatLiteral b);
+ void assertClause(TNode node, SatLiteral a, SatLiteral b);
/**
* Asserts the ternary clause to the sat solver.
* @param b the second literal in the clause
* @param c the thirs literal in the clause
*/
- void assertClause(SatLiteral a, SatLiteral b, SatLiteral c);
+ void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
/**
* Returns true if the node has been cashed in the translation cache.
* @param node node to convert and assert
* @param whether the sat solver can choose to remove this clause
*/
- virtual void convertAndAssert(TNode node) = 0;
+ virtual void convertAndAssert(TNode node, bool lemma = false) = 0;
/**
* Get the node that is represented by the given SatLiteral.
/**
* Convert a given formula to CNF and assert it to the SAT solver.
* @param node the formula to assert
+ * @param lemma is this a lemma that is erasable
*/
- void convertAndAssert(TNode node);
+ void convertAndAssert(TNode node, bool lemma);
/**
* Constructs the stream to use the given sat solver.
}
-bool Solver::addClause(vec<Lit>& ps)
+bool Solver::addClause(vec<Lit>& ps, ClauseType type)
{
assert(decisionLevel() == 0);
if (ps.size() == 0)
return ok = false;
else if (ps.size() == 1){
+ assert(type != CLAUSE_LEMMA);
assert(value(ps[0]) == l_Undef);
uncheckedEnqueue(ps[0]);
return ok = (propagate() == NULL);
}else{
Clause* c = Clause_new(ps, false);
clauses.push(c);
+ if (type == CLAUSE_LEMMA) lemmas.push(c);
attachClause(*c);
}
return true;
+
}
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
trail_lim.shrink(trail_lim.size() - level);
+ // We can erase the lemmas now
+ for (int c = lemmas.size() - 1; c >= lemmas_lim[level]; c--) {
+ // TODO: can_erase[lemma[c]] = true;
+ }
+ lemmas.shrink(lemmas.size() - lemmas_lim[level]);
+ lemmas_lim.shrink(lemmas_lim.size() - level);
}
}
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode.
- bool addClause (vec<Lit>& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
+
+ // Types of clauses
+ enum ClauseType {
+ // Clauses defined by the problem
+ CLAUSE_PROBLEM,
+ // Lemma clauses added by the theories
+ CLAUSE_LEMMA,
+ // Conflict clauses
+ CLAUSE_CONFLICT
+ };
+
+ bool addClause (vec<Lit>& ps, ClauseType type); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
// Solving:
//
vec<char> decision_var; // Declares if a variable is eligible for selection in the decision heuristic.
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
+ vec<Clause*> lemmas; // List of lemmas we added (context dependent)
+ vec<int> lemmas_lim; // Separator indices for different decision levels in 'lemmas'.
vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
vec<int> level; // 'level[var]' contains the level at which the assignment was made.
int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
+ int lhead; // Head of the lemma stack (for backtracking)
int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
inline bool Solver::enqueue (Lit p, Clause* from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
inline bool Solver::locked (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; }
-inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); }
+inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); lemmas_lim.push(lemmas.size()); context->push(); }
inline int Solver::decisionLevel () const { return trail_lim.size(); }
inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level[x] & 31); }
-bool SimpSolver::addClause(vec<Lit>& ps)
+bool SimpSolver::addClause(vec<Lit>& ps, ClauseType type)
{
for (int i = 0; i < ps.size(); i++)
if (isEliminated(var(ps[i])))
if (redundancy_check && implied(ps))
return true;
- if (!Solver::addClause(ps))
+ if (!Solver::addClause(ps, type))
return false;
if (use_simplification && clauses.size() == nclauses + 1){
vec<Lit> resolvent;
for (int i = 0; i < pos.size(); i++)
for (int j = 0; j < neg.size(); j++)
- if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent))
+ if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent, CLAUSE_CONFLICT))
return false;
// DEBUG: For checking that a clause set is saturated with respect to variable elimination.
clause.push(c[j]);
remembered_clauses++;
- check(addClause(clause));
+ check(addClause(clause, CLAUSE_PROBLEM));
free(&c);
}
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false);
- bool addClause (vec<Lit>& ps);
+ bool addClause (vec<Lit>& ps, ClauseType type);
// Variable mode:
//
namespace CVC4 {
namespace prop {
+/** Keeps a boolean flag scoped */
+class ScopedBool {
+
+private:
+
+ bool d_original;
+ bool& d_reference;
+
+public:
+
+ ScopedBool(bool& reference) :
+ d_reference(reference) {
+ d_original = reference;
+ }
+
+ ~ScopedBool() {
+ d_reference = d_original;
+ }
+};
+
PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
TheoryEngine* te, Context* context)
: d_inCheckSat(false),
}
void PropEngine::assertLemma(TNode node) {
+ Assert(d_inCheckSat, "Sat solver should be in solve()!");
Debug("prop") << "assertFormula(" << node << ")" << endl;
// Assert as removable
d_cnfStream->convertAndAssert(node);
Result PropEngine::checkSat() {
Assert(!d_inCheckSat, "Sat solver in solve()!");
Debug("prop") << "PropEngine::checkSat()" << endl;
+
// Mark that we are in the checkSat
+ ScopedBool scopedBool(d_inCheckSat);
d_inCheckSat = true;
+
// Check the problem
bool result = d_satSolver->solve();
- // Not in checkSat any more
- d_inCheckSat = false;
if( result && debugTagIsOn("prop") ) {
printSatisfyingAssignment();
#include "util/result.h"
#include "util/options.h"
#include "util/decision_engine.h"
-#include "theory/theory_engine.h"
namespace CVC4 {
+
+class TheoryEngine;
+
namespace prop {
class CnfStream;
/**
* Converts the given formula to CNF and assert the CNF to the sat solver.
- * The formula can be removed by the sat solver.
+ * The formula can be removed by the sat solver after backtracking lower
+ * than the (SAT and SMT) level at which it was asserted.
+ *
* @param node the formula to assert
*/
void assertLemma(TNode node);
void SatSolver::theoryCheck(SatClause& conflict) {
// Try theory propagation
- if (!d_theoryEngine->check(theory::Theory::FULL_EFFORT)) {
+ bool ok = d_theoryEngine->check(theory::Theory::FULL_EFFORT);
+ // If in conflict construct the conflict clause
+ if (!ok) {
// We have a conflict, get it
Node conflictNode = d_theoryEngine->getConflict();
Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl;
class SatInputInterface {
public:
/** Assert a clause in the solver. */
- virtual void addClause(SatClause& clause) = 0;
+ virtual void addClause(SatClause& clause, bool lemma) = 0;
/** Create a new boolean variable in the solver. */
virtual SatVariable newVar(bool theoryAtom = false) = 0;
};
bool solve();
- void addClause(SatClause& clause);
+ void addClause(SatClause& clause, bool lemma);
SatVariable newVar(bool theoryAtom = false);
return d_minisat->solve();
}
-inline void SatSolver::addClause(SatClause& clause) {
- d_minisat->addClause(clause);
+inline void SatSolver::addClause(SatClause& clause, bool lemma) {
+ d_minisat->addClause(clause, lemma ? minisat::Solver::CLAUSE_LEMMA : minisat::Solver::CLAUSE_PROBLEM);
}
inline SatVariable SatSolver::newVar(bool theoryAtom) {
#include "util/exception.h"
#include "util/options.h"
#include "prop/prop_engine.h"
+#include "theory/theory_engine.h"
+
using namespace CVC4::prop;
using CVC4::context::Context;
NodeManagerScope nms(d_nodeManager);
d_decisionEngine = new DecisionEngine;
- d_theoryEngine = new TheoryEngine(this, d_ctxt);
+ // We have mutual dependancy here, so we add the prop engine to the theory
+ // engine later (it is non-essential there)
+ d_theoryEngine = new TheoryEngine(d_ctxt);
d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt);
+ d_theoryEngine->setPropEngine(d_propEngine);
}
void SmtEngine::shutdown() {
Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
slackEqLeft.setAttribute(TheoryArithPropagated(), true);
- //TODO this has to be wrong no?
- d_out->lemma(slackEqLeft);
+ //TODO this has to be wrong no? YES (dejan)
+ // d_out->lemma(slackEqLeft);
d_tableau.addRow(slackEqLeft);
#include "theory/theory.h"
#include "theory/theoryof_table.h"
+#include "prop/prop_engine.h"
#include "theory/booleans/theory_bool.h"
#include "theory/uf/theory_uf.h"
#include "theory/arith/theory_arith.h"
namespace CVC4 {
-class SmtEngine;
-
// In terms of abstraction, this is below (and provides services to)
// PropEngine.
*/
class TheoryEngine {
- /** Associated SMT engine */
- SmtEngine* d_smt;
+ /** Associated PropEngine engine */
+ prop::PropEngine* d_propEngine;
/** A table of Kinds to pointers to Theory */
theory::TheoryOfTable d_theoryOfTable;
void propagate(TNode, bool) throw(theory::Interrupted) {
}
- void lemma(TNode, bool) throw(theory::Interrupted) {
+ void lemma(TNode node, bool) throw(theory::Interrupted) {
+ d_engine->newLemma(node);
}
void explanation(TNode, bool) throw(theory::Interrupted) {
/**
* Construct a theory engine.
*/
- TheoryEngine(SmtEngine* smt, context::Context* ctxt) :
- d_smt(smt),
+ TheoryEngine(context::Context* ctxt) :
+ d_propEngine(NULL),
d_theoryOut(this, ctxt),
d_bool(ctxt, d_theoryOut),
d_uf(ctxt, d_theoryOut),
d_theoryOfTable.registerTheory(&d_bv);
}
+ void setPropEngine(prop::PropEngine* propEngine)
+ {
+ Assert(d_propEngine == NULL);
+ d_propEngine = propEngine;
+ }
+
/**
* This is called at shutdown time by the SmtEngine, just before
* destruction. It is important because there are destruction
* Check all (currently-active) theories for conflicts.
* @param effort the effort level to use
*/
- inline bool check(theory::Theory::Effort effort) {
+ inline bool check(theory::Theory::Effort effort)
+ {
d_theoryOut.d_conflictNode = Node::null();
+ // Do the checking
try {
//d_bool.check(effort);
d_uf.check(effort);
} catch(const theory::Interrupted&) {
Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
}
+ // Return wheather we have a conflict
return d_theoryOut.d_conflictNode.get().isNull();
}
+ inline void newLemma(TNode node) {
+ d_propEngine->assertLemma(node);
+ }
+
/**
* Returns the last conflict (if any).
*/
projects / cvc5.git / commitdiff