From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Mar 2020 19:42:45 +0000 (-0500)
Subject: Do not make models for quantified function variables (#4039)
X-Git-Tag: cvc5-1.0.0~3500
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9803bedfdfe42bf472654ed8e11bcc888de5df67;p=cvc5.git

Do not make models for quantified function variables (#4039)

If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.
---

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 2b7f78008..1498e54a6 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -356,8 +356,14 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) {
 
 void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
   if( n.getKind()==APPLY_UF ){
-    if( d_models.find(n.getOperator())==d_models.end()) {
-      d_models[n.getOperator()] = new Def;
+    // cannot be a bound variable
+    Node op = n.getOperator();
+    if (op.getKind() != BOUND_VARIABLE)
+    {
+      if (d_models.find(op) == d_models.end())
+      {
+        d_models[op] = new Def;
+      }
     }
   }
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b282e6911..de2091ef6 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1860,6 +1860,7 @@ set(regress_1_tests
   regress1/sygus/issue3839-cond-rewrite.smt2
   regress1/sygus/issue3944-div-rewrite.smt2
   regress1/sygus/issue3947-agg-miniscope.smt2
+  regress1/sygus/issue3995-fmf-var-op.smt2
   regress1/sygus/issue4009-qep.smt2
   regress1/sygus/issue4025-no-rlv-cond.smt2
   regress1/sygus/large-const-simp.sy
diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
new file mode 100644
index 000000000..72ece4064
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inference --fmf-bound --uf-ho --no-bv-div-zero-const
+(set-logic ALL)
+(declare-fun a () (_ BitVec 1))
+(assert (bvsgt (bvsmod a a) #b0))
+(check-sat)