From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 27 May 2019 23:36:17 +0000 (-0700)
Subject: Avoid substituting Boolean term variables (#3022)
X-Git-Tag: cvc5-1.0.0~4137
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=60173f62a82b4d71f2fbac51880d44d883ae5109;p=cvc5.git

Avoid substituting Boolean term variables (#3022)

Fixes #3020. Boolean terms that appear in other terms, e.g. a Boolean
array index, are replaced by `BOOLEAN_TERM_VARIABLE`s to make sure that
they are handled properly in theory combination. When doing this
replacement, an equality of the form `(= <Boolean term> <Boolean term
variable)` is added to the assertions. The problem was that
`Theory::ppAssert()` would derive a substitution when this equality was
registered. The commit fixes the problem by not allowing to add
substitutions for `BOOLEAN_TERM_VARIABLE`s.
---

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 5108e312a..a4b9d1ddf 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -295,13 +295,15 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in,
     // 2) x is not in the term t
     // 3) x : T and t : S, then S <: T
     if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
-        && (in[1].getType()).isSubtypeOf(in[0].getType()))
+        && (in[1].getType()).isSubtypeOf(in[0].getType())
+        && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
     {
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
     if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
-        && (in[0].getType()).isSubtypeOf(in[1].getType()))
+        && (in[0].getType()).isSubtypeOf(in[1].getType())
+        && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
     {
       outSubstitutions.addSubstitution(in[1], in[0]);
       return PP_ASSERT_STATUS_SOLVED;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 565c45eb7..261f8e19c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -35,6 +35,7 @@ set(regress_0_tests
   regress0/arrays/bool-array.smt2
   regress0/arrays/bug272.minimized.smt
   regress0/arrays/bug272.smt
+  regress0/arrays/bug3020.smt2
   regress0/arrays/bug637.delta.smt2
   regress0/arrays/constarr.cvc
   regress0/arrays/constarr.smt2
diff --git a/test/regress/regress0/arrays/bug3020.smt2 b/test/regress/regress0/arrays/bug3020.smt2
new file mode 100644
index 000000000..b5a88700b
--- /dev/null
+++ b/test/regress/regress0/arrays/bug3020.smt2
@@ -0,0 +1,16 @@
+(set-info :status sat)
+(set-logic QF_ABV)
+(declare-const A (Array Bool Bool))
+(declare-const B (Array Bool Bool))
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+(declare-const b3 Bool)
+(declare-const b4 Bool)
+(assert (= A (store B b1 b2)))
+(assert (= b3 (select A (select B b2))))
+(assert (=> b1 b2))
+(assert (not (and b2 b3)))
+(assert (=> b3 b1))
+(assert (= b4 (select B b2)))
+(assert (xor b4 b2))
+(check-sat)