Fix Unif+PI algorithm with symbolic unfolding (#3558)

diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 1ad33d5e7b3f5c04b8d9f66b0e05bc2f708c39cd..47975d4b7671786ce7bdb1ef2a74d774d8b2eff7 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -847,7 +847,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons,
         std::vector<Node> cechildren;
         cechildren.push_back(ce);
         Node ecurr = r == 0 ? e : er;
-        ith = d_unif->d_hd_to_pt.find(e);
+        ith = d_unif->d_hd_to_pt.find(ecurr);
         AlwaysAssert(ith != d_unif->d_hd_to_pt.end());
         cechildren.insert(
             cechildren.end(), ith->second.begin(), ith->second.end());

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ab060bb314308c6a7e6d5313dcff247c59c50e69..413875a7098d96aaa284ca20ee9860184988899c 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1798,6 +1798,7 @@ set(regress_1_tests
   regress1/sygus/uf-abduct.smt2
   regress1/sygus/unbdd_inv_gen_ex7.sy
   regress1/sygus/unbdd_inv_gen_winf1.sy
+  regress1/sygus/unifpi-solve-car_1.lus.sy
   regress1/sygus/univ_2-long-repeat.sy
   regress1/sym/q-constant.smt2
   regress1/sym/q-function.smt2

diff --git a/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy b/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy
new file mode 100644 (file)
index 0000000..38267c1
--- /dev/null
+++ b/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy
@@ -0,0 +1,557 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --sygus-grammar-cons=any-term-concise --sygus-unif-pi=complete
+
+(set-logic LIA)
+
+(define-fun
+  __node_init_Sofar_0 (
+    (Sofar.usr.X_a_0 Bool)
+    (Sofar.usr.Sofar_a_0 Bool)
+    (Sofar.res.init_flag_a_0 Bool)
+  ) Bool
+
+  (and (= Sofar.usr.Sofar_a_0 Sofar.usr.X_a_0) Sofar.res.init_flag_a_0)
+)
+
+(define-fun
+  __node_trans_Sofar_0 (
+    (Sofar.usr.X_a_1 Bool)
+    (Sofar.usr.Sofar_a_1 Bool)
+    (Sofar.res.init_flag_a_1 Bool)
+    (Sofar.usr.X_a_0 Bool)
+    (Sofar.usr.Sofar_a_0 Bool)
+    (Sofar.res.init_flag_a_0 Bool)
+  ) Bool
+
+  (and
+   (= Sofar.usr.Sofar_a_1 (and Sofar.usr.X_a_1 Sofar.usr.Sofar_a_0))
+   (not Sofar.res.init_flag_a_1))
+)
+
+(define-fun
+  __node_init_excludes2_0 (
+    (excludes2.usr.X1_a_0 Bool)
+    (excludes2.usr.X2_a_0 Bool)
+    (excludes2.usr.excludes_a_0 Bool)
+    (excludes2.res.init_flag_a_0 Bool)
+  ) Bool
+
+  (and
+   (=
+    excludes2.usr.excludes_a_0
+    (not (and excludes2.usr.X1_a_0 excludes2.usr.X2_a_0)))
+   excludes2.res.init_flag_a_0)
+)
+
+(define-fun
+  __node_trans_excludes2_0 (
+    (excludes2.usr.X1_a_1 Bool)
+    (excludes2.usr.X2_a_1 Bool)
+    (excludes2.usr.excludes_a_1 Bool)
+    (excludes2.res.init_flag_a_1 Bool)
+    (excludes2.usr.X1_a_0 Bool)
+    (excludes2.usr.X2_a_0 Bool)
+    (excludes2.usr.excludes_a_0 Bool)
+    (excludes2.res.init_flag_a_0 Bool)
+  ) Bool
+
+  (and
+   (=
+    excludes2.usr.excludes_a_1
+    (not (and excludes2.usr.X1_a_1 excludes2.usr.X2_a_1)))
+   (not excludes2.res.init_flag_a_1))
+)
+
+(define-fun
+  __node_init_voiture_0 (
+    (voiture.usr.m_a_0 Bool)
+    (voiture.usr.s_a_0 Bool)
+    (voiture.usr.toofast_a_0 Bool)
+    (voiture.usr.stop_a_0 Bool)
+    (voiture.usr.bump_a_0 Bool)
+    (voiture.usr.dist_a_0 Int)
+    (voiture.usr.speed_a_0 Int)
+    (voiture.usr.time_a_0 Int)
+    (voiture.usr.move_a_0 Bool)
+    (voiture.usr.second_a_0 Bool)
+    (voiture.usr.meter_a_0 Bool)
+    (voiture.res.init_flag_a_0 Bool)
+    (voiture.res.abs_0_a_0 Bool)
+  ) Bool
+
+  (and
+   (= voiture.usr.speed_a_0 0)
+   (= voiture.usr.toofast_a_0 (>= voiture.usr.speed_a_0 3))
+   (= voiture.usr.move_a_0 true)
+   (= voiture.usr.time_a_0 0)
+   (= voiture.usr.dist_a_0 0)
+   (= voiture.usr.bump_a_0 (= voiture.usr.dist_a_0 10))
+   (= voiture.usr.stop_a_0 (>= voiture.usr.time_a_0 4))
+   (=
+    voiture.res.abs_0_a_0
+    (and
+     (and
+      (and voiture.usr.move_a_0 (not voiture.usr.stop_a_0))
+      (not voiture.usr.toofast_a_0))
+     (not voiture.usr.bump_a_0)))
+   (= voiture.usr.second_a_0 false)
+   (= voiture.usr.meter_a_0 false)
+   voiture.res.init_flag_a_0)
+)
+
+(define-fun
+  __node_trans_voiture_0 (
+    (voiture.usr.m_a_1 Bool)
+    (voiture.usr.s_a_1 Bool)
+    (voiture.usr.toofast_a_1 Bool)
+    (voiture.usr.stop_a_1 Bool)
+    (voiture.usr.bump_a_1 Bool)
+    (voiture.usr.dist_a_1 Int)
+    (voiture.usr.speed_a_1 Int)
+    (voiture.usr.time_a_1 Int)
+    (voiture.usr.move_a_1 Bool)
+    (voiture.usr.second_a_1 Bool)
+    (voiture.usr.meter_a_1 Bool)
+    (voiture.res.init_flag_a_1 Bool)
+    (voiture.res.abs_0_a_1 Bool)
+    (voiture.usr.m_a_0 Bool)
+    (voiture.usr.s_a_0 Bool)
+    (voiture.usr.toofast_a_0 Bool)
+    (voiture.usr.stop_a_0 Bool)
+    (voiture.usr.bump_a_0 Bool)
+    (voiture.usr.dist_a_0 Int)
+    (voiture.usr.speed_a_0 Int)
+    (voiture.usr.time_a_0 Int)
+    (voiture.usr.move_a_0 Bool)
+    (voiture.usr.second_a_0 Bool)
+    (voiture.usr.meter_a_0 Bool)
+    (voiture.res.init_flag_a_0 Bool)
+    (voiture.res.abs_0_a_0 Bool)
+  ) Bool
+
+  (and
+   (= voiture.usr.meter_a_1 (and voiture.usr.m_a_1 (not voiture.usr.s_a_1)))
+   (= voiture.usr.second_a_1 voiture.usr.s_a_1)
+   (= voiture.usr.move_a_1 voiture.res.abs_0_a_0)
+   (=
+    voiture.usr.speed_a_1
+    (ite
+     (or (not voiture.usr.move_a_1) voiture.usr.second_a_1)
+     0
+     (ite
+      (and voiture.usr.move_a_1 voiture.usr.meter_a_1)
+      (+ voiture.usr.speed_a_0 1)
+      voiture.usr.speed_a_0)))
+   (= voiture.usr.toofast_a_1 (>= voiture.usr.speed_a_1 3))
+   (=
+    voiture.usr.time_a_1
+    (ite voiture.usr.second_a_1 (+ voiture.usr.time_a_0 1) voiture.usr.time_a_0))
+   (=
+    voiture.usr.dist_a_1
+    (ite
+     (and voiture.usr.move_a_1 voiture.usr.meter_a_1)
+     (+ voiture.usr.dist_a_0 1)
+     voiture.usr.dist_a_0))
+   (= voiture.usr.bump_a_1 (= voiture.usr.dist_a_1 10))
+   (= voiture.usr.stop_a_1 (>= voiture.usr.time_a_1 4))
+   (=
+    voiture.res.abs_0_a_1
+    (and
+     (and
+      (and voiture.usr.move_a_1 (not voiture.usr.stop_a_1))
+      (not voiture.usr.toofast_a_1))
+     (not voiture.usr.bump_a_1)))
+   (not voiture.res.init_flag_a_1))
+)
+
+(define-fun
+  __node_init_top_0 (
+    (top.usr.m_a_0 Bool)
+    (top.usr.s_a_0 Bool)
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+    (top.res.abs_0_a_0 Bool)
+    (top.res.abs_1_a_0 Bool)
+    (top.res.abs_2_a_0 Bool)
+    (top.res.abs_3_a_0 Int)
+    (top.res.abs_4_a_0 Int)
+    (top.res.abs_5_a_0 Int)
+    (top.res.abs_6_a_0 Bool)
+    (top.res.abs_7_a_0 Bool)
+    (top.res.abs_8_a_0 Bool)
+    (top.res.abs_9_a_0 Bool)
+    (top.res.abs_10_a_0 Bool)
+    (top.res.abs_11_a_0 Bool)
+    (top.res.inst_3_a_0 Bool)
+    (top.res.inst_2_a_0 Bool)
+    (top.res.inst_1_a_0 Bool)
+    (top.res.inst_0_a_0 Bool)
+  ) Bool
+
+  (let
+   ((X1 Int top.res.abs_3_a_0))
+   (and
+    (= top.res.abs_10_a_0 (and top.res.abs_9_a_0 (< X1 32767)))
+    (let
+     ((X2 Bool top.res.abs_11_a_0))
+     (and
+      (= top.usr.OK_a_0 (=> X2 (>= X1 0)))
+      (__node_init_voiture_0
+       top.usr.m_a_0
+       top.usr.s_a_0
+       top.res.abs_0_a_0
+       top.res.abs_1_a_0
+       top.res.abs_2_a_0
+       top.res.abs_3_a_0
+       top.res.abs_4_a_0
+       top.res.abs_5_a_0
+       top.res.abs_6_a_0
+       top.res.abs_7_a_0
+       top.res.abs_8_a_0
+       top.res.inst_3_a_0
+       top.res.inst_2_a_0)
+      (__node_init_Sofar_0
+       top.res.abs_10_a_0
+       top.res.abs_11_a_0
+       top.res.inst_1_a_0)
+      (__node_init_excludes2_0
+       top.usr.m_a_0
+       top.usr.s_a_0
+       top.res.abs_9_a_0
+       top.res.inst_0_a_0)
+      top.res.init_flag_a_0))))
+)
+
+(define-fun
+  __node_trans_top_0 (
+    (top.usr.m_a_1 Bool)
+    (top.usr.s_a_1 Bool)
+    (top.usr.OK_a_1 Bool)
+    (top.res.init_flag_a_1 Bool)
+    (top.res.abs_0_a_1 Bool)
+    (top.res.abs_1_a_1 Bool)
+    (top.res.abs_2_a_1 Bool)
+    (top.res.abs_3_a_1 Int)
+    (top.res.abs_4_a_1 Int)
+    (top.res.abs_5_a_1 Int)
+    (top.res.abs_6_a_1 Bool)
+    (top.res.abs_7_a_1 Bool)
+    (top.res.abs_8_a_1 Bool)
+    (top.res.abs_9_a_1 Bool)
+    (top.res.abs_10_a_1 Bool)
+    (top.res.abs_11_a_1 Bool)
+    (top.res.inst_3_a_1 Bool)
+    (top.res.inst_2_a_1 Bool)
+    (top.res.inst_1_a_1 Bool)
+    (top.res.inst_0_a_1 Bool)
+    (top.usr.m_a_0 Bool)
+    (top.usr.s_a_0 Bool)
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+    (top.res.abs_0_a_0 Bool)
+    (top.res.abs_1_a_0 Bool)
+    (top.res.abs_2_a_0 Bool)
+    (top.res.abs_3_a_0 Int)
+    (top.res.abs_4_a_0 Int)
+    (top.res.abs_5_a_0 Int)
+    (top.res.abs_6_a_0 Bool)
+    (top.res.abs_7_a_0 Bool)
+    (top.res.abs_8_a_0 Bool)
+    (top.res.abs_9_a_0 Bool)
+    (top.res.abs_10_a_0 Bool)
+    (top.res.abs_11_a_0 Bool)
+    (top.res.inst_3_a_0 Bool)
+    (top.res.inst_2_a_0 Bool)
+    (top.res.inst_1_a_0 Bool)
+    (top.res.inst_0_a_0 Bool)
+  ) Bool
+
+  (let
+   ((X1 Int top.res.abs_3_a_1))
+   (and
+    (= top.res.abs_10_a_1 (and top.res.abs_9_a_1 (< X1 32767)))
+    (let
+     ((X2 Bool top.res.abs_11_a_1))
+     (and
+      (= top.usr.OK_a_1 (=> X2 (>= X1 0)))
+      (__node_trans_voiture_0
+       top.usr.m_a_1
+       top.usr.s_a_1
+       top.res.abs_0_a_1
+       top.res.abs_1_a_1
+       top.res.abs_2_a_1
+       top.res.abs_3_a_1
+       top.res.abs_4_a_1
+       top.res.abs_5_a_1
+       top.res.abs_6_a_1
+       top.res.abs_7_a_1
+       top.res.abs_8_a_1
+       top.res.inst_3_a_1
+       top.res.inst_2_a_1
+       top.usr.m_a_0
+       top.usr.s_a_0
+       top.res.abs_0_a_0
+       top.res.abs_1_a_0
+       top.res.abs_2_a_0
+       top.res.abs_3_a_0
+       top.res.abs_4_a_0
+       top.res.abs_5_a_0
+       top.res.abs_6_a_0
+       top.res.abs_7_a_0
+       top.res.abs_8_a_0
+       top.res.inst_3_a_0
+       top.res.inst_2_a_0)
+      (__node_trans_Sofar_0
+       top.res.abs_10_a_1
+       top.res.abs_11_a_1
+       top.res.inst_1_a_1
+       top.res.abs_10_a_0
+       top.res.abs_11_a_0
+       top.res.inst_1_a_0)
+      (__node_trans_excludes2_0
+       top.usr.m_a_1
+       top.usr.s_a_1
+       top.res.abs_9_a_1
+       top.res.inst_0_a_1
+       top.usr.m_a_0
+       top.usr.s_a_0
+       top.res.abs_9_a_0
+       top.res.inst_0_a_0)
+      (not top.res.init_flag_a_1)))))
+)
+
+
+
+(synth-inv str_invariant(
+  (top.usr.m Bool)
+  (top.usr.s Bool)
+  (top.usr.OK Bool)
+  (top.res.init_flag Bool)
+  (top.res.abs_0 Bool)
+  (top.res.abs_1 Bool)
+  (top.res.abs_2 Bool)
+  (top.res.abs_3 Int)
+  (top.res.abs_4 Int)
+  (top.res.abs_5 Int)
+  (top.res.abs_6 Bool)
+  (top.res.abs_7 Bool)
+  (top.res.abs_8 Bool)
+  (top.res.abs_9 Bool)
+  (top.res.abs_10 Bool)
+  (top.res.abs_11 Bool)
+  (top.res.inst_3 Bool)
+  (top.res.inst_2 Bool)
+  (top.res.inst_1 Bool)
+  (top.res.inst_0 Bool)
+))
+
+
+(declare-primed-var top.usr.m Bool)
+(declare-primed-var top.usr.s Bool)
+(declare-primed-var top.usr.OK Bool)
+(declare-primed-var top.res.init_flag Bool)
+(declare-primed-var top.res.abs_0 Bool)
+(declare-primed-var top.res.abs_1 Bool)
+(declare-primed-var top.res.abs_2 Bool)
+(declare-primed-var top.res.abs_3 Int)
+(declare-primed-var top.res.abs_4 Int)
+(declare-primed-var top.res.abs_5 Int)
+(declare-primed-var top.res.abs_6 Bool)
+(declare-primed-var top.res.abs_7 Bool)
+(declare-primed-var top.res.abs_8 Bool)
+(declare-primed-var top.res.abs_9 Bool)
+(declare-primed-var top.res.abs_10 Bool)
+(declare-primed-var top.res.abs_11 Bool)
+(declare-primed-var top.res.inst_3 Bool)
+(declare-primed-var top.res.inst_2 Bool)
+(declare-primed-var top.res.inst_1 Bool)
+(declare-primed-var top.res.inst_0 Bool)
+
+(define-fun
+  init (
+    (top.usr.m Bool)
+    (top.usr.s Bool)
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    (top.res.abs_0 Bool)
+    (top.res.abs_1 Bool)
+    (top.res.abs_2 Bool)
+    (top.res.abs_3 Int)
+    (top.res.abs_4 Int)
+    (top.res.abs_5 Int)
+    (top.res.abs_6 Bool)
+    (top.res.abs_7 Bool)
+    (top.res.abs_8 Bool)
+    (top.res.abs_9 Bool)
+    (top.res.abs_10 Bool)
+    (top.res.abs_11 Bool)
+    (top.res.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+  ) Bool
+
+  (let
+   ((X1 Int top.res.abs_3))
+   (and
+    (= top.res.abs_10 (and top.res.abs_9 (< X1 32767)))
+    (let
+     ((X2 Bool top.res.abs_11))
+     (and
+      (= top.usr.OK (=> X2 (>= X1 0)))
+      (__node_init_voiture_0
+       top.usr.m
+       top.usr.s
+       top.res.abs_0
+       top.res.abs_1
+       top.res.abs_2
+       top.res.abs_3
+       top.res.abs_4
+       top.res.abs_5
+       top.res.abs_6
+       top.res.abs_7
+       top.res.abs_8
+       top.res.inst_3
+       top.res.inst_2)
+      (__node_init_Sofar_0 top.res.abs_10 top.res.abs_11 top.res.inst_1)
+      (__node_init_excludes2_0
+       top.usr.m
+       top.usr.s
+       top.res.abs_9
+       top.res.inst_0)
+      top.res.init_flag))))
+)
+
+(define-fun
+  trans (
+
+    ;; Current state.
+    (top.usr.m Bool)
+    (top.usr.s Bool)
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    (top.res.abs_0 Bool)
+    (top.res.abs_1 Bool)
+    (top.res.abs_2 Bool)
+    (top.res.abs_3 Int)
+    (top.res.abs_4 Int)
+    (top.res.abs_5 Int)
+    (top.res.abs_6 Bool)
+    (top.res.abs_7 Bool)
+    (top.res.abs_8 Bool)
+    (top.res.abs_9 Bool)
+    (top.res.abs_10 Bool)
+    (top.res.abs_11 Bool)
+    (top.res.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+
+    ;; Next state.
+    (top.usr.m! Bool)
+    (top.usr.s! Bool)
+    (top.usr.OK! Bool)
+    (top.res.init_flag! Bool)
+    (top.res.abs_0! Bool)
+    (top.res.abs_1! Bool)
+    (top.res.abs_2! Bool)
+    (top.res.abs_3! Int)
+    (top.res.abs_4! Int)
+    (top.res.abs_5! Int)
+    (top.res.abs_6! Bool)
+    (top.res.abs_7! Bool)
+    (top.res.abs_8! Bool)
+    (top.res.abs_9! Bool)
+    (top.res.abs_10! Bool)
+    (top.res.abs_11! Bool)
+    (top.res.inst_3! Bool)
+    (top.res.inst_2! Bool)
+    (top.res.inst_1! Bool)
+    (top.res.inst_0! Bool)
+
+  ) Bool
+
+  (let
+   ((X1 Int top.res.abs_3!))
+   (and
+    (= top.res.abs_10! (and top.res.abs_9! (< X1 32767)))
+    (let
+     ((X2 Bool top.res.abs_11!))
+     (and
+      (= top.usr.OK! (=> X2 (>= X1 0)))
+      (__node_trans_voiture_0
+       top.usr.m!
+       top.usr.s!
+       top.res.abs_0!
+       top.res.abs_1!
+       top.res.abs_2!
+       top.res.abs_3!
+       top.res.abs_4!
+       top.res.abs_5!
+       top.res.abs_6!
+       top.res.abs_7!
+       top.res.abs_8!
+       top.res.inst_3!
+       top.res.inst_2!
+       top.usr.m
+       top.usr.s
+       top.res.abs_0
+       top.res.abs_1
+       top.res.abs_2
+       top.res.abs_3
+       top.res.abs_4
+       top.res.abs_5
+       top.res.abs_6
+       top.res.abs_7
+       top.res.abs_8
+       top.res.inst_3
+       top.res.inst_2)
+      (__node_trans_Sofar_0
+       top.res.abs_10!
+       top.res.abs_11!
+       top.res.inst_1!
+       top.res.abs_10
+       top.res.abs_11
+       top.res.inst_1)
+      (__node_trans_excludes2_0
+       top.usr.m!
+       top.usr.s!
+       top.res.abs_9!
+       top.res.inst_0!
+       top.usr.m
+       top.usr.s
+       top.res.abs_9
+       top.res.inst_0)
+      (not top.res.init_flag!)))))
+)
+
+(define-fun
+  prop (
+    (top.usr.m Bool)
+    (top.usr.s Bool)
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    (top.res.abs_0 Bool)
+    (top.res.abs_1 Bool)
+    (top.res.abs_2 Bool)
+    (top.res.abs_3 Int)
+    (top.res.abs_4 Int)
+    (top.res.abs_5 Int)
+    (top.res.abs_6 Bool)
+    (top.res.abs_7 Bool)
+    (top.res.abs_8 Bool)
+    (top.res.abs_9 Bool)
+    (top.res.abs_10 Bool)
+    (top.res.abs_11 Bool)
+    (top.res.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+  ) Bool
+
+  top.usr.OK
+)
+
+(inv-constraint str_invariant init trans prop)
+
+(check-synth)