diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-12 20:20:24 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-12 20:20:24 +0000 |
commit | 2bc4c351bbf89103577fa9f33ebb395f5d61826a (patch) | |
tree | 37345ddbee75fc7405868afd3de8b7c2ffdd0fdc /src/theory | |
parent | ec320b78deaaf31bdae1b8b048f66cfb1b3a4197 (diff) |
Merge from cc-memout branch. Here are the main points
* Add ContextMemoryAllocator<T> allocator type, conforming to
STL allocator requirements.
* Extend the CDList<> template to take an allocator (defaults
to std::allocator<T>).
* Add a specialized version of the CDList<> template (in
src/context/cdlist_context_memory.h) that allocates a list
in segments, in context memory.
* Add "forward" headers -- cdlist_forward.h, cdmap_forward.h,
and cdset_forward.h. Use these in public headers, and other
places where you don't need the full header (just the
forward-declaration). These types justify their own header
(instead of just forward-declaring yourself), because they
are complex templated types, with default template parameters,
specializations, etc.
* theory_engine.h no longer depends on individual theory headers.
(Instead it forward-declares Theory implementations.) This is
especially important now that theory .cpp files depend on
TheoryEngine (to implement Theory::getValue()). Previously,
any modification to any theory header file required *all*
theories, and the engine, to be completely rebuilt.
* Support memory cleanup for nontrivial CONSTANT kinds. This
resolves an issue with arithmetic where memory leaked for
each distinct Rational or Integer that was wrapped in a Node.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_constants.h | 16 | ||||
-rwxr-xr-x | src/theory/mktheoryof | 24 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 39 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 26 | ||||
-rw-r--r-- | src/theory/theoryof_table_template.h | 2 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 24 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 23 |
7 files changed, 85 insertions, 69 deletions
diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h index 27abd8873..98a202207 100644 --- a/src/theory/arith/arith_constants.h +++ b/src/theory/arith/arith_constants.h @@ -31,7 +31,7 @@ namespace CVC4 { namespace theory { namespace arith { -class ArithConstants{ +class ArithConstants { public: Rational d_ZERO; Rational d_ONE; @@ -52,10 +52,16 @@ public: d_ONE_NODE(nm->mkConst(d_ONE)), d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE)) {} -}; -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ + ~ArithConstants() { + d_ZERO_NODE = Node::null(); + d_ONE_NODE = Node::null(); + d_NEGATIVE_ONE_NODE = Node::null(); + } +};/* class ArithConstants */ + +}/* namespace CVC4::theory::arith */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ #endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */ diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof index 4b7dfcef5..415668b49 100755 --- a/src/theory/mktheoryof +++ b/src/theory/mktheoryof @@ -33,7 +33,7 @@ EOF template=$1; shift -theoryof_table_includes= +theoryof_table_forwards= theoryof_table_registers= seen_theory=false @@ -61,7 +61,23 @@ function theory { echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 fi - theoryof_table_includes="${theoryof_table_includes}#include \"theory/$b/$2\" + 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 */ @@ -103,7 +119,7 @@ function constant { function do_theoryof { check_theory_seen - theoryof_table_registers="${theoryof_table_registers} d_table[::CVC4::kind::$1] = th; + theoryof_table_registers="${theoryof_table_registers} d_table[::CVC4::kind::$1] = (Theory*)th; " } @@ -135,7 +151,7 @@ check_builtin_theory_seen ## output text=$(cat "$template") -for var in theoryof_table_includes theoryof_table_registers; do +for var in theoryof_table_forwards theoryof_table_registers; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 384e2fdd6..29aed8426 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -16,6 +16,9 @@ ** The theory engine. **/ +#include <vector> +#include <list> + #include "theory/theory_engine.h" #include "expr/node.h" #include "expr/attribute.h" @@ -23,8 +26,14 @@ #include "expr/node_builder.h" #include "smt/options.h" -#include <vector> -#include <list> +#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; @@ -141,19 +150,19 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) : d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut); d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut); - d_sharedTermManager->registerTheory(d_builtin); - d_sharedTermManager->registerTheory(d_bool); - d_sharedTermManager->registerTheory(d_uf); - d_sharedTermManager->registerTheory(d_arith); - d_sharedTermManager->registerTheory(d_arrays); - d_sharedTermManager->registerTheory(d_bv); - - d_theoryOfTable.registerTheory(d_builtin); - d_theoryOfTable.registerTheory(d_bool); - d_theoryOfTable.registerTheory(d_uf); - d_theoryOfTable.registerTheory(d_arith); - d_theoryOfTable.registerTheory(d_arrays); - d_theoryOfTable.registerTheory(d_bv); + 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)); } TheoryEngine::~TheoryEngine() { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2d056af28..85e6d2cfc 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -24,18 +24,8 @@ #include "expr/node.h" #include "theory/theory.h" #include "theory/theoryof_table.h" - #include "prop/prop_engine.h" #include "theory/shared_term_manager.h" -#include "theory/builtin/theory_builtin.h" -#include "theory/booleans/theory_bool.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/tim/theory_uf_tim.h" -#include "theory/uf/morgan/theory_uf_morgan.h" -#include "theory/arith/theory_arith.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/bv/theory_bv.h" - #include "util/stats.h" namespace CVC4 { @@ -119,21 +109,19 @@ class TheoryEngine { d_explanationNode = explanationNode; ++(d_engine->d_statistics.d_statExplanation); } - }; - - + };/* class EngineOutputChannel */ EngineOutputChannel d_theoryOut; /** Pointer to Shared Term Manager */ SharedTermManager* d_sharedTermManager; - theory::builtin::TheoryBuiltin* d_builtin; - theory::booleans::TheoryBool* d_bool; - theory::uf::TheoryUF* d_uf; - theory::arith::TheoryArith* d_arith; - theory::arrays::TheoryArrays* d_arrays; - theory::bv::TheoryBV* d_bv; + theory::Theory* d_builtin; + theory::Theory* d_bool; + theory::Theory* d_uf; + theory::Theory* d_arith; + theory::Theory* d_arrays; + theory::Theory* d_bv; /** * Debugging flag to ensure that shutdown() is called before the diff --git a/src/theory/theoryof_table_template.h b/src/theory/theoryof_table_template.h index e0d6fc8c8..5da28f2d4 100644 --- a/src/theory/theoryof_table_template.h +++ b/src/theory/theoryof_table_template.h @@ -25,7 +25,7 @@ #include "expr/kind.h" #include "util/Assert.h" -${theoryof_table_includes} +${theoryof_table_forwards} namespace CVC4 { namespace theory { diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index fe1f3106e..4ee698721 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -34,12 +34,10 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) : d_cc(ctxt, &d_ccChannel), d_unionFind(ctxt), d_disequalities(ctxt), - d_disequality(ctxt), d_conflict(), d_trueNode(), d_falseNode(), - d_trueEqFalseNode(), - d_activeAssertions(ctxt) { + d_trueEqFalseNode() { NodeManager* nm = NodeManager::currentNM(); TypeNode boolType = nm->booleanType(); d_trueNode = nm->mkVar("TRUE_UF", boolType); @@ -51,6 +49,9 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) : } TheoryUFMorgan::~TheoryUFMorgan() { + d_trueNode = Node::null(); + d_falseNode = Node::null(); + d_trueEqFalseNode = Node::null(); } RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) { @@ -189,11 +190,6 @@ void TheoryUFMorgan::merge(TNode a, TNode b) { d_unionFind[a] = b; - if(Debug.isOn("uf") && find(d_trueNode) == find(d_falseNode)) { - Debug("uf") << "ok, pay attention now.." << std::endl; - dump(); - } - DiseqLists::iterator deq_i = d_disequalities.find(a); if(deq_i != d_disequalities.end()) { // a set of other trees we are already disequal to @@ -268,7 +264,8 @@ void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) { DiseqLists::iterator deq_i = d_disequalities.find(of); DiseqList* deq; if(deq_i == d_disequalities.end()) { - deq = new(getContext()->getCMM()) DiseqList(true, getContext()); + deq = new(getContext()->getCMM()) DiseqList(true, getContext(), false, + ContextMemoryAllocator<TNode>(getContext()->getCMM())); d_disequalities.insertDataFromContextMemory(of, deq); } else { deq = (*deq_i).second; @@ -298,7 +295,7 @@ void TheoryUFMorgan::check(Effort level) { Node assertion = get(); - d_activeAssertions.push_back(assertion); + //d_activeAssertions.push_back(assertion); Debug("uf") << "uf check(): " << assertion << std::endl; @@ -349,7 +346,6 @@ void TheoryUFMorgan::check(Effort level) { Node b = assertion[0][1]; addDisequality(assertion[0]); - d_disequality.push_back(assertion[0]); d_cc.addTerm(a); d_cc.addTerm(b); @@ -418,14 +414,17 @@ void TheoryUFMorgan::check(Effort level) { Unhandled(assertion.getKind()); } + /* if(Debug.isOn("uf")) { dump(); } + */ } Assert(d_conflict.isNull()); Debug("uf") << "uf check() done = " << (done() ? "true" : "false") << std::endl; + /* for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); diseqIter != d_disequality.end(); ++diseqIter) { @@ -443,6 +442,7 @@ void TheoryUFMorgan::check(Effort level) { Assert((debugFind(left) == debugFind(right)) == d_cc.areCongruent(left, right)); } + */ Debug("uf") << "uf: end check(" << level << ")" << std::endl; } @@ -477,6 +477,7 @@ Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) { } } +/* void TheoryUFMorgan::dump() { if(!Debug.isOn("uf")) { return; @@ -509,3 +510,4 @@ void TheoryUFMorgan::dump() { } Debug("uf") << "=======================================" << std::endl; } +*/ diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index 7a12f216b..023e100a9 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -11,16 +11,13 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. - ** - ** This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. It is based on the Nelson-Oppen algorithm given in - ** "Fast Decision Procedures Based on Congruence Closure" - ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf) - ** This has been extended to work in a context-dependent way. - ** This interacts heavily with the data-structures given in ecdata.h . + ** \brief Implementation of the theory of uninterpreted functions with + ** equality ** + ** Implementation of the theory of uninterpreted functions with equality, + ** based on CVC4's congruence closure module (which is in turn based on + ** the Nieuwenhuis and Oliveras paper, Fast Congruence Closure and + ** Extensions. **/ #include "cvc4_private.h" @@ -35,7 +32,7 @@ #include "theory/uf/theory_uf.h" #include "context/context.h" -#include "context/cdo.h" +#include "context/context_mm.h" #include "context/cdlist.h" #include "util/congruence_closure.h" @@ -81,19 +78,17 @@ private: typedef context::CDMap<TNode, TNode, TNodeHashFunction> UnionFind; UnionFind d_unionFind; - typedef context::CDList<Node> DiseqList; + typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > DiseqList; typedef context::CDMap<Node, DiseqList*, NodeHashFunction> DiseqLists; /** List of all disequalities this theory has seen. */ DiseqLists d_disequalities; - context::CDList<Node> d_disequality; - Node d_conflict; Node d_trueNode, d_falseNode, d_trueEqFalseNode; - context::CDList<Node> d_activeAssertions; + //context::CDList<Node> d_activeAssertions; public: |