From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 7 Feb 2013 21:18:08 +0000 (-0500)
Subject: Only put quantifier assertions in model equality engine if fullModel==true
X-Git-Tag: cvc5-1.0.0~7391^2~8
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=63ca7c0a10dcd6b3be42d4d513f842db76733392;p=cvc5.git

Only put quantifier assertions in model equality engine if fullModel==true
---

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index a1f8e32fe..be6dd5b08 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -92,14 +92,16 @@ Node TheoryQuantifiers::getValue(TNode n) {
   }
 }
 
-void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){
-  for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
-    if((*i).assertion.getKind() == kind::NOT) {
-      Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
-      m->assertPredicate((*i).assertion[0], false);
-    } else {
-      Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
-      m->assertPredicate(*i, true);
+void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
+  if(fullModel) {
+    for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
+      if((*i).assertion.getKind() == kind::NOT) {
+        Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
+        m->assertPredicate((*i).assertion[0], false);
+      } else {
+        Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
+        m->assertPredicate(*i, true);
+      }
     }
   }
 }