diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-23 23:08:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-23 23:08:03 +0000 |
commit | 5a20a19a30929ad58a9e64a9d8d1f877f3a07ae6 (patch) | |
tree | 2a800e6b1d6773e1c844767f5daed51148b5660b /src/expr | |
parent | 1f2590541aa60f4b62b7c96659362ee4431d2d63 (diff) |
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.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.cpp | 9 | ||||
-rw-r--r-- | src/expr/node_manager.h | 16 |
2 files changed, 13 insertions, 12 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"; } |