partially address bug 486: allow some model inspection of quantifiers

4 files changed, 87 insertions, 56 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 3880aaad9..2333a4394 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -77,66 +77,69 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
 
 Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
 {
-  Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS);
-  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;
-  }
-
-  TypeNode t = n.getType();
-  if (t.isFunction() || t.isPredicate()) {
-    if (d_enableFuncModels) {
-      std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
-      if (it != d_uf_models.end()) {
-        // Existing function
-        return it->second;
-      }
-      // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
-      vector<TypeNode> argTypes = t.getArgTypes();
-      vector<Node> args;
+  if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL) {
+    CheckArgument(d_equalityEngine.hasTerm(n), n, "Cannot get the model value for a previously-unseen quantifier: %s", n.toString().c_str());
+  } else {
+    if(n.getKind() == kind::LAMBDA) {
       NodeManager* nm = NodeManager::currentNM();
-      for (unsigned i = 0; i < argTypes.size(); ++i) {
-        args.push_back(nm->mkBoundVar(argTypes[i]));
-      }
-      Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
-      TypeEnumerator te(t.getRangeType());
-      return nm->mkNode(kind::LAMBDA, boundVarList, *te);
+      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);
     }
-    // TODO: if func models not enabled, throw an error?
-    Unreachable();
-  }
-
-  if (n.getNumChildren() > 0) {
-    std::vector<Node> children;
-    if (n.getKind() == APPLY_UF) {
-      Node op = getModelValue(n.getOperator(), hasBoundVars);
-      children.push_back(op);
+    if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) {
+      return n;
     }
-    else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      children.push_back(n.getOperator());
+
+    TypeNode t = n.getType();
+    if (t.isFunction() || t.isPredicate()) {
+      if (d_enableFuncModels) {
+        std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
+        if (it != d_uf_models.end()) {
+          // Existing function
+          return it->second;
+        }
+        // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
+        vector<TypeNode> argTypes = t.getArgTypes();
+        vector<Node> args;
+        NodeManager* nm = NodeManager::currentNM();
+        for (unsigned i = 0; i < argTypes.size(); ++i) {
+          args.push_back(nm->mkBoundVar(argTypes[i]));
+        }
+        Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
+        TypeEnumerator te(t.getRangeType());
+        return nm->mkNode(kind::LAMBDA, boundVarList, *te);
+      }
+      // TODO: if func models not enabled, throw an error?
+      Unreachable();
     }
-    //evaluate the children
-    for (unsigned i = 0; i < n.getNumChildren(); ++i) {
-      Node val = getModelValue(n[i], hasBoundVars);
-      children.push_back(val);
+
+    if (n.getNumChildren() > 0) {
+      std::vector<Node> children;
+      if (n.getKind() == APPLY_UF) {
+        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], hasBoundVars);
+        children.push_back(val);
+      }
+      Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
+      Assert(hasBoundVars || val.isConst());
+      return val;
     }
-    Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
-    Assert(hasBoundVars || val.isConst());
-    return val;
-  }
 
-  if (!d_equalityEngine.hasTerm(n)) {
-    // Unknown term - return first enumerated value for this type
-    TypeEnumerator te(n.getType());
-    return *te;
+    if (!d_equalityEngine.hasTerm(n)) {
+      // Unknown term - return first enumerated value for this type
+      TypeEnumerator te(n.getType());
+      return *te;
+    }
   }
   Node val = d_equalityEngine.getRepresentative(n);
   Assert(d_reps.find(val) != d_reps.end());
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index b1a7c9927..b5287fff4 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -93,7 +93,9 @@ Node TheoryQuantifiers::getValue(TNode n) {
 }
 
 void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){
-
+  for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
+    m->assertPredicate(*i, true);
+  }
 }
 
 void TheoryQuantifiers::check(Effort e) {
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 3b30a8d9e..d5b35594f 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -149,7 +149,8 @@ TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
 	simplification_bug4.smt2.expect \
-	bug216.smt2.expect
+	bug216.smt2.expect \
+	bug486.cvc
 
 if CVC4_BUILD_PROFILE_COMPETITION
 else
diff --git a/test/regress/regress0/bug486.cvc b/test/regress/regress0/bug486.cvc
new file mode 100644
index 000000000..6e8ee0018
--- /dev/null
+++ b/test/regress/regress0/bug486.cvc
@@ -0,0 +1,25 @@
+prin:TYPE;
+form:TYPE;
+
+signed:(prin,form)->BOOLEAN;
+says:(prin,form)->BOOLEAN;
+
+speaksfor:(prin,prin)->form;
+signedE:BOOLEAN = FORALL(x:prin,y:form) : signed(x,y) => says(x,y);
+saysE:BOOLEAN = FORALL(x,y:prin,z:form) : says(x,speaksfor(y,x)) AND says(y,z) => says(x,z); 
+
+ASSERT(signedE);
+ASSERT(saysE);
+
+julie:prin;
+dave:prin;
+alice:prin;
+openfile:form;
+
+x2:BOOLEAN = signed(alice,openfile);
+ASSERT(x2);
+x3:BOOLEAN = signed(dave,speaksfor(alice,dave));
+ASSERT(x3);
+
+QUERY NOT says(dave,openfile); % this is invalid
+QUERY says(dave,openfile); % this is valid