From: Morgan Deters Date: Fri, 19 Nov 2010 01:37:55 +0000 (+0000) Subject: Merge from ufprop branch, including: X-Git-Tag: cvc5-1.0.0~8724 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=663a6edef6b65d400e2d97dc9c8276da3d3cb0b1;p=cvc5.git Merge from ufprop branch, including: * Theory::staticLearning() for statically adding new T-stuff before normal preprocessing. UF's staticLearning() does transitivity of equality/iff, solving the diamonds. * more aggressive T-propagation for UF * new KEEP_STATISTIC macro to hide Theories from having to register/deregister statistics (and also has the advantage of keeping the statistic type, field name, and the 'tag' used to output the statistic in the same place---instead of scattered in the theory definition and constructor initializer list. See documentation for KEEP_STATISTIC in src/util/stats.h for more of an explanation). * more statistics for UF * restart notifications from SAT (through TheoryEngine) via Theory::notifyRestart() * StackingMap and UnionFind unit tests * build fixes/adjustments * code cleanup; minor other improvements --- 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,15 +444,31 @@ 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 @@ -309,12 +309,23 @@ public: return d_theoryOut.d_conflictNode.get().isNull(); } + /** + * 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& 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 + +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 alreadyDiseqs; if(deq_i != d_disequalities.end()) { - // a set of other trees we are already disequal to - // (for the optimization below) - std::set 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::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::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(getContext()->getCMM())); + deq = new(getContext()->getCMM()) EqList(true, getContext(), false, + ContextMemoryAllocator(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(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::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 workList; + workList.push_back(n); + __gnu_cxx::hash_set 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::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 d_unionFind; - typedef context::CDList > DiseqList; - typedef context::CDMap DiseqLists; + typedef context::CDList > EqList; + typedef context::CDMap 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 d_ccExplanationLength;/*! CC module expl length */ - WrappedStat 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 d_ccExplanationLength; + /** CC module # skolem vars */ + WrappedStat 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 @@ -165,6 +192,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. * @@ -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 inline void UnionFind::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 CareSet; + typedef context::CDSet 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::addTerm(TNode t) { template void CongruenceClosure::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::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::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::highestNode(TNode a, UnionFind_t& unionFi } else { return unionFind[a] = highestNode((*i).second, unionFind); } -} +}/* highestNode() */ template @@ -861,7 +868,10 @@ void CongruenceClosure::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 + +#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* 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(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 + +#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* 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(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); + } +};