Support sygus version 2.1 command assume (#7081)

Adds support for global assumptions in sygus files.

Also guards against cases of declare-const, which should be prohibited in sygus.

4 files changed, 175 insertions, 5 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fd734b321..90ad99e70 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1241,6 +1241,7 @@ set(regress_0_tests
   regress0/strings/unicode-esc.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
+  regress0/sygus/assume-simple.sy
   regress0/sygus/array-grammar-select.sy
   regress0/sygus/ccp16.lus.sy
   regress0/sygus/cegqi-si-string-triv-2fun.sy
@@ -2398,6 +2399,7 @@ set(regress_1_tests
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
   regress1/sygus/replicate-mod.sy
+  regress1/sygus/replicate-mod-assume.sy
   regress1/sygus/rex-strings-alarm.sy
   regress1/sygus/sets-pred-test.sy
   regress1/sygus/simple-regexp.sy
diff --git a/test/regress/regress0/sygus/assume-simple.sy b/test/regress/regress0/sygus/assume-simple.sy
new file mode 100644
index 000000000..58f3753d8
--- /dev/null
+++ b/test/regress/regress0/sygus/assume-simple.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+  ((Start Int))
+  ((Start Int (x 0 1 (+ Start Start)))))
+(declare-var y Int)
+(assume (>= y 0))
+(constraint (>= (f y) 0))
+(constraint (>= (f y) y))
+; lambda x. x is a valid solution
+(check-synth)
diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
index 6a149cc71..cf8e4da31 100644
--- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
+++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
@@ -1,6 +1,6 @@
 ; REQUIRES: no-competition
 ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
-; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type
+; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:78.19: number of arguments does not match the constructor type
 ; EXPECT-ERROR:
 ; EXPECT-ERROR: (Op2 <O2> <F>)
 ; EXPECT-ERROR: ^
@@ -31,8 +31,6 @@
 )
 
 ; Trace Length.
-(declare-const tn Int)
-(assert (= tn 2))
 
 ;cTrace Declaration (trace_index, variable_index)
 (define-fun val ((i Int) (x Var)) Bool
@@ -44,7 +42,7 @@
 
 ;cpLTL Semantics
 (define-fun-rec holds ((f Formula) (t Time)) Bool
-  (and (<= 0 t tn)
+  (and (<= 0 t 2)
        (match f (
          ((P i) (val t i))
 
@@ -54,7 +52,7 @@
 
              (Y (and (< 0 t) (holds g (- t 1))))
 
-             (G (and (holds g t) (or (= t tn) (holds f (+ t 1)))))
+             (G (and (holds g t) (or (= t 2) (holds f (+ t 1)))))
 
              (H (and (holds g t) (or (= t 0) (holds f (- t 1)))))
           )))
diff --git a/test/regress/regress1/sygus/replicate-mod-assume.sy b/test/regress/regress1/sygus/replicate-mod-assume.sy
new file mode 100644
index 000000000..c10cab2f5
--- /dev/null
+++ b/test/regress/regress1/sygus/replicate-mod-assume.sy
@@ -0,0 +1,157 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+(synth-fun fr0 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr1 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr10 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr11 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr12 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr13 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr14 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr15 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr16 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr17 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr18 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr19 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr2 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr20 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr21 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr22 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr23 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr24 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr25 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr26 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr27 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr28 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr29 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr3 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr30 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr31 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr32 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr33 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr34 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr35 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr36 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr4 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr5 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr6 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr7 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr8 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr9 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m0 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m1 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m10 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m11 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m12 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m13 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m14 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m15 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m16 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m17 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m2 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m3 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m4 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m5 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m6 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m7 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m8 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m9 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun p0 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p1 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p2 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p3 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p4 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p5 ((_v Int) (n Int) (x Int)) Int)
+(declare-var n Int)
+(declare-var x Int)
+(declare-var x10 Int)
+(declare-var x11 Int)
+(declare-var x14 Int)
+(declare-var x15 Int)
+(declare-var x2 Int)
+(declare-var x3 Int)
+(declare-var x6 Int)
+(declare-var x7 Int)
+(declare-var _v Int)
+(assume (and (= false (<= n 0)) (>= n 0)))
+(constraint (>= (p4 _v n x) 0))
+(constraint (and (and (and (>= (m6 _v n x) 0) (>= (m8 _v n x) 0)) (>= (m9 _v n x) 0)) (= (m6 _v n x) (+ (m8 _v n x) (m9 _v n x)))))
+(constraint (and (and (and (>= (fr17 _v n x) 0) (>= (fr19 _v n x) 0)) (>= (fr20 _v n x) 0)) (= (fr17 _v n x) (+ (fr19 _v n x) (fr20 _v n x)))))
+(constraint (and (and (and (>= (fr15 _v n x) 0) (>= (fr17 _v n x) 0)) (>= (fr18 _v n x) 0)) (= (fr15 _v n x) (+ (fr17 _v n x) (fr18 _v n x)))))
+(constraint (and (and (and (>= (m1 _v n x) 0) (>= (m6 _v n x) 0)) (>= (m7 _v n x) 0)) (= (m1 _v n x) (+ (m6 _v n x) (m7 _v n x)))))
+(constraint (and (and (and (>= (fr13 _v n x) 0) (>= (fr15 _v n x) 0)) (>= (fr16 _v n x) 0)) (= (fr13 _v n x) (+ (fr15 _v n x) (fr16 _v n x)))))
+(constraint (and (and (and (>= (fr12 _v n x) 0) (>= (fr13 _v n x) 0)) (>= (fr14 _v n x) 0)) (= (fr12 _v n x) (+ (fr13 _v n x) (fr14 _v n x)))))
+(constraint (and (and (and (and (and (and (= (+ (+ (+ 0 (p1 _v n x)) (fr1 _v n x)) 0) (+ (+ (+ 0 0) (fr12 _v n x)) 0)) (>= (fr1 _v n x) 0)) (>= (fr12 _v n x) 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)))
+(constraint (=> (and (and (= false (<= n 0)) (= _v x)) (>= n 0)) (>= 0 (+ (p4 _v n x) (- (+ (fr18 _v n x) 0))))))
+(constraint (>= 0 (- (+ (fr14 _v n x) 0))))
+(constraint (>= (p5 _v n x) (p4 _v n x)))
+(constraint (>= (p5 _v n x) 0))
+(constraint (and (and (and (>= (m10 _v n x) 0) (>= (m12 _v n x) 0)) (>= (m13 _v n x) 0)) (= (m10 _v n x) (+ (m12 _v n x) (m13 _v n x)))))
+(constraint (and (and (and (>= (fr25 _v n x) 0) (>= (fr27 _v n x) 0)) (>= (fr28 _v n x) 0)) (= (fr25 _v n x) (+ (fr27 _v n x) (fr28 _v n x)))))
+(constraint (and (and (and (>= (fr23 _v n x) 0) (>= (fr25 _v n x) 0)) (>= (fr26 _v n x) 0)) (= (fr23 _v n x) (+ (fr25 _v n x) (fr26 _v n x)))))
+(constraint (and (and (and (>= (m7 _v n x) 0) (>= (m10 _v n x) 0)) (>= (m11 _v n x) 0)) (= (m7 _v n x) (+ (m10 _v n x) (m11 _v n x)))))
+(constraint (and (and (and (>= (fr21 _v n x) 0) (>= (fr23 _v n x) 0)) (>= (fr24 _v n x) 0)) (= (fr21 _v n x) (+ (fr23 _v n x) (fr24 _v n x)))))
+(constraint (and (and (and (>= (- (fr16 _v n x) 1) 0) (>= (fr21 _v n x) 0)) (>= (fr22 _v n x) 0)) (= (- (fr16 _v n x) 1) (+ (fr21 _v n x) (fr22 _v n x)))))
+(constraint (=> false (>= 0 (- (+ (fr26 _v n x) 0)))))
+(constraint (and (and (and (>= (m14 _v n x) 0) (>= (m16 _v n x) 0)) (>= (m17 _v n x) 0)) (= (m14 _v n x) (+ (m16 _v n x) (m17 _v n x)))))
+(constraint (and (and (and (>= (fr33 _v n x) 0) (>= (fr35 _v n x) 0)) (>= (fr36 _v n x) 0)) (= (fr33 _v n x) (+ (fr35 _v n x) (fr36 _v n x)))))
+(constraint (and (and (and (>= (fr31 _v n x) 0) (>= (fr33 _v n x) 0)) (>= (fr34 _v n x) 0)) (= (fr31 _v n x) (+ (fr33 _v n x) (fr34 _v n x)))))
+(constraint (and (and (and (>= (m13 _v n x) 0) (>= (m14 _v n x) 0)) (>= (m15 _v n x) 0)) (= (m13 _v n x) (+ (m14 _v n x) (m15 _v n x)))))
+(constraint (and (and (and (>= (fr29 _v n x) 0) (>= (fr31 _v n x) 0)) (>= (fr32 _v n x) 0)) (= (fr29 _v n x) (+ (fr31 _v n x) (fr32 _v n x)))))
+(constraint (and (and (and (>= (fr28 _v n x) 0) (>= (fr29 _v n x) 0)) (>= (fr30 _v n x) 0)) (= (fr28 _v n x) (+ (fr29 _v n x) (fr30 _v n x)))))
+(check-synth)