From: Morgan Deters Date: Thu, 29 Sep 2011 05:15:30 +0000 (+0000) Subject: Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model... X-Git-Tag: cvc5-1.0.0~8448 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c94347913fa464b1ec6a3da2ab21e319c0c42e02;p=cvc5.git 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 --- diff --git a/Makefile.am b/Makefile.am index f8538b548..d2b11fe9c 100644 --- a/Makefile.am +++ b/Makefile.am @@ -12,7 +12,7 @@ systemtests regress regress0 regress1 regress2 regress3: all +(cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1 # We descend into "src" with the "check" target here to ensure that # the test prerequisites are all built. -units: all +units: (cd src && $(MAKE) $(AM_MAKEFLAGS) check) +(cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1 diff --git a/Makefile.builds.in b/Makefile.builds.in index 44326f0ff..7d2e8586b 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -127,7 +127,7 @@ endif check test units: (cd $(CURRENT_BUILD)/src && $(MAKE) check) +(cd $(CURRENT_BUILD)/test && $(MAKE) $@) -systemtests regress: +systemtests regress: all +(cd $(CURRENT_BUILD)/test && $(MAKE) $@) units%: (cd $(CURRENT_BUILD)/src && $(MAKE) check) diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 3ac99f729..2a5365082 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -364,6 +364,10 @@ public: return d_map.size(); } + bool empty() const { + return d_map.empty(); + } + size_t count(const Key& k) const { return d_map.count(k); } diff --git a/src/context/context.h b/src/context/context.h index 1e69964a0..78c06e7d5 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -95,6 +95,10 @@ class Context { friend std::ostream& operator<<(std::ostream&, const Context&) throw(AssertionException); + // disable copy, assignment + Context(const Context&) CVC4_UNUSED; + Context& operator=(const Context&) CVC4_UNUSED; + public: /** * Constructor: create ContextMemoryManager and initial Scope @@ -153,6 +157,22 @@ public: };/* class Context */ + +/** + * A UserContext is different from a Context only because it's used for + * different purposes---so separating the two types gives type errors where + * appropriate. + */ +class UserContext : public Context { +private: + // disable copy, assignment + UserContext(const UserContext&) CVC4_UNUSED; + UserContext& operator=(const UserContext&) CVC4_UNUSED; +public: + UserContext() {} +};/* class UserContext */ + + /** * Conceptually, a Scope encapsulates that portion of the context that * changes after a call to push() and must be undone on a subsequent call to diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index f013c1644..28f990c98 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -71,7 +71,7 @@ using namespace CVC4::kind; namespace CVC4 { ExprManager::ExprManager() : - d_ctxt(new Context), + d_ctxt(new Context()), d_nodeManager(new NodeManager(d_ctxt, this)) { #ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { @@ -84,7 +84,7 @@ ExprManager::ExprManager() : } ExprManager::ExprManager(const Options& options) : - d_ctxt(new Context), + d_ctxt(new Context()), d_nodeManager(new NodeManager(d_ctxt, this, options)) { #ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i <= LAST_TYPE; ++ i) { diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 8f1d54a3a..1d1f447be 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -18,6 +18,7 @@ **/ #include +#include #include #include #include @@ -92,23 +93,38 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, if(d_in == cin) { ::rl_readline_name = "CVC4"; ::rl_completion_entry_function = commandGenerator; + ::using_history(); switch(OutputLanguage lang = toOutputLanguage(d_language)) { case output::LANG_CVC4: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history"; commandsBegin = cvc_commands; commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); break; case output::LANG_SMTLIB: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib"; commandsBegin = smt_commands; commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands); break; case output::LANG_SMTLIB_V2: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; commandsBegin = smt2_commands; commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); break; default: Unhandled(lang); } d_usingReadline = true; + int err = ::read_history(d_historyFilename.c_str()); + ::stifle_history(s_historyLimit); + if(Notice.isOn()) { + if(err == 0) { + Notice() << "Read " << ::history_length << " lines of history from " + << d_historyFilename << std::endl; + } else { + Notice() << "Could not read history from " << d_historyFilename + << ": " << strerror(err) << std::endl; + } + } } else { d_usingReadline = false; } @@ -117,6 +133,16 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, #endif /* HAVE_LIBREADLINE */ }/* InteractiveShell::InteractiveShell() */ +InteractiveShell::~InteractiveShell() { + int err = ::write_history(d_historyFilename.c_str()); + if(err == 0) { + Notice() << "Wrote " << ::history_length << " lines of history to " + << d_historyFilename << std::endl; + } else { + Notice() << "Could not write history to " << d_historyFilename + << ": " << strerror(err) << std::endl; + } +} Command* InteractiveShell::readCommand() { /* Don't do anything if the input is closed or if we've seen a diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index f6852b95b..65fea8494 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -40,11 +40,19 @@ class CVC4_PUBLIC InteractiveShell { bool d_quit; bool d_usingReadline; + std::string d_historyFilename; + static const std::string INPUT_FILENAME; + static const unsigned s_historyLimit = 500; public: InteractiveShell(ExprManager& exprManager, const Options& options); + /** + * Close out the interactive session. + */ + ~InteractiveShell(); + /** * Read a command from the interactive shell. This will read as * many lines as necessary to parse a well-formed command. diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 770433489..f3a85ed5e 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1100,7 +1100,7 @@ lbool Solver::solve_() ok = false; // Cancel the trail downto previous push - popTrail(); + //popTrail(); return status; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 24ebf9bfd..86d06520a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -101,7 +101,7 @@ public: class SmtEnginePrivate { SmtEngine& d_smt; - /** The assertions yet to be preprecessed */ + /** The assertions yet to be preprocessed */ vector d_assertionsToPreprocess; /** Learned literals */ @@ -138,7 +138,10 @@ class SmtEnginePrivate { public: - SmtEnginePrivate(SmtEngine& smt) : d_smt(smt) { } + SmtEnginePrivate(SmtEngine& smt) : + d_smt(smt), + d_topLevelSubstitutions(smt.d_userContext) { + } Node applySubstitutions(TNode node) const { return Rewriter::rewrite(d_topLevelSubstitutions.apply(node)); @@ -172,7 +175,7 @@ using namespace CVC4::smt; SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_context(em->getContext()), - d_userContext(new Context()), + d_userContext(new UserContext()), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), d_private(new smt::SmtEnginePrivate(*this)), @@ -186,9 +189,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime); StatisticsRegistry::registerStat(&d_staticLearningTime); - // We have mutual dependancy here, so we add the prop engine to the theory + // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine = new TheoryEngine(d_context); + d_theoryEngine = new TheoryEngine(d_context, d_userContext); // Add the theories d_theoryEngine->addTheory(theory::THEORY_BUILTIN); @@ -927,8 +930,11 @@ Expr SmtEngine::getValue(const Expr& e) throw ModalException(msg); } + // Apply what was learned from preprocessing + Node n = d_private->applySubstitutions(e.getNode()); + // Normalize for the theories - Node n = theory::Rewriter::rewrite(e.getNode()); + n = theory::Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; Node resultNode = d_theoryEngine->getValue(n); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index d2abf2fce..7a5f39056 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -54,6 +54,7 @@ class StatisticsRegistry; namespace context { class Context; + class UserContext; }/* CVC4::context namespace */ namespace prop { @@ -99,7 +100,7 @@ class CVC4_PUBLIC SmtEngine { /** The context levels of user pushes */ std::vector d_userLevels; /** User level context */ - context::Context* d_userContext; + context::UserContext* d_userContext; /** Our expression manager */ ExprManager* d_exprManager; 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 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 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 #include #include + #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 NodeMap; + typedef context::CDMap 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 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(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 @@ -102,6 +102,11 @@ private: */ context::Context* d_context; + /** + * The user context for the Theory. + */ + context::UserContext* d_userContext; + /** * The assertFact() queue. * @@ -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) { @@ -327,6 +334,13 @@ public: return d_context; } + /** + * Get the context associated to this Theory. + */ + context::UserContext* getUserContext() const { + return d_userContext; + } + /** * Set the output channel associated to this theory. */ 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); diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index c9a2196a5..62117d4c1 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -99,154 +99,159 @@ class CnfStreamBlack : public CxxTest::TestSuite { /** The context */ Context* d_context; + /** The user context */ + UserContext* d_userContext; + /** The node manager */ NodeManager* d_nodeManager; -void setUp() { - d_context = new Context; - d_nodeManager = new NodeManager(d_context, NULL); - NodeManagerScope nms(d_nodeManager); - d_satSolver = new FakeSatSolver; - d_theoryEngine = new TheoryEngine(d_context); - d_theoryEngine->addTheory(theory::THEORY_BUILTIN); - d_theoryEngine->addTheory(theory::THEORY_BOOL); - d_theoryEngine->addTheory(theory::THEORY_ARITH); - theory::Registrar registrar(d_theoryEngine); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar); -} - -void tearDown() { - NodeManagerScope nms(d_nodeManager); - delete d_cnfStream; - d_theoryEngine->shutdown(); - delete d_theoryEngine; - delete d_satSolver; - delete d_nodeManager; - delete d_context; -} + void setUp() { + d_context = new Context(); + d_userContext = new UserContext(); + d_nodeManager = new NodeManager(d_context, NULL); + NodeManagerScope nms(d_nodeManager); + d_satSolver = new FakeSatSolver(); + d_theoryEngine = new TheoryEngine(d_context, d_userContext); + d_theoryEngine->addTheory(theory::THEORY_BUILTIN); + d_theoryEngine->addTheory(theory::THEORY_BOOL); + d_theoryEngine->addTheory(theory::THEORY_ARITH); + theory::Registrar registrar(d_theoryEngine); + d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar); + } + + void tearDown() { + NodeManagerScope nms(d_nodeManager); + delete d_cnfStream; + d_theoryEngine->shutdown(); + delete d_theoryEngine; + delete d_satSolver; + delete d_nodeManager; + delete d_userContext; + delete d_context; + } public: -/* [chris 5/26/2010] In the tests below, we don't attempt to delve into the - * deep structure of the CNF conversion. Firstly, we just want to make sure - * that the conversion doesn't choke on any boolean Exprs. We'll also check - * that addClause got called. We won't check that it gets called a particular - * number of times, or with what. - */ - -void testAnd() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::AND, a, b, c), false, false); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testComplexExpr() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node d = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node e = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node f = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode( - kind::IMPLIES, - d_nodeManager->mkNode(kind::AND, a, b), - d_nodeManager->mkNode( - kind::IFF, - d_nodeManager->mkNode(kind::OR, c, d), - d_nodeManager->mkNode( - kind::NOT, - d_nodeManager->mkNode(kind::XOR, e, f)))), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testFalse() { - NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testIff() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::IFF, a, b), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testImplies() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -// ITEs should be removed before going to CNF -//void testIte() { -// NodeManagerScope nms(d_nodeManager); -// d_cnfStream->convertAndAssert( -// d_nodeManager->mkNode( -// kind::EQUAL, -// d_nodeManager->mkNode( -// kind::ITE, -// d_nodeManager->mkVar(d_nodeManager->booleanType()), -// d_nodeManager->mkVar(d_nodeManager->integerType()), -// d_nodeManager->mkVar(d_nodeManager->integerType()) -// ), -// d_nodeManager->mkVar(d_nodeManager->integerType()) -// ), false, false); -// -//} - -void testNot() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::NOT, a), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testOr() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::OR, a, b, c), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testTrue() { - NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testVar() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(a, false, false); - TS_ASSERT( d_satSolver->addClauseCalled() ); - d_satSolver->reset(); - d_cnfStream->convertAndAssert(b, false, false); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testXor() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::XOR, a, b), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} + /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the + * deep structure of the CNF conversion. Firstly, we just want to make sure + * that the conversion doesn't choke on any boolean Exprs. We'll also check + * that addClause got called. We won't check that it gets called a particular + * number of times, or with what. + */ + + void testAnd() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::AND, a, b, c), false, false); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testComplexExpr() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node d = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node e = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node f = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode( + kind::IMPLIES, + d_nodeManager->mkNode(kind::AND, a, b), + d_nodeManager->mkNode( + kind::IFF, + d_nodeManager->mkNode(kind::OR, c, d), + d_nodeManager->mkNode( + kind::NOT, + d_nodeManager->mkNode(kind::XOR, e, f)))), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testFalse() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testIff() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::IFF, a, b), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testImplies() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + // ITEs should be removed before going to CNF + //void testIte() { + // NodeManagerScope nms(d_nodeManager); + // d_cnfStream->convertAndAssert( + // d_nodeManager->mkNode( + // kind::EQUAL, + // d_nodeManager->mkNode( + // kind::ITE, + // d_nodeManager->mkVar(d_nodeManager->booleanType()), + // d_nodeManager->mkVar(d_nodeManager->integerType()), + // d_nodeManager->mkVar(d_nodeManager->integerType()) + // ), + // d_nodeManager->mkVar(d_nodeManager->integerType()) + // ), false, false); + // + //} + + void testNot() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::NOT, a), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testOr() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::OR, a, b, c), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testTrue() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testVar() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert(a, false, false); + TS_ASSERT( d_satSolver->addClauseCalled() ); + d_satSolver->reset(); + d_cnfStream->convertAndAssert(b, false, false); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testXor() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::XOR, a, b), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } }; diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index ded7cee97..f0073cc0b 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -43,6 +43,7 @@ using namespace std; class TheoryArithWhite : public CxxTest::TestSuite { Context* d_ctxt; + UserContext* d_uctxt; NodeManager* d_nm; NodeManagerScope* d_scope; @@ -92,11 +93,12 @@ public: } void setUp() { - d_ctxt = new Context; + d_ctxt = new Context(); + d_uctxt = new UserContext(); d_nm = new NodeManager(d_ctxt, NULL); d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); - d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL)); + d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL)); preregistered = new std::set(); @@ -115,6 +117,7 @@ public: d_outputChannel.clear(); delete d_scope; delete d_nm; + delete d_uctxt; delete d_ctxt; } diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 2c3ff0bb1..63900c19c 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -95,8 +95,8 @@ public: set d_registered; vector d_getSequence; - DummyTheory(Context* ctxt, OutputChannel& out, Valuation valuation) : - Theory(theory::THEORY_BUILTIN, ctxt, out, valuation) { + DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation) : + Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation) { } void registerTerm(TNode n) { @@ -135,11 +135,12 @@ public: void explain(TNode n, Effort level) {} Node getValue(TNode n) { return Node::null(); } string identify() const { return "DummyTheory"; } -}; +};/* class DummyTheory */ class TheoryBlack : public CxxTest::TestSuite { Context* d_ctxt; + UserContext* d_uctxt; NodeManager* d_nm; NodeManagerScope* d_scope; @@ -153,10 +154,11 @@ class TheoryBlack : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context; + d_ctxt = new Context(); + d_uctxt = new UserContext(); d_nm = new NodeManager(d_ctxt, NULL); d_scope = new NodeManagerScope(d_nm); - d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL)); + d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL)); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); atom1 = d_nm->mkConst(false); @@ -168,6 +170,7 @@ public: delete d_dummy; delete d_scope; delete d_nm; + delete d_uctxt; delete d_ctxt; } diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index e33efb597..7132d9b17 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -104,8 +104,8 @@ class FakeTheory : public Theory { // static std::deque s_expected; public: - FakeTheory(context::Context* ctxt, OutputChannel& out, Valuation valuation) : - Theory(theoryId, ctxt, out, valuation) + FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation) : + Theory(theoryId, ctxt, uctxt, out, valuation) { } /** Register an expected rewrite call */ @@ -222,6 +222,7 @@ public: */ class TheoryEngineWhite : public CxxTest::TestSuite { Context* d_ctxt; + UserContext* d_uctxt; NodeManager* d_nm; NodeManagerScope* d_scope; @@ -231,15 +232,16 @@ class TheoryEngineWhite : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context; + d_ctxt = new Context(); + d_uctxt = new UserContext(); d_nm = new NodeManager(d_ctxt, NULL); d_scope = new NodeManagerScope(d_nm); - d_nullChannel = new FakeOutputChannel; + d_nullChannel = new FakeOutputChannel(); // create the TheoryEngine - d_theoryEngine = new TheoryEngine(d_ctxt); + d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt); d_theoryEngine->addTheory< FakeTheory >(THEORY_BUILTIN); d_theoryEngine->addTheory< FakeTheory >(THEORY_BOOL); @@ -260,6 +262,7 @@ public: delete d_scope; delete d_nm; + delete d_uctxt; delete d_ctxt; }