Fixing function models with Boolean terms. Also, LAMBDA's should not be const.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7df98ef089ae0a24b9182ead2c443cabc6e1e5c3..8330b2a201f208888b076c465eb2dc1018228c86 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2778,21 +2778,9 @@ void SmtEngine::checkModel(bool hardFailure) {
 
       Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl;
 
-      // (1) check that the value is actually a value
-      if(!val.isConst()) {
-        Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl;
-        stringstream ss;
-        ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
-           << "model value for " << func << endl
-           << "             is " << val << endl
-           << "and that is not a constant (.isConst() == false)." << endl
-           << "Run with `--check-models -v' for additional diagnostics.";
-        InternalError(ss.str());
-      }
-
-      // (2) if the value is a lambda, ensure the lambda doesn't contain the
+      // (1) if the value is a lambda, ensure the lambda doesn't contain the
       // function symbol (since then the definition is recursive)
-      if(val.getKind() == kind::LAMBDA) {
+      if (val.getKind() == kind::LAMBDA) {
         // first apply the model substitutions we have so far
         Node n = substitutions.apply(val[1]);
         // now check if n contains func by doing a substitution
@@ -2816,6 +2804,18 @@ void SmtEngine::checkModel(bool hardFailure) {
         }
       }
 
+      // (2) check that the value is actually a value
+      else if (!val.isConst()) {
+        Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl;
+        stringstream ss;
+        ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
+           << "model value for " << func << endl
+           << "             is " << val << endl
+           << "and that is not a constant (.isConst() == false)." << endl
+           << "Run with `--check-models -v' for additional diagnostics.";
+        InternalError(ss.str());
+      }
+
       // (3) checks complete, add the substitution
       substitutions.addSubstitution(func, val);
     }

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 4aa7c0982e871e649078f891eedb6e3fe91a3160..40f838623d15142e369be0959a4c199c51dcb873 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -173,7 +173,7 @@ public:
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
     Assert(n.getKind() == kind::LAMBDA);
-    return true;
+    return false;
   }
 };/* class LambdaTypeRule */
 

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index b117aa1af8a91bdc36de7fe2f8e37167e8e9a34a..826e729fc546df5748a38454ffa7d0b53a3b08dc 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -26,7 +26,7 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 
-TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels ) :
+TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) :
   d_substitutions(c), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
@@ -75,13 +75,19 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
   }
 }
 
-Node TheoryModel::getModelValue(TNode n) const
+Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
 {
   Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS);
-  if(n.isConst()) {
-    return n;
-  }
   if(n.getKind() == kind::LAMBDA) {
+    NodeManager* nm = NodeManager::currentNM();
+    Node body = getModelValue(n[1], true);
+    // This is a bit ugly, but cache inside simplifier can change, so can't be const
+    // The ite simplifier is needed to get rid of artifacts created by Boolean terms
+    body = const_cast<ITESimplifier*>(&d_iteSimp)->simpITE(body);
+    body = Rewriter::rewrite(body);
+    return nm->mkNode(kind::LAMBDA, n[0], body);
+  }
+  if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) {
     return n;
   }
 
@@ -111,31 +117,19 @@ Node TheoryModel::getModelValue(TNode n) const
   if (n.getNumChildren() > 0) {
     std::vector<Node> children;
     if (n.getKind() == APPLY_UF) {
-      Node op = n.getOperator();
-      if (op.getKind() == kind::LAMBDA) {
-        Node rw = Rewriter::rewrite(n);
-        return getModelValue(rw);
-      }
-      std::map< Node, Node >::const_iterator it = d_uf_models.find(op);
-      if (it == d_uf_models.end()) {
-        // Unknown term - return first enumerated value for this type
-        TypeEnumerator te(n.getType());
-        return *te;
-      }else{
-        // Plug in uninterpreted function model
-        children.push_back(it->second);
-      }
+      Node op = getModelValue(n.getOperator(), hasBoundVars);
+      children.push_back(op);
     }
     else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
       children.push_back(n.getOperator());
     }
     //evaluate the children
     for (unsigned i = 0; i < n.getNumChildren(); ++i) {
-      Node val = getModelValue(n[i]);
+      Node val = getModelValue(n[i], hasBoundVars);
       children.push_back(val);
     }
     Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
-    Assert(val.isConst());
+    Assert(hasBoundVars || val.isConst());
     return val;
   }
 

diff --git a/src/theory/model.h b/src/theory/model.h
index 19415ae7b7d1d69dc6df17804a22833665bcc9c8..7ccbe2fc3ba34f38a90eef8572318d8115546798 100644 (file)
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -22,10 +22,13 @@
 #include "theory/rep_set.h"
 #include "theory/substitutions.h"
 #include "theory/type_enumerator.h"
+#include "theory/ite_simplifier.h"
 
 namespace CVC4 {
+
 namespace theory {
 
+
 /** Theory Model class
  *    For Model m, should call m.initialize() before using
  */
@@ -35,8 +38,9 @@ class TheoryModel : public Model
 protected:
   /** substitution map for this model */
   SubstitutionMap d_substitutions;
+  ITESimplifier d_iteSimp;
 public:
-  TheoryModel( context::Context* c, std::string name, bool enableFuncModels );
+  TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
   virtual ~TheoryModel(){}
   /** equality engine containing all known equalities/disequalities */
   eq::EqualityEngine d_equalityEngine;
@@ -55,7 +59,7 @@ protected:
   /**
    * Get model value function.  This function is called by getValue
    */
-  Node getModelValue( TNode n ) const;
+  Node getModelValue(TNode n, bool hasBoundVars = false) const;
 public:
   /**
    * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 42fe10cb9fe627c14347a406913f6b08afea6c99..1742a32a55c0e4ea8e094bf0a7fc11cf3b00ae21 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -106,8 +106,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_quantEngine = new QuantifiersEngine(context, this);
 
   // build model information if applicable
-  d_curr_model = new theory::TheoryModel( userContext, "DefaultModel", true );
-  d_curr_model_builder = new theory::TheoryEngineModelBuilder( this );
+  d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
+  d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
 
   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);