More bug fixes and more checks for models

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3813f964d08d925004f6caee9114213053ce3cd9..55ac15ebcdf7ea4af6450c282d7829a92082a40f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -712,11 +712,22 @@ void SmtEngine::setLogicInternal() throw() {
   if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) {
     //    bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
     //    bool uncSimp = false && !qf_sat && !options::incrementalSolving();
-    bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() &&
+    bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() &&
       (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
     Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
     options::unconstrainedSimp.set(uncSimp);
   }
+  // Unconstrained simp currently does *not* support model generation
+  if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) {
+    if (options::produceModels()) {
+      Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << std::endl;
+      setOption("produce-models", SExpr("false"));
+    }
+    if (options::checkModels()) {
+      Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << std::endl;
+      setOption("check-models", SExpr("false"));
+    }
+  }
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! options::arithRewriteEq.wasSetByUser()) {
     bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified();
@@ -1494,6 +1505,11 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   SubstitutionMap::iterator pos = constantPropagations.begin();
   for (; pos != constantPropagations.end(); ++pos) {
     Node cProp = (*pos).first.eqNode((*pos).second);
+    Node cPropNew = d_topLevelSubstitutions.apply(cProp);
+    if (cProp != cPropNew) {
+      cProp = Rewriter::rewrite(cPropNew);
+      Assert(Rewriter::rewrite(cProp) == cProp);
+    }
     if (s.find(cProp) != s.end()) {
       continue;
     }
@@ -2343,6 +2359,10 @@ void SmtEngine::checkModel(bool hardFailure) {
 
   Notice() << "SmtEngine::checkModel(): generating model" << endl;
   TheoryModel* m = d_theoryEngine->getModel();
+
+  // Check individual theory assertions
+  d_theoryEngine->checkTheoryAssertionsWithModel();
+
   if(Notice.isOn()) {
     // This operator<< routine is non-const (i.e., takes a non-const Model&).
     // This confuses the Notice() output routines, so extract the ostream

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index aa2de656ead062afe24b89c982fc7a5a6ef4bbd9..452317f5b13d16d48a1547eed923bc036834e82d 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -75,6 +75,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
 }
 
 Node TheoryModel::getModelValue( TNode n ) const{
+  Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS && n.getKind() != kind::LAMBDA);
   if( n.isConst() ) {
     return n;
   }

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f24b11c4172a07ce445cf5f55afc2dde28ca4b97..d5c4998d4915c5be670b03b5a47554ab59c506a2 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1338,8 +1338,28 @@ void TheoryEngine::setUserAttribute( std::string& attr, Node n ){
   }
 }
 
+
 void TheoryEngine::handleUserAttribute( const char* attr, Theory* t ){
   Trace("te-attr") << "Handle user attribute " << attr << " " << t << std::endl;
   std::string str( attr );
   d_attr_handle[ str ].push_back( t );
 }
+
+
+void TheoryEngine::checkTheoryAssertionsWithModel()
+{
+  for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
+    Theory* theory = d_theoryTable[theoryId];
+    if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
+      if (theoryId == THEORY_QUANTIFIERS || theoryId == THEORY_REWRITERULES) {
+        continue;
+      }
+      context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+      for (unsigned i = 0; it != it_end; ++ it, ++i) {
+        Node assertion = (*it).assertion;
+        Node val = getModel()->getValue(assertion);
+        Assert(val == d_true);
+      }
+    }
+  }
+}

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index d542d0dd75cd7ebe6cde365c76fabf638ec65eee..8331ef61d10856c1934788198f83989494f1309e 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -710,6 +710,11 @@ public:
     */
   void handleUserAttribute( const char* attr, theory::Theory* t );
 
+  /** Check that the theory assertions are satisfied in the model
+   *  This function is called from the smt engine's checkModel routine
+   */
+  void checkTheoryAssertionsWithModel();
+
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */