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/smt | |
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/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 30 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 |
2 files changed, 34 insertions, 1 deletions
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 === |