return find != d_translationCache.end() && find->second.level >= 0;
}
-bool CnfStream::hasLiteral(TNode n) const {
+bool CnfStream::hasEverHadLiteral(TNode n) const {
TranslationCache::const_iterator find = d_translationCache.find(n);
return find != d_translationCache.end();
}
+bool CnfStream::currentlyHasLiteral(TNode n) const {
+ TranslationCache::const_iterator find = d_translationCache.find(n);
+ return find != d_translationCache.end() && (*find).second.level != -1;
+}
+
SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl;
// Get the literal for this node
SatLiteral lit;
- if (!hasLiteral(node)) {
+ if (!hasEverHadLiteral(node)) {
// If no literal, well make one
lit = variableToLiteral(d_satSolver->newVar(theoryLiteral));
d_translationCache[node].literal = lit;
void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
- if(hasLiteral(node)) {
+ /*
+ if(currentlyHasLiteral(node)) {
Debug("cnf") << "==> fortunate literal detected!" << endl;
++d_fortunateLiterals;
SatLiteral lit = getLiteral(node);
//d_satSolver->renewVar(lit);
assertClause(node, negated ? ~lit : lit);
+ return;
}
+ */
switch(node.getKind()) {
case AND:
TNode getNode(const SatLiteral& literal);
/**
- * Returns true if the node has an assigned literal (it might not be translated).
- * Caches the pair of the node and the literal corresponding to the
- * translation.
+ * Returns true iff the node has an assigned literal (it might not be translated).
* @param node the node
*/
- bool hasLiteral(TNode node) const;
+ bool hasEverHadLiteral(TNode node) const;
+
+ /**
+ * Returns true iff the node has an assigned literal and it's translated.
+ * @param node the node
+ */
+ bool currentlyHasLiteral(TNode node) const;
/**
* Returns the literal that represents the given node in the SAT CNF
}
bool PropEngine::isSatLiteral(TNode node) {
- return d_cnfStream->hasLiteral(node);
+ return d_cnfStream->hasEverHadLiteral(node);
}
bool PropEngine::hasValue(TNode node, bool& value) {
/** Learned literals */
vector<Node> d_nonClausalLearnedLiterals;
+ /** A circuit propagator for non-clausal propositional deduction */
+ booleans::CircuitPropagator d_propagator;
+
/** Assertions to push to sat */
vector<Node> d_assertionsToCheck;
SmtEnginePrivate(SmtEngine& smt) :
d_smt(smt),
+ d_nonClausalLearnedLiterals(),
+ d_propagator(smt.d_userContext, d_nonClausalLearnedLiterals, true, true),
d_topLevelSubstitutions(smt.d_userContext) {
}
StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
StatisticsRegistry::unregisterStat(&d_staticLearningTime);
+ // Deletion order error: circuit propagator has some unsafe TNodes ?!
+ // delete d_private;
delete d_userContext;
delete d_theoryEngine;
void SmtEnginePrivate::nonClausalSimplify() {
- TimerStat::CodeTimer nonclauselTimer(d_smt.d_nonclausalSimplificationTime);
+ TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime);
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
}
- d_nonClausalLearnedLiterals.clear();
- booleans::CircuitPropagator propagator(d_nonClausalLearnedLiterals, true, true);
-
// Assert all the assertions to the propagator
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "asserting to propagator" << endl;
for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- propagator.assert(d_assertionsToPreprocess[i]);
+ d_propagator.assert(d_assertionsToPreprocess[i]);
}
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "propagating" << endl;
- if (propagator.propagate()) {
+ if (d_propagator.propagate()) {
// If in conflict, just return false
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict in non-clausal propagation" << endl;
<< d_userContext->getLevel() << endl;
// FIXME: should we reset d_status here?
// SMT-LIBv2 spec seems to imply no, but it would make sense to..
+ // Still, we want the right exit status after any final sequence
+ // of pops... hm.
}
-void SmtEngine::internalPop() {
- Trace("smt") << "internalPop()" << endl;
- d_propEngine->pop();
- d_userContext->pop();
+void SmtEngine::internalPush() {
+ Trace("smt") << "SmtEngine::internalPush()" << endl;
+ if(Options::current()->incrementalSolving) {
+ d_private->processAssertions();
+ d_userContext->push();
+ d_propEngine->push();
+ }
}
-void SmtEngine::internalPush() {
- Trace("smt") << "internalPush()" << endl;
- // TODO: this is the right thing to do, but needs serious thinking
- // to keep completeness
- //
- // d_private->processAssertions();
- d_userContext->push();
- d_propEngine->push();
+void SmtEngine::internalPop() {
+ Trace("smt") << "SmtEngine::internalPop()" << endl;
+ if(Options::current()->incrementalSolving) {
+ d_propEngine->pop();
+ d_userContext->pop();
+ }
}
StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
/**
* Whether or not a query() or checkSat() has already been made through
- * this SmtEngine. If true, and d_incrementalSolving is false, then
+ * this SmtEngine. If true, and incrementalSolving is false, then
* attempting an additional query() or checkSat() will fail with a
* ModalException.
*/
#include "context/context.h"
#include "util/hash.h"
#include "expr/node.h"
+#include "context/cdset.h"
+#include "context/cdmap.h"
+#include "context/cdo.h"
namespace CVC4 {
namespace theory {
/** The propagation queue */
std::vector<TNode> d_propagationQueue;
+ /** A context-notify object that clears out stale data. */
+ template <class T>
+ class DataClearer : context::ContextNotifyObj {
+ T& d_data;
+ public:
+ DataClearer(context::Context* context, T& data) :
+ context::ContextNotifyObj(context),
+ d_data(data) {
+ }
+
+ void notify() {
+ Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
+ << "(size was " << d_data.size() << ")" << std::endl;
+ d_data.clear();
+ }
+ };/* class DataClearer<T> */
+
+ /**
+ * We have a propagation queue "clearer" object for when the user
+ * context pops. Normally the propagation queue should be empty,
+ * but this keeps us safe in case there's still some rubbish around
+ * on the queue.
+ */
+ DataClearer< std::vector<TNode> > d_propagationQueueClearer;
+
/** Are we in conflict */
- bool d_conflict;
+ context::CDO<bool> d_conflict;
/** Map of substitutions */
std::vector<Node>& d_learnedLiterals;
+ /**
+ * Similar data clearer for learned literals.
+ */
+ DataClearer< std::vector<Node> > d_learnedLiteralClearer;
+
/** Nodes that have been attached already (computed forward edges for) */
// All the nodes we've visited so far
- std::hash_set<TNode, TNodeHashFunction> d_seen;
+ context::CDSet<TNode, TNodeHashFunction> d_seen;
/**
* Assignment status of each node.
*/
- typedef std::hash_map<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
+ typedef context::CDMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
AssignmentMap d_state;
/**
*/
void assignAndEnqueue(TNode n, bool value) {
- Debug("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
+ Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
if (n.getKind() == kind::CONST_BOOLEAN) {
// Assigning a constant to the opposite value is dumb
/** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
bool getAssignment(TNode n) const {
- Assert(d_state.find(n) != d_state.end() && d_state.find(n)->second != UNASSIGNED);
- return d_state.find(n)->second == ASSIGNED_TO_TRUE;
+ AssignmentMap::iterator i = d_state.find(n);
+ Assert(i != d_state.end() && (*i).second != UNASSIGNED);
+ return (*i).second == ASSIGNED_TO_TRUE;
}
/** Predicate for use in STL functions. */
void propagateBackward(TNode parent, bool assignment);
/** Whether to perform forward propagation */
- bool d_forwardPropagation;
+ const bool d_forwardPropagation;
+
/** Whether to perform backward propagation */
- bool d_backwardPropagation;
+ const bool d_backwardPropagation;
public:
/**
- * Construct a new CircuitPropagator with the given atoms and backEdges.
+ * Construct a new CircuitPropagator.
*/
- CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) :
- d_conflict(false),
+ CircuitPropagator(context::Context* context, std::vector<Node>& outLearnedLiterals,
+ bool enableForward = true, bool enableBackward = true) :
+ d_backEdges(),
+ d_propagationQueue(),
+ d_propagationQueueClearer(context, d_propagationQueue),
+ d_conflict(context, false),
d_learnedLiterals(outLearnedLiterals),
+ d_learnedLiteralClearer(context, outLearnedLiterals),
+ d_seen(context),
+ d_state(context),
d_forwardPropagation(enableForward),
d_backwardPropagation(enableBackward) {
}
wiki.18.cvc \
wiki.19.cvc \
wiki.20.cvc \
- wiki.21.cvc
+ wiki.21.cvc \
+ simplification_bug3.cvc
# Regression tests derived from bug reports
BUG_TESTS = \
--- /dev/null
+% COMMAND-LINE: --simplification=incremental
+x, y: BOOLEAN;
+ASSERT x OR y;
+ASSERT NOT x;
+ASSERT NOT y;
+% EXPECT: unsat
+CHECKSAT;
+% EXIT: 20
projects / cvc5.git / commitdiff