summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am14
-rw-r--r--src/lib/Makefile4
-rw-r--r--src/prop/minisat/core/Solver.cc3
-rw-r--r--src/prop/sat.cpp4
-rw-r--r--src/prop/sat.h2
-rw-r--r--src/smt/smt_engine.cpp29
-rw-r--r--src/smt/smt_engine.h3
-rw-r--r--src/theory/builtin/theory_builtin.h6
-rw-r--r--src/theory/output_channel.h5
-rw-r--r--src/theory/theory.h28
-rw-r--r--src/theory/theory_engine.cpp56
-rw-r--r--src/theory/theory_engine.h17
-rw-r--r--src/theory/uf/Makefile.am4
-rw-r--r--src/theory/uf/morgan/Makefile4
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.cpp401
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.h78
-rw-r--r--src/theory/uf/morgan/union_find.h10
-rw-r--r--src/theory/uf/tim/Makefile4
-rw-r--r--src/util/congruence_closure.h26
-rw-r--r--src/util/stats.h27
-rw-r--r--test/regress/regress0/uf/Makefile.am1
-rw-r--r--test/unit/Makefile.am2
-rw-r--r--test/unit/theory/stacking_map_black.h160
-rw-r--r--test/unit/theory/union_find_black.h189
24 files changed, 934 insertions, 143 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index 48e052eef..d65ddc570 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -24,11 +24,12 @@ noinst_LTLIBRARIES = libcvc4_noinst.la
libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION)
-# empty.cpp is a fake file added to "trick" automake into linking us as a
-# C++ library (rather than as a C library, which messes up exception
-# handling support)
-libcvc4_la_SOURCES = empty.cpp
-libcvc4_noinst_la_SOURCES = empty.cpp
+# This "tricks" automake into linking us as a C++ library (rather than
+# as a C library, which messes up exception handling support)
+nodist_EXTRA_libcvc4_noinst_la_SOURCES = dummy.cpp
+nodist_EXTRA_libcvc4_la_SOURCES = dummy.cpp
+libcvc4_noinst_la_SOURCES =
+libcvc4_la_SOURCES =
libcvc4_la_LIBADD = \
@builddir@/util/libutil.la \
@builddir@/expr/libexpr.la \
@@ -56,9 +57,6 @@ EXTRA_DIST = \
include/cvc4_private.h \
include/cvc4_public.h
-# empty.cpp hack; see above
-empty.cpp:; touch empty.cpp
-
publicheaders = \
include/cvc4_public.h \
include/cvc4parser_public.h
diff --git a/src/lib/Makefile b/src/lib/Makefile
new file mode 100644
index 000000000..9811fec4f
--- /dev/null
+++ b/src/lib/Makefile
@@ -0,0 +1,4 @@
+topdir = ../..
+srcdir = src/lib
+
+include $(topdir)/Makefile.subdir
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 4817ec1f5..18ed9b5da 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -986,6 +986,9 @@ lbool Solver::search(int nof_conflicts)
// Reached bound on number of conflicts:
progress_estimate = progressEstimate();
cancelUntil(0);
+ // [mdeters] notify theory engine of restarts for deferred
+ // theory processing
+ proxy->notifyRestart();
return l_Undef; }
// Simplify the set of problem clauses:
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 97c5d1419..b78f20ee8 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -102,5 +102,9 @@ TNode SatSolver::getNode(SatLiteral lit) {
return d_cnfStream->getNode(lit);
}
+void SatSolver::notifyRestart() {
+ d_theoryEngine->notifyRestart();
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 6e244d9d7..cc81ea5c6 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -247,6 +247,8 @@ public:
TNode getNode(SatLiteral lit);
+ void notifyRestart();
+
};/* class SatSolver */
/* Functions that delegate to the concrete SAT solver. */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 99d830077..6bfdda079 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -414,16 +414,31 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n)
}
}
-Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n)
+Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in)
throw(NoSuchFunctionException, AssertionException) {
+
+ Node n;
if(!smt.d_lazyDefinitionExpansion) {
- Node node = expandDefinitions(smt, n);
- Debug("expand") << "have: " << n << endl
- << "made: " << node << endl;
- return smt.d_theoryEngine->preprocess(node);
+ Debug("expand") << "have: " << n << endl;
+ n = expandDefinitions(smt, in);
+ Debug("expand") << "made: " << n << endl;
} else {
- return smt.d_theoryEngine->preprocess(n);
+ n = in;
}
+
+ // For now, don't re-statically-learn from learned facts; this could
+ // be useful though (e.g., theory T1 could learn something further
+ // from something learned previously by T2).
+ NodeBuilder<> learned(kind::AND);
+ learned << n;
+ smt.d_theoryEngine->staticLearning(n, learned);
+ if(learned.getNumChildren() == 1) {
+ learned.clear();
+ } else {
+ n = learned;
+ }
+
+ return smt.d_theoryEngine->preprocess(n);
}
Result SmtEngine::check() {
@@ -516,6 +531,8 @@ Expr SmtEngine::simplify(const Expr& e) {
e.getType(true);// ensure expr is type-checked at this point
}
Debug("smt") << "SMT simplify(" << e << ")" << endl;
+ // probably want to do an addFormula(), to get preprocessing, static
+ // learning, definition expansion...
Unimplemented();
}
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b8a72dc38..c884b2c5f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -289,6 +289,9 @@ public:
/**
* Simplify a formula without doing "much" work. Requires assist
* from the SAT Engine.
+ *
+ * @todo (design) is this meant to give an equivalent or an
+ * equisatisfiable formula?
*/
Expr simplify(const Expr& e);
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index f373d16c2..cce5ac6b8 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -32,8 +32,12 @@ class TheoryBuiltin : public Theory {
static Node blastDistinct(TNode in);
public:
- TheoryBuiltin(int id, context::Context* c, OutputChannel& out) : Theory(id, c, out) { }
+ TheoryBuiltin(int id, context::Context* c, OutputChannel& out) :
+ Theory(id, c, out) {
+ }
+
~TheoryBuiltin() { }
+
void preRegisterTerm(TNode n) { Unreachable(); }
void registerTerm(TNode n) { Unreachable(); }
void check(Effort e) { Unreachable(); }
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 269f28732..7d7da35c5 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -82,8 +82,7 @@ public:
/**
* Propagate a theory literal.
*
- * @param n - a theory consequence at the current decision level.
- *
+ * @param n - a theory consequence at the current decision level
* @param safe - whether it is safe to be interrupted
*/
virtual void propagate(TNode n, bool safe = false)
@@ -91,7 +90,7 @@ public:
/**
* Tell the core that a valid theory lemma at decision level 0 has
- * been detected. (This request a split.)
+ * been detected. (This requests a split.)
*
* @param n - a theory lemma valid at decision level 0
* @param safe - whether it is safe to be interrupted
diff --git a/src/theory/theory.h b/src/theory/theory.h
index de260dd99..3e4aec641 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -444,16 +444,32 @@ public:
virtual Node getValue(TNode n, TheoryEngine* engine) = 0;
/**
- * A Theory is called with presolve exactly one time per user check-sat.
- * presolve() is called after preregistration, rewriting, and Boolean propagation,
- * (other theories' propagation?), but the notified Theory has not yet had its check()
- * or propagate() method called yet.
- * A Theory may empty its assertFact() queue using get().
- * A Theory can raise conflicts, add lemmas, and propagate literals during presolve.
+ * The theory should only add (via .operator<< or .append()) to the
+ * "learned" builder. It is a conjunction to add to the formula at
+ * the top-level and may contain other theories' contributions.
+ */
+ virtual void staticLearning(TNode in, NodeBuilder<>& learned) { }
+
+ /**
+ * A Theory is called with presolve exactly one time per user
+ * check-sat. presolve() is called after preregistration,
+ * rewriting, and Boolean propagation, (other theories'
+ * propagation?), but the notified Theory has not yet had its
+ * check() or propagate() method called. A Theory may empty its
+ * assertFact() queue using get(). A Theory can raise conflicts,
+ * add lemmas, and propagate literals during presolve().
*/
virtual void presolve() = 0;
/**
+ * Notification sent to the theory wheneven the search restarts.
+ * Serves as a good time to do some clean-up work, and you can
+ * assume you're at DL 0 for the purposes of Contexts. This function
+ * should not use the output channel.
+ */
+ virtual void notifyRestart() { }
+
+ /**
* Identify this theory (for debugging, dynamic configuration,
* etc..)
*/
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 48f983b3f..e2c42bccd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -622,15 +622,61 @@ bool TheoryEngine::presolve() {
d_theoryOut.d_conflictNode = Node::null();
d_theoryOut.d_propagatedLiterals.clear();
try {
+ /*
+ d_builtin->presolve();
+ if(!d_theoryOut.d_conflictNode.get().isNull()) {
+ return true;
+ }
+ d_bool->presolve();
+ if(!d_theoryOut.d_conflictNode.get().isNull()) {
+ return true;
+ }
+ */
d_uf->presolve();
+ if(!d_theoryOut.d_conflictNode.get().isNull()) {
+ return true;
+ }
d_arith->presolve();
- //d_arrays->presolve();
- //d_bv->presolve();
+ /*
+ if(!d_theoryOut.d_conflictNode.get().isNull()) {
+ return true;
+ }
+ d_arrays->presolve();
+ if(!d_theoryOut.d_conflictNode.get().isNull()) {
+ return true;
+ }
+ d_bv->presolve();
+ */
} catch(const theory::Interrupted&) {
- Debug("theory") << "TheoryEngine::presolve() => conflict" << std::endl;
+ Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl;
}
- // Return whether we have a conflict
- return d_theoryOut.d_conflictNode.get().isNull();
+ // return whether we have a conflict
+ return !d_theoryOut.d_conflictNode.get().isNull();
+}
+
+
+void TheoryEngine::notifyRestart() {
+ /*
+ d_builtin->notifyRestart();
+ d_bool->notifyRestart();
+ */
+ d_uf->notifyRestart();
+ /*
+ d_arith->notifyRestart();
+ d_arrays->notifyRestart();
+ d_bv->notifyRestart();
+ */
+}
+
+
+void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
+ d_builtin->staticLearning(in, learned);
+ d_bool->staticLearning(in, learned);
+ d_uf->staticLearning(in, learned);
+ d_arith->staticLearning(in, learned);
+ d_arrays->staticLearning(in, learned);
+ d_bv->staticLearning(in, learned);
}
+
}/* CVC4 namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 8ee5c91d7..3176b9698 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -310,11 +310,22 @@ public:
}
/**
+ * Calls staticLearning() on all active theories, accumulating their
+ * combined contributions in the "learned" builder.
+ */
+ void staticLearning(TNode in, NodeBuilder<>& learned);
+
+ /**
* Calls presolve() on all active theories and returns true
* if one of the theories discovers a conflict.
*/
bool presolve();
+ /**
+ * Calls notifyRestart() on all active theories.
+ */
+ void notifyRestart();
+
inline const std::vector<TNode>& getPropagatedLiterals() const {
return d_theoryOut.d_propagatedLiterals;
}
@@ -365,9 +376,9 @@ private:
public:
IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanation;
Statistics():
- d_statConflicts("theory::conflicts",0),
- d_statPropagate("theory::propagate",0),
- d_statLemma("theory::lemma",0),
+ d_statConflicts("theory::conflicts", 0),
+ d_statPropagate("theory::propagate", 0),
+ d_statLemma("theory::lemma", 0),
d_statAugLemma("theory::aug_lemma", 0),
d_statExplanation("theory::explanation", 0)
{
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 85b41bdbe..04fe533ae 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -5,6 +5,10 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libuf.la
+# force automake to link using g++
+nodist_EXTRA_libuf_la_SOURCES = \
+ dummy.cpp
+
libuf_la_SOURCES = \
theory_uf.h \
theory_uf_type_rules.h
diff --git a/src/theory/uf/morgan/Makefile b/src/theory/uf/morgan/Makefile
new file mode 100644
index 000000000..4f6767bdd
--- /dev/null
+++ b/src/theory/uf/morgan/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../../..
+srcdir = src/theory/uf/morgan
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index ad8929692..ef00b5818 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -21,6 +21,10 @@
#include "expr/kind.h"
#include "util/congruence_closure.h"
+#include <map>
+
+using namespace std;
+
using namespace CVC4;
using namespace CVC4::context;
using namespace CVC4::theory;
@@ -34,19 +38,16 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) :
d_cc(ctxt, &d_ccChannel),
d_unionFind(ctxt),
d_disequalities(ctxt),
+ d_equalities(ctxt),
d_conflict(),
d_trueNode(),
d_falseNode(),
d_trueEqFalseNode(),
- d_checkTimer("theory::uf::morgan::checkTime"),
- d_propagateTimer("theory::uf::morgan::propagateTime"),
- d_explainTimer("theory::uf::morgan::explainTime"),
- d_ccExplanationLength("theory::uf::morgan::cc::averageExplanationLength", d_cc.getExplanationLength()),
- d_ccNewSkolemVars("theory::uf::morgan::cc::newSkolemVariables", d_cc.getNewSkolemVars()) {
-
- StatisticsRegistry::registerStat(&d_checkTimer);
- StatisticsRegistry::registerStat(&d_propagateTimer);
- StatisticsRegistry::registerStat(&d_explainTimer);
+ d_ccExplanationLength("theory::uf::morgan::cc::averageExplanationLength",
+ d_cc.getExplanationLength()),
+ d_ccNewSkolemVars("theory::uf::morgan::cc::newSkolemVariables",
+ d_cc.getNewSkolemVars()) {
+
StatisticsRegistry::registerStat(&d_ccExplanationLength);
StatisticsRegistry::registerStat(&d_ccNewSkolemVars);
@@ -65,16 +66,13 @@ TheoryUFMorgan::~TheoryUFMorgan() {
d_falseNode = Node::null();
d_trueEqFalseNode = Node::null();
- StatisticsRegistry::unregisterStat(&d_checkTimer);
- StatisticsRegistry::unregisterStat(&d_propagateTimer);
- StatisticsRegistry::unregisterStat(&d_explainTimer);
StatisticsRegistry::unregisterStat(&d_ccExplanationLength);
StatisticsRegistry::unregisterStat(&d_ccNewSkolemVars);
}
RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
if(topLevel) {
- Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
+ Debug("uf") << "uf: begin rewrite(" << n << ")" << endl;
Node ret(n);
if(n.getKind() == kind::EQUAL ||
n.getKind() == kind::IFF) {
@@ -82,7 +80,7 @@ RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
ret = NodeManager::currentNM()->mkConst(true);
}
}
- Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
+ Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << endl;
return RewriteComplete(ret);
} else {
return RewriteComplete(n);
@@ -90,16 +88,19 @@ RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
}
void TheoryUFMorgan::preRegisterTerm(TNode n) {
- Debug("uf") << "uf: preRegisterTerm(" << n << ")" << std::endl;
+ Debug("uf") << "uf: preRegisterTerm(" << n << ")" << endl;
+ if(n.getKind() == kind::EQUAL || n.getKind() == kind::IFF) {
+ registerEqualityForPropagation(n);
+ }
}
void TheoryUFMorgan::registerTerm(TNode n) {
- Debug("uf") << "uf: registerTerm(" << n << ")" << std::endl;
+ Debug("uf") << "uf: registerTerm(" << n << ")" << endl;
}
Node TheoryUFMorgan::constructConflict(TNode diseq) {
- Debug("uf") << "uf: begin constructConflict()" << std::endl;
- Debug("uf") << "uf: using diseq == " << diseq << std::endl;
+ Debug("uf") << "uf: begin constructConflict()" << endl;
+ Debug("uf") << "uf: using diseq == " << diseq << endl;
Node explanation = d_cc.explain(diseq[0], diseq[1]);
@@ -142,16 +143,16 @@ Node TheoryUFMorgan::constructConflict(TNode diseq) {
Assert(nb.getNumChildren() > 1);
Node conflict = nb;
- Debug("uf") << "conflict constructed : " << conflict << std::endl;
+ Debug("uf") << "conflict constructed : " << conflict << endl;
- Debug("uf") << "uf: ending constructConflict()" << std::endl;
+ Debug("uf") << "uf: ending constructConflict()" << endl;
return conflict;
}
void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
- Debug("uf") << "uf: notified of merge " << a << std::endl
- << " and " << b << std::endl;
+ Debug("uf") << "uf: notified of merge " << a << endl
+ << " and " << b << endl;
if(!d_conflict.isNull()) {
// if already a conflict, we don't care
return;
@@ -164,21 +165,21 @@ 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);
+ EqLists::iterator deq_ia = d_disequalities.find(a);
+ EqLists::iterator deq_ib = d_disequalities.find(b);
if(deq_ia != d_disequalities.end()) {
if(deq_ib == d_disequalities.end() ||
(*deq_ia).second->size() > (*deq_ib).second->size()) {
TNode tmp = a;
a = b;
b = tmp;
- Debug("uf") << " swapping to make a shorter diseqList" << std::endl;
+ Debug("uf") << " swapping to make a shorter diseqList" << endl;
}
}
a = find(a);
b = find(b);
- Debug("uf") << "uf: uf reps are " << a << std::endl
- << " and " << b << std::endl;
+ Debug("uf") << "uf: uf reps are " << a << endl
+ << " and " << b << endl;
if(a == b) {
return;
@@ -189,15 +190,15 @@ void TheoryUFMorgan::merge(TNode a, TNode b) {
d_unionFind.setCanon(a, b);
- DiseqLists::iterator deq_i = d_disequalities.find(a);
+ EqLists::iterator deq_i = d_disequalities.find(a);
+ // a set of other trees we are already disequal to, and their
+ // (TNode) equalities (for optimizations below)
+ map<TNode, TNode> alreadyDiseqs;
if(deq_i != d_disequalities.end()) {
- // a set of other trees we are already disequal to
- // (for the optimization below)
- std::set<TNode> alreadyDiseqs;
- DiseqLists::iterator deq_ib = d_disequalities.find(b);
+ EqLists::iterator deq_ib = d_disequalities.find(b);
if(deq_ib != d_disequalities.end()) {
- DiseqList* deq = (*deq_ib).second;
- for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
+ EqList* deq = (*deq_ib).second;
+ for(EqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
TNode deqn = *j;
TNode s = deqn[0];
TNode t = deqn[1];
@@ -205,30 +206,30 @@ void TheoryUFMorgan::merge(TNode a, TNode b) {
TNode tp = find(t);
Assert(sp == b || tp == b);
if(sp == b) {
- alreadyDiseqs.insert(tp);
+ alreadyDiseqs[tp] = deqn;
} else {
- alreadyDiseqs.insert(sp);
+ alreadyDiseqs[sp] = deqn;
}
}
}
- DiseqList* deq = (*deq_i).second;
+ EqList* deq = (*deq_i).second;
if(Debug.isOn("uf")) {
- Debug("uf") << "a == " << a << std::endl;
- Debug("uf") << "size of deq(a) is " << deq->size() << std::endl;
+ Debug("uf") << "a == " << a << endl;
+ Debug("uf") << "size of deq(a) is " << deq->size() << endl;
}
- for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
- Debug("uf") << " deq(a) ==> " << *j << std::endl;
+ for(EqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
+ Debug("uf") << " deq(a) ==> " << *j << endl;
TNode deqn = *j;
Assert(deqn.getKind() == kind::EQUAL ||
deqn.getKind() == kind::IFF);
TNode s = deqn[0];
TNode t = deqn[1];
if(Debug.isOn("uf")) {
- Debug("uf") << " s ==> " << s << std::endl
- << " t ==> " << t << std::endl
- << " find(s) ==> " << debugFind(s) << std::endl
- << " find(t) ==> " << debugFind(t) << std::endl;
+ Debug("uf") << " s ==> " << s << endl
+ << " t ==> " << t << endl
+ << " find(s) ==> " << debugFind(s) << endl
+ << " find(t) ==> " << debugFind(t) << endl;
}
TNode sp = find(s);
TNode tp = find(t);
@@ -241,37 +242,120 @@ void TheoryUFMorgan::merge(TNode a, TNode b) {
if(sp == b) {
if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
appendToDiseqList(b, deqn);
- alreadyDiseqs.insert(tp);
+ alreadyDiseqs[tp] = deqn;
}
} else {
if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
appendToDiseqList(b, deqn);
- alreadyDiseqs.insert(sp);
+ alreadyDiseqs[sp] = deqn;
}
}
}
- Debug("uf") << "end" << std::endl;
+ Debug("uf") << "end diseq-list." << endl;
+ }
+
+ // Note that at this point, alreadyDiseqs contains everything we're
+ // disequal to, and the attendant disequality
+
+ // FIXME these could be "remembered" and then done in propagation (?)
+ EqLists::iterator eq_i = d_equalities.find(a);
+ if(eq_i != d_equalities.end()) {
+ EqList* eq = (*eq_i).second;
+ if(Debug.isOn("uf")) {
+ Debug("uf") << "a == " << a << endl;
+ Debug("uf") << "size of eq(a) is " << eq->size() << endl;
+ }
+ for(EqList::const_iterator j = eq->begin(); j != eq->end(); ++j) {
+ Debug("uf") << " eq(a) ==> " << *j << endl;
+ TNode eqn = *j;
+ Assert(eqn.getKind() == kind::EQUAL ||
+ eqn.getKind() == kind::IFF);
+ TNode s = eqn[0];
+ TNode t = eqn[1];
+ if(Debug.isOn("uf")) {
+ Debug("uf") << " s ==> " << s << endl
+ << " t ==> " << t << endl
+ << " find(s) ==> " << debugFind(s) << endl
+ << " find(t) ==> " << debugFind(t) << endl;
+ }
+ TNode sp = find(s);
+ TNode tp = find(t);
+ if(sp == tp) {
+ // propagation of equality
+ Debug("uf:prop") << " uf-propagating " << eqn << endl;
+ ++d_propagations;
+ d_out->propagate(eqn);
+ } else {
+ Assert(sp == b || tp == b);
+ appendToEqList(b, eqn);
+ if(sp == b) {
+ map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(tp);
+ if(k != alreadyDiseqs.end()) {
+ // propagation of disequality
+ // FIXME: this will propagate the same disequality on every
+ // subsequent merge, won't it??
+ Node deqn = (*k).second.notNode();
+ Debug("uf:prop") << " uf-propagating " << deqn << endl;
+ ++d_propagations;
+ d_out->propagate(deqn);
+ }
+ } else {
+ map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(sp);
+ if(k != alreadyDiseqs.end()) {
+ // propagation of disequality
+ // FIXME: this will propagate the same disequality on every
+ // subsequent merge, won't it??
+ Node deqn = (*k).second.notNode();
+ Debug("uf:prop") << " uf-propagating " << deqn << endl;
+ ++d_propagations;
+ d_out->propagate(deqn);
+ }
+ }
+ }
+ }
+ Debug("uf") << "end eq-list." << endl;
}
}
void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) {
- Debug("uf") << "appending " << eq << std::endl
- << " to diseq list of " << of << std::endl;
+ Debug("uf") << "appending " << eq << endl
+ << " to diseq list of " << of << endl;
Assert(eq.getKind() == kind::EQUAL ||
eq.getKind() == kind::IFF);
Assert(of == debugFind(of));
- DiseqLists::iterator deq_i = d_disequalities.find(of);
- DiseqList* deq;
+ EqLists::iterator deq_i = d_disequalities.find(of);
+ EqList* deq;
if(deq_i == d_disequalities.end()) {
- deq = new(getContext()->getCMM()) DiseqList(true, getContext(), false,
- ContextMemoryAllocator<TNode>(getContext()->getCMM()));
+ deq = new(getContext()->getCMM()) EqList(true, getContext(), false,
+ ContextMemoryAllocator<TNode>(getContext()->getCMM()));
d_disequalities.insertDataFromContextMemory(of, deq);
} else {
deq = (*deq_i).second;
}
deq->push_back(eq);
if(Debug.isOn("uf")) {
- Debug("uf") << " size is now " << deq->size() << std::endl;
+ Debug("uf") << " size is now " << deq->size() << endl;
+ }
+}
+
+void TheoryUFMorgan::appendToEqList(TNode of, TNode eq) {
+ Debug("uf") << "appending " << eq << endl
+ << " to eq list of " << of << endl;
+ Assert(eq.getKind() == kind::EQUAL ||
+ eq.getKind() == kind::IFF);
+ Assert(of == debugFind(of));
+ EqLists::iterator eq_i = d_equalities.find(of);
+ EqList* eql;
+ if(eq_i == d_equalities.end()) {
+ eql = new(getContext()->getCMM()) EqList(true, getContext(), false,
+ ContextMemoryAllocator<TNode>(getContext()->getCMM()));
+ d_equalities.insertDataFromContextMemory(of, eql);
+ } else {
+ eql = (*eq_i).second;
+ }
+ eql->push_back(eq);
+ if(Debug.isOn("uf")) {
+ Debug("uf") << " size is now " << eql->size() << endl;
}
}
@@ -286,10 +370,28 @@ void TheoryUFMorgan::addDisequality(TNode eq) {
appendToDiseqList(find(b), eq);
}
+void TheoryUFMorgan::registerEqualityForPropagation(TNode eq) {
+ // should NOT be in search at this point, this must be called during
+ // preregistration
+
+ // FIXME with lemmas on demand, this could miss future propagations,
+ // since we are not necessarily at context level 0, but are updating
+ // context-sensitive structures.
+
+ Assert(eq.getKind() == kind::EQUAL ||
+ eq.getKind() == kind::IFF);
+
+ TNode a = eq[0];
+ TNode b = eq[1];
+
+ appendToEqList(find(a), eq);
+ appendToEqList(find(b), eq);
+}
+
void TheoryUFMorgan::check(Effort level) {
TimerStat::CodeTimer codeTimer(d_checkTimer);
- Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
+ Debug("uf") << "uf: begin check(" << level << ")" << endl;
while(!done()) {
Assert(d_conflict.isNull());
@@ -298,7 +400,7 @@ void TheoryUFMorgan::check(Effort level) {
//d_activeAssertions.push_back(assertion);
- Debug("uf") << "uf check(): " << assertion << std::endl;
+ Debug("uf") << "uf check(): " << assertion << endl;
switch(assertion.getKind()) {
case kind::EQUAL:
@@ -307,6 +409,7 @@ void TheoryUFMorgan::check(Effort level) {
if(!d_conflict.isNull()) {
Node conflict = constructConflict(d_conflict);
d_conflict = Node::null();
+ ++d_conflicts;
d_out->conflict(conflict, false);
return;
}
@@ -326,13 +429,14 @@ void TheoryUFMorgan::check(Effort level) {
if(!d_conflict.isNull()) {
Node conflict = constructConflict(d_conflict);
d_conflict = Node::null();
+ ++d_conflicts;
d_out->conflict(conflict, false);
return;
}
if(Debug.isOn("uf")) {
Debug("uf") << "true == false ? "
- << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+ << (find(d_trueNode) == find(d_falseNode)) << endl;
}
Assert(find(d_trueNode) != find(d_falseNode));
@@ -352,10 +456,10 @@ void TheoryUFMorgan::check(Effort level) {
d_cc.addTerm(b);
if(Debug.isOn("uf")) {
- Debug("uf") << " a ==> " << a << std::endl
- << " b ==> " << b << std::endl
- << " find(a) ==> " << debugFind(a) << std::endl
- << " find(b) ==> " << debugFind(b) << std::endl;
+ Debug("uf") << " a ==> " << a << endl
+ << " b ==> " << b << endl
+ << " find(a) ==> " << debugFind(a) << endl
+ << " find(b) ==> " << debugFind(b) << endl;
}
// There are two ways to get a conflict here.
@@ -368,6 +472,7 @@ void TheoryUFMorgan::check(Effort level) {
// catch it, so that we can clear out d_conflict.
Node conflict = constructConflict(d_conflict);
d_conflict = Node::null();
+ ++d_conflicts;
d_out->conflict(conflict, false);
return;
} else if(find(a) == find(b)) {
@@ -375,6 +480,7 @@ void TheoryUFMorgan::check(Effort level) {
// a, b and were notified previously (via notifyCongruent())
// that they were congruent.
Node conflict = constructConflict(assertion[0]);
+ ++d_conflicts;
d_out->conflict(conflict, false);
return;
}
@@ -397,13 +503,14 @@ void TheoryUFMorgan::check(Effort level) {
if(!d_conflict.isNull()) {
Node conflict = constructConflict(d_conflict);
d_conflict = Node::null();
+ ++d_conflicts;
d_out->conflict(conflict, false);
return;
}
if(Debug.isOn("uf")) {
Debug("uf") << "true == false ? "
- << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+ << (find(d_trueNode) == find(d_falseNode)) << endl;
}
Assert(find(d_trueNode) != find(d_falseNode));
@@ -423,7 +530,7 @@ void TheoryUFMorgan::check(Effort level) {
}
Assert(d_conflict.isNull());
Debug("uf") << "uf check() done = " << (done() ? "true" : "false")
- << std::endl;
+ << endl;
/*
for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
@@ -433,34 +540,48 @@ void TheoryUFMorgan::check(Effort level) {
TNode left = (*diseqIter)[0];
TNode right = (*diseqIter)[1];
if(Debug.isOn("uf")) {
- Debug("uf") << "testing left: " << left << std::endl
- << " right: " << right << std::endl
- << " find(L): " << debugFind(left) << std::endl
- << " find(R): " << debugFind(right) << std::endl
+ Debug("uf") << "testing left: " << left << endl
+ << " right: " << right << endl
+ << " find(L): " << debugFind(left) << endl
+ << " find(R): " << debugFind(right) << endl
<< " areCong: " << d_cc.areCongruent(left, right)
- << std::endl;
+ << endl;
}
Assert((debugFind(left) == debugFind(right)) ==
d_cc.areCongruent(left, right));
}
*/
- Debug("uf") << "uf: end check(" << level << ")" << std::endl;
+ Debug("uf") << "uf: end check(" << level << ")" << endl;
}
void TheoryUFMorgan::propagate(Effort level) {
TimerStat::CodeTimer codeTimer(d_propagateTimer);
- Debug("uf") << "uf: begin propagate(" << level << ")" << std::endl;
- Debug("uf") << "uf: end propagate(" << level << ")" << std::endl;
+ Debug("uf") << "uf: begin propagate(" << level << ")" << endl;
+ // propagation is done in check(), for now
+ // FIXME need to find a slick way to propagate predicates
+ Debug("uf") << "uf: end propagate(" << level << ")" << endl;
}
void TheoryUFMorgan::explain(TNode n, Effort level) {
TimerStat::CodeTimer codeTimer(d_explainTimer);
- Debug("uf") << "uf: begin explain([" << n << "], " << level << ")" << std::endl;
+ Debug("uf") << "uf: begin explain([" << n << "], " << level << ")" << endl;
Unimplemented();
- Debug("uf") << "uf: end explain([" << n << "], " << level << ")" << std::endl;
+ Debug("uf") << "uf: end explain([" << n << "], " << level << ")" << endl;
+}
+
+void TheoryUFMorgan::presolve() {
+ TimerStat::CodeTimer codeTimer(d_presolveTimer);
+
+ Debug("uf") << "uf: begin presolve()" << endl;
+ Debug("uf") << "uf: end presolve()" << endl;
+}
+
+void TheoryUFMorgan::notifyRestart() {
+ Debug("uf") << "uf: begin notifyDecisionLevelZero()" << endl;
+ Debug("uf") << "uf: end notifyDecisionLevelZero()" << endl;
}
Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) {
@@ -488,37 +609,145 @@ Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) {
}
}
+void TheoryUFMorgan::staticLearning(TNode n, NodeBuilder<>& learned) {
+ TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
+
+ vector<TNode> workList;
+ workList.push_back(n);
+ __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+
+ while(!workList.empty()) {
+ n = workList.back();
+
+ bool unprocessedChildren = false;
+ for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
+ if(processed.find(*i) == processed.end()) {
+ // unprocessed child
+ workList.push_back(*i);
+ unprocessedChildren = true;
+ }
+ }
+
+ if(unprocessedChildren) {
+ continue;
+ }
+
+ workList.pop_back();
+ // has node n been processed in the meantime ?
+ if(processed.find(n) != processed.end()) {
+ continue;
+ }
+ processed.insert(n);
+
+ // == DIAMONDS ==
+
+ Debug("diamonds") << "===================== looking at" << endl
+ << n << endl;
+
+ // binary OR of binary ANDs of EQUALities
+ if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
+ n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
+ (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) &&
+ (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) &&
+ (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) &&
+ (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) {
+ // now we have (a = b && c = d) || (e = f && g = h)
+
+ Debug("diamonds") << "has form of a diamond!" << endl;
+
+ TNode
+ a = n[0][0][0], b = n[0][0][1],
+ c = n[0][1][0], d = n[0][1][1],
+ e = n[1][0][0], f = n[1][0][1],
+ g = n[1][1][0], h = n[1][1][1];
+
+ // test that one of {a, b} = one of {c, d}, and make "b" the
+ // shared node (i.e. put in the form (a = b && b = d))
+ // note we don't actually care about the shared ones, so the
+ // "swaps" below are one-sided, ignoring b and c
+ if(a == c) {
+ a = b;
+ } else if(a == d) {
+ a = b;
+ d = c;
+ } else if(b == c) {
+ // nothing to do
+ } else if(b == d) {
+ d = c;
+ } else {
+ // condition not satisfied
+ Debug("diamonds") << "+ A fails" << endl;
+ continue;
+ }
+
+ Debug("diamonds") << "+ A holds" << endl;
+
+ // same: one of {e, f} = one of {g, h}, and make "f" the
+ // shared node (i.e. put in the form (e = f && f = h))
+ if(e == g) {
+ e = f;
+ } else if(e == h) {
+ e = f;
+ h = g;
+ } else if(f == g) {
+ // nothing to do
+ } else if(f == h) {
+ h = g;
+ } else {
+ // condition not satisfied
+ Debug("diamonds") << "+ B fails" << endl;
+ continue;
+ }
+
+ Debug("diamonds") << "+ B holds" << endl;
+
+ // now we have (a = b && b = d) || (e = f && f = h)
+ // test that {a, d} == {e, h}
+ if( (a == e && d == h) ||
+ (a == h && d == e) ) {
+ // learn: n implies a == d
+ Debug("diamonds") << "+ C holds" << endl;
+ Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d);
+ Debug("diamonds") << " ==> " << newEquality << endl;
+ learned << n.impNode(newEquality);
+ } else {
+ Debug("diamonds") << "+ C fails" << endl;
+ }
+ }
+ }
+}
+
/*
void TheoryUFMorgan::dump() {
if(!Debug.isOn("uf")) {
return;
}
- Debug("uf") << "============== THEORY_UF ==============" << std::endl;
- Debug("uf") << "Active assertions list:" << std::endl;
+ Debug("uf") << "============== THEORY_UF ==============" << endl;
+ Debug("uf") << "Active assertions list:" << endl;
for(context::CDList<Node>::const_iterator i = d_activeAssertions.begin();
i != d_activeAssertions.end();
++i) {
- Debug("uf") << " " << *i << std::endl;
+ Debug("uf") << " " << *i << endl;
}
- Debug("uf") << "Congruence union-find:" << std::endl;
+ Debug("uf") << "Congruence union-find:" << endl;
for(UnionFind::const_iterator i = d_unionFind.begin();
i != d_unionFind.end();
++i) {
Debug("uf") << " " << (*i).first << " ==> " << (*i).second
- << std::endl;
+ << endl;
}
- Debug("uf") << "Disequality lists:" << std::endl;
- for(DiseqLists::const_iterator i = d_disequalities.begin();
+ Debug("uf") << "Disequality lists:" << endl;
+ for(EqLists::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();
+ Debug("uf") << " " << (*i).first << ":" << endl;
+ EqList* dl = (*i).second;
+ for(EqList::const_iterator j = dl->begin();
j != dl->end();
++j) {
- Debug("uf") << " " << *j << std::endl;
+ Debug("uf") << " " << *j << endl;
}
}
- Debug("uf") << "=======================================" << std::endl;
+ Debug("uf") << "=======================================" << endl;
}
*/
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index 49b6a77ae..99e6f5fbc 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -81,29 +81,60 @@ private:
*/
UnionFind<TNode, TNodeHashFunction> d_unionFind;
- typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > DiseqList;
- typedef context::CDMap<Node, DiseqList*, NodeHashFunction> DiseqLists;
+ typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > EqList;
+ typedef context::CDMap<Node, EqList*, NodeHashFunction> EqLists;
/** List of all disequalities this theory has seen. */
- DiseqLists d_disequalities;
+ EqLists d_disequalities;
+
+ /** List of all (potential) equalities to be propagated. */
+ EqLists d_equalities;
Node d_conflict;
Node d_trueNode, d_falseNode, d_trueEqFalseNode;
// === STATISTICS ===
- TimerStat d_checkTimer;/*! time spent in check() */
- TimerStat d_propagateTimer;/*! time spent in propagate() */
- TimerStat d_explainTimer;/*! time spent in explain() */
- WrappedStat<AverageStat> d_ccExplanationLength;/*! CC module expl length */
- WrappedStat<IntStat> d_ccNewSkolemVars;/*! CC module # skolem vars */
+ /** time spent in check() */
+ KEEP_STATISTIC(TimerStat,
+ d_checkTimer,
+ "theory::uf::morgan::checkTime");
+ /** time spent in propagate() */
+ KEEP_STATISTIC(TimerStat,
+ d_propagateTimer,
+ "theory::uf::morgan::propagateTime");
+
+ /** time spent in explain() */
+ KEEP_STATISTIC(TimerStat,
+ d_explainTimer,
+ "theory::uf::morgan::explainTime");
+ /** time spent in staticLearning() */
+ KEEP_STATISTIC(TimerStat,
+ d_staticLearningTimer,
+ "theory::uf::morgan::staticLearningTime");
+ /** time spent in presolve() */
+ KEEP_STATISTIC(TimerStat,
+ d_presolveTimer,
+ "theory::uf::morgan::presolveTime");
+ /** number of UF conflicts */
+ KEEP_STATISTIC(IntStat,
+ d_conflicts,
+ "theory::uf::morgan::conflicts", 0);
+ /** number of UF propagations */
+ KEEP_STATISTIC(IntStat,
+ d_propagations,
+ "theory::uf::morgan::propagations", 0);
+ /** CC module expl length */
+ WrappedStat<AverageStat> d_ccExplanationLength;
+ /** CC module # skolem vars */
+ WrappedStat<IntStat> d_ccNewSkolemVars;
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
TheoryUFMorgan(int id, context::Context* ctxt, OutputChannel& out);
- /** Destructor for the TheoryUF object. */
+ /** Destructor for UF theory, cleans up memory and statistics. */
~TheoryUFMorgan();
/**
@@ -138,10 +169,6 @@ public:
*/
void check(Effort level);
- void presolve() {
- // do nothing for now
- }
-
/**
* Rewrites a node in the theory of uninterpreted functions.
* This is fairly basic and only ensures that atoms that are
@@ -166,6 +193,29 @@ public:
void explain(TNode n, Effort level);
/**
+ * The theory should only add (via .operator<< or .append()) to the
+ * "learned" builder. It is a conjunction to add to the formula at
+ * the top-level and may contain other theories' contributions.
+ */
+ void staticLearning(TNode in, NodeBuilder<>& learned);
+
+ /**
+ * A Theory is called with presolve exactly one time per user
+ * check-sat. presolve() is called after preregistration,
+ * rewriting, and Boolean propagation, (other theories'
+ * propagation?), but the notified Theory has not yet had its
+ * check() or propagate() method called. A Theory may empty its
+ * assertFact() queue using get(). A Theory can raise conflicts,
+ * add lemmas, and propagate literals during presolve().
+ */
+ void presolve();
+
+ /**
+ * Notification sent to the Theory when the search restarts.
+ */
+ void notifyRestart();
+
+ /**
* Gets a theory value.
*
* Overloads Node getValue(TNode n); from theory.h.
@@ -184,7 +234,9 @@ private:
inline TNode debugFind(TNode a) const;
void appendToDiseqList(TNode of, TNode eq);
+ void appendToEqList(TNode of, TNode eq);
void addDisequality(TNode eq);
+ void registerEqualityForPropagation(TNode eq);
/**
* Receives a notification from the congruence closure module that
diff --git a/src/theory/uf/morgan/union_find.h b/src/theory/uf/morgan/union_find.h
index b848be526..c378e5a8b 100644
--- a/src/theory/uf/morgan/union_find.h
+++ b/src/theory/uf/morgan/union_find.h
@@ -132,10 +132,12 @@ template <class NodeType, class NodeHash>
inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
Assert(d_map.find(n) == d_map.end());
Assert(d_map.find(newParent) == d_map.end());
- Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << endl;
- d_map[n] = newParent;
- d_trace.push_back(make_pair(n, TNode::null()));
- d_offset = d_trace.size();
+ if(n != newParent) {
+ Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << endl;
+ d_map[n] = newParent;
+ d_trace.push_back(make_pair(n, TNode::null()));
+ d_offset = d_trace.size();
+ }
}
}/* CVC4::theory::uf::morgan namespace */
diff --git a/src/theory/uf/tim/Makefile b/src/theory/uf/tim/Makefile
new file mode 100644
index 000000000..e1db2cbf9
--- /dev/null
+++ b/src/theory/uf/tim/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../../..
+srcdir = src/theory/uf/tim
+
+include $(topdir)/Makefile.subdir
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
index 094fb1d03..8a13e3587 100644
--- a/src/util/congruence_closure.h
+++ b/src/util/congruence_closure.h
@@ -140,7 +140,7 @@ class CongruenceClosure {
* The set of terms we care about (i.e. those that have been given
* us with addTerm() and their representatives).
*/
- typedef context::CDSet<Node, NodeHashFunction> CareSet;
+ typedef context::CDSet<TNode, TNodeHashFunction> CareSet;
CareSet d_careSet;
// === STATISTICS ===
@@ -201,7 +201,9 @@ public:
Node flatten(TNode t) {
if(t.getKind() == kind::APPLY_UF) {
NodeBuilder<> appb(kind::APPLY_UF);
- appb << replace(flatten(t.getOperator()));
+ Assert(replace(flatten(t.getOperator())) == t.getOperator(),
+ "CongruenceClosure:: bad state: higher-order term ??");
+ appb << t.getOperator();
for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
appb << replace(flatten(*i));
}
@@ -445,6 +447,9 @@ void CongruenceClosure<OutputChannel>::addTerm(TNode t) {
template <class OutputChannel>
void CongruenceClosure<OutputChannel>::addEq(TNode eq, TNode inputEq) {
+ Assert(!eq[0].getType().isFunction() && !eq[1].getType().isFunction(),
+ "CongruenceClosure:: equality between function symbols not allowed");
+
d_proofRewrite[eq] = inputEq;
if(Trace.isOn("cc")) {
@@ -502,7 +507,8 @@ Node CongruenceClosure<OutputChannel>::buildRepresentativesOfApply(TNode apply,
Assert(apply.getKind() == kind::APPLY_UF);
NodeBuilder<> argspb(kindToBuild);
// FIXME probably don't have to do find() of operator
- Assert(find(apply.getOperator()) == apply.getOperator());
+ Assert(find(apply.getOperator()) == apply.getOperator(),
+ "CongruenceClosure:: bad state: function symbol merged with another");
argspb << apply.getOperator();
for(TNode::iterator i = apply.begin(); i != apply.end(); ++i) {
argspb << find(*i);
@@ -790,9 +796,10 @@ Node CongruenceClosure<OutputChannel>::normalize(TNode t) const
return t;
} else {// t is an apply
NodeBuilder<> apb(kind::TUPLE);
- TNode op = t.getOperator();
- Node n = normalize(op);
- apb << n;
+ Assert(normalize(t.getOperator()) == t.getOperator(),
+ "CongruenceClosure:: bad state: function symbol merged with another");
+ apb << t.getOperator();
+ Node n;
bool allConstants = (n.getKind() != kind::APPLY_UF);
for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
TNode c = *i;
@@ -836,7 +843,7 @@ Node CongruenceClosure<OutputChannel>::highestNode(TNode a, UnionFind_t& unionFi
} else {
return unionFind[a] = highestNode((*i).second, unionFind);
}
-}
+}/* highestNode() */
template <class OutputChannel>
@@ -861,7 +868,10 @@ void CongruenceClosure<OutputChannel>::explainAlongPath(TNode a, TNode c, Pendin
Assert(e[1][0].getKind() == kind::APPLY_UF);
Assert(e[1][1].getKind() != kind::APPLY_UF);
Assert(e[0][0].getNumChildren() == e[1][0].getNumChildren());
- pending.push_back(std::make_pair(e[0][0].getOperator(), e[1][0].getOperator()));
+ Assert(e[0][0].getOperator() == e[1][0].getOperator(),
+ "CongruenceClosure:: bad state: function symbols should be equal");
+ // shouldn't have to prove this for operators
+ //pending.push_back(std::make_pair(e[0][0].getOperator(), e[1][0].getOperator()));
for(int i = 0, nc = e[0][0].getNumChildren(); i < nc; ++i) {
pending.push_back(std::make_pair(e[0][0][i], e[1][0][i]));
}
diff --git a/src/util/stats.h b/src/util/stats.h
index c0660bf88..d68836812 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -475,6 +475,33 @@ public:
}
};/* class TimerStat */
+/**
+ * To use a statistic, you need to declare it, initialize it in your
+ * constructor, register it in your constructor, and deregister it in
+ * your destructor. Instead, this macro does it all for you (and
+ * therefore also keeps the statistic type, field name, and output
+ * string all in the same place in your class's header. Its use is
+ * like in this example, which takes the place of the declaration of a
+ * statistics field "d_checkTimer":
+ *
+ * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::morgan::checkTime");
+ *
+ * If any args need to be passed to the constructor, you can specify
+ * them after the string.
+ *
+ * The macro works by creating a nested class type, derived from the
+ * statistic type you give it, which declares a registry-aware
+ * constructor/destructor pair.
+ */
+#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...) \
+ struct Statistic_##_StatField : public _StatType { \
+ Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) { \
+ StatisticsRegistry::registerStat(this); \
+ } \
+ ~Statistic_##_StatField() { \
+ StatisticsRegistry::unregisterStat(this); \
+ } \
+ } _StatField
#undef __CVC4_USE_STATISTICS
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 1471d8814..2e05386e0 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -19,6 +19,7 @@ TESTS = \
eq_diamond1.smt \
eq_diamond14.reduced.smt \
eq_diamond14.reduced2.smt \
+ eq_diamond23.smt \
NEQ016_size5_reduced2a.smt \
NEQ016_size5_reduced2b.smt \
dead_dnd002.smt \
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 3583770b6..725d4a4bb 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -5,6 +5,8 @@ UNIT_TESTS = \
theory/theory_black \
theory/theory_uf_tim_white \
theory/theory_arith_white \
+ theory/stacking_map_black \
+ theory/union_find_black \
expr/expr_public \
expr/expr_manager_public \
expr/node_white \
diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h
new file mode 100644
index 000000000..39dad4732
--- /dev/null
+++ b/test/unit/theory/stacking_map_black.h
@@ -0,0 +1,160 @@
+/********************* */
+/*! \file stacking_map_black.h
+ ** \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 Black box testing of CVC4::theory::uf::morgan::StackingMap
+ **
+ ** Black box testing of CVC4::theory::uf::morgan::StackingMap.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/uf/morgan/stacking_map.h"
+
+using namespace CVC4;
+using namespace CVC4::theory::uf::morgan;
+using namespace CVC4::context;
+
+using namespace std;
+
+/**
+ * Test the StackingMap.
+ */
+class StackingMapBlack : public CxxTest::TestSuite {
+ Context* d_ctxt;
+ StackingMap<TNode, TNodeHashFunction>* d_map;
+ NodeManager* d_nm;
+ NodeManagerScope* d_scope;
+
+ Node a, b, c, d, e, f, g;
+
+public:
+
+ void setUp() {
+ d_ctxt = new Context;
+ d_nm = new NodeManager(d_ctxt);
+ d_scope = new NodeManagerScope(d_nm);
+ d_map = new StackingMap<TNode, TNodeHashFunction>(d_ctxt);
+
+ a = d_nm->mkVar("a", d_nm->realType());
+ b = d_nm->mkVar("b", d_nm->realType());
+ c = d_nm->mkVar("c", d_nm->realType());
+ d = d_nm->mkVar("d", d_nm->realType());
+ e = d_nm->mkVar("e", d_nm->realType());
+ f = d_nm->mkVar("f", d_nm->realType());
+ g = d_nm->mkVar("g", d_nm->realType());
+ }
+
+ void tearDown() {
+ g = Node::null();
+ f = Node::null();
+ e = Node::null();
+ d = Node::null();
+ c = Node::null();
+ b = Node::null();
+ a = Node::null();
+
+ delete d_map;
+ delete d_scope;
+ delete d_nm;
+ delete d_ctxt;
+ }
+
+ void testSimpleContextual() {
+ TS_ASSERT(d_map->find(a).isNull());
+ TS_ASSERT(d_map->find(b).isNull());
+ TS_ASSERT(d_map->find(c).isNull());
+ TS_ASSERT(d_map->find(d).isNull());
+ TS_ASSERT(d_map->find(e).isNull());
+ TS_ASSERT(d_map->find(f).isNull());
+ TS_ASSERT(d_map->find(g).isNull());
+
+ d_map->set(a, b);
+
+ TS_ASSERT(d_map->find(a) == b);
+ TS_ASSERT(d_map->find(b).isNull());
+ TS_ASSERT(d_map->find(c).isNull());
+ TS_ASSERT(d_map->find(d).isNull());
+ TS_ASSERT(d_map->find(e).isNull());
+ TS_ASSERT(d_map->find(f).isNull());
+ TS_ASSERT(d_map->find(g).isNull());
+
+ d_ctxt->push();
+ {
+ TS_ASSERT(d_map->find(a) == b);
+ TS_ASSERT(d_map->find(b).isNull());
+ TS_ASSERT(d_map->find(c).isNull());
+ TS_ASSERT(d_map->find(d).isNull());
+ TS_ASSERT(d_map->find(e).isNull());
+ TS_ASSERT(d_map->find(f).isNull());
+ TS_ASSERT(d_map->find(g).isNull());
+
+ d_map->set(c, d);
+ d_map->set(f, e);
+
+ TS_ASSERT(d_map->find(a) == b);
+ TS_ASSERT(d_map->find(b).isNull());
+ TS_ASSERT(d_map->find(c) == d);
+ TS_ASSERT(d_map->find(d).isNull());
+ TS_ASSERT(d_map->find(e).isNull());
+ TS_ASSERT(d_map->find(f) == e);
+ TS_ASSERT(d_map->find(g).isNull());
+
+ d_ctxt->push();
+ {
+
+ TS_ASSERT(d_map->find(a) == b);
+ TS_ASSERT(d_map->find(b).isNull());
+ TS_ASSERT(d_map->find(c) == d);
+ TS_ASSERT(d_map->find(d).isNull());
+ TS_ASSERT(d_map->find(e).isNull());
+ TS_ASSERT(d_map->find(f) == e);
+ TS_ASSERT(d_map->find(g).isNull());
+
+ d_map->set(a, c);
+ d_map->set(f, f);
+ d_map->set(e, d);
+ d_map->set(c, Node::null());
+ d_map->set(g, a);
+
+ TS_ASSERT(d_map->find(a) == c);
+ TS_ASSERT(d_map->find(b).isNull());
+ TS_ASSERT(d_map->find(c).isNull());
+ TS_ASSERT(d_map->find(d).isNull());
+ TS_ASSERT(d_map->find(e) == d);
+ TS_ASSERT(d_map->find(f) == f);
+ TS_ASSERT(d_map->find(g) == a);
+
+ }
+ d_ctxt->pop();
+
+ TS_ASSERT(d_map->find(a) == b);
+ TS_ASSERT(d_map->find(b).isNull());
+ TS_ASSERT(d_map->find(c) == d);
+ TS_ASSERT(d_map->find(d).isNull());
+ TS_ASSERT(d_map->find(e).isNull());
+ TS_ASSERT(d_map->find(f) == e);
+ TS_ASSERT(d_map->find(g).isNull());
+ }
+ d_ctxt->pop();
+
+ TS_ASSERT(d_map->find(a) == b);
+ TS_ASSERT(d_map->find(b).isNull());
+ TS_ASSERT(d_map->find(c).isNull());
+ TS_ASSERT(d_map->find(d).isNull());
+ TS_ASSERT(d_map->find(e).isNull());
+ TS_ASSERT(d_map->find(f).isNull());
+ TS_ASSERT(d_map->find(g).isNull());
+ }
+};
diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h
new file mode 100644
index 000000000..b9b4e58ce
--- /dev/null
+++ b/test/unit/theory/union_find_black.h
@@ -0,0 +1,189 @@
+/********************* */
+/*! \file union_find_black.h
+ ** \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 Black box testing of CVC4::theory::uf::morgan::UnionFind
+ **
+ ** Black box testing of CVC4::theory::uf::morgan::UnionFind.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/uf/morgan/union_find.h"
+
+using namespace CVC4;
+using namespace CVC4::theory::uf::morgan;
+using namespace CVC4::context;
+
+using namespace std;
+
+/**
+ * Test the UnionFind.
+ */
+class UnionFindBlack : public CxxTest::TestSuite {
+ Context* d_ctxt;
+ UnionFind<TNode, TNodeHashFunction>* d_uf;
+ NodeManager* d_nm;
+ NodeManagerScope* d_scope;
+
+ Node a, b, c, d, e, f, g;
+
+public:
+
+ void setUp() {
+ d_ctxt = new Context;
+ d_nm = new NodeManager(d_ctxt);
+ d_scope = new NodeManagerScope(d_nm);
+ d_uf = new UnionFind<TNode, TNodeHashFunction>(d_ctxt);
+
+ a = d_nm->mkVar("a", d_nm->realType());
+ b = d_nm->mkVar("b", d_nm->realType());
+ c = d_nm->mkVar("c", d_nm->realType());
+ d = d_nm->mkVar("d", d_nm->realType());
+ e = d_nm->mkVar("e", d_nm->realType());
+ f = d_nm->mkVar("f", d_nm->realType());
+ g = d_nm->mkVar("g", d_nm->realType());
+ }
+
+ void tearDown() {
+ g = Node::null();
+ f = Node::null();
+ e = Node::null();
+ d = Node::null();
+ c = Node::null();
+ b = Node::null();
+ a = Node::null();
+
+ delete d_uf;
+ delete d_scope;
+ delete d_nm;
+ delete d_ctxt;
+ }
+
+ void testSimpleContextual() {
+ TS_ASSERT(d_uf->find(a) == a);
+ TS_ASSERT(d_uf->find(b) == b);
+ TS_ASSERT(d_uf->find(c) == c);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == e);
+ TS_ASSERT(d_uf->find(f) == f);
+ TS_ASSERT(d_uf->find(g) == g);
+
+ d_ctxt->push();
+
+ d_uf->setCanon(a, b);
+
+ TS_ASSERT(d_uf->find(a) == b);
+ TS_ASSERT(d_uf->find(b) == b);
+ TS_ASSERT(d_uf->find(c) == c);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == e);
+ TS_ASSERT(d_uf->find(f) == f);
+ TS_ASSERT(d_uf->find(g) == g);
+
+ d_ctxt->push();
+ {
+ TS_ASSERT(d_uf->find(a) == b);
+ TS_ASSERT(d_uf->find(b) == b);
+ TS_ASSERT(d_uf->find(c) == c);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == e);
+ TS_ASSERT(d_uf->find(f) == f);
+ TS_ASSERT(d_uf->find(g) == g);
+
+ d_uf->setCanon(c, d);
+ d_uf->setCanon(f, e);
+
+ TS_ASSERT(d_uf->find(a) == b);
+ TS_ASSERT(d_uf->find(b) == b);
+ TS_ASSERT(d_uf->find(c) == d);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == e);
+ TS_ASSERT(d_uf->find(f) == e);
+ TS_ASSERT(d_uf->find(g) == g);
+
+ d_ctxt->push();
+ {
+
+ TS_ASSERT(d_uf->find(a) == b);
+ TS_ASSERT(d_uf->find(b) == b);
+ TS_ASSERT(d_uf->find(c) == d);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == e);
+ TS_ASSERT(d_uf->find(f) == e);
+ TS_ASSERT(d_uf->find(g) == g);
+
+#ifdef CVC4_ASSERTIONS
+ TS_ASSERT_THROWS(d_uf->setCanon(a, c), AssertionException);
+ TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(a), c), AssertionException);
+ TS_ASSERT_THROWS(d_uf->setCanon(a, d_uf->find(c)), AssertionException);
+#endif /* CVC4_ASSERTIONS */
+ d_uf->setCanon(d_uf->find(a), d_uf->find(c));
+ d_uf->setCanon(d_uf->find(f), g);
+ d_uf->setCanon(d_uf->find(e), d);
+#ifdef CVC4_ASSERTIONS
+ TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(c), f), AssertionException);
+#endif /* CVC4_ASSERTIONS */
+ d_uf->setCanon(d_uf->find(c), d_uf->find(f));
+
+ TS_ASSERT(d_uf->find(a) == d);
+ TS_ASSERT(d_uf->find(b) == d);
+ TS_ASSERT(d_uf->find(c) == d);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == d);
+ TS_ASSERT(d_uf->find(f) == d);
+ TS_ASSERT(d_uf->find(g) == d);
+
+ d_uf->setCanon(d_uf->find(g), d_uf->find(a));
+
+ TS_ASSERT(d_uf->find(a) == d);
+ TS_ASSERT(d_uf->find(b) == d);
+ TS_ASSERT(d_uf->find(c) == d);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == d);
+ TS_ASSERT(d_uf->find(f) == d);
+ TS_ASSERT(d_uf->find(g) == d);
+
+ }
+ d_ctxt->pop();
+
+ TS_ASSERT(d_uf->find(a) == b);
+ TS_ASSERT(d_uf->find(b) == b);
+ TS_ASSERT(d_uf->find(c) == d);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == e);
+ TS_ASSERT(d_uf->find(f) == e);
+ TS_ASSERT(d_uf->find(g) == g);
+ }
+ d_ctxt->pop();
+
+ TS_ASSERT(d_uf->find(a) == b);
+ TS_ASSERT(d_uf->find(b) == b);
+ TS_ASSERT(d_uf->find(c) == c);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == e);
+ TS_ASSERT(d_uf->find(f) == f);
+ TS_ASSERT(d_uf->find(g) == g);
+
+ d_ctxt->pop();
+
+ TS_ASSERT(d_uf->find(a) == a);
+ TS_ASSERT(d_uf->find(b) == b);
+ TS_ASSERT(d_uf->find(c) == c);
+ TS_ASSERT(d_uf->find(d) == d);
+ TS_ASSERT(d_uf->find(e) == e);
+ TS_ASSERT(d_uf->find(f) == f);
+ TS_ASSERT(d_uf->find(g) == g);
+ }
+};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback