Unified fairness scheme for cegis unif (#1941)

2 files changed, 537 insertions, 0 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 687ed3c86..745183a6b 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1471,6 +1471,7 @@ REG1_TESTS = \
 	regress1/sygus/array_sum_2_5.sy \
 	regress1/sygus/cegar1.sy \
 	regress1/sygus/cegisunif-depth1.sy \
+	regress1/sygus/cegis-unif-inv-eq-fair.sy \
 	regress1/sygus/cggmp.sy \
 	regress1/sygus/clock-inc-tuple.sy \
 	regress1/sygus/commutative.sy \
diff --git a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
new file mode 100644
index 000000000..7d1c35234
--- /dev/null
+++ b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
@@ -0,0 +1,536 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-unif --sygus-bool-ite-return-const --sygus-out=status
+(set-logic LIA)
+
+(define-fun
+  __node_init_Sofar_0 (
+    (Sofar.usr.X@0 Bool)
+    (Sofar.usr.Sofar@0 Bool)
+    (Sofar.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and (= Sofar.usr.Sofar@0 Sofar.usr.X@0) Sofar.res.init_flag@0)
+)
+
+(define-fun
+  __node_trans_Sofar_0 (
+    (Sofar.usr.X@1 Bool)
+    (Sofar.usr.Sofar@1 Bool)
+    (Sofar.res.init_flag@1 Bool)
+    (Sofar.usr.X@0 Bool)
+    (Sofar.usr.Sofar@0 Bool)
+    (Sofar.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and
+   (= Sofar.usr.Sofar@1 (and Sofar.usr.X@1 Sofar.usr.Sofar@0))
+   (not Sofar.res.init_flag@1))
+)
+
+(define-fun
+  __node_init_excludes2_0 (
+    (excludes2.usr.X1@0 Bool)
+    (excludes2.usr.X2@0 Bool)
+    (excludes2.usr.excludes@0 Bool)
+    (excludes2.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and
+   (=
+    excludes2.usr.excludes@0
+    (not (and excludes2.usr.X1@0 excludes2.usr.X2@0)))
+   excludes2.res.init_flag@0)
+)
+
+(define-fun
+  __node_trans_excludes2_0 (
+    (excludes2.usr.X1@1 Bool)
+    (excludes2.usr.X2@1 Bool)
+    (excludes2.usr.excludes@1 Bool)
+    (excludes2.res.init_flag@1 Bool)
+    (excludes2.usr.X1@0 Bool)
+    (excludes2.usr.X2@0 Bool)
+    (excludes2.usr.excludes@0 Bool)
+    (excludes2.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and
+   (=
+    excludes2.usr.excludes@1
+    (not (and excludes2.usr.X1@1 excludes2.usr.X2@1)))
+   (not excludes2.res.init_flag@1))
+)
+
+(define-fun
+  __node_init_voiture_0 (
+    (voiture.usr.m@0 Bool)
+    (voiture.usr.s@0 Bool)
+    (voiture.usr.toofast@0 Bool)
+    (voiture.usr.stop@0 Bool)
+    (voiture.usr.bump@0 Bool)
+    (voiture.usr.dist@0 Int)
+    (voiture.usr.speed@0 Int)
+    (voiture.usr.time@0 Int)
+    (voiture.usr.move@0 Bool)
+    (voiture.usr.second@0 Bool)
+    (voiture.usr.meter@0 Bool)
+    (voiture.res.init_flag@0 Bool)
+    (voiture.res.abs_0@0 Bool)
+  ) Bool
+  
+  (and
+   (= voiture.usr.speed@0 0)
+   (= voiture.usr.toofast@0 (>= voiture.usr.speed@0 3))
+   (= voiture.usr.move@0 true)
+   (= voiture.usr.time@0 0)
+   (= voiture.usr.dist@0 0)
+   (= voiture.usr.bump@0 (= voiture.usr.dist@0 10))
+   (= voiture.usr.stop@0 (>= voiture.usr.time@0 4))
+   (=
+    voiture.res.abs_0@0
+    (and
+     (and
+      (and voiture.usr.move@0 (not voiture.usr.stop@0))
+      (not voiture.usr.toofast@0))
+     (not voiture.usr.bump@0)))
+   (= voiture.usr.second@0 false)
+   (= voiture.usr.meter@0 false)
+   voiture.res.init_flag@0)
+)
+
+(define-fun
+  __node_trans_voiture_0 (
+    (voiture.usr.m@1 Bool)
+    (voiture.usr.s@1 Bool)
+    (voiture.usr.toofast@1 Bool)
+    (voiture.usr.stop@1 Bool)
+    (voiture.usr.bump@1 Bool)
+    (voiture.usr.dist@1 Int)
+    (voiture.usr.speed@1 Int)
+    (voiture.usr.time@1 Int)
+    (voiture.usr.move@1 Bool)
+    (voiture.usr.second@1 Bool)
+    (voiture.usr.meter@1 Bool)
+    (voiture.res.init_flag@1 Bool)
+    (voiture.res.abs_0@1 Bool)
+    (voiture.usr.m@0 Bool)
+    (voiture.usr.s@0 Bool)
+    (voiture.usr.toofast@0 Bool)
+    (voiture.usr.stop@0 Bool)
+    (voiture.usr.bump@0 Bool)
+    (voiture.usr.dist@0 Int)
+    (voiture.usr.speed@0 Int)
+    (voiture.usr.time@0 Int)
+    (voiture.usr.move@0 Bool)
+    (voiture.usr.second@0 Bool)
+    (voiture.usr.meter@0 Bool)
+    (voiture.res.init_flag@0 Bool)
+    (voiture.res.abs_0@0 Bool)
+  ) Bool
+  
+  (and
+   (= voiture.usr.meter@1 (and voiture.usr.m@1 (not voiture.usr.s@1)))
+   (= voiture.usr.second@1 voiture.usr.s@1)
+   (= voiture.usr.move@1 voiture.res.abs_0@0)
+   (=
+    voiture.usr.speed@1
+    (ite
+     (or (not voiture.usr.move@1) voiture.usr.second@1)
+     0
+     (ite
+      (and voiture.usr.move@1 voiture.usr.meter@1)
+      (+ (- voiture.usr.speed@0 1) 1)
+      voiture.usr.speed@0)))
+   (= voiture.usr.toofast@1 (>= voiture.usr.speed@1 3))
+   (=
+    voiture.usr.time@1
+    (ite voiture.usr.second@1 (+ voiture.usr.time@0 1) voiture.usr.time@0))
+   (=
+    voiture.usr.dist@1
+    (ite
+     (and voiture.usr.move@1 voiture.usr.meter@1)
+     (+ voiture.usr.dist@0 1)
+     voiture.usr.dist@0))
+   (= voiture.usr.bump@1 (= voiture.usr.dist@1 10))
+   (= voiture.usr.stop@1 (>= voiture.usr.time@1 4))
+   (=
+    voiture.res.abs_0@1
+    (and
+     (and
+      (and voiture.usr.move@1 (not voiture.usr.stop@1))
+      (not voiture.usr.toofast@1))
+     (not voiture.usr.bump@1)))
+   (not voiture.res.init_flag@1))
+)
+
+(define-fun
+  __node_init_top_0 (
+    (top.usr.m@0 Bool)
+    (top.usr.s@0 Bool)
+    (top.usr.OK@0 Bool)
+    (top.res.init_flag@0 Bool)
+    (top.res.abs_0@0 Bool)
+    (top.res.abs_1@0 Bool)
+    (top.res.abs_2@0 Bool)
+    (top.res.abs_3@0 Int)
+    (top.res.abs_4@0 Int)
+    (top.res.abs_5@0 Int)
+    (top.res.abs_6@0 Bool)
+    (top.res.abs_7@0 Bool)
+    (top.res.abs_8@0 Bool)
+    (top.res.abs_9@0 Bool)
+    (top.res.abs_10@0 Bool)
+    (top.res.inst_3@0 Bool)
+    (top.res.inst_2@0 Bool)
+    (top.res.inst_1@0 Bool)
+    (top.res.inst_0@0 Bool)
+  ) Bool
+  
+  (let
+   ((X1 Bool top.res.abs_10@0))
+   (let
+    ((X2 Int top.res.abs_4@0))
+    (and
+     (= top.usr.OK@0 (=> X1 (< X2 4)))
+     (__node_init_voiture_0
+      top.usr.m@0
+      top.usr.s@0
+      top.res.abs_0@0
+      top.res.abs_1@0
+      top.res.abs_2@0
+      top.res.abs_3@0
+      top.res.abs_4@0
+      top.res.abs_5@0
+      top.res.abs_6@0
+      top.res.abs_7@0
+      top.res.abs_8@0
+      top.res.inst_3@0
+      top.res.inst_2@0)
+     (__node_init_Sofar_0 top.res.abs_9@0 top.res.abs_10@0 top.res.inst_1@0)
+     (__node_init_excludes2_0
+      top.usr.m@0
+      top.usr.s@0
+      top.res.abs_9@0
+      top.res.inst_0@0)
+     top.res.init_flag@0)))
+)
+
+(define-fun
+  __node_trans_top_0 (
+    (top.usr.m@1 Bool)
+    (top.usr.s@1 Bool)
+    (top.usr.OK@1 Bool)
+    (top.res.init_flag@1 Bool)
+    (top.res.abs_0@1 Bool)
+    (top.res.abs_1@1 Bool)
+    (top.res.abs_2@1 Bool)
+    (top.res.abs_3@1 Int)
+    (top.res.abs_4@1 Int)
+    (top.res.abs_5@1 Int)
+    (top.res.abs_6@1 Bool)
+    (top.res.abs_7@1 Bool)
+    (top.res.abs_8@1 Bool)
+    (top.res.abs_9@1 Bool)
+    (top.res.abs_10@1 Bool)
+    (top.res.inst_3@1 Bool)
+    (top.res.inst_2@1 Bool)
+    (top.res.inst_1@1 Bool)
+    (top.res.inst_0@1 Bool)
+    (top.usr.m@0 Bool)
+    (top.usr.s@0 Bool)
+    (top.usr.OK@0 Bool)
+    (top.res.init_flag@0 Bool)
+    (top.res.abs_0@0 Bool)
+    (top.res.abs_1@0 Bool)
+    (top.res.abs_2@0 Bool)
+    (top.res.abs_3@0 Int)
+    (top.res.abs_4@0 Int)
+    (top.res.abs_5@0 Int)
+    (top.res.abs_6@0 Bool)
+    (top.res.abs_7@0 Bool)
+    (top.res.abs_8@0 Bool)
+    (top.res.abs_9@0 Bool)
+    (top.res.abs_10@0 Bool)
+    (top.res.inst_3@0 Bool)
+    (top.res.inst_2@0 Bool)
+    (top.res.inst_1@0 Bool)
+    (top.res.inst_0@0 Bool)
+  ) Bool
+  
+  (let
+   ((X1 Bool top.res.abs_10@1))
+   (let
+    ((X2 Int top.res.abs_4@1))
+    (and
+     (= top.usr.OK@1 (=> X1 (< X2 4)))
+     (__node_trans_voiture_0
+      top.usr.m@1
+      top.usr.s@1
+      top.res.abs_0@1
+      top.res.abs_1@1
+      top.res.abs_2@1
+      top.res.abs_3@1
+      top.res.abs_4@1
+      top.res.abs_5@1
+      top.res.abs_6@1
+      top.res.abs_7@1
+      top.res.abs_8@1
+      top.res.inst_3@1
+      top.res.inst_2@1
+      top.usr.m@0
+      top.usr.s@0
+      top.res.abs_0@0
+      top.res.abs_1@0
+      top.res.abs_2@0
+      top.res.abs_3@0
+      top.res.abs_4@0
+      top.res.abs_5@0
+      top.res.abs_6@0
+      top.res.abs_7@0
+      top.res.abs_8@0
+      top.res.inst_3@0
+      top.res.inst_2@0)
+     (__node_trans_Sofar_0
+      top.res.abs_9@1
+      top.res.abs_10@1
+      top.res.inst_1@1
+      top.res.abs_9@0
+      top.res.abs_10@0
+      top.res.inst_1@0)
+     (__node_trans_excludes2_0
+      top.usr.m@1
+      top.usr.s@1
+      top.res.abs_9@1
+      top.res.inst_0@1
+      top.usr.m@0
+      top.usr.s@0
+      top.res.abs_9@0
+      top.res.inst_0@0)
+     (not top.res.init_flag@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.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.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.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+  ) Bool
+  
+  (let
+   ((X1 Bool top.res.abs_10))
+   (let
+    ((X2 Int top.res.abs_4))
+    (and
+     (= top.usr.OK (=> X1 (< X2 4)))
+     (__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_9 top.res.abs_10 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.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.inst_3! Bool)
+    (top.res.inst_2! Bool)
+    (top.res.inst_1! Bool)
+    (top.res.inst_0! Bool)
+  
+  ) Bool
+  
+  (let
+   ((X1 Bool top.res.abs_10!))
+   (let
+    ((X2 Int top.res.abs_4!))
+    (and
+     (= top.usr.OK! (=> X1 (< X2 4)))
+     (__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_9!
+      top.res.abs_10!
+      top.res.inst_1!
+      top.res.abs_9
+      top.res.abs_10
+      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.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)