diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
commit | c94347913fa464b1ec6a3da2ab21e319c0c42e02 (patch) | |
tree | 6c8252385365e5dacc86ce8c364c3d06332d39a7 /src/theory | |
parent | 7adcbaf2eac82be6ca8cf1569bab80c961710950 (diff) |
Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 4 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 4 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 4 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-rw-r--r-- | src/theory/example/theory_uf_tim.cpp | 4 | ||||
-rw-r--r-- | src/theory/example/theory_uf_tim.h | 4 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 20 | ||||
-rw-r--r-- | src/theory/substitutions.h | 49 | ||||
-rw-r--r-- | src/theory/theory.h | 26 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 26 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 10 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 14 |
17 files changed, 106 insertions, 78 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index be8feb245..c69960d37 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -59,8 +59,8 @@ static const uint32_t RESET_START = 2; struct SlackAttrID; typedef expr::Attribute<SlackAttrID, bool> Slack; -TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) : - Theory(THEORY_ARITH, c, out, valuation), +TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : + Theory(THEORY_ARITH, c, u, out, valuation), learner(d_pbSubstitutions), d_nextIntegerCheckVar(0), d_partialModel(c), @@ -68,6 +68,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valu d_diseq(c), d_tableau(), d_diosolver(c, d_tableau, d_partialModel), + d_pbSubstitutions(u), d_restartsCounter(0), d_rowHasBeenAdded(false), d_tableauResetDensity(1.6), diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 6bcf6a613..4731bea30 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -163,7 +163,7 @@ private: SimplexDecisionProcedure d_simplex; public: - TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation); + TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); virtual ~TheoryArith(); /** diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 0aff30d74..f82b6c670 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -32,8 +32,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::arrays; -TheoryArrays::TheoryArrays(Context* c, OutputChannel& out, Valuation valuation) : - Theory(THEORY_ARRAY, c, out, valuation), +TheoryArrays::TheoryArrays(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) : + Theory(THEORY_ARRAY, c, u, out, valuation), d_ccChannel(this), d_cc(c, &d_ccChannel), d_unionFind(c), diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index a984cb342..7fa215bfc 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -364,7 +364,7 @@ private: Node recursivePreprocessTerm(TNode term); public: - TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation); + TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); ~TheoryArrays(); /** diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index d53337fa7..bd4c8d565 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(context::Context* c, OutputChannel& out, Valuation valuation) : - Theory(THEORY_BOOL, c, out, valuation) { + TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : + Theory(THEORY_BOOL, c, u, out, valuation) { } Node getValue(TNode n); diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 5c3c70443..f5a46b799 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -29,8 +29,8 @@ namespace builtin { class TheoryBuiltin : public Theory { public: - TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) : - Theory(THEORY_BUILTIN, c, out, valuation) {} + TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : + Theory(THEORY_BUILTIN, c, u, out, valuation) {} Node getValue(TNode n); std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8ab806bd8..11ddceaae 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -122,8 +122,8 @@ private: public: - TheoryBV(context::Context* c, OutputChannel& out, Valuation valuation) - : Theory(THEORY_BV, c, out, valuation), + TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BV, c, u, out, valuation), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_context(c), diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 4e185febc..08b142fe3 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -53,8 +53,8 @@ Node TheoryDatatypes::getConstructorForSelector( Node sel ) } -TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valuation) : - Theory(THEORY_DATATYPES, c, out, valuation), +TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) : + Theory(THEORY_DATATYPES, c, u, out, valuation), d_currAsserts(c), d_currEqualities(c), d_selectors(c), diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index d91e9e7f4..433af38c3 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -140,7 +140,7 @@ private: CongruenceClosureExplainer<CongruenceChannel, CONGRUENCE_OPERATORS_2 (kind::APPLY_CONSTRUCTOR, kind::APPLY_SELECTOR)> d_cce; public: - TheoryDatatypes(context::Context* c, OutputChannel& out, Valuation valuation); + TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); ~TheoryDatatypes(); void preRegisterTerm(TNode n); void presolve(); diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp index ae37dfe99..03787703a 100644 --- a/src/theory/example/theory_uf_tim.cpp +++ b/src/theory/example/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(Context* c, OutputChannel& out, Valuation valuation) : - TheoryUF(c, out, valuation), +TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) : + Theory(THEORY_UF, c, u, out, valuation), d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), diff --git a/src/theory/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h index 70c60728f..b47536f07 100644 --- a/src/theory/example/theory_uf_tim.h +++ b/src/theory/example/theory_uf_tim.h @@ -43,7 +43,7 @@ namespace theory { namespace uf { namespace tim { -class TheoryUFTim : public TheoryUF { +class TheoryUFTim : public Theory { private: @@ -85,7 +85,7 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation); + TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); /** Destructor for the TheoryUF object. */ ~TheoryUFTim(); diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 88e5b3dba..cdcf33f6a 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -67,7 +67,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeMap& substitutionCache) { } for (unsigned i = 0; i < current.getNumChildren(); ++ i) { Assert(substitutionCache.find(current[i]) != substitutionCache.end()); - builder << substitutionCache[current[i]]; + builder << Node(substitutionCache[current[i]]); } // Mark the substitution and continue Node result = builder; @@ -104,14 +104,14 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) { Assert(d_substitutions.find(x) == d_substitutions.end()); // Temporary substitution cache - NodeMap tempCache; + NodeMap tempCache(d_context); tempCache[x] = t; // Put in the new substitutions into the old ones NodeMap::iterator it = d_substitutions.begin(); NodeMap::iterator it_end = d_substitutions.end(); for(; it != it_end; ++ it) { - it->second = internalSubstitute(it->second, tempCache); + d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache); } // Put the new substitution in @@ -123,11 +123,12 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) { } } -bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) { +static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED; +static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) { SubstitutionMap::NodeMap::const_iterator it = substitutions.begin(); SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end(); for (; it != it_end; ++ it) { - if (node.hasSubterm(it->first)) { + if (node.hasSubterm((*it).first)) { return false; } } @@ -140,7 +141,12 @@ Node SubstitutionMap::apply(TNode t) { // Setup the cache if (d_cacheInvalidated) { - d_substitutionCache = d_substitutions; + SubstitutionMap::NodeMap::const_iterator it = d_substitutions.begin(); + SubstitutionMap::NodeMap::const_iterator it_end = d_substitutions.end(); + d_substitutionCache.clear(); + for (; it != it_end; ++ it) { + d_substitutionCache[(*it).first] = (*it).second; + } d_cacheInvalidated = false; } @@ -157,7 +163,7 @@ void SubstitutionMap::print(ostream& out) const { NodeMap::const_iterator it = d_substitutions.begin(); NodeMap::const_iterator it_end = d_substitutions.end(); for (; it != it_end; ++ it) { - out << it->first << " -> " << it->second << endl; + out << (*it).first << " -> " << (*it).second << endl; } } diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 849c8f166..253507645 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -24,7 +24,11 @@ #include <utility> #include <vector> #include <algorithm> + #include "expr/node.h" +#include "context/context.h" +#include "context/cdo.h" +#include "context/cdmap.h" namespace CVC4 { namespace theory { @@ -32,17 +36,22 @@ namespace theory { /** * The type for the Substitutions mapping output by * Theory::simplify(), TheoryEngine::simplify(), and - * Valuation::simplify(). This is in its own header to avoid circular - * dependences between those three. + * Valuation::simplify(). This is in its own header to + * avoid circular dependences between those three. + * + * This map is context-dependent. */ class SubstitutionMap { public: - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap; private: + /** The context within which this SubstitutionMap was constructed. */ + context::Context* d_context; + /** The variables, in order of addition */ NodeMap d_substitutions; @@ -50,14 +59,19 @@ private: NodeMap d_substitutionCache; /** Has the cache been invalidated */ - bool d_cacheInvalidated; + context::CDO<bool> d_cacheInvalidated; - /** Internaal method that performs substitution */ + /** Internal method that performs substitution */ Node internalSubstitute(TNode t, NodeMap& substitutionCache); public: - SubstitutionMap(): d_cacheInvalidated(true) {} + SubstitutionMap(context::Context* context) : + d_context(context), + d_substitutions(context), + d_substitutionCache(context), + d_cacheInvalidated(context) { + } /** * Adds a substitution from x to t @@ -77,24 +91,11 @@ public: return const_cast<SubstitutionMap*>(this)->apply(t); } - /** - * Clear out the accumulated substitutions, resetting this - * SubstitutionMap to the way it was when first constructed. - */ - void clear() { - d_substitutions.clear(); - d_substitutionCache.clear(); - d_cacheInvalidated = true; - } - - /** - * Swap the contents of this SubstitutionMap with those of another. - */ - void swap(SubstitutionMap& map) { - d_substitutions.swap(map.d_substitutions); - d_substitutionCache.swap(map.d_substitutionCache); - std::swap(d_cacheInvalidated, map.d_cacheInvalidated); - } + // NOTE [MGD]: removed clear() and swap() from the interface + // when this data structure became context-dependent + // because they weren't used---and it's not clear how they + // should // best interact with cache invalidation on context + // pops. /** * Print to the output stream diff --git a/src/theory/theory.h b/src/theory/theory.h index 931b1155e..17c9ef14a 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -103,6 +103,11 @@ private: context::Context* d_context; /** + * The user context for the Theory. + */ + context::UserContext* d_userContext; + + /** * The assertFact() queue. * * These can not be TNodes as some atoms (such as equalities) are sent @@ -133,13 +138,15 @@ protected: /** * Construct a Theory. */ - Theory(TheoryId id, context::Context* ctxt, OutputChannel& out, Valuation valuation) throw() : + Theory(TheoryId id, context::Context* context, context::UserContext* userContext, + OutputChannel& out, Valuation valuation) throw() : d_id(id), - d_context(ctxt), - d_facts(ctxt), - d_factsHead(ctxt, 0), - d_sharedTermsIndex(ctxt, 0), - d_sharedTerms(ctxt), + d_context(context), + d_userContext(userContext), + d_facts(context), + d_factsHead(context, 0), + d_sharedTermsIndex(context, 0), + d_sharedTerms(context), d_out(&out), d_valuation(valuation) { @@ -328,6 +335,13 @@ public: } /** + * Get the context associated to this Theory. + */ + context::UserContext* getUserContext() const { + return d_userContext; + } + + /** * Set the output channel associated to this theory. */ void setOutputChannel(OutputChannel& out) { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5bb71532c..93df4fe38 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -37,22 +37,24 @@ using namespace std; using namespace CVC4; using namespace CVC4::theory; -TheoryEngine::TheoryEngine(context::Context* ctxt) +TheoryEngine::TheoryEngine(context::Context* context, + context::UserContext* userContext) : d_propEngine(NULL), - d_context(ctxt), + d_context(context), + d_userContext(userContext), d_activeTheories(0), - d_sharedTerms(ctxt), + d_sharedTerms(context), d_atomPreprocessingCache(), d_possiblePropagations(), - d_hasPropagated(ctxt), - d_inConflict(ctxt, false), + d_hasPropagated(context), + d_inConflict(context, false), d_hasShutDown(false), - d_incomplete(ctxt, false), - d_sharedAssertions(ctxt), + d_incomplete(context, false), + d_sharedAssertions(context), d_logic(""), - d_propagatedLiterals(ctxt), - d_propagatedLiteralsIndex(ctxt, 0), - d_preRegistrationVisitor(this, ctxt), + d_propagatedLiterals(context), + d_propagatedLiteralsIndex(context, 0), + d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms) { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { @@ -378,10 +380,10 @@ void TheoryEngine::shutdown() { theory::Rewriter::shutdown(); } -theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) { +theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) { TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl; - Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut); + Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitutionOut); Trace("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl; return solveStatus; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 04f15e89f..915373074 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -80,6 +80,9 @@ class TheoryEngine { /** Our context */ context::Context* d_context; + /** Our user context */ + context::UserContext* d_userContext; + /** * A table of from theory IDs to theory pointers. Never use this table * directly, use theoryOf() instead. @@ -343,7 +346,7 @@ class TheoryEngine { public: /** Constructs a theory engine */ - TheoryEngine(context::Context* ctxt); + TheoryEngine(context::Context* context, context::UserContext* userContext); /** Destroys a theory engine */ ~TheoryEngine(); @@ -356,7 +359,7 @@ public: inline void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); - d_theoryTable[theoryId] = new TheoryClass(d_context, *d_theoryOut[theoryId], theory::Valuation(this)); + d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this)); } /** @@ -407,7 +410,8 @@ public: /** * Solve the given literal with a theory that owns it. */ - theory::Theory::SolveStatus solve(TNode literal, theory::SubstitutionMap& substitionOut); + theory::Theory::SolveStatus solve(TNode literal, + theory::SubstitutionMap& substitutionOut); /** * Preregister a Theory atom with the responsible theory (or diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 6cea8b85b..f8e17b1de 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -97,14 +97,14 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation): - Theory(THEORY_UF, ctxt, out, valuation), + TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation): + Theory(THEORY_UF, c, u, out, valuation), d_notify(*this), - d_equalityEngine(d_notify, ctxt, "theory::uf::TheoryUF"), - d_knownFacts(ctxt), - d_conflict(ctxt, false), - d_literalsToPropagate(ctxt), - d_literalsToPropagateIndex(ctxt, 0) + d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"), + d_knownFacts(c), + d_conflict(c, false), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); |