From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Apr 2020 03:02:31 +0000 (-0500)
Subject: Always assign function values in higher order (#4279)
X-Git-Tag: cvc5-1.0.0~3371
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e994acb6fe6b6128d71a1f618fb6e5629118c67;p=cvc5.git

Always assign function values in higher order (#4279)

Fixes #4277.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 844d25379..531dfa512 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -864,6 +864,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       // by default, use store axioms only if --ho-elim is set
       options::hoElimStoreAx.set(options::hoElim());
     }
+    if (!options::assignFunctionValues())
+    {
+      // must assign function values
+      options::assignFunctionValues.set(true);
+    }
     // Cannot use macros, since lambda lifting and macro elimination are inverse
     // operations.
     if (options::macrosQuant())
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index e96bee410..10e57e794 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -34,6 +34,8 @@ TheoryModel::TheoryModel(context::Context* c,
       d_using_model_core(false),
       d_enableFuncModels(enableFuncModels)
 {
+  // must use function models when ufHo is enabled
+  Assert(d_enableFuncModels || !options::ufHo());
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3c104862f..19ccc91e4 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -501,6 +501,7 @@ set(regress_0_tests
   regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
   regress0/fp/issue3536.smt2
+  regress0/fp/issue4277-assign-func.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/rti_3_5_bug_report.smt2
   regress0/fp/simple.smt2
diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2
new file mode 100644
index 000000000..5c39abc5f
--- /dev/null
+++ b/test/regress/regress0/fp/issue4277-assign-func.smt2
@@ -0,0 +1,10 @@
+; REQUIRES: symfpu
+(set-logic ALL)
+(set-option :uf-ho true)
+(set-option :assign-function-values false)
+(set-info :status sat)
+(declare-fun b () (_ BitVec 1))
+(declare-fun c () (_ BitVec 8))
+(declare-fun d () (_ BitVec 23))
+(assert (= 0 (fp.to_real (fp b c d))))
+(check-sat)