diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
| commit | f9a4fe48a4ec2355f8fec93d3f47242577df2511 (patch) | |
| tree | eb49b7760b16aa17666d59464c96979b445fbcc8 /src | |
| parent | eecc1e4f301711dbb2bf1508ea0ba6cd20acd593 (diff) | |
Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
Diffstat (limited to 'src')
61 files changed, 1970 insertions, 1601 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index d2b9197cb..12e7f2ff0 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -10,7 +10,6 @@ libexpr_la_SOURCES = \ node.cpp \ type_node.h \ type_node.cpp \ - type_constant.h \ node_builder.h \ convenience_node_builders.h \ type.h \ diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 3b1232772..932ec31c8 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -24,6 +24,8 @@ #include <iostream> #include <sstream> +#include "util/Assert.h" + namespace CVC4 { namespace kind { @@ -88,6 +90,70 @@ struct KindHashStrategy { };/* struct KindHashStrategy */ }/* CVC4::kind namespace */ + +/** + * The enumeration for the built-in atomic types. + */ +enum TypeConstant { + ${type_constant_list} + LAST_TYPE +};/* enum TypeConstant */ + +/** + * We hash the constants with their values. + */ +struct TypeConstantHashStrategy { + static inline size_t hash(TypeConstant tc) { + return tc; + } +};/* struct BoolHashStrategy */ + +inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { + switch(typeConstant) { + ${type_constant_descriptions} + default: + out << "UNKNOWN_TYPE_CONSTANT"; + break; + } + return out; +} + +namespace theory { + +enum TheoryId { + ${theory_enum} + THEORY_LAST +}; + +inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { + switch(theoryId) { + ${theory_descriptions} + default: + out << "UNKNOWN_THEORY"; + break; + } + return out; +} + +inline TheoryId kindToTheoryId(::CVC4::Kind k) { + switch (k) { + ${kind_to_theory_id} + default: + Unreachable(); + } +} + +inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) { + switch (typeConstant) { + ${type_constant_to_theory_id} + default: + Unreachable(); + } +} + +}/* theory namespace */ + + }/* CVC4 namespace */ #endif /* __CVC4__KIND_H */ diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 35a245a84..0b384d518 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -72,22 +72,42 @@ function theory { # 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 [ "$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" ]; then + 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 "$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 + 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 } +function rewriter { + # rewriter class header + lineno=${BASH_LINENO[0]} +} + +function properties { + # properties prop* + lineno=${BASH_LINENO[0]} +} + +function endtheory { + # endtheory + lineno=${BASH_LINENO[0]} +} + +function sort { + # sort TYPE ["comment"] + lineno=${BASH_LINENO[0]} +} + function variable { # variable K ["comment"] diff --git a/src/expr/mkkind b/src/expr/mkkind index ab80224eb..d790a0195 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -37,10 +37,18 @@ template=$1; shift kind_decls= kind_printers= +kind_to_theory_id= + +type_constant_descriptions= +type_constant_list= +type_constant_to_theory_id= seen_theory=false seen_theory_builtin=false +theory_enum= +theory_descriptions= + function theory { # theory T header @@ -49,20 +57,50 @@ function theory { # 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 [ "$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" ]; then + 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 "$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 + 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_enum="$1, + ${theory_enum}" + theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; +" +} + +function properties { + # rewriter class header + lineno=${BASH_LINENO[0]} +} + +function endtheory { + # endtheory + lineno=${BASH_LINENO[0]} +} + +function rewriter { + # properties prop* + lineno=${BASH_LINENO[0]} +} + +function sort { + # sort TYPE ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_sort "$1" "$2" } function variable { @@ -101,6 +139,18 @@ function constant { register_kind "$1" 0 "$5" } +function register_sort { + id=$1 + comment=$2 + + type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ +" + type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break; +" + type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; +" +} + function register_kind { r=$1 nc=$2 @@ -110,6 +160,8 @@ function register_kind { " kind_printers="${kind_printers} case $r: out << \"$r\"; break; " + kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; +" } function check_theory_seen { @@ -144,7 +196,7 @@ check_builtin_theory_seen ## output text=$(cat "$template") -for var in kind_decls kind_printers; do +for var in kind_decls kind_printers kind_to_theory_id theory_enum type_constant_list type_constant_descriptions type_constant_to_theory_id theory_descriptions; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 4ce0c6262..0d0ff4475 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -60,18 +60,18 @@ function theory { # 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 [ "$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" ]; then + 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 "$1" : '\(::*\)' >/dev/null; then + elif ! expr "$2" : '\(::*\)' >/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 + elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 fi @@ -80,6 +80,26 @@ function theory { // #include \"theory/$b/$2\"" } +function properties { + # properties prop* + lineno=${BASH_LINENO[0]} +} + +function endtheory { + # endtheory + lineno=${BASH_LINENO[0]} +} + +function rewriter { + # rewriter class header + lineno=${BASH_LINENO[0]} +} + +function sort { + # sort TYPE ["comment"] + lineno=${BASH_LINENO[0]} +} + function variable { # variable K ["comment"] diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 04de81b1c..117497539 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -974,6 +974,7 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { Node n = mkVar(type); + n.setAttribute(TypeAttr(), type); n.setAttribute(expr::VarNameAttr(), name); return n; } @@ -981,6 +982,7 @@ inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) { Node* n = mkVarPtr(type); + n->setAttribute(TypeAttr(), type); n->setAttribute(expr::VarNameAttr(), name); return n; } diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h deleted file mode 100644 index 23c23cc9f..000000000 --- a/src/expr/type_constant.h +++ /dev/null @@ -1,76 +0,0 @@ -/********************* */ -/*! \file type_constant.h - ** \verbatim - ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** 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 Interface for expression types. - ** - ** Interface for expression types - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__TYPE_CONSTANT_H -#define __CVC4__TYPE_CONSTANT_H - -#include <iostream> - -namespace CVC4 { - -/** - * The enumeration for the built-in atomic types. - */ -enum TypeConstant { - /** The Boolean type */ - BOOLEAN_TYPE, - /** The integer type */ - INTEGER_TYPE, - /** The real type */ - REAL_TYPE, - /** The kind type (type of types) */ - KIND_TYPE, - /** The builtin operator type (type of non-PARAMETERIZED operators) */ - BUILTIN_OPERATOR_TYPE -};/* enum TypeConstant */ - -/** - * We hash the constants with their values. - */ -struct TypeConstantHashStrategy { - static inline size_t hash(TypeConstant tc) { - return tc; - } -};/* struct BoolHashStrategy */ - -inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { - switch(typeConstant) { - case BOOLEAN_TYPE: - out << "BOOLEAN"; - break; - case INTEGER_TYPE: - out << "INTEGER"; - break; - case REAL_TYPE: - out << "REAL"; - break; - case KIND_TYPE: - out << "KIND"; - break; - default: - out << "UNKNOWN_TYPE_CONSTANT"; - break; - } - return out; -} - -}/* CVC4 namespace */ - -#endif /* __CVC4__TYPE_CONSTANT_H */ diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index da6638ea8..bfac4f300 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -38,6 +38,7 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL logicMap["QF_SAT"] = QF_SAT; logicMap["QF_UF"] = QF_UF; logicMap["QF_UFIDL"] = QF_UFIDL; + logicMap["QF_UFLRA"] = QF_UFLRA; return logicMap; } diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index b78f20ee8..1db7bf446 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -63,9 +63,9 @@ void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) { void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); - Debug("prop-explain") << "explainPropagation(" << lNode.toString() << ")" << std::endl; + Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; Node theoryExplanation = d_theoryEngine->getExplanation(lNode); - Debug("prop-explain") << "explainPropagation() => " << theoryExplanation.toString() << std::endl; + Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; if (theoryExplanation.getKind() == kind::AND) { Node::const_iterator it = theoryExplanation.begin(); Node::const_iterator it_end = theoryExplanation.end(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6bfdda079..273b2322a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -36,6 +36,15 @@ #include "util/exception.h" #include "util/options.h" #include "util/output.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" + using namespace std; using namespace CVC4; @@ -133,6 +142,24 @@ void SmtEngine::init(const Options& opts) throw() { // We have mutual dependancy here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine = new TheoryEngine(d_context, opts); + + // Add the theories + d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(); + d_theoryEngine->addTheory<theory::booleans::TheoryBool>(); + d_theoryEngine->addTheory<theory::arith::TheoryArith>(); + d_theoryEngine->addTheory<theory::arrays::TheoryArrays>(); + d_theoryEngine->addTheory<theory::bv::TheoryBV>(); + switch(opts.uf_implementation) { + case Options::TIM: + d_theoryEngine->addTheory<theory::uf::tim::TheoryUFTim>(); + break; + case Options::MORGAN: + d_theoryEngine->addTheory<theory::uf::morgan::TheoryUFMorgan>(); + break; + default: + Unhandled(opts.uf_implementation); + } + d_propEngine = new PropEngine(d_theoryEngine, d_context, opts); d_theoryEngine->setPropEngine(d_propEngine); 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. |