Enabled new UF theory by default.
Added some UF regressions.
Some work on the whole equality-over-bool-removed-in-favor-of-IFF
thing. (Congruence closure module and other things have to handle
IFF as a special case of equality, etc..)
Added pre-rewriting to TheoryBool which rewrites:
* (IFF true x) => x
* (IFF false x) => (NOT x)
* (IFF x true) => x
* (IFF x false) => (NOT x)
* (IFF x x) => true
* (IFF x (NOT x)) => false
* (IFF (NOT x) x) => false
* (ITE true x y) => x
* (ITE false x y) => y
* (ITE cond x x) => x
Added post-rewriting that does all of the above, plus normalize IFF and ITE:
* (IFF x y) => (IFF y x), if y < x
* (ITE (NOT cond) x y) => (ITE cond y x)
(Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.)
A little more debugging output from CNF stream, context pushes/pops,
ITE removal.
Some more documentation.
Fixed some typos.
void Context::push() {
- Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push {" << std::endl;
+ Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to "
+ << getLevel() + 1 << "] {" << std::endl;
// Create a new memory region
d_pCMM->push();
pCNO = pCNO->d_pCNOnext;
}
- Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop" << std::endl;
+ Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
+ << getLevel() << "]" << std::endl;
}
printf("morgan\n");
exit(1);
} else {
- throw OptionException(string("unknown language for --uf: `") +
+ throw OptionException(string("unknown option for --uf: `") +
optarg + "'. Try --uf help.");
}
}
}
SatLiteral CnfStream::convertAtom(TNode node) {
- Assert(!isCached(node), "atom already mapped!");
-
Debug("cnf") << "convertAtom(" << node << ")" << endl;
+ Assert(!isCached(node), "atom already mapped!");
+
bool theoryLiteral = node.getKind() != kind::VARIABLE;
SatLiteral lit = newLiteral(node, theoryLiteral);
Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
+ Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
+
// Convert the children to CNF
SatLiteral a = toCNF(iffNode[0]);
SatLiteral b = toCNF(iffNode[1]);
Assert(iteNode.getKind() == ITE);
Assert(iteNode.getNumChildren() == 3);
- Debug("cnf") << "handlIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
+ Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
SatLiteral condLit = toCNF(iteNode[0]);
SatLiteral thenLit = toCNF(iteNode[1]);
nodeLit = handleAnd(node);
break;
case EQUAL:
- if(node[0].getType().isBoolean() && node[1].getType().isBoolean()) {
- nodeLit = handleIff(node[0].iffNode(node[1]));
+ if(node[0].getType().isBoolean()) {
+ // should have an IFF instead
+ Unreachable("= Bool Bool shouldn't be possible ?!");
+ //nodeLit = handleIff(node[0].iffNode(node[1]));
} else {
nodeLit = convertAtom(node);
}
* Also writes relations with constants on both sides to TRUE or FALSE.
* If it can, it returns true and sets res to this value.
*
- * This is for optimizing rewriteAtom() to avoid the more compuationally
+ * This is for optimizing rewriteAtom() to avoid the more computationally
* expensive general rewriting procedure.
*
* If simplification is not done, it returns Node::null()
Node sub = makeUnaryMinusNode(t[0]);
return rewrite(sub);
}else{
- Unreachable();
- return Node::null();
+ Unhandled(t);
}
}
case GEQ: return LEQ;
case GT: return LT;
default:
- Unhandled();
+ Unhandled(k);
}
return NULL_EXPR;
}else{
}
RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
+ // ensure a hard link to the node we're returning
+ Node out;
+
// Look for multiplications with a 0 argument and rewrite the whole
// thing as 0
if(n.getKind() == MULT) {
for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
if((*i).getKind() == CONST_RATIONAL) {
if((*i).getConst<Rational>() == ratZero) {
- n = NodeManager::currentNM()->mkConst(ratZero);
+ out = NodeManager::currentNM()->mkConst(ratZero);
break;
}
} else if((*i).getKind() == CONST_INTEGER) {
if((*i).getConst<Integer>() == intZero) {
if(n.getType().isInteger()) {
- n = NodeManager::currentNM()->mkConst(intZero);
+ out = NodeManager::currentNM()->mkConst(intZero);
break;
} else {
- n = NodeManager::currentNM()->mkConst(ratZero);
+ out = NodeManager::currentNM()->mkConst(ratZero);
break;
}
}
}
}
+ } else if(n.getKind() == EQUAL) {
+ if(n[0] == n[1]) {
+ out = NodeManager::currentNM()->mkConst(true);
+ }
+ }
+
+ if(out.isNull()) {
+ // no preRewrite to perform
+ return RewriteComplete(Node(n));
+ } else {
+ // out is always a constant, so doesn't need to be rewritten again
+ return RewriteComplete(out);
}
- return RewriteComplete(Node(n));
}
Node TheoryArith::rewrite(TNode n){
libbooleans_la_SOURCES = \
theory_bool.h \
+ theory_bool.cpp \
theory_bool_type_rules.h
EXTRA_DIST = kinds
--- /dev/null
+/********************* */
+/*! \file theory_bool.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The theory of booleans.
+ **
+ ** The theory of booleans.
+ **/
+
+#include "theory/theory.h"
+#include "theory/booleans/theory_bool.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+
+RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) {
+ if(n.getKind() == kind::IFF) {
+ NodeManager* nodeManager = NodeManager::currentNM();
+ Node tt = nodeManager->mkConst(true);
+ Node ff = nodeManager->mkConst(false);
+
+ // rewrite simple cases of IFF
+ if(n[0] == tt) {
+ // IFF true x
+ return RewriteAgain(n[1]);
+ } else if(n[1] == tt) {
+ // IFF x true
+ return RewriteAgain(n[0]);
+ } else if(n[0] == ff) {
+ // IFF false x
+ return RewriteAgain(n[1].notNode());
+ } else if(n[1] == ff) {
+ // IFF x false
+ return RewriteAgain(n[0].notNode());
+ } else if(n[0] == n[1]) {
+ // IFF x x
+ return RewriteComplete(tt);
+ } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
+ // IFF (NOT x) x
+ return RewriteComplete(ff);
+ } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
+ // IFF x (NOT x)
+ return RewriteComplete(ff);
+ }
+ } else if(n.getKind() == kind::ITE) {
+ // non-Boolean-valued ITEs should have been removed in place of
+ // a variable
+ Assert(n.getType().isBoolean());
+
+ NodeManager* nodeManager = NodeManager::currentNM();
+
+ // rewrite simple cases of ITE
+ if(n[0] == nodeManager->mkConst(true)) {
+ // ITE true x y
+ return RewriteAgain(n[1]);
+ } else if(n[0] == nodeManager->mkConst(false)) {
+ // ITE false x y
+ return RewriteAgain(n[2]);
+ } else if(n[1] == n[2]) {
+ // ITE c x x
+ return RewriteAgain(n[1]);
+ }
+ }
+
+ return RewriteComplete(n);
+}
+
+
+RewriteResponse TheoryBool::postRewrite(TNode n, bool topLevel) {
+ if(n.getKind() == kind::IFF) {
+ NodeManager* nodeManager = NodeManager::currentNM();
+ Node tt = nodeManager->mkConst(true);
+ Node ff = nodeManager->mkConst(false);
+
+ // rewrite simple cases of IFF
+ if(n[0] == tt) {
+ // IFF true x
+ return RewriteComplete(n[1]);
+ } else if(n[1] == tt) {
+ // IFF x true
+ return RewriteComplete(n[0]);
+ } else if(n[0] == ff) {
+ // IFF false x
+ return RewriteAgain(n[1].notNode());
+ } else if(n[1] == ff) {
+ // IFF x false
+ return RewriteAgain(n[0].notNode());
+ } else if(n[0] == n[1]) {
+ // IFF x x
+ return RewriteComplete(tt);
+ } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
+ // IFF (NOT x) x
+ return RewriteComplete(ff);
+ } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
+ // IFF x (NOT x)
+ return RewriteComplete(ff);
+ }
+
+ if(n[1] < n[0]) {
+ // normalize (IFF x y) ==> (IFF y x), if y < x
+ return RewriteComplete(n[1].iffNode(n[0]));
+ }
+ } else if(n.getKind() == kind::ITE) {
+ // non-Boolean-valued ITEs should have been removed in place of
+ // a variable
+ Assert(n.getType().isBoolean());
+
+ NodeManager* nodeManager = NodeManager::currentNM();
+
+ // rewrite simple cases of ITE
+ if(n[0] == nodeManager->mkConst(true)) {
+ // ITE true x y
+ return RewriteComplete(n[1]);
+ } else if(n[0] == nodeManager->mkConst(false)) {
+ // ITE false x y
+ return RewriteComplete(n[2]);
+ } else if(n[1] == n[2]) {
+ // ITE c x x
+ return RewriteComplete(n[1]);
+ }
+
+ if(n[0].getKind() == kind::NOT) {
+ // rewrite (ITE (NOT c) x y) to (ITE c y x)
+ Node out = nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1]);
+ return RewriteComplete(out);
+ }
+ }
+
+ return RewriteComplete(n);
+}
+
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
void check(Effort e) { Unimplemented(); }
void propagate(Effort e) { Unimplemented(); }
void explain(TNode n, Effort e) { Unimplemented(); }
+
+ RewriteResponse preRewrite(TNode n, bool topLevel);
+ RewriteResponse postRewrite(TNode n, bool topLevel);
+
std::string identify() const { return std::string("TheoryBool"); }
};
#include "expr/kind.h"
using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory::builtin;
namespace CVC4 {
namespace theory {
if(in.getNumChildren() == 2) {
// if this is the case exactly 1 != pair will be generated so the
// AND is not required
- Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]);
- Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
+ Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ?
+ kind::IFF : kind::EQUAL,
+ in[0], in[1]);
+ Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
return neq;
}
// assume that in.getNumChildren() > 2 => diseqs.size() > 1
for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
TNode::iterator j = i;
while(++j != in.end()) {
- Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j);
- Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
+ Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ?
+ kind::IFF : kind::EQUAL,
+ *i, *j);
+ Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
diseqs.push_back(neq);
}
}
- Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs);
+ Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs);
return out;
}
* rewrite a term to a strictly larger term that contains itself, as
* this will cause a loop of hard Node links in the cache (and thus
* memory leakage).
+ *
+ * Be careful with the return value. If a preRewrite() can return a
+ * sub-expression, and that sub-expression can be a member of the
+ * same theory and could be rewritten, make sure to return
+ * RewriteAgain instead of RewriteComplete. This is an easy mistake
+ * to make, as preRewrite() is often a short-circuiting version of
+ * the same rewrites that occur in postRewrite(); however, in the
+ * postRewrite() case, the subexpressions have all been
+ * post-rewritten. In the preRewrite() case, they have NOT yet been
+ * pre-rewritten. For example, (ITE true (ITE true x y) z) should
+ * pre-rewrite to x; but if the outer preRewrite() returns
+ * RewriteComplete, the result of the pre-rewrite will be
+ * (ITE true x y).
*/
virtual RewriteResponse preRewrite(TNode n, bool topLevel) {
Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl;
// }
}
else if (fact.getKind() == kind::EQUAL) {
+ // FIXME: kind::IFF as well ?
// Automatically track all asserted equalities in the shared term manager
d_engine->getSharedTermManager()->addEq(fact);
}
if(! fact.getAttribute(RegisteredAttr())) {
- std::list<TNode> toReg;
+ list<TNode> toReg;
toReg.push_back(fact);
- Debug("theory") << "Theory::get(): registering new atom" << std::endl;
+ Debug("theory") << "Theory::get(): registering new atom" << endl;
/* Essentially this is doing a breadth-first numbering of
* non-registered subterms with children. Any non-registered
* leaves are immediately registered. */
- for(std::list<TNode>::iterator workp = toReg.begin();
+ for(list<TNode>::iterator workp = toReg.begin();
workp != toReg.end();
++workp) {
* and the above registration of leaves, this should ensure that
* all subterms in the entire tree were registered in
* reverse-topological order. */
- for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+ for(list<TNode>::reverse_iterator i = toReg.rbegin();
i != toReg.rend();
++i) {
Node cachedRewrite;
NodeManager *nodeManager = NodeManager::currentNM();
if(nodeManager->getAttribute(node, theory::IteRewriteAttr(), cachedRewrite)) {
+ Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
}
Node noItes = removeITEs(in);
Node out;
+ Debug("theory-rewrite") << "removeITEs of: " << in << endl
+ << " is: " << noItes << endl;
+
// descend top-down into the theory rewriters
vector<RewriteStackElement> stack;
stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), topLevel));
rse.d_node.toString().c_str(),
rewrittenAgain.toString().c_str());
}
-
setPostRewriteCache(original, wasTopLevel, rse.d_node);
out = rse.d_node;
#include "util/congruence_closure.h"
using namespace CVC4;
-using namespace CVC4::kind;
using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::uf;
d_disequality(ctxt),
d_conflict(),
d_trueNode(),
- d_falseNode() {
+ d_falseNode(),
+ d_activeAssertions(ctxt) {
TypeNode boolType = NodeManager::currentNM()->booleanType();
d_trueNode = NodeManager::currentNM()->mkVar("TRUE_UF", boolType);
d_falseNode = NodeManager::currentNM()->mkVar("FALSE_UF", boolType);
if(topLevel) {
Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
Node ret(n);
- if(n.getKind() == EQUAL) {
+ if(n.getKind() == kind::EQUAL ||
+ n.getKind() == kind::IFF) {
if(n[0] == n[1]) {
ret = NodeManager::currentNM()->mkConst(true);
}
nb << *i;
}
} else {
- Assert(explanation.getKind() == kind::EQUAL);
+ Assert(explanation.getKind() == kind::EQUAL ||
+ explanation.getKind() == kind::IFF);
nb << explanation;
}
nb << diseq.notNode();
}
}
-void TheoryUFMorgan::unionClasses(TNode a, TNode b) {
- if(a == b) {
- return;
- }
- Assert(d_unionFind.find(a) == d_unionFind.end());
- Assert(d_unionFind.find(b) == d_unionFind.end());
- d_unionFind[a] = b;
-}
-
void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
Debug("uf") << "uf: notified of merge " << a << std::endl
<< " and " << b << std::endl;
return;
}
+ merge(a, b);
+}
+
+void TheoryUFMorgan::merge(TNode a, TNode b) {
+ Assert(d_conflict.isNull());
+
// make "a" the one with shorter diseqList
DiseqLists::iterator deq_ia = d_disequalities.find(a);
DiseqLists::iterator deq_ib = d_disequalities.find(b);
b = find(b);
Debug("uf") << "uf: uf reps are " << a << std::endl
<< " and " << b << std::endl;
- unionClasses(a, b);
+
+ if(a == b) {
+ return;
+ }
+
+ d_unionFind[a] = b;
DiseqLists::iterator deq_i = d_disequalities.find(a);
if(deq_i != d_disequalities.end()) {
std::set<TNode> alreadyDiseqs;
DiseqLists::iterator deq_ib = d_disequalities.find(b);
if(deq_ib != d_disequalities.end()) {
- DiseqList* deq = (*deq_i).second;
+ DiseqList* deq = (*deq_ib).second;
for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
TNode deqn = *j;
TNode s = deqn[0];
for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
Debug("uf") << " deq(a) ==> " << *j << std::endl;
TNode deqn = *j;
- Assert(deqn.getKind() == kind::EQUAL);
+ Assert(deqn.getKind() == kind::EQUAL ||
+ deqn.getKind() == kind::IFF);
TNode s = deqn[0];
TNode t = deqn[1];
Debug("uf") << " s ==> " << s << std::endl
void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) {
Debug("uf") << "appending " << eq << std::endl
<< " to diseq list of " << of << std::endl;
- Assert(eq.getKind() == kind::EQUAL);
+ Assert(eq.getKind() == kind::EQUAL ||
+ eq.getKind() == kind::IFF);
Assert(of == debugFind(of));
DiseqLists::iterator deq_i = d_disequalities.find(of);
DiseqList* deq;
}
void TheoryUFMorgan::addDisequality(TNode eq) {
- Assert(eq.getKind() == kind::EQUAL);
+ Assert(eq.getKind() == kind::EQUAL ||
+ eq.getKind() == kind::IFF);
- Node a = eq[0];
- Node b = eq[1];
+ TNode a = eq[0];
+ TNode b = eq[1];
appendToDiseqList(find(a), eq);
appendToDiseqList(find(b), eq);
while(!done()) {
Node assertion = get();
+ d_activeAssertions.push_back(assertion);
+
Debug("uf") << "uf check(): " << assertion << std::endl;
switch(assertion.getKind()) {
- case EQUAL:
+ case kind::EQUAL:
+ case kind::IFF:
d_cc.addEquality(assertion);
if(!d_conflict.isNull()) {
Node conflict = constructConflict(d_conflict);
d_out->conflict(conflict, false);
return;
}
+ merge(assertion[0], assertion[1]);
break;
- case APPLY_UF:
+ case kind::APPLY_UF:
{ // predicate
- Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion, d_trueNode);
+
+ // assert it's a predicate
+ Assert(assertion.getOperator().getType().getRangeType().isBoolean());
+
+ Node eq = NodeManager::currentNM()->mkNode(kind::IFF,
+ assertion, d_trueNode);
d_cc.addTerm(assertion);
d_cc.addEquality(eq);
- Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+ Debug("uf") << "true == false ? "
+ << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+
Assert(find(d_trueNode) != find(d_falseNode));
+
+ merge(eq[0], eq[1]);
}
break;
- case NOT:
- if(assertion[0].getKind() == kind::EQUAL) {
+ case kind::NOT:
+ if(assertion[0].getKind() == kind::EQUAL ||
+ assertion[0].getKind() == kind::IFF) {
Node a = assertion[0][0];
Node b = assertion[0][1];
// to this disequality.
Assert(!d_cc.areCongruent(a, b));
} else {
+ // negation of a predicate
Assert(assertion[0].getKind() == kind::APPLY_UF);
- Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion[0], d_falseNode);
+
+ // assert it's a predicate
+ Assert(assertion[0].getOperator().getType().getRangeType().isBoolean());
+
+ Node eq = NodeManager::currentNM()->mkNode(kind::IFF, assertion[0], d_falseNode);
d_cc.addTerm(assertion[0]);
d_cc.addEquality(eq);
- Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+
+ Debug("uf") << "true == false ? "
+ << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+
Assert(find(d_trueNode) != find(d_falseNode));
+
+ merge(eq[0], eq[1]);
}
break;
default:
Unhandled(assertion.getKind());
}
+
+ if(Debug.isOn("uf")) {
+ dump();
+ }
}
Debug("uf") << "uf check() done = " << (done() ? "true" : "false") << std::endl;
Debug("uf") << "uf: begin propagate(" << level << ")" << std::endl;
Debug("uf") << "uf: end propagate(" << level << ")" << std::endl;
}
+
+void TheoryUFMorgan::dump() {
+ Debug("uf") << "============== THEORY_UF ==============" << std::endl;
+ Debug("uf") << "Active assertions list:" << std::endl;
+ for(context::CDList<Node>::const_iterator i = d_activeAssertions.begin();
+ i != d_activeAssertions.end();
+ ++i) {
+ Debug("uf") << " " << *i << std::endl;
+ }
+ Debug("uf") << "Congruence union-find:" << std::endl;
+ for(UnionFind::const_iterator i = d_unionFind.begin();
+ i != d_unionFind.end();
+ ++i) {
+ Debug("uf") << " " << (*i).first << " ==> " << (*i).second << std::endl;
+ }
+ Debug("uf") << "Disequality lists:" << std::endl;
+ for(DiseqLists::const_iterator i = d_disequalities.begin();
+ i != d_disequalities.end();
+ ++i) {
+ Debug("uf") << " " << (*i).first << ":" << std::endl;
+ DiseqList* dl = (*i).second;
+ for(DiseqList::const_iterator j = dl->begin();
+ j != dl->end();
+ ++j) {
+ Debug("uf") << " " << *j << std::endl;
+ }
+ }
+ Debug("uf") << "=======================================" << std::endl;
+}
Node d_trueNode, d_falseNode;
+ context::CDList<Node> d_activeAssertions;
+
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
TNode find(TNode a);
TNode debugFind(TNode a) const;
- void unionClasses(TNode a, TNode b);
void appendToDiseqList(TNode of, TNode eq);
void addDisequality(TNode eq);
*/
void notifyCongruent(TNode a, TNode b);
+ /**
+ * Internally handle a congruence, whether generated by the CC
+ * module or from a theory check(). Merges the classes from a and b
+ * and looks for a conflict. If there is one, sets d_conflict.
+ */
+ void merge(TNode a, TNode b);
+
+ void dump();
+
};/* class TheoryUFMorgan */
}/* CVC4::theory::uf::morgan namespace */
*/
void addEquality(TNode inputEq) {
Debug("cc") << "CC addEquality[" << d_context->getLevel() << "]: " << inputEq << std::endl;
- Assert(inputEq.getKind() == kind::EQUAL);
- NodeBuilder<> eqb(kind::EQUAL);
+ Assert(inputEq.getKind() == kind::EQUAL ||
+ inputEq.getKind() == kind::IFF);
+ NodeBuilder<> eqb(inputEq.getKind());
if(inputEq[1].getKind() == kind::APPLY_UF &&
inputEq[0].getKind() != kind::APPLY_UF) {
eqb << flatten(inputEq[1]) << inputEq[0];
EqMap::iterator i = d_eqMap.find(t);
if(i == d_eqMap.end()) {
Node v = NodeManager::currentNM()->mkSkolem(t.getType());
- addEq(NodeManager::currentNM()->mkNode(kind::EQUAL, t, v), TNode::null());
+ addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null());
d_eqMap.insert(t, v);
return v;
} else {
*/
inline Node explain(TNode eq)
throw(CongruenceClosureException, AssertionException) {
- Assert(eq.getKind() == kind::EQUAL);
+ Assert(eq.getKind() == kind::EQUAL ||
+ eq.getKind() == kind::IFF);
return explain(eq[0], eq[1]);
}
return TNode::null();
} else {
TNode l = (*i).second;
- Assert(l.getKind() == kind::EQUAL);
+ Assert(l.getKind() == kind::EQUAL ||
+ l.getKind() == kind::IFF);
return l;
}
}
*/
inline void setLookup(TNode a, TNode b) {
Assert(a.getKind() == kind::TUPLE);
- Assert(b.getKind() == kind::EQUAL);
+ Assert(b.getKind() == kind::EQUAL ||
+ b.getKind() == kind::IFF);
d_lookup[a] = b;
}
*/
inline void appendToUseList(TNode of, TNode eq) {
Debug("cc") << "adding " << eq << " to use list of " << of << std::endl;
- Assert(eq.getKind() == kind::EQUAL);
+ Assert(eq.getKind() == kind::EQUAL ||
+ eq.getKind() == kind::IFF);
Assert(of == find(of));
UseLists::iterator usei = d_useList.find(of);
UseList* ul;
d_proofRewrite[eq] = inputEq;
Debug("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl;
- Assert(eq.getKind() == kind::EQUAL);
+ Assert(eq.getKind() == kind::EQUAL ||
+ eq.getKind() == kind::IFF);
Assert(eq[1].getKind() != kind::APPLY_UF);
if(areCongruent(eq[0], eq[1])) {
Debug("cc") << "CC -- redundant, ignoring...\n";
Debug("cc") << "=== e is " << e << " ===" << std::endl;
TNode a, b;
- if(e.getKind() == kind::EQUAL) {
+ if(e.getKind() == kind::EQUAL ||
+ e.getKind() == kind::IFF) {
// e is an equality a = b (a, b are constants)
a = e[0];
Assert(e.getKind() == kind::TUPLE);
Assert(e.getNumChildren() == 2);
- Assert(e[0].getKind() == kind::EQUAL);
- Assert(e[1].getKind() == kind::EQUAL);
+ Assert(e[0].getKind() == kind::EQUAL ||
+ e[0].getKind() == kind::IFF);
+ Assert(e[1].getKind() == kind::EQUAL ||
+ e[1].getKind() == kind::IFF);
// tuple is (eq, lookup)
a = e[0][1];
++i) {
TNode eq = *i;
Debug("cc") << "CC -- useList: " << eq << std::endl;
- Assert(eq.getKind() == kind::EQUAL);
+ Assert(eq.getKind() == kind::EQUAL ||
+ eq.getKind() == kind::IFF);
// change from paper
// use list elts can have form (apply c..) = x OR x = (apply c..)
Assert(eq[0].getKind() == kind::APPLY_UF || eq[1].getKind() == kind::APPLY_UF);
Node theLookup = lookup(ap);
if(allConstants && !theLookup.isNull()) {
- Assert(theLookup.getKind() == kind::EQUAL);
+ Assert(theLookup.getKind() == kind::EQUAL ||
+ theLookup.getKind() == kind::IFF);
Assert(theLookup[0].getKind() == kind::APPLY_UF);
Assert(theLookup[1].getKind() != kind::APPLY_UF);
return find(theLookup[1]);
while(a != c) {
Node b = d_proof[a];
Node e = d_proofLabel[a];
- if(e.getKind() == kind::EQUAL) {
+ if(e.getKind() == kind::EQUAL ||
+ e.getKind() == kind::IFF) {
pf.push_back(e);
} else {
Assert(e.getKind() == kind::TUPLE);
out << " " << (*i).first << " => " << n << std::endl;
}
+ out << "Care set:" << std::endl;
+ for(typename CongruenceClosure<OutputChannel>::CareSet::const_iterator i = cc.d_careSet.begin(); i != cc.d_careSet.end(); ++i) {
+ out << " " << *i << std::endl;
+ }
+
out << "==============================================" << std::endl;
return out;
err(0),
verbosity(0),
lang(parser::LANG_AUTO),
- uf_implementation(TIM),
+ uf_implementation(MORGAN),
parseOnly(false),
semanticChecks(true),
memoryMap(false),
eq_diamond1.smt \
eq_diamond14.smt \
eq_diamond14.reduced.smt \
+ eq_diamond14.reduced2.smt \
dead_dnd002.smt \
iso_brn001.smt \
simple.01.cvc \
:extrafuns ((y1 V))
:extrafuns ((x1 V))
:extrafuns ((y0 V))
-:status unknown
:formula
(flet ($n1 (= x0 y0))
(flet ($n2 (= y0 x1))
--- /dev/null
+(benchmark eq_diamond14
+:logic QF_UF
+:extrasorts (V)
+:extrafuns ((z9 V))
+:extrafuns ((x10 V))
+:extrafuns ((x9 V))
+:extrafuns ((x13 V))
+:extrafuns ((x0 V))
+:extrafuns ((z12 V))
+:extrafuns ((x12 V))
+:extrafuns ((y12 V))
+:extrafuns ((z11 V))
+:extrafuns ((x11 V))
+:extrafuns ((y11 V))
+:extrafuns ((z10 V))
+:extrafuns ((y10 V))
+:extrafuns ((y8 V))
+:extrafuns ((x8 V))
+:extrafuns ((y7 V))
+:extrafuns ((x7 V))
+:extrafuns ((z6 V))
+:extrafuns ((x6 V))
+:extrafuns ((y6 V))
+:extrafuns ((z5 V))
+:extrafuns ((x5 V))
+:extrafuns ((y5 V))
+:extrafuns ((y4 V))
+:extrafuns ((x4 V))
+:extrafuns ((y3 V))
+:extrafuns ((x3 V))
+:extrafuns ((y2 V))
+:extrafuns ((x2 V))
+:extrafuns ((y1 V))
+:extrafuns ((x1 V))
+:extrafuns ((y0 V))
+:status unsat
+:formula
+(flet ($n1 (= x0 y0))
+(flet ($n2 (= y0 x1))
+(flet ($n3 (and $n1 $n2))
+(flet ($n4 (= x1 y1))
+(flet ($n5 (= y1 x2))
+(flet ($n6 (and $n4 $n5))
+(flet ($n7 (= x2 y2))
+(flet ($n8 (= y2 x3))
+(flet ($n9 (and $n7 $n8))
+(flet ($n10 (= x3 y3))
+(flet ($n11 (= y3 x4))
+(flet ($n12 (and $n10 $n11))
+(flet ($n13 (= x4 y4))
+(flet ($n14 (= y4 x5))
+(flet ($n15 (and $n13 $n14))
+(flet ($n16 false)
+(flet ($n17 (= y5 x6))
+(flet ($n18 (and $n16 $n17))
+(flet ($n19 (= x5 z5))
+(flet ($n20 (= x6 z5))
+(flet ($n21 (and $n19 $n20))
+(flet ($n22 (or $n18 $n21))
+(flet ($n23 (= x6 y6))
+(flet ($n24 (= y6 x7))
+(flet ($n25 (and $n23 $n24))
+(flet ($n26 (= x6 z6))
+(flet ($n27 (= x7 z6))
+(flet ($n28 (and $n26 $n27))
+(flet ($n29 (or $n25 $n28))
+(flet ($n30 (= x7 y7))
+(flet ($n31 (= y7 x8))
+(flet ($n32 (and $n30 $n31))
+(flet ($n33 (= x8 y8))
+(flet ($n34 (= y8 x9))
+(flet ($n35 (and $n33 $n34))
+(flet ($n36 (= x10 y10))
+(flet ($n37 (= y10 x11))
+(flet ($n38 (and $n36 $n37))
+(flet ($n39 (= x10 z10))
+(flet ($n40 (= x11 z10))
+(flet ($n41 (and $n39 $n40))
+(flet ($n42 (or $n38 $n41))
+(flet ($n43 (= x11 y11))
+(flet ($n44 (= y11 x12))
+(flet ($n45 (and $n43 $n44))
+(flet ($n46 (= x11 z11))
+(flet ($n47 (= x12 z11))
+(flet ($n48 (and $n46 $n47))
+(flet ($n49 (or $n45 $n48))
+(flet ($n50 (= x12 y12))
+(flet ($n51 (= y12 x13))
+(flet ($n52 (and $n50 $n51))
+(flet ($n53 (= x12 z12))
+(flet ($n54 (= x13 z12))
+(flet ($n55 (and $n53 $n54))
+(flet ($n56 (or $n52 $n55))
+(flet ($n57 (= x0 x13))
+(flet ($n58 (not $n57))
+(flet ($n59 (= x9 z9))
+(flet ($n60 (= x10 z9))
+(flet ($n61 (and $n59 $n60))
+(flet ($n62 (or $n16 $n61))
+(flet ($n63 (and $n3 $n6 $n9 $n12 $n15 $n22 $n29 $n32 $n35 $n42 $n49 $n56 $n58 $n62))
+$n63
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
--- /dev/null
+(benchmark euf_simp1.smt
+:status sat
+:logic QF_UF
+:category { crafted }
+
+:extrafuns ((x U))
+:extrafuns ((y U))
+:extrapreds ((f U))
+
+
+
+:formula
+(and
+ (f x)
+ (iff (f x) (f y))
+ (not (f y))
+)
+)
cvc4full="$cvc4dirfull/$cvc4base"
echo running $cvc4full `basename "$benchmark"` from `dirname "$benchmark"`
( cd `dirname "$benchmark"`;
- "$cvc4full" --segv-nospin `basename "$benchmark"`;
+ "$cvc4full" -d extra-checking --segv-nospin `basename "$benchmark"`;
echo $? >"$exitstatusfile"
) > "$outfile" 2> "$errfile"
projects / cvc5.git / commitdiff