From 4a8d2407468eee50c91fc6cbe19f5edd8feeb688 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Mar 2022 20:11:55 -0500 Subject: [PATCH] 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. --- src/theory/arith/theory_arith.cpp | 5 +++++ test/regress/CMakeLists.txt | 1 + .../regress0/arrays/issue8276-arith-getModelValue.smt2 | 10 ++++++++++ 3 files changed, 16 insertions(+) create mode 100644 test/regress/regress0/arrays/issue8276-arith-getModelValue.smt2 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::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) -- 2.30.2