From ddd3797ee72443bd35f6cea146c3752ea0dd2286 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 26 Oct 2012 02:37:38 +0000
Subject: [PATCH] More bug fixes and more checks for models

---
 src/smt/smt_engine.cpp       | 22 +++++++++++++++++++++-
 src/theory/model.cpp         |  1 +
 src/theory/theory_engine.cpp | 20 ++++++++++++++++++++
 src/theory/theory_engine.h   |  5 +++++
 4 files changed, 47 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3813f964d..55ac15ebc 100644
--- 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 aa2de656e..452317f5b 100644
--- 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 f24b11c41..d5c4998d4 100644
--- 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 d542d0dd7..8331ef61d 100644
--- 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 */
-- 
2.30.2