diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-27 11:35:22 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-27 11:35:22 -0600 |
commit | bcbf52ffbe0416ecf70bdb644017c338c0540793 (patch) | |
tree | 4f0478968f00c97b21d9fe528fa586cf7a227deb /src/smt/smt_engine.cpp | |
parent | 7528e6596c85abc337aa9c795fc2e7627255148e (diff) |
some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 66c7e4cbc..1d98ce115 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -69,6 +69,7 @@ #include "theory/arrays/options.h" #include "util/sort_inference.h" #include "theory/quantifiers/macros.h" +#include "theory/datatypes/options.h" using namespace std; using namespace CVC4; @@ -977,6 +978,13 @@ void SmtEngine::setLogicInternal() throw() { setOption("check-models", SExpr("false")); } } + + //datatypes theory should assign values to all datatypes terms if logic is quantified + if (d_logic.isQuantified() && d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { + if( !options::dtForceAssignment.wasSetByUser() ){ + options::dtForceAssignment.set(true); + } + } } void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) @@ -2253,7 +2261,7 @@ void SmtEnginePrivate::processAssertions() { collectSkolems((*pos).first, skolemSet, cache); collectSkolems((*pos).second, skolemSet, cache); } - + // We need to ensure: // 1. iteExpr has the form (ite cond (sk = t) (sk = e)) // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk |