From bcbf52ffbe0416ecf70bdb644017c338c0540793 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 27 Jan 2013 11:35:22 -0600 Subject: some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields --- src/smt/smt_engine.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'src/smt/smt_engine.cpp') 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 -- cgit v1.2.3