From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 16 Mar 2022 01:11:55 +0000 (-0500)
Subject: Fix getModelValue for arithmetic (#8316)
X-Git-Tag: cvc5-1.0.0~245
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a8d2407468eee50c91fc6cbe19f5edd8feeb688;p=cvc5.git

Fix getModelValue for arithmetic (#8316)

Fixes #8276.

Theory::getModelValue is used as an optimization for computing the care graph of arrays. This method was wrong for (non-linear) arithmetic when the NL extension repaired values in the model.
---

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 252dd5d54..624a7d7cd 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -353,6 +353,11 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
 }
 
 Node TheoryArith::getModelValue(TNode var) {
+  std::map<Node, Node>::iterator it = d_arithModelCache.find(var);
+  if (it != d_arithModelCache.end())
+  {
+    return it->second;
+  }
   return d_internal->getModelValue( var );
 }
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 32604095f..eaeaebdbc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -129,6 +129,7 @@ set(regress_0_tests
   regress0/arrays/issue6807-idem-rew.smt2
   regress0/arrays/issue7596-define-array-uminus.smt2
   regress0/arrays/issue8103-1-weak-equiv-models.smt2
+  regress0/arrays/issue8276-arith-getModelValue.smt2
   regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
   regress0/arrays/x2.smtv1.smt2
   regress0/arrays/x3.smtv1.smt2
diff --git a/test/regress/regress0/arrays/issue8276-arith-getModelValue.smt2 b/test/regress/regress0/arrays/issue8276-arith-getModelValue.smt2
new file mode 100644
index 000000000..c511a92a3
--- /dev/null
+++ b/test/regress/regress0/arrays/issue8276-arith-getModelValue.smt2
@@ -0,0 +1,10 @@
+(set-logic ANRA)
+(set-info :status sat)
+(declare-fun r4 () Real)
+(declare-fun r9 () Real)
+(declare-fun arr () (Array Bool (Array Real Real)))
+(declare-fun r38 () Real)
+(assert (< r38 r9))
+(assert (= 1.0 (* r4 (select (select arr true) 0.0))))
+(assert (= 0.0 (* r9 (select (select arr true) r9))))
+(check-sat)