Add notions of evaluated kinds in TheoryModel (#1947)

5 files changed, 27 insertions, 0 deletions

diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp
index cedd2a2ed..52ce4407a 100644
--- a/src/theory/quantifiers/fmf/ambqi_builder.cpp
+++ b/src/theory/quantifiers/fmf/ambqi_builder.cpp
@@ -744,6 +744,11 @@ QModelBuilder( c, qe ){
 //------------------------model construction----------------------------
 
 bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
+  if (!m->areFunctionValuesEnabled())
+  {
+    // nothing to do if no functions
+    return true;
+  }
   Trace("ambqi-debug") << "process build model " << std::endl;
   FirstOrderModel* f = (FirstOrderModel*)m;
   FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 0ec8b00b2..e97f716cb 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "options/quantifiers_options.h"
+#include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
@@ -370,6 +371,11 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
 }
 
 bool FullModelChecker::processBuildModel(TheoryModel* m){
+  if (!m->areFunctionValuesEnabled())
+  {
+    // nothing to do if no functions
+    return true;
+  }
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
   Trace("fmc") << "---Full Model Check reset() " << std::endl;
   d_quant_models.clear();
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 9e7961172..055bee231 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -183,6 +183,11 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::
 */
 
 bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
+  if (!m->areFunctionValuesEnabled())
+  {
+    // nothing to do if no functions
+    return true;
+  }
   FirstOrderModel* f = (FirstOrderModel*)m;
   FirstOrderModelIG* fm = f->asFirstOrderModelIG();
   Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl;
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 74d8269f9..5016bd87f 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -73,6 +73,15 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
 
 }
 
+void TheoryQuantifiers::finishInit()
+{
+  // quantifiers are not evaluated in getModelValue
+  TheoryModel* tm = d_valuation.getModel();
+  Assert(tm != nullptr);
+  tm->setUnevaluatedKind(EXISTS);
+  tm->setUnevaluatedKind(FORALL);
+}
+
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
   if( n.getKind()==FORALL ){
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 4bb28fe79..4f0302bf3 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -42,6 +42,8 @@ class TheoryQuantifiers : public Theory {
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
   void addSharedTerm(TNode t) override;
   void notifyEq(TNode lhs, TNode rhs);
+  /** finish initialization */
+  void finishInit() override;
   void preRegisterTerm(TNode n) override;
   void presolve() override;
   void ppNotifyAssertions(const std::vector<Node>& assertions) override;