if (lemmas.size() > 0) {
recheck = true;
return updateLemmas();
+ } else {
+ return confl;
}
}
static RewriteResponse preRewrite(TNode n);
static RewriteResponse postRewrite(TNode n);
+ static Node rewriteEquality(TNode equality) {
+ // Arithmetic owns the domain, so this is totally ok
+ return Rewriter::rewrite(equality);
+ }
static void init() { }
learner.clear();
check(FULL_EFFORT);
}
+
+EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
+ if (getValue(a) == getValue(b)) {
+ return EQUALITY_TRUE_IN_MODEL;
+ } else {
+ return EQUALITY_FALSE_IN_MODEL;
+ }
+
+}
std::string identify() const { return std::string("TheoryArith"); }
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
+
private:
/** The constant zero. */
DeltaRational d_DELTA_ZERO;
}
if (node[0] > node[1]) {
Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
- // If we've switched theories, we need to rewrite again (TODO: THIS IS HACK, once theories accept eq, change)
- if (Theory::theoryOf(newNode[0]) != Theory::theoryOf(newNode[1])) {
- return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
- } else {
- return RewriteResponse(REWRITE_DONE, newNode);
- }
+ return RewriteResponse(REWRITE_DONE, newNode);
}
break;
}
return RewriteResponse(REWRITE_DONE, node);
}
+ static Node rewriteEquality(TNode node) {
+ return postRewrite(node).node;
+ }
+
static inline void init() {}
static inline void shutdown() {}
return preRewrite(node);
}
+ static Node rewriteEquality(TNode node) {
+ Unreachable();
+ return node;
+ }
+
static void init() {}
static void shutdown() {}
public:
static inline RewriteResponse postRewrite(TNode node) {
- if(node.getKind() == kind::EQUAL) {
- return Rewriter::callPostRewrite(Theory::theoryOf(node[0]), node);
- }
return RewriteResponse(REWRITE_DONE, node);
}
switch(node.getKind()) {
case kind::DISTINCT:
return RewriteResponse(REWRITE_DONE, blastDistinct(node));
- case kind::EQUAL:
- return Rewriter::callPreRewrite(Theory::theoryOf(node[0]), node);
default:
return RewriteResponse(REWRITE_DONE, node);
}
}
+ static inline Node rewriteEquality(TNode equality) {
+ Unreachable();
+ return equality;
+ }
+
static inline void init() {}
static inline void shutdown() {}
return RewriteResponse(REWRITE_DONE, node);
}
+ static inline Node rewriteEquality(TNode node) {
+ return postRewrite(node).node;
+ }
+
static void init();
static void shutdown();
};/* class TheoryBVRewriter */
return RewriteResponse(REWRITE_DONE, in);
}
+ static Node rewriteEquality(TNode equality) {
+ return postRewrite(equality).node;
+ }
+
static inline void init() {}
static inline void shutdown() {}
post_rewrite_get_cache=
post_rewrite_set_cache=
+rewrite_equality_calls=
+
seen_theory=false
seen_theory_builtin=false
post_rewrite_set_cache="${post_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache);
"
+ rewrite_equality_calls="${rewrite_equality_calls} case ${theory_id}: return ${class}::rewriteEquality(node);
+"
+
lineno=${BASH_LINENO[0]}
check_theory_seen
}
rewriter_includes \
pre_rewrite_calls \
post_rewrite_calls \
+ rewrite_equality_calls \
pre_rewrite_get_cache \
post_rewrite_get_cache \
pre_rewrite_set_cache \
return rewriteTo(theory::Theory::theoryOf(node), node);
}
+Node Rewriter::rewriteEquality(theory::TheoryId theoryId, TNode node) {
+ Trace("rewriter") << "Rewriter::rewriteEquality(" << theoryId << "," << node << ")"<< std::endl;
+ return Rewriter::callRewriteEquality(theoryId, node);
+}
+
Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
Rewriter() CVC4_UNUSED;
Rewriter(const Rewriter&) CVC4_UNUSED;
-public:
+ /**
+ * Rewrites the node using the given theory rewriter.
+ */
+ static Node rewriteTo(theory::TheoryId theoryId, Node node);
/** Calls the pre-rewriter for the given theory */
static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node);
/** Calls the post-rewriter for the given theory */
static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node);
+ /**
+ * Calls the equality-rewruter for the given theory.
+ */
+ static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
+
+public:
+
+
/**
* Rewrites the node using theoryOf() to determine which rewriter to
* use on the node.
static Node rewrite(Node node);
/**
- * Rewrites the node using the given theory rewriter.
+ * Rewrite an equality between two terms that are already in normal form, so
+ * that the equality is in theory-normal form.
*/
- static Node rewriteTo(theory::TheoryId theoryId, Node node);
+ static Node rewriteEquality(theory::TheoryId theoryId, TNode node);
/**
* Should be called before the rewriter gets used for the first time.
}
}
+Node Rewriter::callRewriteEquality(theory::TheoryId theoryId, TNode node) {
+ switch(theoryId) {
+${rewrite_equality_calls}
+ default:
+ Unreachable();
+ }
+}
+
Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) {
switch(theoryId) {
${pre_rewrite_get_cache}
// We don't care about the terms of different types
continue;
}
- switch (equalityStatus(a, b)) {
- case EQUALITY_TRUE:
- case EQUALITY_FALSE:
+ switch (getEqualityStatus(a, b)) {
+ case EQUALITY_TRUE_AND_PROPAGATED:
+ case EQUALITY_FALSE_AND_PROPAGATED:
// If we know about it, we should have propagated it, so we can skip
break;
default:
namespace theory {
/**
- * The status of an equality in the current context.
+ * Information about an assertion for the theories.
*/
-enum EqualityStatus {
- /** The eqaulity is known to be true */
- EQUALITY_TRUE,
- /** The equality is known to be false */
- EQUALITY_FALSE,
- /** The equality is not known, but is true in the current model */
- EQUALITY_TRUE_IN_MODEL,
- /** The equality is not known, but is false in the current model */
- EQUALITY_FALSE_IN_MODEL,
- /** The equality is completely unknown */
- EQUALITY_UNKNOWN
+struct Assertion {
+
+ /** The assertion */
+ Node assertion;
+ /** Has this assertion been preregistered with this theory */
+ bool isPreregistered;
+
+ Assertion(TNode assertion, bool isPreregistered)
+ : assertion(assertion), isPreregistered(isPreregistered) {}
+
+ /**
+ * Convert the assertion to a TNode.
+ */
+ operator TNode () const {
+ return assertion;
+ }
+
+ /**
+ * Convert the assertion to a Node.
+ */
+ operator Node () const {
+ return assertion;
+ }
};
/**
* These can not be TNodes as some atoms (such as equalities) are sent
* across theories without being stored in a global map.
*/
- context::CDList<TNode> d_facts;
+ context::CDList<Assertion> d_facts;
/** Index into the head of the facts list */
context::CDO<unsigned> d_factsHead;
*
* @return the next assertion in the assertFact() queue
*/
- TNode get() {
+ Assertion get() {
Assert( !done(), "Theory`() called with assertion queue empty!" );
// Get the assertion
- TNode fact = d_facts[d_factsHead];
+ Assertion fact = d_facts[d_factsHead];
d_factsHead = d_factsHead + 1;
Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
if(Dump.isOn("state")) {
- Dump("state") << AssertCommand(fact.toExpr()) << std::endl;
+ Dump("state") << AssertCommand(fact.assertion.toExpr()) << std::endl;
}
return fact;
*
* @return the iterator to the beginning of the fact queue
*/
- context::CDList<TNode>::const_iterator facts_begin() const {
+ context::CDList<Assertion>::const_iterator facts_begin() const {
return d_facts.begin();
}
*
* @return the iterator to the end of the fact queue
*/
- context::CDList<TNode>::const_iterator facts_end() const {
+ context::CDList<Assertion>::const_iterator facts_end() const {
return d_facts.end();
}
/**
* Assert a fact in the current context.
*/
- void assertFact(TNode assertion) {
- Trace("theory") << "Theory<" << getId() << ">::assertFact(" << assertion << ")" << std::endl;
- d_facts.push_back(assertion);
+ void assertFact(TNode assertion, bool isPreregistered) {
+ Trace("theory") << "Theory<" << getId() << ">::assertFact(" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl;
+ d_facts.push_back(Assertion(assertion, isPreregistered));
}
/**
* Return the status of two terms in the current context. Should be implemented in
* sub-theories to enable more efficient theory-combination.
*/
- virtual EqualityStatus equalityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; }
+ virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; }
/**
* This method is called by the shared term manager when a shared
: d_propEngine(NULL),
d_context(context),
d_userContext(userContext),
- d_activeTheories(0),
+ d_activeTheories(context, 0),
d_sharedTerms(context),
d_atomPreprocessingCache(),
d_possiblePropagations(),
d_hasPropagated(context),
d_inConflict(context, false),
+ d_sharedTermsExist(context, false),
d_hasShutDown(false),
d_incomplete(context, false),
d_sharedAssertions(context),
if (multipleTheories) {
// Collect the shared terms if there are multipe theories
NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
+ // Mark the multiple theories flag
+ d_sharedTermsExist = true;
}
}
while (true) {
+ Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
+
// Do the checking
CVC4_FOR_EACH_THEORY;
<< CheckSatCommand() << endl;
}
+ Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << std::endl;
+
// We are still satisfiable, propagate as much as possible
propagate(effort);
// If we have any propagated equalities, we enqueue them to the theories and re-check
if (d_propagatedEqualities.size() > 0) {
+ Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl;
assertSharedEqualities();
continue;
}
// If we added any lemmas, we're done
if (d_lemmasAdded) {
+ Debug("theory") << "TheoryEngine::check(" << effort << "): lemmas added, done" << std::endl;
break;
}
// If in full check and no lemmas added, run the combination
- if (Theory::fullEffort(effort)) {
+ if (Theory::fullEffort(effort) && d_sharedTermsExist) {
// Do the combination
+ Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << std::endl;
combineTheories();
// If we have any propagated equalities, we enqueue them to the theories and re-check
if (d_propagatedEqualities.size() > 0) {
+ Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl;
assertSharedEqualities();
} else {
// No propagated equalities, we're either sat, or there are lemmas added
// Clear any leftover propagated equalities
d_propagatedEqualities.clear();
+ Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << std::endl;
+
} catch(const theory::Interrupted&) {
Trace("theory") << "TheoryEngine::check() => conflict" << endl;
}
for (unsigned i = 0; i < d_propagatedEqualities.size(); ++ i) {
const SharedEquality& eq = d_propagatedEqualities[i];
// Check if the theory already got this one
- if (d_sharedAssertions.find(eq.toAssert) != d_sharedAssertions.end()) {
+ // TODO: the real shared (non-sat) equalities
+ if (d_sharedAssertions.find(eq.toAssert) == d_sharedAssertions.end()) {
+ Debug("sharing") << "TheoryEngine::assertSharedEqualities(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << " from " << eq.toExplain.theory << std::endl;
d_sharedAssertions[eq.toAssert] = eq.toExplain;
- theoryOf(eq.toAssert.theory)->assertFact(eq.toAssert.node);
+ theoryOf(eq.toAssert.theory)->assertFact(eq.toAssert.node, false);
}
}
// Clear the equalities
void TheoryEngine::combineTheories() {
+ Debug("sharing") << "TheoryEngine::combineTheories()" << std::endl;
+
CareGraph careGraph;
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
#undef CVC4_FOR_EACH_THEORY_STATEMENT
for (unsigned i = 0; i < careGraph.size(); ++ i) {
const CarePair& carePair = careGraph[i];
+ Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl;
+
Node equality = carePair.a.eqNode(carePair.b);
Node normalizedEquality = Rewriter::rewrite(equality);
// If the node has a literal, it has been asserted so we should just check it
bool value;
if (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value)) {
+ Debug("sharing") << "TheoryEngine::combineTheories(): has a literal " << std::endl;
+
// Normalize the equality to the theory that requested it
- Node toAssert = Rewriter::rewriteTo(carePair.theory, equality);
+ Node toAssert = Rewriter::rewriteEquality(carePair.theory, equality);
+
if (value) {
- d_propagatedEqualities.push_back(SharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory));
+ SharedEquality sharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory);
+ Assert(d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end());
+ d_propagatedEqualities.push_back(sharedEquality);
} else {
- d_propagatedEqualities.push_back(SharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory));
+ SharedEquality sharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory);
+ Assert(d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end());
+ d_propagatedEqualities.push_back(sharedEquality);
}
} else {
+ Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
+
// There is no value, so we need to split on it
lemma(equality.orNode(equality.notNode()), false, false);
}
}
}
-Node TheoryEngine::getExplanation(TNode node, theory::Theory* theory) {
- Node explanation = theory->explain(node);
- if(Dump.isOn("t-explanations")) {
- Dump("t-explanations")
- << CommentCommand(string("theory explanation from ") + theory->identify() + ": expect valid") << endl
- << QueryCommand(explanation.impNode(node).toExpr()) << endl;
- }
- return explanation;
-}
-
bool TheoryEngine::properConflict(TNode conflict) const {
bool value;
if (conflict.getKind() == kind::AND) {
TNode atom = node.getKind() == kind::NOT ? node[0] : node;
// Assert the fact to the apropriate theory
- theoryOf(atom)->assertFact(node);
+ theoryOf(atom)->assertFact(node, true);
// If any shared terms, notify the theories
if (d_sharedTerms.hasSharedTerms(atom)) {
}
}
d_sharedTerms.markNotified(term, theories);
+ markActive(theories);
}
}
}
void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
- Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl;
+ Debug("theory") << "EngineOutputChannel::propagate(" << literal << ", " << theory << ")" << std::endl;
d_propEngine->checkTime();
d_hasPropagated.insert(literal);
}
- if (literal.getKind() != kind::EQUAL) {
+ TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
+
+ if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL) {
// If not an equality it must be a SAT literal so we enlist it, and it can only
// be propagated by the theory that owns it, as it is the only one that got
// a preregister call with it.
Node normalizedEquality = Rewriter::rewrite(literal);
if (d_propEngine->isSatLiteral(normalizedEquality)) {
// If there is a literal, just enqueue it, same as above
- d_propagatedLiterals.push_back(literal);
- } else {
- // Otherwise, we assert it to all interested theories
+ d_propagatedLiterals.push_back(normalizedEquality);
+ }
+ // Otherwise, we assert it to all interested theories
+ Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(atom[0]);
+ Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(atom[1]);
+ // Now notify the theories
+ if (Theory::setIntersection(lhsNotified, rhsNotified) != 0) {
bool negated = literal.getKind() == kind::NOT;
- Node equality = negated ? literal[0] : literal;
- Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(equality[0]);
- Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(equality[1]);
- // Now notify the theories
- for (TheoryId current = theory::THEORY_FIRST; current != theory::THEORY_LAST; ++ current) {
- if (Theory::setContains(current, lhsNotified) && Theory::setContains(current, rhsNotified)) {
+ for (TheoryId currentTheory = theory::THEORY_FIRST; currentTheory != theory::THEORY_LAST; ++ currentTheory) {
+ if (currentTheory == theory) {
+ // Don't reassert to the same theory
+ continue;
+ }
+ // Assert if theory is interested in both terms
+ if (Theory::setContains(currentTheory, lhsNotified) && Theory::setContains(currentTheory, rhsNotified)) {
// Normalize the equality
- Node equalityNormalized = Rewriter::rewriteTo(current, equality);
+ Node equality = Rewriter::rewriteEquality(currentTheory, atom);
// The assertion
- Node assertion = negated ? equalityNormalized.notNode() : equalityNormalized;
+ Node assertion = negated ? equality.notNode() : equality;
// Remember it to assert later
- d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, current));
+ d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, currentTheory));
}
}
}
}
}
+
+theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
+ Assert(a.getType() == b.getType());
+ return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
+}
+
+Node TheoryEngine::getExplanation(TNode node)
+{
+ Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl;
+
+ TNode atom = node.getKind() == kind::NOT ? node[0] : node;
+
+ Node explanation;
+
+ // The theory that has explaining to do
+ Theory* theory = theoryOf(atom);
+ if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) {
+ SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST));
+ if (find == d_sharedAssertions.end()) {
+ theory = theoryOf(atom);
+ }
+ }
+
+ // Get the explanation
+ explanation = theory->explain(node);
+
+ // Explain any shared equalities that might be in the explanation
+ if (d_sharedTermsExist) {
+ NodeBuilder<> nb(kind::AND);
+ explainEqualities(theory->getId(), explanation, nb);
+ explanation = nb;
+ }
+
+ Assert(!explanation.isNull());
+ if(Dump.isOn("t-explanations")) {
+ Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") << std::endl
+ << QueryCommand(explanation.impNode(node).toExpr()) << std::endl;
+ }
+ Assert(properExplanation(node, explanation));
+
+ return explanation;
+}
+
+void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
+
+ // Mark that we are in conflict
+ d_inConflict = true;
+
+ if(Dump.isOn("t-conflicts")) {
+ Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl
+ << CheckSatCommand(conflict.toExpr()) << std::endl;
+ }
+
+ if (d_sharedTermsExist) {
+ // In the multiple-theories case, we need to reconstruct the conflict
+ NodeBuilder<> nb(kind::AND);
+ explainEqualities(theoryId, conflict, nb);
+ Node fullConflict = nb;
+ Assert(properConflict(fullConflict));
+ Debug("theory") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): " << fullConflict << std::endl;
+ lemma(fullConflict, true, false);
+ } else {
+ // When only one theory, the conflict should need no processing
+ Assert(properConflict(conflict));
+ lemma(conflict, true, false);
+ }
+}
+
+void TheoryEngine::explainEqualities(TheoryId theoryId, TNode literals, NodeBuilder<>& builder) {
+ Debug("theory") << "TheoryEngine::explainEqualities(" << theoryId << ", " << literals << ")" << std::endl;
+ if (literals.getKind() == kind::AND) {
+ for (unsigned i = 0, i_end = literals.getNumChildren(); i != i_end; ++ i) {
+ TNode literal = literals[i];
+ TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
+ if (atom.getKind() == kind::EQUAL) {
+ explainEquality(theoryId, literal, builder);
+ } else {
+ builder << literal;
+ }
+ }
+ } else {
+ TNode atom = literals.getKind() == kind::NOT ? literals[0] : literals;
+ if (atom.getKind() == kind::EQUAL) {
+ explainEquality(theoryId, literals, builder);
+ } else {
+ builder << literals;
+ }
+ }
+}
+
+void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder) {
+ Assert(eqLiteral.getKind() == kind::EQUAL || (eqLiteral.getKind() == kind::NOT && eqLiteral[0].getKind() == kind::EQUAL));
+
+ SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(eqLiteral, theoryId));
+ if (find == d_sharedAssertions.end()) {
+ // Not a shared assertion, just add it since it must be SAT literal
+ builder << eqLiteral;
+ } else {
+ TheoryId explainingTheory = (*find).second.theory;
+ if (explainingTheory == theory::THEORY_LAST) {
+ // If the theory is from the SAT solver, just take the normalized one
+ builder << (*find).second.node;
+ } else {
+ // Explain it using the theory that propagated it
+ Node explanation = theoryOf(explainingTheory)->explain((*find).second.node);
+ explainEqualities(explainingTheory, explanation, builder);
+ }
+ }
+}
+
* runs (no sharing), can reduce the cost of walking the DAG on
* registration, etc.
*/
- theory::Theory::Set d_activeTheories;
+ context::CDO<theory::Theory::Set> d_activeTheories;
/**
* The database of shared terms.
void conflict(TNode conflictNode) throw(AssertionException) {
Trace("theory") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
++ d_statistics.conflicts;
- d_engine->conflict(conflictNode);
+ d_engine->conflict(conflictNode, d_theory);
}
void propagate(TNode literal) throw(AssertionException) {
*/
context::CDO<bool> d_inConflict;
- void conflict(TNode conflict) {
-
- Assert(properConflict(conflict), "not a proper conflict: %s", conflict.toString().c_str());
+ /**
+ * Does the context contain terms shared among multiple theories.
+ */
+ context::CDO<bool> d_sharedTermsExist;
- // Mark that we are in conflict
- d_inConflict = true;
+ /**
+ * Explain the equality literals and push all the explaining literals into the builder. All
+ * the non-equality literals are pushed to the builder.
+ */
+ void explainEqualities(theory::TheoryId theoryId, TNode literals, NodeBuilder<>& builder);
- if(Dump.isOn("t-conflicts")) {
- Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl
- << CheckSatCommand(conflict.toExpr()) << std::endl;
- }
+ /**
+ * Same as above, but just for single equalities.
+ */
+ void explainEquality(theory::TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder);
- // Construct the lemma (note that no CNF caching should happen as all the literals already exists)
- lemma(conflict, true, false);
- }
+ /**
+ * Called by the theories to notify of a conflict.
+ */
+ void conflict(TNode conflict, theory::TheoryId theoryId);
/**
* Debugging flag to ensure that shutdown() is called before the
NodeTheoryPair toExplain;
SharedEquality(TNode assertion, TNode original, theory::TheoryId sendingTheory, theory::TheoryId receivingTheory)
- : toAssert(assertion, sendingTheory),
- toExplain(original, receivingTheory)
+ : toAssert(assertion, receivingTheory),
+ toExplain(original, sendingTheory)
{ }
};
+ /**
+ * Map from equalities asserted to a theory, to the theory that can explain them.
+ */
+ typedef context::CDMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap;
+
/**
* A map from asserted facts to where they came from (for explanations).
*/
- context::CDMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> d_sharedAssertions;
+ SharedAssertionsMap d_sharedAssertions;
/**
* Assert a shared equalities propagated by theories.
}
}
- Node getExplanation(TNode node, theory::Theory* theory);
-
bool properConflict(TNode conflict) const;
bool properPropagation(TNode lit) const;
bool properExplanation(TNode node, TNode expl) const;
- inline Node getExplanation(TNode node) {
- TNode atom = node.getKind() == kind::NOT ? node[0] : node;
- Node explanation = theoryOf(atom)->explain(node);
- Assert(!explanation.isNull());
- if(Dump.isOn("t-explanations")) {
- Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") << std::endl
- << QueryCommand(explanation.impNode(node).toExpr()) << std::endl;
- }
- Assert(properExplanation(node, explanation));
- return explanation;
- }
+ Node getExplanation(TNode node);
Node getValue(TNode node);
return d_theoryTable[theoryId];
}
+ /**
+ * Returns the equality status of the two terms, from the theory that owns the domain type.
+ * The types of a and b must be the same.
+ */
+ theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
+
private:
/** Default visitor for pre-registration */
* Creates a new node, which is in a list of it's own.
*/
EqualityNode(EqualityNodeId nodeId = null_id)
- : d_size(1), d_findId(nodeId), d_nextId(nodeId), d_useList(null_uselist_id) {}
+ : d_size(1),
+ d_findId(nodeId),
+ d_nextId(nodeId),
+ d_useList(null_uselist_id)
+ {}
/**
* Retuerns the uselist.
private:
+ /** The context we are using */
+ context::Context* d_context;
+
+ /** Whether to notify or not (temporarily disabled on equality checks) */
+ bool d_performNotify;
+
/** The class to notify when a representative changes for a term */
NotifyClass d_notify;
*/
std::vector<TriggerId> d_nodeTriggers;
+ /**
+ * List of terms that are marked as individual triggers.
+ */
+ std::vector<EqualityNodeId> d_individualTriggers;
+
+ /**
+ * Size of the individual triggers list.
+ */
+ context::CDO<unsigned> d_individualTriggersSize;
+
+ /**
+ * Map from ids to the individual trigger id representative.
+ */
+ std::vector<EqualityNodeId> d_nodeIndividualTrigger;
+
/**
* Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId.
*/
*/
void debugPrintGraph() const;
+ /** The true node */
+ Node d_true;
+ /** The false node */
+ Node d_false;
+
public:
/**
*/
EqualityEngine(NotifyClass& notify, context::Context* context, std::string name)
: ContextNotifyObj(context),
+ d_context(context),
+ d_performNotify(true),
d_notify(notify),
d_nodesCount(context, 0),
d_assertedEqualitiesCount(context, 0),
d_equalityTriggersCount(context, 0),
+ d_individualTriggersSize(context, 0),
d_stats(name)
{
Debug("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id << std::endl;
Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl;
Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl;
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
}
/**
*/
void addEquality(TNode t1, TNode t2, TNode reason);
+ /**
+ * Adds an dis-equality t1 != t2 to the database.
+ */
+ void addDisequality(TNode t1, TNode t2, TNode reason);
+
/**
* Returns the representative of the term t.
*/
*/
void getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const;
+ /**
+ * Add term to the trigger terms. The notify class will get notified when two
+ * trigger terms become equal. Thihs will only happen on trigger term
+ * representatives.
+ */
+ void addTriggerTerm(TNode t);
+
+ /**
+ * Returns true if t is a trigger term or equal to some other trigger term.
+ */
+ bool isTriggerTerm(TNode t) const;
+
/**
* Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with
- * (t1 = t2).
+ * trigger.
*/
void addTriggerEquality(TNode t1, TNode t2, TNode trigger);
+ /**
+ * Adds a notify trigger for dis-equality t1 != t2, i.e. when t1 != t2 the notify will be called with
+ * trigger.
+ */
+ void addTriggerDisequality(TNode t1, TNode t2, TNode trigger);
+
+ /**
+ * Check whether the two terms are equal.
+ */
+ bool areEqual(TNode t1, TNode t2);
+
+ /**
+ * Check whether the two term are dis-equal.
+ */
+ bool areDisequal(TNode t1, TNode t2);
};
} // Namespace uf
d_nodeTriggers.push_back(+null_trigger);
// Add it to the equality graph
d_equalityGraph.push_back(+null_edge);
+ // Mark the no-individual trigger
+ d_nodeIndividualTrigger.push_back(+null_id);
// Add the equality node to the nodes
d_equalityNodes.push_back(EqualityNode(newId));
Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
// Add the terms if they are not already in the database
- EqualityNodeId t1Id = getNodeId(t1);
- EqualityNodeId t2Id = getNodeId(t2);
+ addTerm(t1);
+ addTerm(t2);
// Add to the queue and propagate
+ EqualityNodeId t1Id = getNodeId(t1);
+ EqualityNodeId t2Id = getNodeId(t2);
enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason));
propagate();
}
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addDisequality(TNode t1, TNode t2, TNode reason) {
+
+ Debug("equality") << "EqualityEngine::addDisequality(" << t1 << "," << t2 << ")" << std::endl;
+
+ Node equality = t1.eqNode(t2);
+ addEquality(equality, d_false, reason);
+}
+
+
template <typename NotifyClass>
TNode EqualityEngine<NotifyClass>::getRepresentative(TNode t) const {
// Now merge the lists
class1.merge<true>(class2);
+
+ // Notfiy the triggers
+ EqualityNodeId class1triggerId = d_nodeIndividualTrigger[class1Id];
+ EqualityNodeId class2triggerId = d_nodeIndividualTrigger[class2Id];
+ if (class2triggerId != +null_id) {
+ if (class1triggerId == +null_id) {
+ // If class1 is not an individual trigger, but class2 is, mark it
+ d_nodeIndividualTrigger[class1Id] = class2triggerId;
+ // Add it to the list for backtracking
+ d_individualTriggers.push_back(class1Id);
+ d_individualTriggersSize = d_individualTriggersSize + 1;
+ } else {
+ // Notify when done
+ if (d_performNotify) {
+ d_notify.notify(d_nodes[class1triggerId], d_nodes[class2triggerId]);
+ }
+ }
+ }
}
template <typename NotifyClass>
d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
}
+ if (d_individualTriggers.size() > d_individualTriggersSize) {
+ // Unset the individual triggers
+ for (int i = d_individualTriggers.size() - 1, i_end = d_individualTriggersSize; i >= i_end; -- i) {
+ d_nodeIndividualTrigger[d_individualTriggers[i]] = +null_id;
+ }
+ d_individualTriggers.resize(d_individualTriggersSize);
+ }
+
if (d_equalityTriggers.size() > d_equalityTriggersCount) {
// Unlink the triggers from the lists
for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) {
- const Trigger& trigger = d_equalityTriggers[i];
- d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
+ const Trigger& trigger = d_equalityTriggers[i];
+ d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
}
// Get rid of the triggers
d_equalityTriggers.resize(d_equalityTriggersCount);
d_nodes.resize(d_nodesCount);
d_applications.resize(d_nodesCount);
d_nodeTriggers.resize(d_nodesCount);
+ d_nodeIndividualTrigger.resize(d_nodesCount);
d_equalityGraph.resize(d_nodesCount);
d_equalityNodes.resize(d_nodesCount);
}
}
}
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTriggerDisequality(TNode t1, TNode t2, TNode trigger) {
+ Node equality = t1.eqNode(t2);
+ addTerm(equality);
+ addTriggerEquality(equality, d_false, trigger);
+}
+
template <typename NotifyClass>
void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode trigger) {
// If the trigger is already on, we propagate
if (t1classId == t2classId) {
Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << "): triggered at setup time" << std::endl;
- d_notify.notifyEquality(trigger); // Don't care about the return value
+ if (d_performNotify) {
+ d_notify.notify(trigger); // Don't care about the return value
+ }
}
Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
Assert(node1.getFind() == t1classId);
Assert(node2.getFind() == t2classId);
+ // Add the actuall equality to the equality graph
+ addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
+
+ // One more equality added
+ d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
+
// Depending on the merge preference (such as size), merge them
std::vector<TriggerId> triggers;
if (node2.getSize() > node1.getSize()) {
Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
- merge(node2, node1, triggers);
d_assertedEqualities.push_back(Equality(t2classId, t1classId));
+ merge(node2, node1, triggers);
} else {
Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl;
- merge(node1, node2, triggers);
d_assertedEqualities.push_back(Equality(t1classId, t2classId));
+ merge(node1, node2, triggers);
}
- // Add the actuall equality to the equality graph
- addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
-
- // One more equality added
- d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
-
- Assert(2*d_assertedEqualities.size() == d_equalityEdges.size());
- Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount);
-
// Notify the triggers
- for (size_t trigger = 0, trigger_end = triggers.size(); trigger < trigger_end && !done; ++ trigger) {
- // Notify the trigger and exit if it fails
- done = !d_notify.notifyEquality(d_equalityTriggersOriginal[triggers[trigger]]);
+ if (d_performNotify) {
+ for (size_t trigger = 0, trigger_end = triggers.size(); trigger < trigger_end && !done; ++ trigger) {
+ // Notify the trigger and exit if it fails
+ done = !d_notify.notify(d_equalityTriggersOriginal[triggers[trigger]]);
+ }
}
}
}
}
}
+class ScopedBool {
+ bool& watch;
+ bool oldValue;
+public:
+ ScopedBool(bool& watch, bool newValue)
+ : watch(watch), oldValue(watch) {
+ watch = newValue;
+ }
+ ~ScopedBool() {
+ watch = oldValue;
+ }
+};
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::areEqual(TNode t1, TNode t2)
+{
+ // Don't notify during this check
+ ScopedBool turnOfNotify(d_performNotify, false);
+
+ // Push the context, so that we can remove the terms later
+ d_context->push();
+
+ // Add the terms
+ addTerm(t1);
+ addTerm(t2);
+ bool equal = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
+
+ // Pop the context (triggers new term removal)
+ d_context->pop();
+
+ // Return whether the two terms are equal
+ return equal;
+}
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
+{
+ // Don't notify during this check
+ ScopedBool turnOfNotify(d_performNotify, false);
+
+ // Push the context, so that we can remove the terms later
+ d_context->push();
+
+ // Add the terms
+ addTerm(t1);
+ addTerm(t2);
+
+ // Check (t1 = t2) = false
+ Node equality1 = t1.eqNode(t2);
+ addTerm(equality1);
+ if (getEqualityNode(equality1).getFind() == getEqualityNode(d_false).getFind()) {
+ return true;
+ }
+
+ // Check (t2 = t1) = false
+ Node equality2 = t2.eqNode(t1);
+ addTerm(equality2);
+ if (getEqualityNode(equality2).getFind() == getEqualityNode(d_false).getFind()) {
+ return true;
+ }
+
+ // Pop the context (triggers new term removal)
+ d_context->pop();
+
+ // Return whether the terms are disequal
+ return false;
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTriggerTerm(TNode t)
+{
+ Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ")" << std::endl;
+
+ // Add the term if it's not already there
+ addTerm(t);
+
+ // Get the node id
+ EqualityNodeId eqNodeId = getNodeId(t);
+ EqualityNode& eqNode = getEqualityNode(eqNodeId);
+ EqualityNodeId classId = eqNode.getFind();
+
+ if (d_nodeIndividualTrigger[classId] != +null_id) {
+ // No need to keep it, just propagate the existing individual triggers
+ if (d_performNotify) {
+ d_notify.notify(t, d_nodes[d_nodeIndividualTrigger[classId]]);
+ }
+ } else {
+ // Add it to the list for backtracking
+ d_individualTriggers.push_back(classId);
+ d_individualTriggersSize = d_individualTriggersSize + 1;
+ // Mark the class id as a trigger
+ d_nodeIndividualTrigger[classId] = eqNodeId;
+ }
+}
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::isTriggerTerm(TNode t) const {
+ if (!hasTerm(t)) return false;
+ EqualityNodeId classId = getEqualityNode(t).getFind();
+ return d_nodeIndividualTrigger[classId] != +null_id;
+}
+
} // Namespace uf
} // Namespace theory
} // Namespace CVC4
void TheoryUF::check(Effort level) {
- while (!done() && !d_conflict) {
+ while (!done() && !d_conflict)
+ {
// Get all the assertions
- TNode assertion = get();
- Debug("uf") << "TheoryUF::check(): processing " << assertion << std::endl;
+ Assertion assertion = get();
+ TNode fact = assertion.assertion;
- // Fo the work
- switch (assertion.getKind()) {
+ Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
+
+ // If the assertion doesn't have a literal, it's a shared equality, so we set it up
+ if (!assertion.isPreregistered) {
+ Debug("uf") << "TheoryUF::check(): shared equality, setting up " << fact << std::endl;
+ if (fact.getKind() == kind::NOT) {
+ preRegisterTerm(fact[0]);
+ } else {
+ preRegisterTerm(fact);
+ }
+ }
+
+ // Do the work
+ switch (fact.getKind()) {
case kind::EQUAL:
- d_equalityEngine.addEquality(assertion[0], assertion[1], assertion);
+ d_equalityEngine.addEquality(fact[0], fact[1], fact);
break;
case kind::APPLY_UF:
- d_equalityEngine.addEquality(assertion, d_true, assertion);
+ d_equalityEngine.addEquality(fact, d_true, fact);
break;
case kind::NOT:
- if (assertion[0].getKind() == kind::APPLY_UF) {
- d_equalityEngine.addEquality(assertion[0], d_false, assertion);
+ if (fact[0].getKind() == kind::APPLY_UF) {
+ d_equalityEngine.addEquality(fact[0], d_false, fact);
} else {
- // Disequality check
- TNode equality = assertion[0];
- if (d_equalityEngine.getRepresentative(equality[0]) == d_equalityEngine.getRepresentative(equality[1])) {
- std::vector<TNode> assumptions;
- assumptions.push_back(assertion);
- explain(equality, assumptions);
- d_conflictNode = mkAnd(assumptions);
- d_conflict = true;
- }
// Assert the dis-equality
- d_equalityEngine.addEquality(assertion[0], d_false, assertion);
+ d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
}
break;
default:
d_equalityEngine.addTerm(node[1]);
// Add the trigger for equality
d_equalityEngine.addTriggerEquality(node[0], node[1], node);
- // Add the disequality terms and triggers
- d_equalityEngine.addTerm(node);
- d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
+ d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
break;
case kind::APPLY_UF:
// Function applications/predicates
d_equalityEngine.addTriggerEquality(node, d_true, node);
d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
}
+ // Remember the function and predicate terms
+ d_functionsTerms.push_back(node);
break;
default:
// Variables etc
d_symb.assertFormula(n);
}
}
+
+EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
+ if (d_equalityEngine.areEqual(a, b)) {
+ // The terms are implied to be equal
+ return EQUALITY_TRUE;
+ }
+ if (d_equalityEngine.areDisequal(a, b)) {
+ // The rems are implied to be dis-equal
+ return EQUALITY_FALSE;
+ }
+ // All other terms we interpret as dis-equal in the model
+ return EQUALITY_FALSE_IN_MODEL;
+}
+
+void TheoryUF::addSharedTerm(TNode t) {
+ Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
+ d_equalityEngine.addTriggerTerm(t);
+}
+
+void TheoryUF::computeCareGraph(CareGraph& careGraph) {
+
+ if (d_sharedTerms.size() > 0) {
+
+ std::vector<CarePair> currentPairs;
+
+ // Go through the function terms and see if there are any to split on
+ unsigned functionTerms = d_functionsTerms.size();
+ for (unsigned i = 0; i < functionTerms; ++ i) {
+ TNode f1 = d_functionsTerms[i];
+ Node op = f1.getOperator();
+ for (unsigned j = i + 1; j < functionTerms; ++ j) {
+
+ TNode f2 = d_functionsTerms[j];
+
+ // If the operators are not the same, we can skip this pair
+ if (f2.getOperator() != op) {
+ continue;
+ }
+
+ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
+
+ // If the terms are already known to be equal, we are also in good shape
+ if (d_equalityEngine.areEqual(f1, f2)) {
+ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal, skipping" << std::endl;
+ continue;
+ }
+
+ // We have two functions f(x1, ..., xn) and f(y1, ..., yn) no known to be equal
+ // We split on the argument pairs that are are not known, unless there is some
+ // argument pair that is already dis-equal.
+ bool somePairIsDisequal = false;
+ currentPairs.clear();
+ for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
+
+ TNode x = f1[k];
+ TNode y = f2[k];
+
+ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking arguments " << x << " and " << y << std::endl;
+
+ EqualityStatus eqStatusUf = getEqualityStatus(x, y);
+
+ if (eqStatusUf == EQUALITY_FALSE) {
+ // Mark that there is a dis-equal pair and break
+ somePairIsDisequal = true;
+ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): disequal, disregarding all" << std::endl;
+ break;
+ }
+
+ if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) {
+ // Not connected to shared terms, we don't care
+ continue;
+ }
+
+ if (eqStatusUf == EQUALITY_TRUE) {
+ // We don't neeed this one
+ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal" << std::endl;
+ continue;
+ }
+
+ // Otherwise, we need to figure it out
+ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl;
+ currentPairs.push_back(CarePair(x, y, THEORY_UF));
+ }
+
+ if (!somePairIsDisequal) {
+ careGraph.insert(careGraph.end(), currentPairs.begin(), currentPairs.end());
+ }
+ }
+ }
+ }
+}
public:
NotifyClass(TheoryUF& uf): d_uf(uf) {}
- bool notifyEquality(TNode reason) {
- Debug("uf") << "NotifyClass::notifyEquality(" << reason << ")" << std::endl;
+ bool notify(TNode propagation) {
+ Debug("uf") << "NotifyClass::notify(" << propagation << ")" << std::endl;
// Just forward to uf
- return d_uf.propagate(reason);
+ return d_uf.propagate(propagation);
+ }
+
+ void notify(TNode t1, TNode t2) {
+ Debug("uf") << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+ Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+ d_uf.propagate(equality);
}
};
/** Equaltity engine */
EqualityEngine<NotifyClass> d_equalityEngine;
- /** All the literals known to be true */
- context::CDSet<TNode, TNodeHashFunction> d_knownFacts;
-
/** Are we in conflict */
context::CDO<bool> d_conflict;
void explain(TNode literal, std::vector<TNode>& assumptions);
/** Literals to propagate */
- context::CDList<TNode> d_literalsToPropagate;
+ context::CDList<Node> d_literalsToPropagate;
/** Index of the next literal to propagate */
context::CDO<unsigned> d_literalsToPropagateIndex;
+ /** All the function terms that the theory has seen */
+ context::CDList<TNode> d_functionsTerms;
/** True node for predicates = true */
Node d_true;
Theory(THEORY_UF, c, u, out, valuation),
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
- d_knownFacts(c),
d_conflict(c, false),
d_literalsToPropagate(c),
- d_literalsToPropagateIndex(c, 0)
+ d_literalsToPropagateIndex(c, 0),
+ d_functionsTerms(c)
{
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::APPLY_UF);
void staticLearning(TNode in, NodeBuilder<>& learned);
void presolve();
+ void addSharedTerm(TNode n);
+ void computeCareGraph(CareGraph& careGraph);
+
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
+
std::string identify() const {
return "THEORY_UF";
}
}
if (node[0] > node[1]) {
Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
- // If we've switched theories, we need to rewrite again (TODO: THIS IS HACK, once theories accept eq, change)
- if (Theory::theoryOf(newNode[0]) != Theory::theoryOf(newNode[1])) {
- return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
- } else {
- return RewriteResponse(REWRITE_DONE, newNode);
- }
+ return RewriteResponse(REWRITE_DONE, newNode);
}
}
return RewriteResponse(REWRITE_DONE, node);
return RewriteResponse(REWRITE_DONE, node);
}
+ static Node rewriteEquality(TNode equality) {
+ return postRewrite(equality).node;
+ }
+
static inline void init() {}
static inline void shutdown() {}
namespace CVC4 {
namespace theory {
+bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2) {
+ switch (s1) {
+ case EQUALITY_TRUE:
+ case EQUALITY_TRUE_IN_MODEL:
+ case EQUALITY_TRUE_AND_PROPAGATED:
+ switch (s2) {
+ case EQUALITY_TRUE:
+ case EQUALITY_TRUE_IN_MODEL:
+ case EQUALITY_TRUE_AND_PROPAGATED:
+ return true;
+ default:
+ return false;
+ }
+ break;
+ case EQUALITY_FALSE:
+ case EQUALITY_FALSE_IN_MODEL:
+ case EQUALITY_FALSE_AND_PROPAGATED:
+ switch (s2) {
+ case EQUALITY_FALSE:
+ case EQUALITY_FALSE_IN_MODEL:
+ case EQUALITY_FALSE_AND_PROPAGATED:
+ return true;
+ default:
+ return false;
+ }
+ break;
+ default:
+ return false;
+ }
+}
+
+
Node Valuation::getValue(TNode n) const {
return d_engine->getValue(n);
}
}
bool Valuation::hasSatValue(TNode n, bool& value) const {
- return d_engine->getPropEngine()->hasValue(n, value);
+ Node normalized = Rewriter::rewrite(n);
+ if (d_engine->getPropEngine()->isSatLiteral(normalized)) {
+ return d_engine->getPropEngine()->hasValue(normalized, value);
+ } else {
+ return false;
+ }
+}
+
+EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) {
+ return d_engine->getEqualityStatus(a, b);
}
Node Valuation::ensureLiteral(TNode n) {
namespace theory {
+/**
+ * The status of an equality in the current context.
+ */
+enum EqualityStatus {
+ /** The equality is known to be true, and has been propagated */
+ EQUALITY_TRUE_AND_PROPAGATED,
+ /** The equality is known to be true and has been propagated */
+ EQUALITY_FALSE_AND_PROPAGATED,
+ /** The equality is known to be true */
+ EQUALITY_TRUE,
+ /** The equality is known to be false */
+ EQUALITY_FALSE,
+ /** The equality is not known, but is true in the current model */
+ EQUALITY_TRUE_IN_MODEL,
+ /** The equality is not known, but is false in the current model */
+ EQUALITY_FALSE_IN_MODEL,
+ /** The equality is completely unknown */
+ EQUALITY_UNKNOWN
+};
+
+/**
+ * Returns true if the two statuses are compatible, i.e. bot TRUE
+ * or both FALSE (regardles of inmodel/propagation).
+ */
+bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
+
class Valuation {
TheoryEngine* d_engine;
public:
*/
bool hasSatValue(TNode n, bool& value) const;
+ /**
+ * Returns the equality status of the two terms, from the theory that owns the domain type.
+ * The types of a and b must be the same.
+ */
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
+
/**
* Ensure that the given node will have a designated SAT literal
* that is definitionally equal to it. The result of this function
// Notify of a start
visitor.start(node);
- // Do a topological sort of the subexpressions and preregister them
+ // Do a topological sort of the subexpressions
std::vector<stack_element> toVisit;
toVisit.push_back(stack_element(node, node));
while (!toVisit.empty()) {
arith-int-017.cvc \
arith-int-018.cvc \
arith-int-019.cvc \
- arith-int-020.cvc \
- arith-int-021.cvc \
- arith-int-023.cvc \
- arith-int-024.cvc \
- arith-int-025.cvc \
- arith-int-026.cvc \
- arith-int-027.cvc \
- arith-int-028.cvc \
- arith-int-029.cvc \
- arith-int-030.cvc \
- arith-int-031.cvc \
- arith-int-032.cvc \
- arith-int-033.cvc \
- arith-int-034.cvc \
- arith-int-035.cvc \
- arith-int-036.cvc \
- arith-int-037.cvc \
- arith-int-038.cvc \
- arith-int-039.cvc \
- arith-int-040.cvc \
- arith-int-041.cvc \
- arith-int-044.cvc \
- arith-int-045.cvc \
- arith-int-046.cvc \
- arith-int-048.cvc \
- arith-int-049.cvc \
- arith-int-051.cvc \
- arith-int-052.cvc \
- arith-int-053.cvc \
- arith-int-054.cvc \
- arith-int-055.cvc \
- arith-int-056.cvc \
- arith-int-057.cvc \
- arith-int-058.cvc \
- arith-int-059.cvc \
- arith-int-060.cvc \
- arith-int-061.cvc \
- arith-int-062.cvc \
- arith-int-063.cvc \
- arith-int-064.cvc \
- arith-int-065.cvc \
- arith-int-066.cvc \
- arith-int-067.cvc \
- arith-int-068.cvc \
- arith-int-069.cvc \
- arith-int-070.cvc \
- arith-int-071.cvc \
- arith-int-072.cvc \
- arith-int-073.cvc \
- arith-int-074.cvc \
- arith-int-075.cvc \
- arith-int-076.cvc \
- arith-int-077.cvc \
- arith-int-078.cvc \
- arith-int-079.cvc \
- arith-int-080.cvc \
- arith-int-081.cvc \
- arith-int-083.cvc \
- arith-int-085.cvc \
- arith-int-086.cvc \
- arith-int-087.cvc \
- arith-int-088.cvc \
- arith-int-089.cvc \
- arith-int-090.cvc \
- arith-int-091.cvc \
- arith-int-092.cvc \
- arith-int-093.cvc \
- arith-int-094.cvc \
- arith-int-095.cvc \
- arith-int-096.cvc \
- arith-int-099.cvc
+ arith-int-020.cvc
EXTRA_DIST = $(TESTS) \
arith-int-008.cvc \
# put it below in "TESTS +="
# Regression tests for SMT inputs
-#SMT_TESTS = \
-# pb_real_10_0100_10_10.smt \
-# pb_real_10_0100_10_11.smt \
-# pb_real_10_0100_10_15.smt \
-# pb_real_10_0100_10_16.smt \
-# pb_real_10_0100_10_19.smt \
-# pb_real_10_0200_10_22.smt \
-# pb_real_10_0200_10_26.smt \
-# pb_real_10_0200_10_29.smt
+SMT_TESTS = \
+ simple.01.cvc \
+ simple.02.cvc \
+ simple.03.cvc \
+ simple.04.cvc \
+ pb_real_10_0100_10_10.smt \
+ pb_real_10_0100_10_11.smt \
+ pb_real_10_0100_10_15.smt \
+ pb_real_10_0100_10_16.smt \
+ pb_real_10_0100_10_19.smt \
+ pb_real_10_0200_10_22.smt \
+ pb_real_10_0200_10_26.smt \
+ pb_real_10_0200_10_29.smt
# Regression tests for SMT2 inputs
SMT2_TESTS =
--- /dev/null
+% EXPECT: sat
+% EXIT: 10
+x, y: REAL;
+f: REAL -> REAL;
+
+CHECKSAT NOT (f(x) = f(y));
\ No newline at end of file
--- /dev/null
+% EXPECT: unsat
+% EXIT: 20
+x, y: REAL;
+f: REAL -> REAL;
+
+ASSERT (x <= y);
+ASSERT (y <= x);
+ASSERT NOT (f(x) = f(y));
+
+CHECKSAT;
\ No newline at end of file
--- /dev/null
+% EXPECT: sat
+% EXIT: 10
+x1, y1, z1: REAL;
+x2, y2, z2: REAL;
+f: REAL -> REAL;
+g: (REAL, REAL) -> REAL;
+
+ASSERT (z1 = f(x1));
+ASSERT (z2 = f(y1));
+ASSERT NOT (g(z1, z2) = g(z2, y2));
+
+CHECKSAT;
\ No newline at end of file
--- /dev/null
+% EXPECT: unsat
+% EXIT: 20
+x1, x2: REAL;
+y1, y2: REAL;
+f: REAL -> REAL;
+g: (REAL, REAL) -> REAL;
+
+ASSERT (x1 <= x2) AND (x2 <= x1);
+
+ASSERT NOT (g(x1, y1) = g(x2, y2));
+
+ASSERT (y1 <= f(x1)) AND (f(x1) <= y1);
+ASSERT (y2 <= f(x2)) AND (f(x2) <= y2);
+
+CHECKSAT;
\ No newline at end of file
Node leq = d_nm->mkNode(LEQ, x, c);
fakeTheoryEnginePreprocess(leq);
- d_arith->assertFact(leq);
+ d_arith->assertFact(leq, true);
d_arith->check(d_level);
fakeTheoryEnginePreprocess(leq1);
fakeTheoryEnginePreprocess(geq1);
- d_arith->assertFact(lt1);
+ d_arith->assertFact(lt1, true);
d_arith->check(d_level);
fakeTheoryEnginePreprocess(leq1);
fakeTheoryEnginePreprocess(geq1);
- d_arith->assertFact(leq0);
+ d_arith->assertFact(leq0, true);
d_arith->check(d_level);
fakeTheoryEnginePreprocess(leq1);
fakeTheoryEnginePreprocess(geq1);
- d_arith->assertFact(leq1);
+ d_arith->assertFact(leq1, true);
d_arith->check(d_level);
void testDone() {
TS_ASSERT(d_dummy->doneWrapper());
- d_dummy->assertFact(atom0);
- d_dummy->assertFact(atom1);
+ d_dummy->assertFact(atom0, true);
+ d_dummy->assertFact(atom1, true);
TS_ASSERT(!d_dummy->doneWrapper());
projects / cvc5.git / commitdiff