diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-27 11:35:22 -0600 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-27 13:38:21 -0500 |
commit | 73aa7b9dbc5415b6904539c2dd24683e77ca9b20 (patch) | |
tree | 64d4301b21d3c35c84238cc4242df500f564d3a8 /src/smt | |
parent | 5f58ecb6638f0e0fe63b67f1790b997684655bdd (diff) |
some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields
(cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)
Diffstat (limited to 'src/smt')
-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 |