From f3ecc4bfe17776d08efbbb5ed76a5879efa419ca Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Wed, 14 Apr 2021 07:36:58 -0700
Subject: Merge equivalent sub-obligations instead of discarding them. (#6353)

This PR modifies the behavior of the reconstruction algorithm when the term to reconstruct contains two or more equivalent sub-terms, but one is easier to reconstruct than the others. Since we do not know which one is easier to reconstruct by matching, we match against all sub-terms. If a solution is found for one sub-term, we use it to solve the others.
---
 test/regress/CMakeLists.txt               |  1 +
 test/regress/regress1/sygus/eq-sub-obs.sy | 22 ++++++++++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 test/regress/regress1/sygus/eq-sub-obs.sy

(limited to 'test')

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5c3ceec21..710c06f96 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2170,6 +2170,7 @@ set(regress_1_tests
   regress1/sygus/double.sy
   regress1/sygus/dt-test-ns.sy
   regress1/sygus/dup-op.sy
+  regress1/sygus/eq-sub-obs.sy
   regress1/sygus/error1-dt.sy
   regress1/sygus/eval-uc.sy
   regress1/sygus/extract.sy
diff --git a/test/regress/regress1/sygus/eq-sub-obs.sy b/test/regress/regress1/sygus/eq-sub-obs.sy
new file mode 100644
index 000000000..4c24a498d
--- /dev/null
+++ b/test/regress/regress1/sygus/eq-sub-obs.sy
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --sygus-si=all  --sygus-out=status
+; EXPECT: unsat
+
+; This regression tests the behavior of the reconstruction algorithm when the
+; term to reconstruct contains two equivalent sub-terms, but one is easier to
+; reconstruct than the other.
+
+(set-logic UF)
+
+(synth-fun f ((p Bool) (q Bool) (r Bool)) Bool
+  ((Start Bool))
+  ((Start Bool (true false p q r (not Start) (and Start Start) (or Start Start)))))
+
+(define-fun eqReduce ((p Bool) (q Bool)) Bool (or (and p q) (and (not p) (not q))))
+
+(declare-var p Bool)
+(declare-var q Bool)
+(declare-var r Bool)
+
+(constraint (= (f p q r) (and (= (and p q) (and q r)) (eqReduce (and p q) (and q r)))))
+
+(check-synth)
-- 
cgit v1.2.3