diff options
Diffstat (limited to 'src/theory')
51 files changed, 1765 insertions, 1507 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 639e9eb4c..5af56ec44 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -18,9 +18,13 @@ libtheory_la_SOURCES = \ shared_term_manager.h \ shared_term_manager.cpp \ shared_data.h \ - shared_data.cpp + shared_data.cpp \ + rewriter.h \ + rewriter_attributes.h \ + rewriter.cpp nodist_libtheory_la_SOURCES = \ - theoryof_table.h + rewriter_tables.h \ + theory_traits.h libtheory_la_LIBADD = \ @builddir@/builtin/libbuiltin.la \ @@ -31,22 +35,34 @@ libtheory_la_LIBADD = \ @builddir@/bv/libbv.la EXTRA_DIST = \ - theoryof_table_template.h \ + rewriter_tables_template.h \ + theory_traits_template.h \ mktheoryof \ Makefile.subdirs BUILT_SOURCES = \ - theoryof_table.h + rewriter_tables.h \ + theory_traits.h CLEANFILES = \ - theoryof_table.h + rewriter_tables.h \ + theory_traits.h include @top_srcdir@/src/theory/Makefile.subdirs -theoryof_table.h: theoryof_table_template.h mktheoryof @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mktheoryof +rewriter_tables.h: rewriter_tables_template.h mkrewriter @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mkrewriter $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mktheoryof \ + $(AM_V_GEN)(@srcdir@/mkrewriter \ $< \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) + +theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mktheorytraits + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@//mktheorytraits \ + $< \ + `cat @top_builddir@/src/theory/.subdirs` \ + > $@) || (rm -f $@ && exit 1) +
\ No newline at end of file diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 9f4388b54..75216dac6 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -27,11 +27,12 @@ #include <set> #include <stack> - using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; +arith::ArithConstants* ArithRewriter::s_constants = NULL; + bool isVariable(TNode t){ return t.getMetaKind() == kind::metakind::VARIABLE; } @@ -40,25 +41,25 @@ RewriteResponse ArithRewriter::rewriteConstant(TNode t){ Assert(t.getMetaKind() == kind::metakind::CONSTANT); Node val = coerceToRationalNode(t); - return RewriteComplete(val); + return RewriteResponse(REWRITE_DONE, val); } RewriteResponse ArithRewriter::rewriteVariable(TNode t){ Assert(isVariable(t)); - return RewriteComplete(t); + return RewriteResponse(REWRITE_DONE, t); } RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){ Assert(t.getKind()== kind::MINUS); - if(t[0] == t[1]) return RewriteComplete(d_constants->d_ZERO_NODE); + if(t[0] == t[1]) return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE); Node noMinus = makeSubtractionNode(t[0],t[1]); if(pre){ - return RewriteComplete(noMinus); + return RewriteResponse(REWRITE_DONE, noMinus); }else{ - return FullRewriteNeeded(noMinus); + return RewriteResponse(REWRITE_AGAIN_FULL, noMinus); } } @@ -67,9 +68,9 @@ RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){ Node noUminus = makeUnaryMinusNode(t[0]); if(pre) - return RewriteComplete(noUminus); + return RewriteResponse(REWRITE_DONE, noUminus); else - return RewriteAgain(noUminus); + return RewriteResponse(REWRITE_AGAIN, noUminus); } RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ @@ -85,7 +86,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ if(t[0].getKind()== kind::CONST_RATIONAL){ return rewriteDivByConstant(t, true); }else{ - return RewriteComplete(t); + return RewriteResponse(REWRITE_DONE, t); } }else if(t.getKind() == kind::PLUS){ return preRewritePlus(t); @@ -123,25 +124,25 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){ for(TNode::iterator i = t.begin(); i != t.end(); ++i) { if((*i).getKind() == kind::CONST_RATIONAL) { - if((*i).getConst<Rational>() == d_constants->d_ZERO) { - return RewriteComplete(d_constants->d_ZERO_NODE); + if((*i).getConst<Rational>() == s_constants->d_ZERO) { + return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE); } } else if((*i).getKind() == kind::CONST_INTEGER) { if((*i).getConst<Integer>() == intZero) { if(t.getType().isInteger()) { - return RewriteComplete(NodeManager::currentNM()->mkConst(intZero)); + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(intZero)); } else { - return RewriteComplete(d_constants->d_ZERO_NODE); + return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE); } } } } - return RewriteComplete(t); + return RewriteResponse(REWRITE_DONE, t); } RewriteResponse ArithRewriter::preRewritePlus(TNode t){ Assert(t.getKind()== kind::PLUS); - return RewriteComplete(t); + return RewriteResponse(REWRITE_DONE, t); } RewriteResponse ArithRewriter::postRewritePlus(TNode t){ @@ -156,7 +157,7 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t){ res = res + currPoly; } - return RewriteComplete(res.getNode()); + return RewriteResponse(REWRITE_DONE, res.getNode()); } RewriteResponse ArithRewriter::postRewriteMult(TNode t){ @@ -171,7 +172,7 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ res = res * currPoly; } - return RewriteComplete(res.getNode()); + return RewriteResponse(REWRITE_DONE, res.getNode()); } RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){ @@ -182,7 +183,7 @@ RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){ Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right)); if(cmp.isBoolean()){ - return RewriteComplete(cmp.getNode()); + return RewriteResponse(REWRITE_DONE, cmp.getNode()); } if(cmp.getLeft().containsConstant()){ @@ -209,7 +210,7 @@ RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){ Assert(cmp.getLeft().getHead().coefficientIsOne()); Assert(cmp.isBoolean() || cmp.isNormalForm()); - return RewriteComplete(cmp.getNode()); + return RewriteResponse(REWRITE_DONE, cmp.getNode()); } RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ @@ -222,8 +223,8 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ }else{ //Transform this to: (left - right) |><| 0 Node diff = makeSubtractionNode(left, right); - Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE); - return FullRewriteNeeded(reduction); + Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, s_constants->d_ZERO_NODE); + return RewriteResponse(REWRITE_AGAIN_FULL, reduction); } } @@ -233,7 +234,7 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ if(atom.getKind() == kind::EQUAL) { if(atom[0] == atom[1]) { - return RewriteComplete(currNM->mkConst(true)); + return RewriteResponse(REWRITE_DONE, currNM->mkConst(true)); } } @@ -246,7 +247,7 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ //Transform this to: (left - right) |><| 0 Node diff = makeSubtractionNode(left, right); - reduction = currNM->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE); + reduction = currNM->mkNode(atom.getKind(), diff, s_constants->d_ZERO_NODE); } if(reduction.getKind() == kind::GT){ @@ -257,25 +258,25 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ reduction = currNM->mkNode(kind::NOT, geq); } - return RewriteComplete(reduction); + return RewriteResponse(REWRITE_DONE, reduction); } RewriteResponse ArithRewriter::postRewrite(TNode t){ if(isTerm(t)){ RewriteResponse response = postRewriteTerm(t); - if(Debug.isOn("arith::rewriter") && response.isDone()) { - Polynomial::parsePolynomial(response.getNode()); + if(Debug.isOn("arith::rewriter") && response.status == REWRITE_DONE) { + Polynomial::parsePolynomial(response.node); } return response; }else if(isAtom(t)){ RewriteResponse response = postRewriteAtom(t); - if(Debug.isOn("arith::rewriter") && response.isDone()) { - Comparison::parseNormalForm(response.getNode()); + if(Debug.isOn("arith::rewriter") && response.status == REWRITE_DONE) { + Comparison::parseNormalForm(response.node); } return response; }else{ Unreachable(); - return RewriteComplete(Node::null()); + return RewriteResponse(REWRITE_DONE, Node::null()); } } @@ -286,12 +287,12 @@ RewriteResponse ArithRewriter::preRewrite(TNode t){ return preRewriteAtom(t); }else{ Unreachable(); - return RewriteComplete(Node::null()); + return RewriteResponse(REWRITE_DONE, Node::null()); } } Node ArithRewriter::makeUnaryMinusNode(TNode n){ - return NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n); + return NodeManager::currentNM()->mkNode(kind::MULT,s_constants->d_NEGATIVE_ONE_NODE,n); } Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){ @@ -311,7 +312,7 @@ RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){ const Rational& den = right.getConst<Rational>(); - Assert(den != d_constants->d_ZERO); + Assert(den != s_constants->d_ZERO); Rational div = den.inverse(); @@ -319,8 +320,8 @@ RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){ Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result); if(pre){ - return RewriteComplete(mult); + return RewriteResponse(REWRITE_DONE, mult); }else{ - return RewriteAgain(mult); + return RewriteResponse(REWRITE_AGAIN, mult); } } diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index f7ef8c0c7..e161bd8d6 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -17,10 +17,13 @@ ** \todo document this file **/ -#include "theory/arith/arith_constants.h" #include "theory/theory.h" +#include "theory/arith/arith_constants.h" +#include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" +#include "theory/rewriter.h" + #ifndef __CVC4__THEORY__ARITH__REWRITER_H #define __CVC4__THEORY__ARITH__REWRITER_H @@ -28,46 +31,67 @@ namespace CVC4 { namespace theory { namespace arith { -class ArithRewriter{ +class ArithRewriter { + private: - ArithConstants* d_constants; - Node makeSubtractionNode(TNode l, TNode r); - Node makeUnaryMinusNode(TNode n); + static arith::ArithConstants* s_constants; + + static Node makeSubtractionNode(TNode l, TNode r); + static Node makeUnaryMinusNode(TNode n); - RewriteResponse preRewriteTerm(TNode t); - RewriteResponse postRewriteTerm(TNode t); + static RewriteResponse preRewriteTerm(TNode t); + static RewriteResponse postRewriteTerm(TNode t); - RewriteResponse rewriteVariable(TNode t); - RewriteResponse rewriteConstant(TNode t); - RewriteResponse rewriteMinus(TNode t, bool pre); - RewriteResponse rewriteUMinus(TNode t, bool pre); - RewriteResponse rewriteDivByConstant(TNode t, bool pre); + static RewriteResponse rewriteVariable(TNode t); + static RewriteResponse rewriteConstant(TNode t); + static RewriteResponse rewriteMinus(TNode t, bool pre); + static RewriteResponse rewriteUMinus(TNode t, bool pre); + static RewriteResponse rewriteDivByConstant(TNode t, bool pre); - RewriteResponse preRewritePlus(TNode t); - RewriteResponse postRewritePlus(TNode t); + static RewriteResponse preRewritePlus(TNode t); + static RewriteResponse postRewritePlus(TNode t); - RewriteResponse preRewriteMult(TNode t); - RewriteResponse postRewriteMult(TNode t); + static RewriteResponse preRewriteMult(TNode t); + static RewriteResponse postRewriteMult(TNode t); - RewriteResponse preRewriteAtom(TNode t); - RewriteResponse postRewriteAtom(TNode t); - RewriteResponse postRewriteAtomConstantRHS(TNode t); + static RewriteResponse preRewriteAtom(TNode t); + static RewriteResponse postRewriteAtom(TNode t); + static RewriteResponse postRewriteAtomConstantRHS(TNode t); public: - ArithRewriter(ArithConstants* ac) : d_constants(ac) {} - RewriteResponse preRewrite(TNode n); - RewriteResponse postRewrite(TNode n); + static RewriteResponse preRewrite(TNode n); + static RewriteResponse postRewrite(TNode n); + + static void init() { + if (s_constants == NULL) { + s_constants = new arith::ArithConstants(NodeManager::currentNM()); + } + } + + static void shutdown() { + if (s_constants != NULL) { + delete s_constants; + s_constants = NULL; + } + } private: - bool isAtom(TNode n) const { return isRelationOperator(n.getKind()); } - bool isTerm(TNode n) const { return !isAtom(n); } + + static inline bool isAtom(TNode n) { + return arith::isRelationOperator(n.getKind()); + } + + static inline bool isTerm(TNode n) { + return !isAtom(n); + } + }; -}; /* namesapce arith */ +}; /* namesapce rewrite */ }; /* namespace theory */ }; /* namespace CVC4 */ diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 6808e3d8f..9e2e3a3a7 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -4,7 +4,12 @@ # src/theory/builtin/kinds. # -theory ::CVC4::theory::arith::TheoryArith "theory_arith.h" +theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h" + +properties stable-infinite check propagate staticLearning presolve + +rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" + operator PLUS 2: "arithmetic addition" operator MULT 2: "arithmetic multiplication" @@ -12,6 +17,9 @@ operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" operator DIVISION 2 "arithmetic division" +sort REAL_TYPE "Real type" +sort INTEGER_TYPE "Integer type" + constant CONST_RATIONAL \ ::CVC4::Rational \ ::CVC4::RationalHashStrategy \ @@ -28,3 +36,5 @@ operator LT 2 "less than, x < y" operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" + +endtheory
\ No newline at end of file diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 766a8fc0a..2a8c1077e 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -30,9 +30,10 @@ bool VarList::isSorted(iterator start, iterator end) { } bool VarList::isMember(Node n) { - if(n.getNumChildren() == 0) { - return Variable::isMember(n); - } else if(n.getKind() == kind::MULT) { + if(Variable::isMember(n)) { + return true; + } + if(n.getKind() == kind::MULT) { Node::iterator curr = n.begin(), end = n.end(); Node prev = *curr; if(!Variable::isMember(prev)) return false; @@ -59,7 +60,7 @@ int VarList::cmp(const VarList& vl) const { } VarList VarList::parseVarList(Node n) { - if(n.getNumChildren() == 0) { + if(Variable::isMember(n)) { return VarList(Variable(n)); } else { Assert(n.getKind() == kind::MULT); diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 1c9b2685d..29db6cdb9 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "expr/node_self_iterator.h" #include "util/rational.h" +#include "theory/theory.h" #include "theory/arith/arith_constants.h" #include "theory/arith/arith_utilities.h" @@ -183,8 +184,11 @@ public: Assert(isMember(getNode())); } + // TODO: check if it's a theory leaf also static bool isMember(Node n) { - return n.getMetaKind() == kind::metakind::VARIABLE; + if (n.getKind() == kind::CONST_INTEGER) return false; + if (n.getKind() == kind::CONST_RATIONAL) return false; + return Theory::isLeafOf(n, theory::THEORY_ARITH); } bool isNormalForm() { return isMember(getNode()); } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index bf5f285a5..b9c983215 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -53,15 +53,14 @@ using namespace CVC4::theory::arith; struct SlackAttrID; typedef expr::Attribute<SlackAttrID, Node> Slack; -TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) : - Theory(id, c, out), +TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : + Theory(THEORY_ARITH, c, out), d_constants(NodeManager::currentNM()), d_partialModel(c), d_basicManager(), d_activityMonitor(), d_diseq(c), d_tableau(d_activityMonitor, d_basicManager), - d_rewriter(&d_constants), d_propagator(c, out), d_simplex(d_constants, d_partialModel, d_basicManager, d_out, d_activityMonitor, d_tableau), d_statistics() @@ -116,7 +115,7 @@ void TheoryArith::preRegisterTerm(TNode n) { d_out->setIncomplete(); } - if(isTheoryLeaf(n) || isStrictlyVarList){ + if(isLeaf(n) || isStrictlyVarList){ ++(d_statistics.d_statUserVariables); ArithVar varN = requestArithVar(n,false); setupInitialValue(varN); @@ -144,13 +143,8 @@ void TheoryArith::preRegisterTerm(TNode n) { } - -bool TheoryArith::isTheoryLeaf(TNode x) const{ - return x.getMetaKind() == kind::metakind::VARIABLE; -} - ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ - Assert(isTheoryLeaf(x)); + Assert(isLeaf(x)); Assert(!hasArithVar(x)); ArithVar varX = d_variables.size(); @@ -179,7 +173,9 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v Node n = variable.getNode(); - Assert(isTheoryLeaf(n)); + Debug("rewriter") << "should be var: " << n << endl; + + Assert(isLeaf(n)); Assert(hasArithVar(n)); ArithVar av = asArithVar(n); @@ -191,8 +187,6 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v void TheoryArith::setupSlack(TNode left){ - - ++(d_statistics.d_statSlackVariables); TypeNode real_type = NodeManager::currentNM()->realType(); Node slack = NodeManager::currentNM()->mkVar(real_type); @@ -242,10 +236,6 @@ void TheoryArith::setupInitialValue(ArithVar x){ Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl; }; -RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { - return d_rewriter.preRewrite(n); -} - void TheoryArith::registerTerm(TNode tn){ Debug("arith") << "registerTerm(" << tn << ")" << endl; } @@ -270,7 +260,7 @@ TNode getSide(TNode assertion, Kind simpleKind){ ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){ TNode left = getSide<true>(assertion, simpleKind); - if(isTheoryLeaf(left)){ + if(isLeaf(left)){ return asArithVar(left); }else{ Assert(left.hasAttribute(Slack())); @@ -457,7 +447,7 @@ void TheoryArith::check(Effort effortLevel){ } } -void TheoryArith::explain(TNode n, Effort e) { +void TheoryArith::explain(TNode n) { // Node explanation = d_propagator.explain(n); // Debug("arith") << "arith::explain("<<explanation<<")->" // << explanation << endl; @@ -552,3 +542,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { Unhandled(n.getKind()); } } + +void TheoryArith::notifyEq(TNode lhs, TNode rhs) { + +} diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e9ff06adb..c95ca6cc4 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -94,31 +94,14 @@ private: */ Tableau d_tableau; - /** - * The rewriter module for arithmetic. - */ - ArithRewriter d_rewriter; - ArithUnatePropagator d_propagator; SimplexDecisionProcedure d_simplex; public: - TheoryArith(int id, context::Context* c, OutputChannel& out); + TheoryArith(context::Context* c, OutputChannel& out); ~TheoryArith(); /** - * Rewriting optimizations. - */ - RewriteResponse preRewrite(TNode n, bool topLevel); - - /** - * Plug in old rewrite to the new (pre,post)rewrite interface. - */ - RewriteResponse postRewrite(TNode n, bool topLevel) { - return d_rewriter.postRewrite(n); - } - - /** * Does non-context dependent setup for a node connected to a theory. */ void preRegisterTerm(TNode n); @@ -128,7 +111,9 @@ public: void check(Effort e); void propagate(Effort e); - void explain(TNode n, Effort e); + void explain(TNode n); + + void notifyEq(TNode lhs, TNode rhs); Node getValue(TNode n, TheoryEngine* engine); @@ -144,8 +129,6 @@ public: private: - bool isTheoryLeaf(TNode x) const; - ArithVar determineLeftVariable(TNode assertion, Kind simpleKind); diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 8a0a180db..578915d69 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libarrays.la libarrays_la_SOURCES = \ theory_arrays_type_rules.h \ + theory_arrays_rewriter.h \ theory_arrays.h \ theory_arrays.cpp diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 4ad9c7463..7738f50ca 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -4,7 +4,11 @@ # src/theory/builtin/kinds. # -theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h" +theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" + +properties polite stable-infinite + +rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h" operator ARRAY_TYPE 2 "array type" @@ -13,3 +17,5 @@ operator SELECT 2 "array select" # store a i e is a[i] <= e operator STORE 3 "array store" + +endtheory
\ No newline at end of file diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 55a539f44..ad7550a6c 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -30,8 +30,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::arrays; -TheoryArrays::TheoryArrays(int id, Context* c, OutputChannel& out) : - Theory(id, c, out) +TheoryArrays::TheoryArrays(Context* c, OutputChannel& out) : + Theory(THEORY_ARRAY, c, out) { } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 22a0148e1..d3472f952 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -31,32 +31,18 @@ namespace arrays { class TheoryArrays : public Theory { public: - TheoryArrays(int id, context::Context* c, OutputChannel& out); + TheoryArrays(context::Context* c, OutputChannel& out); ~TheoryArrays(); void preRegisterTerm(TNode n) { } void registerTerm(TNode n) { } - RewriteResponse preRewrite(TNode in, bool topLevel) { - Debug("arrays-rewrite") << "pre-rewriting " << in - << " topLevel==" << topLevel << std::endl; - return RewriteComplete(in); - } - - RewriteResponse postRewrite(TNode in, bool topLevel) { - Debug("arrays-rewrite") << "post-rewriting " << in - << " topLevel==" << topLevel << std::endl; - return RewriteComplete(in); - } - - void presolve() { - Unimplemented(); - } + void presolve() { } void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void check(Effort e); void propagate(Effort e) { } - void explain(TNode n, Effort e) { } + void explain(TNode n) { } Node getValue(TNode n, TheoryEngine* engine); void shutdown() { } std::string identify() const { return std::string("TheoryArrays"); } diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h new file mode 100644 index 000000000..103707601 --- /dev/null +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -0,0 +1,37 @@ +/* + * theory_arrays_rewriter.h + * + * Created on: Dec 21, 2010 + * Author: dejan + */ + +#pragma once + + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +class TheoryArraysRewriter { + +public: + + static inline RewriteResponse postRewrite(TNode node) { + return RewriteResponse(REWRITE_DONE, node); + } + + static inline RewriteResponse preRewrite(TNode node) { + return RewriteResponse(REWRITE_DONE, node); + } + + static inline void init() {} + static inline void shutdown() {} + +}; + +} +} +} + diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index c8a9b4dbd..0263ae017 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -8,6 +8,8 @@ noinst_LTLIBRARIES = libbooleans.la libbooleans_la_SOURCES = \ theory_bool.h \ theory_bool.cpp \ - theory_bool_type_rules.h + theory_bool_type_rules.h \ + theory_bool_rewriter.h \ + theory_bool_rewriter.cpp EXTRA_DIST = kinds diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index ac6b05881..25ca1cfe3 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -4,7 +4,13 @@ # src/theory/builtin/kinds. # -theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h" +theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h" + +properties finite + +rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h" + +sort BOOLEAN_TYPE "Boolean type" constant CONST_BOOLEAN \ bool \ @@ -19,3 +25,5 @@ operator IMPLIES 2 "logical implication" operator OR 2: "logical or" operator XOR 2 "exclusive or" operator ITE 3 "if-then-else" + +endtheory
\ No newline at end of file diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index b1ff472ac..f8071d45d 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -24,122 +24,6 @@ namespace CVC4 { namespace theory { namespace booleans { -RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) { - if(n.getKind() == kind::IFF) { - NodeManager* nodeManager = NodeManager::currentNM(); - Node tt = nodeManager->mkConst(true); - Node ff = nodeManager->mkConst(false); - - // rewrite simple cases of IFF - if(n[0] == tt) { - // IFF true x - return RewriteAgain(n[1]); - } else if(n[1] == tt) { - // IFF x true - return RewriteAgain(n[0]); - } else if(n[0] == ff) { - // IFF false x - return RewriteAgain(n[1].notNode()); - } else if(n[1] == ff) { - // IFF x false - return RewriteAgain(n[0].notNode()); - } else if(n[0] == n[1]) { - // IFF x x - return RewriteComplete(tt); - } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) { - // IFF (NOT x) x - return RewriteComplete(ff); - } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { - // IFF x (NOT x) - return RewriteComplete(ff); - } - } else if(n.getKind() == kind::ITE) { - // non-Boolean-valued ITEs should have been removed in place of - // a variable - Assert(n.getType().isBoolean()); - - NodeManager* nodeManager = NodeManager::currentNM(); - - // rewrite simple cases of ITE - if(n[0] == nodeManager->mkConst(true)) { - // ITE true x y - return RewriteAgain(n[1]); - } else if(n[0] == nodeManager->mkConst(false)) { - // ITE false x y - return RewriteAgain(n[2]); - } else if(n[1] == n[2]) { - // ITE c x x - return RewriteAgain(n[1]); - } - } - - return RewriteComplete(n); -} - - -RewriteResponse TheoryBool::postRewrite(TNode n, bool topLevel) { - if(n.getKind() == kind::IFF) { - NodeManager* nodeManager = NodeManager::currentNM(); - Node tt = nodeManager->mkConst(true); - Node ff = nodeManager->mkConst(false); - - // rewrite simple cases of IFF - if(n[0] == tt) { - // IFF true x - return RewriteComplete(n[1]); - } else if(n[1] == tt) { - // IFF x true - return RewriteComplete(n[0]); - } else if(n[0] == ff) { - // IFF false x - return RewriteAgain(n[1].notNode()); - } else if(n[1] == ff) { - // IFF x false - return RewriteAgain(n[0].notNode()); - } else if(n[0] == n[1]) { - // IFF x x - return RewriteComplete(tt); - } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) { - // IFF (NOT x) x - return RewriteComplete(ff); - } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { - // IFF x (NOT x) - return RewriteComplete(ff); - } - - if(n[1] < n[0]) { - // normalize (IFF x y) ==> (IFF y x), if y < x - return RewriteComplete(n[1].iffNode(n[0])); - } - } else if(n.getKind() == kind::ITE) { - // non-Boolean-valued ITEs should have been removed in place of - // a variable - Assert(n.getType().isBoolean()); - - NodeManager* nodeManager = NodeManager::currentNM(); - - // rewrite simple cases of ITE - if(n[0] == nodeManager->mkConst(true)) { - // ITE true x y - return RewriteComplete(n[1]); - } else if(n[0] == nodeManager->mkConst(false)) { - // ITE false x y - return RewriteComplete(n[2]); - } else if(n[1] == n[2]) { - // ITE c x x - return RewriteComplete(n[1]); - } - - if(n[0].getKind() == kind::NOT) { - // rewrite (ITE (NOT c) x y) to (ITE c y x) - Node out = nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1]); - return RewriteComplete(out); - } - } - - return RewriteComplete(n); -} - Node TheoryBool::getValue(TNode n, TheoryEngine* engine) { NodeManager* nodeManager = NodeManager::currentNM(); diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index fa826539c..5d91842d7 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -30,8 +30,8 @@ namespace booleans { class TheoryBool : public Theory { public: - TheoryBool(int id, context::Context* c, OutputChannel& out) : - Theory(id, c, out) { + TheoryBool(context::Context* c, OutputChannel& out) : + Theory(THEORY_BOOL, c, out) { } void preRegisterTerm(TNode n) { @@ -42,17 +42,9 @@ public: Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl; Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl; } - void check(Effort e) { Unimplemented(); } - void propagate(Effort e) { Unimplemented(); } - void explain(TNode n, Effort e) { Unimplemented(); } - - void presolve(){ Unimplemented(); } Node getValue(TNode n, TheoryEngine* engine); - RewriteResponse preRewrite(TNode n, bool topLevel); - RewriteResponse postRewrite(TNode n, bool topLevel); - std::string identify() const { return std::string("TheoryBool"); } }; diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp new file mode 100644 index 000000000..a62bc6fa0 --- /dev/null +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -0,0 +1,72 @@ +#include <algorithm> +#include "theory/booleans/theory_bool_rewriter.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { + NodeManager* nodeManager = NodeManager::currentNM(); + Node tt = nodeManager->mkConst(true); + Node ff = nodeManager->mkConst(false); + + switch(n.getKind()) { + case kind::NOT: { + if (n[0] == tt) return RewriteResponse(REWRITE_DONE, ff); + if (n[0] == ff) return RewriteResponse(REWRITE_DONE, tt); + if (n[0].getKind() == kind::NOT) return RewriteResponse(REWRITE_AGAIN, n[0][0]); + break; + } + case kind::IFF: { + // rewrite simple cases of IFF + if(n[0] == tt) { + // IFF true x + return RewriteResponse(REWRITE_AGAIN, n[1]); + } else if(n[1] == tt) { + // IFF x true + return RewriteResponse(REWRITE_AGAIN, n[0]); + } else if(n[0] == ff) { + // IFF false x + return RewriteResponse(REWRITE_AGAIN, n[1].notNode()); + } else if(n[1] == ff) { + // IFF x false + return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + } else if(n[0] == n[1]) { + // IFF x x + return RewriteResponse(REWRITE_DONE, tt); + } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) { + // IFF (NOT x) x + return RewriteResponse(REWRITE_DONE, ff); + } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { + // IFF x (NOT x) + return RewriteResponse(REWRITE_DONE, ff); + } + break; + } + case kind::ITE: { + // non-Boolean-valued ITEs should have been removed in place of + // a variable + Assert(n.getType().isBoolean()); + // rewrite simple cases of ITE + if(n[0] == tt) { + // ITE true x y + return RewriteResponse(REWRITE_AGAIN, n[1]); + } else if(n[0] == ff) { + // ITE false x y + return RewriteResponse(REWRITE_AGAIN, n[2]); + } else if(n[1] == n[2]) { + // ITE c x x + return RewriteResponse(REWRITE_AGAIN, n[1]); + } + break; + } + default: + return RewriteResponse(REWRITE_DONE, n); + } + return RewriteResponse(REWRITE_DONE, n); +} + +} +} +} + diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h new file mode 100644 index 000000000..62eed9e2b --- /dev/null +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -0,0 +1,32 @@ +/* + * theory_bool_rewriter.h + * + * Created on: Dec 21, 2010 + * Author: dejan + */ + +#pragma once + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +class TheoryBoolRewriter { + +public: + + static RewriteResponse preRewrite(TNode node); + static RewriteResponse postRewrite(TNode node) { + return preRewrite(node); + } + + static void init() {} + static void shutdown() {} + +}; + +} +} +} diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am index d1df0e425..9856cdbe6 100644 --- a/src/theory/builtin/Makefile.am +++ b/src/theory/builtin/Makefile.am @@ -7,6 +7,8 @@ noinst_LTLIBRARIES = libbuiltin.la libbuiltin_la_SOURCES = \ theory_builtin_type_rules.h \ + theory_builtin_rewriter.h \ + theory_builtin_rewriter.cpp \ theory_builtin.h \ theory_builtin.cpp diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index ad442fc2f..2831161c3 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -106,7 +106,14 @@ # commands. # -theory builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h" +theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h" + +properties stable-infinite + +# Rewriter responisble for all the terms of the theory +rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h" + +sort BUILTIN_OPERATOR_TYPE "Built in type for built in operators" # A kind representing "inlined" operators defined with OPERATOR # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's @@ -130,7 +137,9 @@ operator TUPLE 2: "a tuple" constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ ::CVC4::TypeConstantHashStrategy \ - "expr/type_constant.h" \ + "expr/kind.h" \ "basic types" operator FUNCTION_TYPE 2: "function type" operator TUPLE_TYPE 2: "tuple type" + +endtheory
\ No newline at end of file diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 810cd1d39..489c97e67 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -26,49 +26,6 @@ namespace CVC4 { namespace theory { namespace builtin { -Node TheoryBuiltin::blastDistinct(TNode in) { - Debug("theory-rewrite") << "TheoryBuiltin::blastDistinct: " - << in << std::endl; - Assert(in.getKind() == kind::DISTINCT); - if(in.getNumChildren() == 2) { - // if this is the case exactly 1 != pair will be generated so the - // AND is not required - Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ? - kind::IFF : kind::EQUAL, - in[0], in[1]); - Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); - return neq; - } - // assume that in.getNumChildren() > 2 => diseqs.size() > 1 - vector<Node> diseqs; - for(TNode::iterator i = in.begin(); i != in.end(); ++i) { - TNode::iterator j = i; - while(++j != in.end()) { - Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ? - kind::IFF : kind::EQUAL, - *i, *j); - Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); - diseqs.push_back(neq); - } - } - Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs); - return out; -} - -RewriteResponse TheoryBuiltin::preRewrite(TNode in, bool topLevel) { - switch(in.getKind()) { - case kind::DISTINCT: - return RewriteComplete(blastDistinct(in)); - - case kind::EQUAL: - // EQUAL is a special case that should never end up here - Unreachable("TheoryBuiltin can't rewrite EQUAL !"); - - default: - return RewriteComplete(in); - } -} - Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) { switch(n.getKind()) { diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index cce5ac6b8..baa1493b6 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -28,25 +28,10 @@ namespace theory { namespace builtin { class TheoryBuiltin : public Theory { - /** rewrite a DISTINCT expr */ - static Node blastDistinct(TNode in); - public: - 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(); } - void propagate(Effort e) { Unreachable(); } - void explain(TNode n, Effort e) { Unreachable(); } - void presolve() { Unreachable(); } + TheoryBuiltin(context::Context* c, OutputChannel& out) : + Theory(THEORY_BUILTIN, c, out) {} Node getValue(TNode n, TheoryEngine* engine); - void shutdown() { } - RewriteResponse preRewrite(TNode n, bool topLevel); std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp new file mode 100644 index 000000000..05f7891d6 --- /dev/null +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -0,0 +1,35 @@ +#include "theory/builtin/theory_builtin_rewriter.h" + +namespace CVC4 { +namespace theory { +namespace builtin { + +Node TheoryBuiltinRewriter::blastDistinct(TNode in) { + + Assert(in.getKind() == kind::DISTINCT); + + if(in.getNumChildren() == 2) { + // if this is the case exactly 1 != pair will be generated so the + // AND is not required + Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ? kind::IFF : kind::EQUAL, in[0], in[1]); + Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); + return neq; + } + + // assume that in.getNumChildren() > 2 => diseqs.size() > 1 + vector<Node> diseqs; + for(TNode::iterator i = in.begin(); i != in.end(); ++i) { + TNode::iterator j = i; + while(++j != in.end()) { + Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ? kind::IFF : kind::EQUAL, *i, *j); + Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); + diseqs.push_back(neq); + } + } + Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs); + return out; +} + +} +} +} diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h new file mode 100644 index 000000000..7da4289b1 --- /dev/null +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -0,0 +1,48 @@ +/* + * theory_builtin_rewriter.h + * + * Created on: Dec 21, 2010 + * Author: dejan + */ + +#pragma once + +#include "theory/rewriter.h" +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace builtin { + +class TheoryBuiltinRewriter { + + static Node blastDistinct(TNode node); + +public: + + static inline RewriteResponse postRewrite(TNode node) { + if (node.getKind() == kind::EQUAL) { + return Rewriter::callPostRewrite(Theory::theoryOf(node[0]), node); + } + return RewriteResponse(REWRITE_DONE, node); + } + + static inline RewriteResponse preRewrite(TNode node) { + switch(node.getKind()) { + case kind::DISTINCT: + return RewriteResponse(REWRITE_DONE, blastDistinct(node)); + case kind::EQUAL: + return Rewriter::callPreRewrite(Theory::theoryOf(node[0]), node); + default: + return RewriteResponse(REWRITE_DONE, node); + } + } + + static inline void init() {} + static inline void shutdown() {} + +}; + +} +} +} diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index c07bf018e..3e84f482c 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -12,6 +12,8 @@ libbv_la_SOURCES = \ theory_bv_rewrite_rules.h \ theory_bv_rewrite_rules.cpp \ theory_bv_type_rules.h \ + theory_bv_rewriter.h \ + theory_bv_rewriter.cpp \ equality_engine.h \ equality_engine.cpp diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index e7374284e..9f6c42aa6 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -4,7 +4,11 @@ # src/theory/builtin/kinds. # -theory ::CVC4::theory::bv::TheoryBV "theory_bv.h" +theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h" + +properties finite check + +rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" constant BITVECTOR_TYPE \ ::CVC4::BitVectorSize \ @@ -90,3 +94,5 @@ parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero- parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend" parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" + +endtheory
\ No newline at end of file diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 69ff48721..c9e7c397e 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -19,7 +19,6 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/theory_engine.h" @@ -41,63 +40,6 @@ void TheoryBV::preRegisterTerm(TNode node) { } } -RewriteResponse TheoryBV::postRewrite(TNode node, bool topLevel) { - - Debug("bitvector") << "TheoryBV::postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ")" << std::endl; - - Node result; - - if (node.getKind() == kind::CONST_BITVECTOR /* || isLeaf(n)) */) - result = node; - else { - switch (node.getKind()) { - case kind::BITVECTOR_CONCAT: - result = LinearRewriteStrategy< - // Flatten the top level concatenations - CoreRewriteRules::ConcatFlatten, - // Merge the adjacent extracts on non-constants - CoreRewriteRules::ConcatExtractMerge, - // Merge the adjacent extracts on constants - CoreRewriteRules::ConcatConstantMerge, - // At this point only Extract-Whole could apply, if the result is only one extract - // or at some sub-expression if the result is a concatenation. - ApplyRuleToChildren<kind::BITVECTOR_CONCAT, CoreRewriteRules::ExtractWhole> - >::apply(node); - break; - case kind::BITVECTOR_EXTRACT: - result = LinearRewriteStrategy< - // Extract over a constant gives a constant - CoreRewriteRules::ExtractConstant, - // Extract over an extract is simplified to one extract - CoreRewriteRules::ExtractExtract, - // Extract over a concatenation is distributed to the appropriate concatenations - CoreRewriteRules::ExtractConcat, - // At this point only Extract-Whole could apply - CoreRewriteRules::ExtractWhole - >::apply(node); - break; - case kind::EQUAL: - result = LinearRewriteStrategy< - // Two distinct values rewrite to false - CoreRewriteRules::FailEq, - // If both sides are equal equality is true - CoreRewriteRules::SimplifyEq - >::apply(node); - break; - default: - // TODO: figure out when this is an operator - result = node; - break; - // Unhandled(); - } - } - - Debug("bitvector") << "TheoryBV::postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ") => " << result << std::endl; - - return RewriteComplete(result); -} - - void TheoryBV::check(Effort e) { Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index f6073eff9..dfae3b965 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -61,8 +61,8 @@ private: public: - TheoryBV(int id, context::Context* c, OutputChannel& out) : - Theory(id, c, out), d_eqEngine(*this, c), d_assertions(c) { + TheoryBV(context::Context* c, OutputChannel& out) : + Theory(THEORY_BV, c, out), d_eqEngine(*this, c), d_assertions(c) { } void preRegisterTerm(TNode n); @@ -71,18 +71,14 @@ public: void check(Effort e); - void presolve(){ - Unimplemented(); - } + void presolve() { } - void propagate(Effort e) {} + void propagate(Effort e) { } - void explain(TNode n, Effort e) { } + void explain(TNode n) { } Node getValue(TNode n, TheoryEngine* engine); - RewriteResponse postRewrite(TNode n, bool topLevel); - std::string identify() const { return std::string("TheoryBV"); } };/* class TheoryBV */ diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp new file mode 100644 index 000000000..cd2efd64f --- /dev/null +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -0,0 +1,70 @@ +/* + * theory_bv_rewriter.cpp + * + * Created on: Dec 21, 2010 + * Author: dejan + */ + +#include "theory/bv/theory_bv_rewriter.h" +#include "theory/bv/theory_bv_rewrite_rules.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + +RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { + + Debug("bitvector") << "TheoryBV::postRewrite(" << node << ")" << std::endl; + + Node result; + + if (node.getKind() == kind::CONST_BITVECTOR /* || isLeaf(n)) */) + result = node; + else { + switch (node.getKind()) { + case kind::BITVECTOR_CONCAT: + result = LinearRewriteStrategy< + // Flatten the top level concatenations + CoreRewriteRules::ConcatFlatten, + // Merge the adjacent extracts on non-constants + CoreRewriteRules::ConcatExtractMerge, + // Merge the adjacent extracts on constants + CoreRewriteRules::ConcatConstantMerge, + // At this point only Extract-Whole could apply, if the result is only one extract + // or at some sub-expression if the result is a concatenation. + ApplyRuleToChildren<kind::BITVECTOR_CONCAT, CoreRewriteRules::ExtractWhole> + >::apply(node); + break; + case kind::BITVECTOR_EXTRACT: + result = LinearRewriteStrategy< + // Extract over a constant gives a constant + CoreRewriteRules::ExtractConstant, + // Extract over an extract is simplified to one extract + CoreRewriteRules::ExtractExtract, + // Extract over a concatenation is distributed to the appropriate concatenations + CoreRewriteRules::ExtractConcat, + // At this point only Extract-Whole could apply + CoreRewriteRules::ExtractWhole + >::apply(node); + break; + case kind::EQUAL: + result = LinearRewriteStrategy< + // Two distinct values rewrite to false + CoreRewriteRules::FailEq, + // If both sides are equal equality is true + CoreRewriteRules::SimplifyEq + >::apply(node); + break; + default: + // TODO: figure out when this is an operator + result = node; + break; + // Unhandled(); + } + } + + Debug("bitvector") << "TheoryBV::postRewrite(" << node << ") => " << result << std::endl; + + return RewriteResponse(REWRITE_DONE, result); +} + diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h new file mode 100644 index 000000000..741b9fcbc --- /dev/null +++ b/src/theory/bv/theory_bv_rewriter.h @@ -0,0 +1,35 @@ +/* + * theory_bv_rewriter.h + * + * Created on: Dec 21, 2010 + * Author: dejan + */ + +#pragma once + + + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +class TheoryBVRewriter { + +public: + + static RewriteResponse postRewrite(TNode node); + + static inline RewriteResponse preRewrite(TNode node) { + return RewriteResponse(REWRITE_DONE, node); + } + + static inline void init() {} + static inline void shutdown() {} + +}; + +} +} +} diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter new file mode 100755 index 000000000..8eb29bb15 --- /dev/null +++ b/src/theory/mkrewriter @@ -0,0 +1,165 @@ +#!/bin/bash +# +# mkrewriter +# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2010 The CVC4 Project +# +# The purpose of this script is to create kind.h from a template and a +# list of theory kinds. +# +# Invocation: +# +# mkkind template-file theory-kind-files... +# +# Output is to standard out. +# + +copyright=2010 + +cat <<EOF +/********************* */ +/** kind.h + ** + ** Copyright $copyright The AcSys Group, New York University, and as below. + ** + ** This header file automatically generated by: + ** + ** $0 $@ + ** + ** for the CVC4 project. + **/ + +EOF + +me=$(basename "$0") + +template=$1; shift + +rewriter_includes= +rewrite_init= +rewrite_shutdown= + +pre_rewrite_calls= +pre_rewrite_get_cache= +pre_rewrite_set_cache= + +post_rewrite_calls= +post_rewrite_get_cache= +post_rewrite_set_cache= + +seen_theory=false +seen_theory_builtin=false + +function theory { + # theory T header + + lineno=${BASH_LINENO[0]} + + # this script doesn't care about the theory class information, but + # makes does make sure it's there + seen_theory=true + if [ "$1" = THEORY_BUILTIN ]; then + if $seen_theory_builtin; then + echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2 + exit 1 + fi + seen_theory_builtin=true + elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then + echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 + exit 1 + elif ! expr "$2" : '\(::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2 + elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 + fi + + theory_id="$1" +} + +function properties { + # properties prop* + lineno=${BASH_LINENO[0]} +} + +function endtheory { + # endtheory + lineno=${BASH_LINENO[0]} +} + +function rewriter { + # rewriter class header + class="$1" + header="$2" + + rewriter_includes="${rewriter_includes}#include \"$header\" +" + rewrite_init="${rewrite_init} ${class}::init(); +" + rewrite_shutdown="${rewrite_shutdown} ${class}::shutdown(); +" + + pre_rewrite_calls="${pre_rewrite_calls} case ${theory_id}: return ${class}::preRewrite(node); +" + pre_rewrite_get_cache="${pre_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node); +" + pre_rewrite_set_cache="${pre_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache); +" + + post_rewrite_calls="${post_rewrite_calls} case ${theory_id}: return ${class}::postRewrite(node); +" + post_rewrite_get_cache="${post_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node); +" + post_rewrite_set_cache="${post_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache); +" + + lineno=${BASH_LINENO[0]} + +} + +function sort { + # sort TYPE ["comment"] + lineno=${BASH_LINENO[0]} +} + +function variable { + # variable K ["comment"] + lineno=${BASH_LINENO[0]} +} + +function operator { + # operator K #children ["comment"] + lineno=${BASH_LINENO[0]} +} + +function parameterized { + # parameterized K1 K2 #children ["comment"] + lineno=${BASH_LINENO[0]} +} + +function constant { + # constant K T Hasher header ["comment"] + lineno=${BASH_LINENO[0]} +} + +while [ $# -gt 0 ]; do + kf=$1 + seen_theory=false + b=$(basename $(dirname "$kf")) + source "$kf" + check_theory_seen + shift +done +check_builtin_theory_seen + +## output + +text=$(cat "$template") +for var in rewriter_includes pre_rewrite_calls post_rewrite_calls pre_rewrite_get_cache post_rewrite_get_cache pre_rewrite_set_cache post_rewrite_set_cache rewrite_init rewrite_shutdown; do + eval text="\${text//\\\$\\{$var\\}/\${$var}}" +done +error=`expr "$text" : '.*\${\([^}]*\)}.*'` +if [ -n "$error" ]; then + echo "$template:0: error: undefined replacement \${$error}" >&2 + exit 1 +fi +echo "$text" diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof deleted file mode 100755 index 415668b49..000000000 --- a/src/theory/mktheoryof +++ /dev/null @@ -1,162 +0,0 @@ -#!/bin/bash -# -# mktheoryof -# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010 The CVC4 Project -# -# The purpose of this script is to create theoryof_table.h from a -# template and a list of theory kinds. -# -# Invocation: -# -# mktheoryof template-file theory-kind-files... -# -# Output is to standard out. -# - -copyright=2010 - -cat <<EOF -/********************* */ -/** theoryof_table.h - ** - ** Copyright $copyright The AcSys Group, New York University, and as below. - ** - ** This header file automatically generated by: - ** - ** $0 $@ - ** - ** for the CVC4 project. - **/ - -EOF - -template=$1; shift - -theoryof_table_forwards= -theoryof_table_registers= - -seen_theory=false -seen_theory_builtin=false - -function theory { - lineno=${BASH_LINENO[0]} - - # this script doesn't care about the theory class information, but - # makes does make sure it's there - seen_theory=true - if [ "$1" = builtin ]; then - if $seen_theory_builtin; then - echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2 - exit 1 - fi - seen_theory_builtin=true - shift - elif [ -z "$1" -o -z "$2" ]; then - echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 - exit 1 - elif ! expr "$1" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2 - elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 - fi - - decl= - last= - num=0 - for ns in `echo "$1" | sed 's,::, ,g'`; do - if [ -n "$last" ]; then - decl="${decl}namespace $last { " - let ++num - fi - last="$ns" - done - decl="${decl}class $last;" - while [ $num -gt 0 ]; do - decl="${decl} }" - let --num - done - - theoryof_table_forwards="${theoryof_table_forwards}$decl // #include \"theory/$b/$2\" -" - theoryof_table_registers="${theoryof_table_registers} - /* from $b */ - void registerTheory($1* th) { -" -} - -function variable { - # variable K ["comment"] - - lineno=${BASH_LINENO[0]} - - do_theoryof "$1" -} - -function operator { - # operator K #children ["comment"] - - lineno=${BASH_LINENO[0]} - - do_theoryof "$1" -} - -function parameterized { - # parameterized K #children ["comment"] - - lineno=${BASH_LINENO[0]} - - do_theoryof "$1" -} - -function constant { - # constant K T Hasher header ["comment"] - - lineno=${BASH_LINENO[0]} - - do_theoryof "$1" -} - -function do_theoryof { - check_theory_seen - theoryof_table_registers="${theoryof_table_registers} d_table[::CVC4::kind::$1] = (Theory*)th; -" -} - -function check_theory_seen { - if ! $seen_theory; then - echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 - exit 1 - fi -} - -function check_builtin_theory_seen { - if ! $seen_theory_builtin; then - echo "$me: warning: no declaration for the builtin theory found" >&2 - fi -} - -while [ $# -gt 0 ]; do - kf=$1 - seen_theory=false - b=$(basename $(dirname "$kf")) - source "$kf" - check_theory_seen - theoryof_table_registers="${theoryof_table_registers} } -" - shift -done -check_builtin_theory_seen - -## output - -text=$(cat "$template") -for var in theoryof_table_forwards theoryof_table_registers; do - eval text="\${text//\\\$\\{$var\\}/\${$var}}" -done -error=`expr "$text" : '.*\${\([^}]*\)}.*'` -if [ -n "$error" ]; then - echo "$template:0: error: undefined replacement \${$error}" >&2 - exit 1 -fi -echo "$text" diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits new file mode 100755 index 000000000..58e5e4381 --- /dev/null +++ b/src/theory/mktheorytraits @@ -0,0 +1,263 @@ +#!/bin/bash +# +# mktheorytraits +# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2010 The CVC4 Project +# +# The purpose of this script is to create kind.h from a template and a +# list of theory kinds. +# +# Invocation: +# +# mkkind template-file theory-kind-files... +# +# Output is to standard out. +# + +copyright=2010 + +cat <<EOF +/********************* */ +/** theory_traits.h + ** + ** Copyright $copyright The AcSys Group, New York University, and as below. + ** + ** This header file automatically generated by: + ** + ** $0 $@ + ** + ** for the CVC4 project. + **/ + +EOF + +me=$(basename "$0") + +template=$1; shift + +theory_traits= +theory_includes= +theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\ +" + +theory_has_check="false" +theory_has_propagate="false" +theory_has_static_learning="false" +theory_has_presolve="false" + +theory_stable_infinite="false" +theory_finite="false" +theory_polite="false" + +rewriter_class= +rewriter_header= + +theory_id= +theory_class= + +seen_theory=false +seen_theory_builtin=false + +function theory { + # theory T header + + lineno=${BASH_LINENO[0]} + + # this script doesn't care about the theory class information, but + # makes does make sure it's there + seen_theory=true + if [ "$1" = THEORY_BUILTIN ]; then + if $seen_theory_builtin; then + echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2 + exit 1 + fi + seen_theory_builtin=true + elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then + echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 + exit 1 + elif ! expr "$2" : '\(::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2 + elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 + fi + + theory_id="$1" + theory_class="$2" + + theory_includes="${theory_includes}#include \"$3\" +" + theory_for_each_macro="${theory_for_each_macro} CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::${theory_id}) \\ +" +} + +function rewriter { + # rewriter class header + lineno=${BASH_LINENO[0]} + + rewriter_class="$1" + rewriter_header="$2" + + theory_includes="${theory_includes}#include \"$2\" +" + +} + +function endtheory { + # endtheory + + theory_traits="${theory_traits} +template<> +struct TheoryTraits<${theory_id}> { + typedef ${theory_class} theory_class; + typedef ${rewriter_class} rewriter_class; + + static const bool isStableInfinite = ${theory_stable_infinite}; + static const bool isFinite = ${theory_finite}; + static const bool isPolite = ${theory_polite}; + + static const bool hasCheck = ${theory_has_check}; + static const bool hasPropagate = ${theory_has_propagate}; + static const bool hasStaticLearning = ${theory_has_static_learning}; + static const bool hasPresolve = ${theory_has_presolve}; +}; +" + + theory_has_check="false" + theory_has_propagate="false" + theory_has_static_learning="false" + theory_has_presolve="false" + + theory_stable_infinite="false" + theory_finite="false" + theory_polite="false" + + rewriter_class= + rewriter_header= + + theory_id= + theory_class= + + lineno=${BASH_LINENO[0]} +} + + +function properties { + # properties property* + lineno=${BASH_LINENO[0]} + while (( $# )); + do + property="$1" + case "$property" in + finite) theory_finite="true";; + stable-infinite) theory_stable_infinite="true";; + polite) theory_polite="true";; + check) theory_has_check="true";; + propagate) theory_has_propagate="true";; + staticLearning) theory_has_static_learning="true";; + presolve) theory_has_presolve="true"; + esac + shift + done; +} + +function sort { + # sort TYPE ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_sort "$1" "$2" +} + +function variable { + # variable K ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" 0 "$2" +} + +function operator { + # operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" "$2" "$3" +} + +function parameterized { + # parameterized K1 K2 #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" "$3" "$4" +} + +function constant { + # constant K T Hasher header ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" 0 "$5" +} + +function register_sort { + id=$1 + comment=$2 + type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; +" +} + +function register_kind { + r=$1 + nc=$2 + comment=$3 + kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; +" +} + +function check_theory_seen { + if ! $seen_theory; then + echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 + exit 1 + fi +} + +function check_builtin_theory_seen { + if ! $seen_theory_builtin; then + echo "$me: warning: no declaration for the builtin theory found" >&2 + fi +} + +while [ $# -gt 0 ]; do + kf=$1 + seen_theory=false + b=$(basename $(dirname "$kf")) + kind_decls="${kind_decls} + /* from $b */ +" + kind_printers="${kind_printers} + /* from $b */ +" + source "$kf" + check_theory_seen + shift +done +check_builtin_theory_seen + +## output + +text=$(cat "$template") +for var in theory_traits theory_for_each_macro theory_includes; do + eval text="\${text//\\\$\\{$var\\}/\${$var}}" +done +error=`expr "$text" : '.*\${\([^}]*\)}.*'` +if [ -n "$error" ]; then + echo "$template:0: error: undefined replacement \${$error}" >&2 + exit 1 +fi +echo "$text" diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp new file mode 100644 index 000000000..fe7ad7a9a --- /dev/null +++ b/src/theory/rewriter.cpp @@ -0,0 +1,173 @@ +/* + * rewriter.cpp + * + * Created on: Dec 13, 2010 + * Author: dejan + */ + +#include "theory/theory.h" +#include "theory/rewriter.h" +#include "theory/rewriter_tables.h" + +namespace CVC4 { +namespace theory { + +/** + * TheoryEngine::rewrite() keeps a stack of things that are being pre- + * and post-rewritten. Each element of the stack is a + * RewriteStackElement. + */ +struct RewriteStackElement { + + /** The node we're currently rewriting */ + Node node; + /** Original node */ + Node original; + /** Id of the theory that's currently rewriting this node */ + unsigned theoryId : 8; + /** Id of the original theory that started the rewrite */ + unsigned originalTheoryId : 8; + /** Index of the child this node is done rewriting */ + unsigned nextChild : 32; + /** Builder for this node */ + NodeBuilder<> builder; + + /** + * Construct a fresh stack element. + */ + RewriteStackElement(Node node, TheoryId theoryId) : + node(node), + original(node), + theoryId(theoryId), + originalTheoryId(theoryId), + nextChild(0) { + } +}; + +Node Rewriter::rewrite(Node node) { + return rewriteTo(theory::Theory::theoryOf(node), node); +} + +Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { + + Debug("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl; + + // Put the node on the stack in order to start the "recursive" rewrite + vector<RewriteStackElement> rewriteStack; + rewriteStack.push_back(RewriteStackElement(node, theoryId)); + + // Rewrite until the stack is empty + for (;;){ + + // Get the top of the recursion stack + RewriteStackElement& rewriteStackTop = rewriteStack.back(); + + Debug("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl; + + // Before rewriting children we need to do a pre-rewrite of the node + if (rewriteStackTop.nextChild == 0) { + + // Check if the pre-rewrite has already been done (it's in the cache) + Node cached = Rewriter::getPreRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); + if (cached.isNull()) { + // Rewrite until fix-point is reached + for(;;) { + // Perform the pre-rewrite + RewriteResponse response = Rewriter::callPreRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); + // Put the rewritten node to the top of the stack + rewriteStackTop.node = response.node; + TheoryId newTheory = Theory::theoryOf(rewriteStackTop.node); + // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite + if (newTheory == (TheoryId) rewriteStackTop.theoryId && response.status == REWRITE_DONE) { + break; + } + rewriteStackTop.theoryId = newTheory; + } + // Cache the rewrite + Rewriter::setPreRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node); + } + // Otherwise we're have already been pre-rewritten (in pre-rewrite cache) + else { + // Continue with the cached version + rewriteStackTop.node = cached; + rewriteStackTop.theoryId = Theory::theoryOf(cached); + } + } + + // Now it's time to rewrite the children, check if this has already been done + Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); + // If not, go through the children + if(cached.isNull()) { + + // The child we need to rewrite + unsigned child = rewriteStackTop.nextChild++; + + // To build the rewritten expression we set up the builder + if(child == 0) { + if (rewriteStackTop.node.getNumChildren() > 0) { + // The children will add themselves to the builder once they're done + rewriteStackTop.builder << rewriteStackTop.node.getKind(); + kind::MetaKind metaKind = rewriteStackTop.node.getMetaKind(); + if (metaKind == kind::metakind::PARAMETERIZED) { + rewriteStackTop.builder << rewriteStackTop.node.getOperator(); + } + } + } + + // Process the next child + if(child < rewriteStackTop.node.getNumChildren()) { + // The child node + Node childNode = rewriteStackTop.node[child]; + // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now) + rewriteStack.push_back(RewriteStackElement(childNode, Theory::theoryOf(childNode))); + // Go on with the rewriting + continue; + } + + // Incorporate the children if necessary + if (rewriteStackTop.node.getNumChildren() > 0) { + rewriteStackTop.node = rewriteStackTop.builder; + rewriteStackTop.theoryId = Theory::theoryOf(rewriteStackTop.node); + } + + // Done with all pre-rewriting, so let's do the post rewrite + for(;;) { + // Do the post-rewrite + RewriteResponse response = Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); + // We continue with the response we got + rewriteStackTop.node = response.node; + TheoryId newTheoryId = Theory::theoryOf(rewriteStackTop.node); + if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) { + // In the post rewrite if we've changed theories, we must do a full rewrite + rewriteStackTop.node = rewriteTo(newTheoryId, rewriteStackTop.node); + break; + } else if (response.status == REWRITE_DONE) { + break; + } + } + // We're done with the post rewrite, so we add to the cache + Rewriter::setPostRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node); + + } else { + // We were already in cache, so just remember it + rewriteStackTop.node = cached; + rewriteStackTop.theoryId = Theory::theoryOf(cached); + } + + // If this is the last node, just return + if (rewriteStack.size() == 1) { + return rewriteStackTop.node; + } + + // We're done with this node, append it to the parent + rewriteStack[rewriteStack.size() - 2].builder << rewriteStackTop.node; + rewriteStack.pop_back(); + } + + Unreachable(); + return Node::null(); +} + + +} +} diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h new file mode 100644 index 000000000..403ccf755 --- /dev/null +++ b/src/theory/rewriter.h @@ -0,0 +1,79 @@ +/* + * rewriter.h + * + * Created on: Dec 13, 2010 + * Author: dejan + */ + +#pragma once + +#include "expr/node.h" +#include "expr/attribute.h" + +namespace CVC4 { +namespace theory { + +enum RewriteStatus { + REWRITE_DONE, + REWRITE_AGAIN, + REWRITE_AGAIN_FULL +}; + +/** + * Instances of this class serve as response codes from + * Theory::preRewrite() and Theory::postRewrite(). Instances of + * derived classes RewriteComplete(n), RewriteAgain(n), and + * FullRewriteNeeded(n) should be used, giving self-documenting + * rewrite behavior. + */ +struct RewriteResponse { + const RewriteStatus status; + const Node node; + RewriteResponse(RewriteStatus status, Node node) : status(status), node(node) {} +}; + +class Rewriter { + + /** Returns the appropriate cache for a node */ + static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node); + + /** Returns the appropriate cache for a node */ + static Node getPostRewriteCache(theory::TheoryId theoryId, TNode node); + + /** Sets the appropriate cache for a node */ + static void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache); + + /** Sets the appropriate cache for a node */ + static void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache); + +public: + + /** Calls the pre rewrite for the given theory */ + static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node); + + /** Calls the post rewrite for the given theory */ + static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node); + + /** + * Rewrites the node using theoryOf to determine which rewriter to use on the node. + */ + static Node rewrite(Node node); + + /** + * Rewrites the node using the given theory rewriter. + */ + static Node rewriteTo(theory::TheoryId theoryId, Node node); + + /** + * Should be called before the rewriter get's used for the first time. + */ + static void init(); + + /** + * Should be called to clean up any state. + */ + static void shutdown(); +}; + +} // Namesapce theory +} // Namespace CVC4 diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h new file mode 100644 index 000000000..d33d7314e --- /dev/null +++ b/src/theory/rewriter_attributes.h @@ -0,0 +1,86 @@ +/* + * rewriter_attributes.h + * + * Created on: Dec 27, 2010 + * Author: dejan + */ + +#pragma once + +namespace CVC4 { +namespace theory { + +template <bool pre, theory::TheoryId theoryId> +struct RewriteCacheTag {}; + +template <theory::TheoryId theoryId> +struct RewriteAttibute { + + typedef expr::Attribute< RewriteCacheTag<true, theoryId>, Node> pre_rewrite; + typedef expr::Attribute< RewriteCacheTag<false, theoryId>, Node> post_rewrite; + + /** + * Get the value of the pre-rewrite cache. + */ + static Node getPreRewriteCache(TNode node) throw() { + Node cache; + if (node.hasAttribute(pre_rewrite())) { + node.getAttribute(pre_rewrite(), cache); + } else { + return Node::null(); + } + if (cache.isNull()) { + return node; + } else { + return cache; + } + } + + /** + * Set the value of the pre-rewrite cache. + */ + static void setPreRewriteCache(TNode node, TNode cache) throw() { + Debug("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl; + Assert(!cache.isNull()); + if (node == cache) { + node.setAttribute(pre_rewrite(), Node::null()); + } else { + node.setAttribute(pre_rewrite(), cache); + } + } + + /** + * Get the value of the post-rewrite cache. + * none). + */ + static Node getPostRewriteCache(TNode node) throw() { + Node cache; + if (node.hasAttribute(post_rewrite())) { + node.getAttribute(post_rewrite(), cache); + } else { + return Node::null(); + } + if (cache.isNull()) { + return node; + } else { + return cache; + } + } + + /** + * Set the value of the post-rewrite cache. v cannot be a null Node. + */ + static void setPostRewriteCache(TNode node, TNode cache) throw() { + Assert(!cache.isNull()); + Debug("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl; + if (node == cache) { + node.setAttribute(post_rewrite(), Node::null()); + } else { + node.setAttribute(post_rewrite(), cache); + } + } +}; + +} // Namespace CVC4 +} // Namespace theory + diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h new file mode 100644 index 000000000..e26c879e4 --- /dev/null +++ b/src/theory/rewriter_tables_template.h @@ -0,0 +1,69 @@ +#pragma once + +#include "theory/rewriter.h" +#include "theory/rewriter_attributes.h" + +${rewriter_includes} + +namespace CVC4 { +namespace theory { + +RewriteResponse Rewriter::callPreRewrite(theory::TheoryId theoryId, TNode node) { + switch(theoryId) { +${pre_rewrite_calls} + default: + Unreachable(); + } +} + +RewriteResponse Rewriter::callPostRewrite(theory::TheoryId theoryId, TNode node) { + switch(theoryId) { +${post_rewrite_calls} + default: + Unreachable(); + } +} + +Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) { + switch(theoryId) { +${pre_rewrite_get_cache} + default: + Unreachable(); + } +} + +Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) { + switch(theoryId) { +${post_rewrite_get_cache} + default: + Unreachable(); + } +} + +void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) { + switch(theoryId) { +${pre_rewrite_set_cache} + default: + Unreachable(); + } +} + +void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) { + switch(theoryId) { +${post_rewrite_set_cache} + default: + Unreachable(); + } +} + + +void Rewriter::init() { +${rewrite_init} +} + +void Rewriter::shutdown() { +${rewrite_shutdown} +} + +} +} diff --git a/src/theory/theory.h b/src/theory/theory.h index 77ae6ecd6..a4682710f 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -37,83 +37,6 @@ class TheoryEngine; namespace theory { -// rewrite cache support -template <bool topLevel> struct PreRewriteCacheTag {}; -typedef expr::Attribute<PreRewriteCacheTag<true>, Node> PreRewriteCacheTop; -typedef expr::Attribute<PreRewriteCacheTag<false>, Node> PreRewriteCache; -template <bool topLevel> struct PostRewriteCacheTag {}; -typedef expr::Attribute<PostRewriteCacheTag<true>, Node> PostRewriteCacheTop; -typedef expr::Attribute<PostRewriteCacheTag<false>, Node> PostRewriteCache; - -/** - * Instances of this class serve as response codes from - * Theory::preRewrite() and Theory::postRewrite(). Instances of - * derived classes RewriteComplete(n), RewriteAgain(n), and - * FullRewriteNeeded(n) should be used, giving self-documenting - * rewrite behavior. - */ -class RewriteResponse { -protected: - enum Status { DONE, REWRITE, REWRITE_FULL }; - - RewriteResponse(Status s, Node n) : d_status(s), d_node(n) {} - -private: - const Status d_status; - const Node d_node; - -public: - bool isDone() const { return d_status == DONE; } - bool needsMoreRewriting() const { return d_status != DONE; } - bool needsFullRewriting() const { return d_status == REWRITE_FULL; } - Node getNode() const { return d_node; } -};/* class RewriteResponse */ - -/** - * Signal that (pre,post)rewriting of the Node is complete at n. Note - * that if theory A returns this, and the Node is in another theory B, - * theory B will still be called on to pre- or postrewrite it. - */ -class RewriteComplete : public RewriteResponse { -public: - RewriteComplete(Node n) : RewriteResponse(DONE, n) {} -};/* class RewriteComplete */ - -/** - * Return n, but request additional rewriting of it; if this is - * returned from preRewrite(), this re-preRewrite()'s the Node. If - * this is returned from postRewrite(), this re-postRewrite()'s the - * Node, but does NOT re-preRewrite() it, nor does it rewrite the - * Node's children. - * - * Note that this is the behavior if a theory returns - * RewriteComplete() for a Node belonging to another theory. - */ -class RewriteAgain : public RewriteResponse { -public: - RewriteAgain(Node n) : RewriteResponse(REWRITE, n) {} -};/* class RewriteAgain */ - -/** - * Return n, but request an additional complete rewriting pass over - * it. This has the same behavior as RewriteAgain() for - * pre-rewriting. However, in post-rewriting, FullRewriteNeeded will - * _completely_ pre- and post-rewrite the term and the term's children - * (though it will use the cache to elide what calls it can). Use - * with caution; it has bad effects on performance. This might be - * useful if theory A rewrites a term into something quite different, - * and certain child nodes might belong to another theory whose normal - * form is unknown to theory A. For example, if the builtin theory - * post-rewrites (DISTINCT a b c) into pairwise NOT EQUAL expressions, - * the theories owning a, b, and c might need to rewrite that EQUAL. - * (This came up, but the fix was to rewrite DISTINCT in - * pre-rewriting, obviating the problem. See bug #168.) - */ -class FullRewriteNeeded : public RewriteResponse { -public: - FullRewriteNeeded(Node n) : RewriteResponse(REWRITE_FULL, n) {} -};/* class FullRewriteNeeded */ - /** * Base class for T-solvers. Abstract DPLL(T). * @@ -137,7 +60,7 @@ private: /** * A unique integer identifying the theory */ - int d_id; + TheoryId d_id; /** * The context for the Theory. @@ -147,11 +70,10 @@ private: /** * The assertFact() queue. * - * These can safely be TNodes because the literal map maintained in - * the SAT solver keeps them live. As an added benefit, if we have - * them as TNodes, dtors are cheap (optimized away?). + * These can not be TNodes as some atoms (such as equalities) are sent across theories withouth being stored + * in a global map. */ - context::CDList<TNode> d_facts; + context::CDList<Node> d_facts; /** Index into the head of the facts list */ context::CDO<unsigned> d_factsHead; @@ -161,7 +83,7 @@ protected: /** * Construct a Theory. */ - Theory(int id, context::Context* ctxt, OutputChannel& out) throw() : + Theory(TheoryId id, context::Context* ctxt, OutputChannel& out) throw() : d_id(id), d_context(ctxt), d_facts(ctxt), @@ -185,13 +107,6 @@ protected: */ OutputChannel* d_out; - /** - * Returns true if the assertFact queue is empty - */ - bool done() throw() { - return d_factsHead == d_facts.size(); - } - /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */ struct PreRegistered {}; /** The "preRegisterTerm()-has-been-called" flag on Nodes */ @@ -215,6 +130,48 @@ protected: public: + static inline TheoryId theoryOf(TypeNode typeNode) { + if (typeNode.getKind() == kind::TYPE_CONSTANT) { + return typeConstantToTheoryId(typeNode.getConst<TypeConstant>()); + } else { + return kindToTheoryId(typeNode.getKind()); + } + } + + /** + * Returns the theory responsible for the node. + */ + static inline TheoryId theoryOf(TNode node) { + if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) { + // Constants, variables, 0-ary constructors + return theoryOf(node.getType()); + } else { + // Regular nodes + return kindToTheoryId(node.getKind()); + } + } + + /** + * Checks if the node is a leaf node of this theory + */ + inline bool isLeaf(TNode node) const { + return node.getNumChildren() == 0 || theoryOf(node) != d_id; + } + + /** + * Checks if the node is a leaf node of a theory. + */ + inline static bool isLeafOf(TNode node, TheoryId theoryId) { + return node.getNumChildren() == 0 || theoryOf(node) != theoryId; + } + + /** + * Returns true if the assertFact queue is empty + */ + bool done() throw() { + return d_factsHead == d_facts.size(); + } + /** * Destructs a Theory. This implementation does nothing, but we * need a virtual destructor for safety in case subclasses have a @@ -250,7 +207,7 @@ public: /** * Get the id for this Theory. */ - int getId() const { + TheoryId getId() const { return d_id; } @@ -285,46 +242,7 @@ public: /** * Pre-register a term. Done one time for a Node, ever. */ - virtual void preRegisterTerm(TNode) = 0; - - /** - * Pre-rewrite a term. This default base-class implementation - * simply returns RewriteComplete(n). A theory should never - * rewrite a term to a strictly larger term that contains itself, as - * this will cause a loop of hard Node links in the cache (and thus - * memory leakage). - * - * Be careful with the return value. If a preRewrite() can return a - * sub-expression, and that sub-expression can be a member of the - * same theory and could be rewritten, make sure to return - * RewriteAgain instead of RewriteComplete. This is an easy mistake - * to make, as preRewrite() is often a short-circuiting version of - * the same rewrites that occur in postRewrite(); however, in the - * postRewrite() case, the subexpressions have all been - * post-rewritten. In the preRewrite() case, they have NOT yet been - * pre-rewritten. For example, (ITE true (ITE true x y) z) should - * pre-rewrite to x; but if the outer preRewrite() returns - * RewriteComplete, the result of the pre-rewrite will be - * (ITE true x y). - */ - virtual RewriteResponse preRewrite(TNode n, bool topLevel) { - Debug("theory-rewrite") << "no pre-rewriting to perform for " - << n << std::endl; - return RewriteComplete(n); - } - - /** - * Post-rewrite a term. This default base-class implementation - * simply returns RewriteComplete(n). A theory should never - * rewrite a term to a strictly larger term that contains itself, as - * this will cause a loop of hard Node links in the cache (and thus - * memory leakage). - */ - virtual RewriteResponse postRewrite(TNode n, bool topLevel) { - Debug("theory-rewrite") << "no post-rewriting to perform for " - << n << std::endl; - return RewriteComplete(n); - } + virtual void preRegisterTerm(TNode) { } /** * Register a term. @@ -337,14 +255,14 @@ public: * setup() MUST NOT MODIFY context-dependent objects that it hasn't * itself just created. */ - virtual void registerTerm(TNode) = 0; + virtual void registerTerm(TNode) { } /** * Assert a fact in the current context. */ - void assertFact(TNode n) { - Debug("theory") << "Theory::assertFact(" << n << ")" << std::endl; - d_facts.push_back(n); + void assertFact(TNode node) { + Debug("theory") << "Theory::assertFact(" << node << ")" << std::endl; + d_facts.push_back(node); } /** @@ -375,19 +293,19 @@ public: * - throw an exception * - or call get() until done() is true. */ - virtual void check(Effort level = FULL_EFFORT) = 0; + virtual void check(Effort level = FULL_EFFORT) { } /** * T-propagate new literal assignments in the current context. */ - virtual void propagate(Effort level = FULL_EFFORT) = 0; + virtual void propagate(Effort level = FULL_EFFORT) { } /** * Return an explanation for the literal represented by parameter n * (which was previously propagated by this theory). Report * explanations to an output channel. */ - virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0; + virtual void explain(TNode n) { } /** * Return the value of a node (typically used after a ). If the @@ -437,7 +355,7 @@ public: * assertFact() queue using get(). A Theory can raise conflicts, * add lemmas, and propagate literals during presolve(). */ - virtual void presolve() = 0; + virtual void presolve() { }; /** * Notification sent to the theory wheneven the search restarts. @@ -497,96 +415,6 @@ protected: return true; } - /** - * Check whether a node is in the pre-rewrite cache or not. - */ - static bool inPreRewriteCache(TNode n, bool topLevel) throw() { - if(topLevel) { - return n.hasAttribute(PreRewriteCacheTop()); - } else { - return n.hasAttribute(PreRewriteCache()); - } - } - - /** - * Get the value of the pre-rewrite cache (or Node::null()) if there is - * none). - */ - static Node getPreRewriteCache(TNode n, bool topLevel) throw() { - if(topLevel) { - Node out; - if(n.getAttribute(PreRewriteCacheTop(), out)) { - return out.isNull() ? Node(n) : out; - } - } else { - Node out; - if(n.getAttribute(PreRewriteCache(), out)) { - return out.isNull() ? Node(n) : out; - } - } - return Node::null(); - } - - /** - * Set the value of the pre-rewrite cache. v cannot be a null Node. - */ - static void setPreRewriteCache(TNode n, bool topLevel, TNode v) throw() { - AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()"); - AssertArgument(!v.isNull(), v, "v cannot be null in setPreRewriteCache()"); - // mappings from n -> n are actually stored as n -> null as a - // special case, to avoid cycles in the reference-counting of Nodes - if(topLevel) { - n.setAttribute(PreRewriteCacheTop(), n == v ? TNode::null() : v); - } else { - n.setAttribute(PreRewriteCache(), n == v ? TNode::null() : v); - } - } - - /** - * Check whether a node is in the post-rewrite cache or not. - */ - static bool inPostRewriteCache(TNode n, bool topLevel) throw() { - if(topLevel) { - return n.hasAttribute(PostRewriteCacheTop()); - } else { - return n.hasAttribute(PostRewriteCache()); - } - } - - /** - * Get the value of the post-rewrite cache (or Node::null()) if there is - * none). - */ - static Node getPostRewriteCache(TNode n, bool topLevel) throw() { - if(topLevel) { - Node out; - if(n.getAttribute(PostRewriteCacheTop(), out)) { - return out.isNull() ? Node(n) : out; - } - } else { - Node out; - if(n.getAttribute(PostRewriteCache(), out)) { - return out.isNull() ? Node(n) : out; - } - } - return Node::null(); - } - - /** - * Set the value of the post-rewrite cache. v cannot be a null Node. - */ - static void setPostRewriteCache(TNode n, bool topLevel, TNode v) throw() { - AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()"); - AssertArgument(!v.isNull(), v, "v cannot be null in setPostRewriteCache()"); - // mappings from n -> n are actually stored as n -> null as a - // special case, to avoid cycles in the reference-counting of Nodes - if(topLevel) { - n.setAttribute(PostRewriteCacheTop(), n == v ? TNode::null() : v); - } else { - n.setAttribute(PostRewriteCache(), n == v ? TNode::null() : v); - } - } - };/* class Theory */ std::ostream& operator<<(std::ostream& os, Theory::Effort level); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e2c42bccd..25fe29c67 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -26,14 +26,8 @@ #include "theory/theory.h" #include "theory/theory_engine.h" -#include "theory/builtin/theory_builtin.h" -#include "theory/booleans/theory_bool.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/morgan/theory_uf_morgan.h" -#include "theory/uf/tim/theory_uf_tim.h" -#include "theory/arith/theory_arith.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/bv/theory_bv.h" +#include "theory/rewriter.h" +#include "theory/theory_traits.h" using namespace std; @@ -41,6 +35,12 @@ using namespace CVC4; using namespace CVC4::theory; namespace CVC4 { + +/** Tag for the "registerTerm()-has-been-called" flag on Nodes */ +struct Registered {}; +/** The "registerTerm()-has-been-called" flag on Nodes */ +typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; + namespace theory { struct PreRegisteredTag {}; @@ -129,150 +129,101 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) : d_propEngine(NULL), + d_context(ctxt), d_theoryOut(this, ctxt), d_theoryRegistration(opts.theoryRegistration), d_hasShutDown(false), d_incomplete(ctxt, false), d_statistics() { - d_sharedTermManager = new SharedTermManager(this, ctxt); + Rewriter::init(); - d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut); - d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut); - switch(opts.uf_implementation) { - case Options::TIM: - d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut); - break; - case Options::MORGAN: - d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut); - break; - default: - Unhandled(opts.uf_implementation); - } - d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut); - d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut); - d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut); - - d_sharedTermManager->registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin)); - d_sharedTermManager->registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool)); - d_sharedTermManager->registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf)); - d_sharedTermManager->registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith)); - d_sharedTermManager->registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays)); - d_sharedTermManager->registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv)); - - d_theoryOfTable.registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin)); - d_theoryOfTable.registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool)); - d_theoryOfTable.registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf)); - d_theoryOfTable.registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith)); - d_theoryOfTable.registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays)); - d_theoryOfTable.registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv)); + d_sharedTermManager = new SharedTermManager(this, ctxt); } TheoryEngine::~TheoryEngine() { Assert(d_hasShutDown); - delete d_bv; - delete d_arrays; - delete d_arith; - delete d_uf; - delete d_bool; - delete d_builtin; - - delete d_sharedTermManager; -} - -Theory* TheoryEngine::theoryOf(TypeNode t) { - // FIXME: we don't yet have a Type-to-Theory map. When we do, - // look up the type of the var and return that Theory (?) - - // The following JUST hacks around this lack of a table - Kind k = t.getKind(); - if(k == kind::TYPE_CONSTANT) { - switch(TypeConstant tc = t.getConst<TypeConstant>()) { - case BOOLEAN_TYPE: - return d_theoryOfTable[kind::CONST_BOOLEAN]; - case INTEGER_TYPE: - return d_theoryOfTable[kind::CONST_INTEGER]; - case REAL_TYPE: - return d_theoryOfTable[kind::CONST_RATIONAL]; - case KIND_TYPE: - default: - Unhandled(tc); + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++ theoryId) { + if (d_theoryTable[theoryId]) { + delete d_theoryTable[theoryId]; } } - return d_theoryOfTable[k]; + delete d_sharedTermManager; } +struct preprocess_stack_element { + TNode node; + bool children_added; + preprocess_stack_element(TNode node) + : node(node), children_added(false) {} +}; -Theory* TheoryEngine::theoryOf(TNode n) { - Kind k = n.getKind(); +Node TheoryEngine::preprocess(TNode node) { - Assert(k >= 0 && k < kind::LAST_KIND); + // Remove ITEs and rewrite the node + Node preprocessed = Rewriter::rewrite(removeITEs(node)); - if(n.getMetaKind() == kind::metakind::VARIABLE) { - return theoryOf(n.getType()); - } else if(k == kind::EQUAL) { - // equality is special: use LHS - return theoryOf(n[0]); - } else { - // use our Kind-to-Theory mapping - return d_theoryOfTable[k]; + // If we are pre-registered already we are done + if (preprocessed.getAttribute(PreRegistered())) { + return preprocessed; } -} - -Node TheoryEngine::preprocess(TNode t) { - Node top = rewrite(t); - Debug("rewrite") << "rewrote: " << t << endl << "to : " << top << endl; - - list<TNode> toReg; - toReg.push_back(top); - - /* Essentially this is doing a breadth-first numbering of - * non-registered subterms with children. Any non-registered - * leaves are immediately registered. */ - for(list<TNode>::iterator workp = toReg.begin(); - workp != toReg.end(); - ++workp) { - - TNode n = *workp; - for(TNode::iterator i = n.begin(); i != n.end(); ++i) { - TNode c = *i; - - if(!c.getAttribute(theory::PreRegistered())) {// c not yet registered - if(c.getNumChildren() == 0) { - c.setAttribute(theory::PreRegistered(), true); - theoryOf(c)->preRegisterTerm(c); + // Do a topological sort of the subexpressions and preregister them + vector<preprocess_stack_element> toVisit; + toVisit.push_back((TNode) preprocessed); + while (!toVisit.empty()) { + preprocess_stack_element& stackHead = toVisit.back(); + // The current node we are processing + TNode current = stackHead.node; + // If we already added all the children its time to register or just pop from the stack + if (stackHead.children_added || current.getAttribute(PreRegistered())) { + if (!current.getAttribute(PreRegistered())) { + // Mark it as registered + current.setAttribute(PreRegistered(), true); + // Register this node + if (current.getKind() == kind::EQUAL) { + TheoryId theoryLHS = Theory::theoryOf(current[0]); + Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; + d_theoryTable[theoryLHS]->preRegisterTerm(current); +// TheoryId theoryRHS = Theory::theoryOf(current[1]); +// if (theoryLHS != theoryRHS) { +// d_theoryTable[theoryRHS]->preRegisterTerm(current); +// Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl; +// } +// TheoryId typeTheory = Theory::theoryOf(current[0].getType()); +// if (typeTheory != theoryLHS && typeTheory != theoryRHS) { +// d_theoryTable[typeTheory]->preRegisterTerm(current); +// Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; +// } } else { - toReg.push_back(c); + TheoryId theory = Theory::theoryOf(current); + Debug("register") << "preregistering " << current << " with " << theory << std::endl; + d_theoryTable[theory]->preRegisterTerm(current); + TheoryId typeTheory = Theory::theoryOf(current.getType()); + if (theory != typeTheory) { + Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; + d_theoryTable[typeTheory]->preRegisterTerm(current); + } + } + } + // Done with this node, remove from the stack + toVisit.pop_back(); + } else { + // Mark that we have added the children + stackHead.children_added = true; + // We need to add the children + for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { + TNode childNode = *child_it; + if (!childNode.getAttribute(PreRegistered())) { + toVisit.push_back(childNode); } } } } - /* Now register the list of terms in reverse order. Between this - * and the above registration of leaves, this should ensure that - * all subterms in the entire tree were registered in - * reverse-topological order. */ - for(list<TNode>::reverse_iterator i = toReg.rbegin(); - i != toReg.rend(); - ++i) { - - TNode n = *i; - - /* Note that a shared TNode in the DAG rooted at "fact" could - * appear twice on the list, so we have to avoid hitting it - * twice. */ - // FIXME when ExprSets are online, use one of those to avoid - // duplicates in the above? - if(!n.getAttribute(theory::PreRegistered())) { - n.setAttribute(theory::PreRegistered(), true); - theoryOf(n)->preRegisterTerm(n); - } - } - - return top; + return preprocessed; } /* Our goal is to tease out any ITE's sitting under a theory operator. */ @@ -289,9 +240,9 @@ Node TheoryEngine::removeITEs(TNode node) { if(node.getKind() == kind::ITE){ Assert( node.getNumChildren() == 3 ); - TypeNode nodeType = node[1].getType(); + TypeNode nodeType = node.getType(); if(!nodeType.isBoolean()){ - Node skolem = nodeManager->mkVar(node.getType()); + Node skolem = nodeManager->mkVar(nodeType); Node newAssertion = nodeManager->mkNode(kind::ITE, node[0], @@ -299,7 +250,7 @@ Node TheoryEngine::removeITEs(TNode node) { nodeManager->mkNode(kind::EQUAL, skolem, node[2])); nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem); - Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])" + Debug("ite") << "removeITEs([" << node.getId() << "," << node << "," << nodeType << "])" << "->" << "["<<newAssertion.getId() << "," << newAssertion << "]" << endl; @@ -330,277 +281,6 @@ Node TheoryEngine::removeITEs(TNode node) { } } -namespace theory { -namespace rewrite { - -/** - * TheoryEngine::rewrite() keeps a stack of things that are being pre- - * and post-rewritten. Each element of the stack is a - * RewriteStackElement. - */ -struct RewriteStackElement { - /** - * The node at this rewrite level. For example (AND (OR x y) z) - * will have, as it's rewriting x, the stack: - * x - * (OR x y) - * (AND (OR x y) z) - */ - Node d_node; - - /** - * The theory associated to d_node. Cached here to avoid having to - * look it up again. - */ - Theory* d_theory; - - /** - * Whether or not this was a top-level rewrite. Note that at theory - * boundaries, topLevel is forced to true, so it's not the case that - * this is true only at the lowest stack level. - */ - bool d_topLevel; - - /** - * A saved index to the "next child" to pre- and post-rewrite. In - * the case when (AND (OR x y) z) is being rewritten, the AND, OR, - * and x are pre-rewritten, then (assuming they don't change), x is - * post-rewritten, then y is pre- and post-rewritten, then the OR is - * post-rewritten, then z is pre-rewritten, then the AND is - * post-rewritten. At each stack level, we need to remember the - * child index we're currently processing. - */ - int d_nextChild; - - /** - * A (re)builder for this node. As this node's children are - * post-rewritten, in order, they append to this builder. When this - * node is post-rewritten, it is reformed from d_builder since the - * children may have changed. Note Nodes aren't rebuilt if they - * have metakinds CONSTANT (which is illegal) or VARIABLE (which - * would create a fresh variable, not what we want)---which is fine, - * since those types don't have children anyway. - */ - NodeBuilder<> d_builder; - - /** - * Construct a fresh stack element. - */ - RewriteStackElement(Node n, Theory* thy, bool topLevel) : - d_node(n), - d_theory(thy), - d_topLevel(topLevel), - d_nextChild(0) { - } -}; - -}/* CVC4::theory::rewrite namespace */ -}/* CVC4::theory namespace */ - -Node TheoryEngine::rewrite(TNode in, bool topLevel) { - using theory::rewrite::RewriteStackElement; - - Node noItes = removeITEs(in); - Node out; - - Debug("theory-rewrite") << "removeITEs of: " << in << endl - << " is: " << noItes << endl; - - // descend top-down into the theory rewriters - vector<RewriteStackElement> stack; - stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), topLevel)); - Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl - << " " << noItes << " " << theoryOf(noItes) - << " " << (topLevel ? "TOP-LEVEL " : "") - << "0" << endl; - // This whole thing is essentially recursive, but we avoid actually - // doing any recursion. - do {// do until the stack is empty.. - RewriteStackElement& rse = stack.back(); - bool done; - - Debug("theory-rewrite") << "rewriter looking at level " << stack.size() - << endl - << " " << rse.d_node << " " << rse.d_theory - << "[" << *rse.d_theory << "]" - << " " << (rse.d_topLevel ? "TOP-LEVEL " : "") - << rse.d_nextChild << endl; - - if(rse.d_nextChild == 0) { - Node original = rse.d_node; - bool wasTopLevel = rse.d_topLevel; - Node cached = getPreRewriteCache(original, wasTopLevel); - if(cached.isNull()) { - do { - Debug("theory-rewrite") << "doing pre-rewrite in " << *rse.d_theory - << " topLevel==" << rse.d_topLevel << endl; - RewriteResponse response = - rse.d_theory->preRewrite(rse.d_node, rse.d_topLevel); - rse.d_node = response.getNode(); - Assert(!rse.d_node.isNull(), "node illegally rewritten to null"); - Theory* thy2 = theoryOf(rse.d_node); - Assert(thy2 != NULL, "node illegally rewritten to null theory"); - Debug("theory-rewrite") << "got back " << rse.d_node << " " - << thy2 << "[" << *thy2 << "]" - << (response.needsMoreRewriting() ? - (response.needsFullRewriting() ? - " FULL-REWRITING" : " MORE-REWRITING") - : " DONE") - << endl; - if(rse.d_theory != thy2) { - Debug("theory-rewrite") << "pre-rewritten from " << *rse.d_theory - << " into " << *thy2 - << ", marking top-level and !done" << endl; - rse.d_theory = thy2; - done = false; - // FIXME how to handle the "top-levelness" of a node that's - // rewritten from theory T1 into T2, then back to T1 ? - rse.d_topLevel = true; - } else { - done = response.isDone(); - } - } while(!done); - setPreRewriteCache(original, wasTopLevel, rse.d_node); - } else {// is in pre-rewrite cache - Debug("theory-rewrite") << "in pre-cache: " << cached << endl; - rse.d_node = cached; - Theory* thy2 = theoryOf(cached); - if(rse.d_theory != thy2) { - Debug("theory-rewrite") << "[cache-]pre-rewritten from " - << *rse.d_theory << " into " << *thy2 - << ", marking top-level" << endl; - rse.d_theory = thy2; - rse.d_topLevel = true; - } - } - } - - // children - Node original = rse.d_node; - bool wasTopLevel = rse.d_topLevel; - Node cached = getPostRewriteCache(original, wasTopLevel); - - if(cached.isNull()) { - unsigned nch = rse.d_nextChild++; - - if(nch == 0 && - rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) { - // this is an apply, so we have to push the operator - TNode op = rse.d_node.getOperator(); - Debug("theory-rewrite") << "pushing operator " << op - << " of " << rse.d_node << endl; - rse.d_builder << op; - } - - if(nch < rse.d_node.getNumChildren()) { - Debug("theory-rewrite") << "pushing child " << nch - << " of " << rse.d_node << endl; - Node c = rse.d_node[nch]; - Theory* t = theoryOf(c); - stack.push_back(RewriteStackElement(c, t, t != rse.d_theory)); - continue;// break out of this node, do its child - } - - // incorporate the children's rewrites - if(rse.d_node.getMetaKind() != kind::metakind::VARIABLE && - rse.d_node.getMetaKind() != kind::metakind::CONSTANT) { - Debug("theory-rewrite") << "builder here is " << &rse.d_builder - << " and it gets " << rse.d_node.getKind() - << endl; - rse.d_builder << rse.d_node.getKind(); - rse.d_node = Node(rse.d_builder); - } - - // post-rewriting - do { - Debug("theory-rewrite") << "doing post-rewrite of " - << rse.d_node << endl - << " in " << *rse.d_theory - << " topLevel==" << rse.d_topLevel << endl; - RewriteResponse response = - rse.d_theory->postRewrite(rse.d_node, rse.d_topLevel); - rse.d_node = response.getNode(); - Assert(!rse.d_node.isNull(), "node illegally rewritten to null"); - Theory* thy2 = theoryOf(rse.d_node); - Assert(thy2 != NULL, "node illegally rewritten to null theory"); - Debug("theory-rewrite") << "got back " << rse.d_node << " " - << thy2 << "[" << *thy2 << "]" - << (response.needsMoreRewriting() ? - (response.needsFullRewriting() ? - " FULL-REWRITING" : " MORE-REWRITING") - : " DONE") - << endl; - if(rse.d_theory != thy2) { - Debug("theory-rewrite") << "post-rewritten from " << *rse.d_theory - << " into " << *thy2 - << ", marking top-level and !done" << endl; - rse.d_theory = thy2; - done = false; - // FIXME how to handle the "top-levelness" of a node that's - // rewritten from theory T1 into T2, then back to T1 ? - rse.d_topLevel = true; - } else { - done = response.isDone(); - } - if(response.needsFullRewriting()) { - Debug("theory-rewrite") << "full-rewrite requested for node " - << rse.d_node.getId() << ", invoking..." - << endl; - Node n = rewrite(rse.d_node, rse.d_topLevel); - Debug("theory-rewrite") << "full-rewrite finished for node " - << rse.d_node.getId() << ", got node " - << n << " output." << endl; - rse.d_node = n; - done = true; - } - } while(!done); - - /* If extra-checking is on, do _another_ rewrite before putting - * in the cache to make sure they are the same. This is - * especially necessary if a theory post-rewrites something into - * a term of another theory. */ - if(Debug.isOn("extra-checking") && - !Debug.isOn("$extra-checking:inside-rewrite")) { - ScopedDebug d("$extra-checking:inside-rewrite"); - Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel); - Assert(rewrittenAgain == rse.d_node, - "\nExtra-checking assumption failed, " - "node is not completely rewritten.\n\n" - "Original : %s\n" - "Rewritten: %s\n" - "Again : %s\n", - original.toString().c_str(), - rse.d_node.toString().c_str(), - rewrittenAgain.toString().c_str()); - } - setPostRewriteCache(original, wasTopLevel, rse.d_node); - - out = rse.d_node; - } else { - Debug("theory-rewrite") << "in post-cache: " << cached << endl; - out = cached; - Theory* thy2 = theoryOf(cached); - if(rse.d_theory != thy2) { - Debug("theory-rewrite") << "[cache-]post-rewritten from " - << *rse.d_theory << " into " << *thy2 << endl; - rse.d_theory = thy2; - } - } - - stack.pop_back(); - if(!stack.empty()) { - Debug("theory-rewrite") << "asserting " << out << " to previous builder " - << &stack.back().d_builder << endl; - stack.back().d_builder << out; - } - } while(!stack.empty()); - - Debug("theory-rewrite") << "DONE with theory rewriter." << endl; - Debug("theory-rewrite") << "result is:" << endl << out << endl; - - return out; -}/* TheoryEngine::rewrite(TNode in) */ - Node TheoryEngine::getValue(TNode node) { kind::MetaKind metakind = node.getMetaKind(); @@ -617,36 +297,16 @@ Node TheoryEngine::getValue(TNode node) { return theoryOf(node)->getValue(node, this); }/* TheoryEngine::getValue(TNode node) */ - 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(); - /* - if(!d_theoryOut.d_conflictNode.get().isNull()) { - return true; - } - d_arrays->presolve(); - if(!d_theoryOut.d_conflictNode.get().isNull()) { - return true; - } - d_bv->presolve(); - */ + for(unsigned i = 0; i < THEORY_LAST; ++ i) { + d_theoryTable[i]->presolve(); + if(!d_theoryOut.d_conflictNode.get().isNull()) { + return true; + } + } } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl; } @@ -656,26 +316,20 @@ bool TheoryEngine::presolve() { void TheoryEngine::notifyRestart() { - /* - d_builtin->notifyRestart(); - d_bool->notifyRestart(); - */ - d_uf->notifyRestart(); - /* - d_arith->notifyRestart(); - d_arrays->notifyRestart(); - d_bv->notifyRestart(); - */ + for(unsigned i = 0; i < THEORY_LAST; ++ i) { + if (d_theoryTable[i]) { + d_theoryTable[i]->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); + for(unsigned i = 0; i < THEORY_LAST; ++ i) { + if (d_theoryTable[i]) { + d_theoryTable[i]->staticLearning(in, learned); + } + } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3176b9698..bb0e9c10e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -21,11 +21,14 @@ #ifndef __CVC4__THEORY_ENGINE_H #define __CVC4__THEORY_ENGINE_H +#include <deque> + #include "expr/node.h" #include "prop/prop_engine.h" #include "theory/shared_term_manager.h" #include "theory/theory.h" -#include "theory/theoryof_table.h" +#include "theory/theory_traits.h" +#include "theory/rewriter.h" #include "util/options.h" #include "util/stats.h" @@ -45,13 +48,11 @@ class TheoryEngine { /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; - /** A table of Kinds to pointers to Theory */ - theory::TheoryOfTable d_theoryOfTable; + /** Our context */ + context::Context* d_context; - /** Tag for the "registerTerm()-has-been-called" flag on Nodes */ - struct Registered {}; - /** The "registerTerm()-has-been-called" flag on Nodes */ - typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; + /** A table of from theory ifs to theory pointers */ + theory::Theory* d_theoryTable[theory::THEORY_LAST]; /** * An output channel for Theory that passes messages @@ -124,13 +125,6 @@ class TheoryEngine { /** Pointer to Shared Term Manager */ SharedTermManager* d_sharedTermManager; - theory::Theory* d_builtin; - theory::Theory* d_bool; - theory::Theory* d_uf; - theory::Theory* d_arith; - theory::Theory* d_arrays; - theory::Theory* d_bv; - /** * Whether or not theory registration is on. May not be safe to * turn off with some theories. @@ -150,56 +144,6 @@ class TheoryEngine { context::CDO<bool> d_incomplete; /** - * Check whether a node is in the pre-rewrite cache or not. - */ - static bool inPreRewriteCache(TNode n, bool topLevel) throw() { - return theory::Theory::inPreRewriteCache(n, topLevel); - } - - /** - * Get the value of the pre-rewrite cache (or Node::null()) if there is - * none). - */ - static Node getPreRewriteCache(TNode n, bool topLevel) throw() { - return theory::Theory::getPreRewriteCache(n, topLevel); - } - - /** - * Set the value of the pre-rewrite cache. v cannot be a null Node. - */ - static void setPreRewriteCache(TNode n, bool topLevel, TNode v) throw() { - return theory::Theory::setPreRewriteCache(n, topLevel, v); - } - - /** - * Check whether a node is in the post-rewrite cache or not. - */ - static bool inPostRewriteCache(TNode n, bool topLevel) throw() { - return theory::Theory::inPostRewriteCache(n, topLevel); - } - - /** - * Get the value of the post-rewrite cache (or Node::null()) if there is - * none). - */ - static Node getPostRewriteCache(TNode n, bool topLevel) throw() { - return theory::Theory::getPostRewriteCache(n, topLevel); - } - - /** - * Set the value of the post-rewrite cache. v cannot be a null Node. - */ - static void setPostRewriteCache(TNode n, bool topLevel, TNode v) throw() { - return theory::Theory::setPostRewriteCache(n, topLevel, v); - } - - /** - * This is the top rewrite entry point, called during preprocessing. - * It dispatches to the proper theories to rewrite the given Node. - */ - Node rewrite(TNode in, bool topLevel = true); - - /** * Replace ITE forms in a node. */ Node removeITEs(TNode t); @@ -216,6 +160,16 @@ public: */ ~TheoryEngine(); + /** + * Adds a theory. Only one theory per theoryId can be present, so if there is another theory it will be deleted. + */ + template <class TheoryClass> + void addTheory() { + TheoryClass* theory = new TheoryClass(d_context, d_theoryOut); + d_theoryTable[theory->getId()] = theory; + d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory)); + } + SharedTermManager* getSharedTermManager() { return d_sharedTermManager; } @@ -243,20 +197,25 @@ public: // matters. d_hasShutDown = true; - d_builtin->shutdown(); - d_bool->shutdown(); - d_uf->shutdown(); - d_arith->shutdown(); - d_arrays->shutdown(); - d_bv->shutdown(); + // Shutdown all the theories + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++ theoryId) { + if (d_theoryTable[theoryId]) { + d_theoryTable[theoryId]->shutdown(); + } + } + + theory::Rewriter::shutdown(); } /** - * Get the theory associated to a given TypeNode. + * Get the theory associated to a given Node. * - * @returns the theory owning the type + * @returns the theory, or NULL if the TNode is + * of built-in type. */ - theory::Theory* theoryOf(TypeNode t); + inline theory::Theory* theoryOf(TNode node) { + return d_theoryTable[theory::Theory::theoryOf(node)]; + } /** * Get the theory associated to a given Node. @@ -264,7 +223,9 @@ public: * @returns the theory, or NULL if the TNode is * of built-in type. */ - theory::Theory* theoryOf(TNode n); + inline theory::Theory* theoryOf(const TypeNode& typeNode) { + return d_theoryTable[theory::Theory::theoryOf(typeNode)]; + } /** * Preprocess a node. This involves theory-specific rewriting, then @@ -274,14 +235,33 @@ public: Node preprocess(TNode n); /** - * Assert the formula to the apropriate theory. + * Assert the formula to the appropriate theory. * @param node the assertion */ inline void assertFact(TNode node) { Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; - theory::Theory* theory = - node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node); - if(theory != NULL) { + + // Get the atom + TNode atom = node.getKind() == kind::NOT ? node[0] : node; + + // Again, eqaulity is a special case + if (atom.getKind() == kind::EQUAL) { + theory::TheoryId theoryLHS = theory::Theory::theoryOf(atom[0]); + Debug("theory") << "asserting " << node << " to " << theoryLHS << std::endl; + d_theoryTable[theoryLHS]->assertFact(node); +// theory::TheoryId theoryRHS = theory::Theory::theoryOf(atom[1]); +// if (theoryLHS != theoryRHS) { +// Debug("theory") << "asserting " << node << " to " << theoryRHS << std::endl; +// d_theoryTable[theoryRHS]->assertFact(node); +// } +// theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType()); +// if (typeTheory!= theoryLHS && typeTheory != theoryRHS) { +// Debug("theory") << "asserting " << node << " to " << typeTheory << std::endl; +// d_theoryTable[typeTheory]->assertFact(node); +// } + } else { + theory::Theory* theory = theoryOf(atom); + Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl; theory->assertFact(node); } } @@ -294,19 +274,26 @@ public: { d_theoryOut.d_conflictNode = Node::null(); d_theoryOut.d_propagatedLiterals.clear(); + +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasCheck) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \ + if (!d_theoryOut.d_conflictNode.get().isNull()) { \ + return false; \ + } \ + } + // Do the checking try { - //d_builtin->check(effort); - //d_bool->check(effort); - d_uf->check(effort); - d_arith->check(effort); - d_arrays->check(effort); - d_bv->check(effort); + CVC4_FOR_EACH_THEORY } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; } - // Return whether we have a conflict - return d_theoryOut.d_conflictNode.get().isNull(); + + return true; } /** @@ -346,14 +333,18 @@ public: } inline void propagate() { - d_theoryOut.d_propagatedLiterals.clear(); - // Do the propagation - //d_builtin->propagate(theory::Theory::FULL_EFFORT); - //d_bool->propagate(theory::Theory::FULL_EFFORT); - d_uf->propagate(theory::Theory::FULL_EFFORT); - d_arith->propagate(theory::Theory::FULL_EFFORT); - d_arrays->propagate(theory::Theory::FULL_EFFORT); - //d_bv->propagate(theory::Theory::FULL_EFFORT); + + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPropagate) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ + } + + // Propagate for each theory using the statement above + CVC4_FOR_EACH_THEORY } inline Node getExplanation(TNode node, theory::Theory* theory) { @@ -363,9 +354,13 @@ public: inline Node getExplanation(TNode node) { d_theoryOut.d_explanationNode = Node::null(); - theory::Theory* theory = - node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node); - theory->explain(node); + TNode atom = node.getKind() == kind::NOT ? node[0] : node; + if (atom.getKind() == kind::EQUAL) { + theoryOf(atom[0])->explain(node); + } else { + theoryOf(atom)->explain(node); + } + Assert(!d_theoryOut.d_explanationNode.get().isNull()); return d_theoryOut.d_explanationNode; } diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h new file mode 100644 index 000000000..067fe55d0 --- /dev/null +++ b/src/theory/theory_traits_template.h @@ -0,0 +1,26 @@ +/* + * theory_traits_template.h + * + * Created on: Dec 23, 2010 + * Author: dejan + */ + +#pragma once + +#include "theory/theory.h" + +${theory_includes} + +namespace CVC4 { + +namespace theory { + +template <TheoryId theoryId> +struct TheoryTraits; + +${theory_traits} + +${theory_for_each_macro} + +}/* theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/theoryof_table_template.h b/src/theory/theoryof_table_template.h deleted file mode 100644 index 5da28f2d4..000000000 --- a/src/theory/theoryof_table_template.h +++ /dev/null @@ -1,66 +0,0 @@ -/********************* */ -/*! \file theoryof_table_template.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 The template for the automatically-generated theoryOf table. - ** - ** The template for the automatically-generated theoryOf table. - ** See the mktheoryof script. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__THEORYOF_TABLE_H -#define __CVC4__THEORY__THEORYOF_TABLE_H - -#include "expr/kind.h" -#include "util/Assert.h" - -${theoryof_table_forwards} - -namespace CVC4 { -namespace theory { - -class Theory; - -class TheoryOfTable { - - Theory** d_table; - -public: - - TheoryOfTable() : - d_table(new Theory*[::CVC4::kind::LAST_KIND]) { - } - - ~TheoryOfTable() { - delete [] d_table; - } - - Theory* operator[](TNode n) { - Assert(n.getKind() >= 0 && n.getKind() < ::CVC4::kind::LAST_KIND, - "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)"); - return d_table[n.getKind()]; - } - - Theory* operator[](::CVC4::Kind k) { - Assert(k >= 0 && k < ::CVC4::kind::LAST_KIND, - "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)"); - return d_table[k]; - } -${theoryof_table_registers} -};/* class TheoryOfTable */ - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__THEORYOF_TABLE_H */ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 04fe533ae..e4647b442 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -11,7 +11,8 @@ nodist_EXTRA_libuf_la_SOURCES = \ libuf_la_SOURCES = \ theory_uf.h \ - theory_uf_type_rules.h + theory_uf_type_rules.h \ + theory_uf_rewriter.h libuf_la_LIBADD = \ @builddir@/tim/libuftim.la \ diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 8cd6aec70..a1fcac1df 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -4,9 +4,17 @@ # src/theory/builtin/kinds. # -theory ::CVC4::theory::uf::TheoryUF "theory_uf.h" +theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" + +properties stable-infinite check propagate staticLearning presolve + +rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" + +sort KIND_TYPE "Uninterpreted Sort" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" variable SORT_TAG "sort tag" parameterized SORT_TYPE SORT_TAG 0: "sort type" + +endtheory
\ No newline at end of file diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index cd9ee79c3..33c8bc7b6 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -31,8 +31,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; using namespace CVC4::theory::uf::morgan; -TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) : - TheoryUF(id, ctxt, out), +TheoryUFMorgan::TheoryUFMorgan(Context* ctxt, OutputChannel& out) : + TheoryUF(ctxt, out), d_assertions(ctxt), d_ccChannel(this), d_cc(ctxt, &d_ccChannel), @@ -70,23 +70,6 @@ TheoryUFMorgan::~TheoryUFMorgan() { StatisticsRegistry::unregisterStat(&d_ccNewSkolemVars); } -RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) { - if(topLevel) { - Debug("uf") << "uf: begin rewrite(" << n << ")" << endl; - Node ret(n); - if(n.getKind() == kind::EQUAL || - n.getKind() == kind::IFF) { - if(n[0] == n[1]) { - ret = NodeManager::currentNM()->mkConst(true); - } - } - Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << endl; - return RewriteComplete(ret); - } else { - return RewriteComplete(n); - } -} - void TheoryUFMorgan::preRegisterTerm(TNode n) { Debug("uf") << "uf: preRegisterTerm(" << n << ")" << endl; if(n.getKind() == kind::EQUAL || n.getKind() == kind::IFF) { @@ -258,63 +241,63 @@ void TheoryUFMorgan::merge(TNode a, TNode b) { // 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; - } +// 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) { @@ -564,12 +547,12 @@ void TheoryUFMorgan::propagate(Effort level) { Debug("uf") << "uf: end propagate(" << level << ")" << endl; } -void TheoryUFMorgan::explain(TNode n, Effort level) { +void TheoryUFMorgan::explain(TNode n) { TimerStat::CodeTimer codeTimer(d_explainTimer); - Debug("uf") << "uf: begin explain([" << n << "], " << level << ")" << endl; + Debug("uf") << "uf: begin explain([" << n << "])" << endl; Unimplemented(); - Debug("uf") << "uf: end explain([" << n << "], " << level << ")" << endl; + Debug("uf") << "uf: end explain([" << n << "])" << endl; } void TheoryUFMorgan::presolve() { diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index cbc5f1eab..2a079603b 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -132,7 +132,7 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFMorgan(int id, context::Context* ctxt, OutputChannel& out); + TheoryUFMorgan(context::Context* ctxt, OutputChannel& out); /** Destructor for UF theory, cleans up memory and statistics. */ ~TheoryUFMorgan(); @@ -170,13 +170,6 @@ public: void check(Effort level); /** - * Rewrites a node in the theory of uninterpreted functions. - * This is fairly basic and only ensures that atoms that are - * unsatisfiable or a valid are rewritten to false or true respectively. - */ - RewriteResponse postRewrite(TNode n, bool topLevel); - - /** * Propagates theory literals. * * Overloads void propagate(Effort level); from theory.h. @@ -190,7 +183,7 @@ public: * Overloads void explain(TNode n, Effort level); from theory.h. * See theory/theory.h for more information about this method. */ - void explain(TNode n, Effort level); + void explain(TNode n); /** * The theory should only add (via .operator<< or .append()) to the diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index f745cf402..be3d7ac69 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -37,8 +37,8 @@ class TheoryUF : public Theory { public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(int id, context::Context* ctxt, OutputChannel& out) - : Theory(id, ctxt, out) {} + TheoryUF(context::Context* ctxt, OutputChannel& out) + : Theory(THEORY_UF, ctxt, out) {} };/* class TheoryUF */ diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h new file mode 100644 index 000000000..e71f74fea --- /dev/null +++ b/src/theory/uf/theory_uf_rewriter.h @@ -0,0 +1,49 @@ +/* + * theory_uf_rewriter.h + * + * Created on: Dec 21, 2010 + * Author: dejan + */ + +#pragma once + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +class TheoryUfRewriter { + +public: + + static RewriteResponse postRewrite(TNode node) { + if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { + if(node[0] == node[1]) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + if (node[0] > node[1]) { + Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]); + // If we've switched theories, we need to rewrite again (TODO: THIS IS HACK, once theories accept eq, change) + if (Theory::theoryOf(newNode[0]) != Theory::theoryOf(newNode[1])) { + return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + } else { + return RewriteResponse(REWRITE_DONE, newNode); + } + } + } + return RewriteResponse(REWRITE_DONE, node); + } + + static RewriteResponse preRewrite(TNode node) { + return RewriteResponse(REWRITE_DONE, node); + } + + static inline void init() {} + static inline void shutdown() {} + +}; + +} +} +} diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp index ccc37a24b..db0574d4f 100644 --- a/src/theory/uf/tim/theory_uf_tim.cpp +++ b/src/theory/uf/tim/theory_uf_tim.cpp @@ -27,8 +27,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; using namespace CVC4::theory::uf::tim; -TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) : - TheoryUF(id, c, out), +TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out) : + TheoryUF(c, out), d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), @@ -39,18 +39,6 @@ TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) : TheoryUFTim::~TheoryUFTim() { } -Node TheoryUFTim::rewrite(TNode n){ - Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl; - Node ret(n); - if(n.getKind() == EQUAL){ - Assert(n.getNumChildren() == 2); - if(n[0] == n[1]) { - ret = NodeManager::currentNM()->mkConst(true); - } - } - Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl; - return ret; -} void TheoryUFTim::preRegisterTerm(TNode n) { Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h index 73033f387..cdaa7975c 100644 --- a/src/theory/uf/tim/theory_uf_tim.h +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -86,7 +86,7 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFTim(int id, context::Context* c, OutputChannel& out); + TheoryUFTim(context::Context* c, OutputChannel& out); /** Destructor for the TheoryUF object. */ ~TheoryUFTim(); @@ -130,20 +130,6 @@ public: } /** - * Rewrites a node in the theory of uninterpreted functions. - * This is fairly basic and only ensures that atoms that are - * unsatisfiable or a valid are rewritten to false or true respectively. - */ - Node rewrite(TNode n); - - /** - * Plug in old rewrite to the new (pre,post)rewrite interface. - */ - RewriteResponse postRewrite(TNode n, bool topLevel) { - return RewriteComplete(topLevel ? rewrite(n) : Node(n)); - } - - /** * Propagates theory literals. Currently does nothing. * * Overloads void propagate(Effort level); from theory.h. @@ -157,7 +143,7 @@ public: * Overloads void explain(TNode n, Effort level); from theory.h. * See theory/theory.h for more information about this method. */ - void explain(TNode n, Effort level) {} + void explain(TNode n) {} /** * Get a theory value. |