From 5a20a19a30929ad58a9e64a9d8d1f877f3a07ae6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 23 Feb 2012 23:08:03 +0000 Subject: [PATCH] Added ability to set a "cvc4-specific logic" in standards-compliant SMT-LIBv1 and SMT-LIBv2 input: In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance: (benchmark actually_a_sat_benchmark_but_looks_like_uf :logic QF_UF :cvc4_logic { QF_SAT } [...] In SMT-LIBv2, you use a set-info; for instance: (set-logic QF_UF) (set-info :cvc4-logic "QF_SAT") [...] Right now, the only thing this does is disable the symmetry breaker for benchmarks like the above ones. As part of this work, TheoryEngine::setLogic() was removed (the logic field there wasn't actually used anywhere, its need disappeared when Theory::setUninterpretedSortOwner() was provided). Also, Theory::d_uninterpretedSortOwner got a name change to Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory class. This represents a breakage of our separation goals for CVC4, since it means that two SmtEngines cannot be created separately to solve a QF_AX and QF_UF problem. A bug report is pending. --- src/expr/node_manager.cpp | 9 +++------ src/expr/node_manager.h | 16 ++++++++++------ src/main/driver.cpp | 8 -------- src/main/driver_portfolio.cpp | 8 -------- src/smt/smt_engine.cpp | 30 +++++++++++++++++++++++++++++- src/smt/smt_engine.h | 5 +++++ src/theory/theory.cpp | 2 +- src/theory/theory.h | 9 ++++++--- src/theory/theory_engine.cpp | 7 ------- src/theory/theory_engine.h | 3 --- 10 files changed, 54 insertions(+), 43 deletions(-) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 1d4b7d3d1..c647e128c 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -81,8 +81,7 @@ struct NVReclaim { NodeManager::NodeManager(context::Context* ctxt, ExprManager* exprManager) : - d_optionsAllocated(new Options()), - d_options(d_optionsAllocated), + d_options(), d_statisticsRegistry(new StatisticsRegistry()), next_id(0), d_attrManager(ctxt), @@ -96,8 +95,7 @@ NodeManager::NodeManager(context::Context* ctxt, NodeManager::NodeManager(context::Context* ctxt, ExprManager* exprManager, const Options& options) : - d_optionsAllocated(NULL), - d_options(&options), + d_options(options), d_statisticsRegistry(new StatisticsRegistry()), next_id(0), d_attrManager(ctxt), @@ -155,7 +153,6 @@ NodeManager::~NodeManager() { } delete d_statisticsRegistry; - delete d_optionsAllocated; } void NodeManager::reclaimZombies() { @@ -254,7 +251,7 @@ TypeNode NodeManager::getType(TNode n, bool check) Debug("getType") << "getting type for " << n << std::endl; - if(needsCheck && !d_options->earlyTypeChecking) { + if(needsCheck && !d_options.earlyTypeChecking) { /* Iterate and compute the children bottom up. This avoids stack overflows in computeType() when the Node graph is really deep, which should only affect us when we're type checking lazily. */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index e446b7d71..704e930b5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -82,8 +82,7 @@ class NodeManager { static CVC4_THREADLOCAL(NodeManager*) s_current; - const Options* d_optionsAllocated; - const Options* d_options; + Options d_options; StatisticsRegistry* d_statisticsRegistry; NodeValuePool d_nodeValuePool; @@ -266,9 +265,14 @@ public: /** The node manager in the current public-facing CVC4 library context */ static NodeManager* currentNM() { return s_current; } - /** Get this node manager's options */ + /** Get this node manager's options (const version) */ const Options* getOptions() const { - return d_options; + return &d_options; + } + + /** Get this node manager's options (non-const version) */ + Options* getOptions() { + return &d_options; } /** Get this node manager's statistics registry */ @@ -752,14 +756,14 @@ public: // Expr is destructed, there's no active node manager. //Assert(nm != NULL); NodeManager::s_current = nm; - Options::s_current = nm ? nm->d_options : NULL; + Options::s_current = nm ? &nm->d_options : NULL; Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } ~NodeManagerScope() { NodeManager::s_current = d_oldNodeManager; - Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; + Options::s_current = d_oldNodeManager ? &d_oldNodeManager->d_options : NULL; Debug("current") << "node manager scope: " << "returning to " << NodeManager::s_current << "\n"; } diff --git a/src/main/driver.cpp b/src/main/driver.cpp index e9bfde024..fa42e0b28 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -331,14 +331,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { status = doCommand(smt, *subcmd, options) && status; } } else { - // by default, symmetry breaker is on only for QF_UF - if(! options.ufSymmetryBreakerSetByUser) { - SetBenchmarkLogicCommand *logic = dynamic_cast(cmd); - if(logic != NULL) { - options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); - } - } - if(options.verbosity > 0) { *options.out << "Invoking: " << *cmd << endl; } diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index 5c8f908f8..7b0c70a8a 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -655,14 +655,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { status = doCommand(smt, *subcmd, options) && status; } } else { - // by default, symmetry breaker is on only for QF_UF - if(! options.ufSymmetryBreakerSetByUser) { - SetBenchmarkLogicCommand *logic = dynamic_cast(cmd); - if(logic != NULL) { - options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); - } - } - if(options.verbosity > 0) { *options.out << "Invoking: " << *cmd << endl; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f9539a1a4..12288e40a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -303,12 +303,22 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { Dump("benchmark") << SetBenchmarkLogicCommand(s) << endl; } + setLogicInternal(s); +} + +void SmtEngine::setLogicInternal(const std::string& s) throw() { d_logic = s; - d_theoryEngine->setLogic(s); + + // by default, symmetry breaker is on only for QF_UF + if(! Options::current()->ufSymmetryBreakerSetByUser) { + NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = (s == "QF_UF"); + } // If in arrays, set the UF handler to arrays if(s == "QF_AX") { theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY); + } else { + theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF); } } @@ -318,6 +328,24 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) if(Dump.isOn("benchmark")) { Dump("benchmark") << SetInfoCommand(key, value) << endl; } + + // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") + if(key.length() > 6) { + string prefix = key.substr(0, 6); + if(prefix == ":cvc4-" || prefix == ":cvc4_") { + string cvc4key = key.substr(6); + if(cvc4key == "logic") { + if(! value.isAtom()) { + throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string"); + } + d_logic = ""; + setLogic(value.getValue()); + return; + } + } + } + + // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...) if(key == ":name" || key == ":source" || key == ":category" || diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 52a98f414..17717e440 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -206,6 +206,11 @@ class CVC4_PUBLIC SmtEngine { void internalPop(); + /** + * Internally handle the setting of a logic. + */ + void setLogicInternal(const std::string& logic) throw(); + friend class ::CVC4::smt::SmtEnginePrivate; // === STATISTICS === diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index ff2feb121..fa2eed861 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -27,7 +27,7 @@ namespace CVC4 { namespace theory { /** Default value for the uninterpreted sorts is the UF theory */ -TheoryId Theory::d_uninterpretedSortOwner = THEORY_UF; +TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF; std::ostream& operator<<(std::ostream& os, Theory::Effort level){ switch(level){ diff --git a/src/theory/theory.h b/src/theory/theory.h index cf986a1f2..fade1e3c7 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -208,7 +208,7 @@ protected: /** * The theory that owns the uninterpreted sort. */ - static TheoryId d_uninterpretedSortOwner; + static TheoryId s_uninterpretedSortOwner; public: @@ -216,6 +216,7 @@ public: * Return the ID of the theory responsible for the given type. */ static inline TheoryId theoryOf(TypeNode typeNode) { + Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl; TheoryId id; if (typeNode.getKind() == kind::TYPE_CONSTANT) { id = typeConstantToTheoryId(typeNode.getConst()); @@ -223,7 +224,8 @@ public: id = kindToTheoryId(typeNode.getKind()); } if (id == THEORY_BUILTIN) { - return d_uninterpretedSortOwner; + Trace("theory") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl; + return s_uninterpretedSortOwner; } return id; } @@ -233,6 +235,7 @@ public: * Returns the ID of the theory responsible for the given node. */ static inline TheoryId theoryOf(TNode node) { + Trace("theory") << "theoryOf(" << node << ")" << std::endl; // Constants, variables, 0-ary constructors if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) { return theoryOf(node.getType()); @@ -249,7 +252,7 @@ public: * Set the owner of the uninterpreted sort. */ static void setUninterpretedSortOwner(TheoryId theory) { - d_uninterpretedSortOwner = theory; + s_uninterpretedSortOwner = theory; } /** diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c4a8dc591..3486d9075 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -52,7 +52,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_hasShutDown(false), d_incomplete(context, false), d_sharedAssertions(context), - d_logic(""), d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_decisionRequests(context), @@ -78,12 +77,6 @@ TheoryEngine::~TheoryEngine() { } } -void TheoryEngine::setLogic(std::string logic) { - Assert(d_logic.empty()); - // Set the logic - d_logic = logic; -} - void TheoryEngine::preRegister(TNode preprocessed) { if(Dump.isOn("missed-t-propagations")) { d_possiblePropagations.push_back(preprocessed); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index be1c3abaf..2c1c9a436 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -323,9 +323,6 @@ class TheoryEngine { */ void assertSharedEqualities(); - /** The logic of the problem */ - std::string d_logic; - /** * Literals that are propagated by the theory. Note that these are TNodes. * The theory can only propagate nodes that have an assigned literal in the -- 2.30.2