From 5cafed748989602263b8ad1a27ac6b9bd159a441 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Nov 2017 15:36:38 -0500 Subject: Sygus clean main (#1297) * Remove front end hack for sygus. * Remove other hack, add sygus solution output mode. * Clang format * Minor * Fix * Minor * Remove unused field. --- test/regress/regress0/expect/scrub.07.sy | 2 +- test/regress/regress0/expect/scrub.08.sy | 2 +- test/regress/regress0/sygus/General_plus10.sy | 2 +- test/regress/regress0/sygus/array_search_2.sy | 2 +- test/regress/regress0/sygus/array_sum_2_5.sy | 2 +- test/regress/regress0/sygus/cegar1.sy | 2 +- test/regress/regress0/sygus/cggmp.sy | 2 +- test/regress/regress0/sygus/clock-inc-tuple.sy | 2 +- test/regress/regress0/sygus/commutative.sy | 2 +- test/regress/regress0/sygus/const-var-test.sy | 2 +- test/regress/regress0/sygus/constant.sy | 2 +- test/regress/regress0/sygus/dt-no-syntax.sy | 2 +- test/regress/regress0/sygus/dt-test-ns.sy | 2 +- test/regress/regress0/sygus/dup-op.sy | 2 +- test/regress/regress0/sygus/enum-test.sy | 2 +- test/regress/regress0/sygus/fg_polynomial3.sy | 2 +- test/regress/regress0/sygus/hd-01-d1-prog.sy | 2 +- test/regress/regress0/sygus/icfp_14.12.sy | 2 +- test/regress/regress0/sygus/icfp_28_10.sy | 2 +- test/regress/regress0/sygus/icfp_easy-ite.sy | 2 +- test/regress/regress0/sygus/inv-example.sy | 2 +- test/regress/regress0/sygus/let-ringer.sy | 2 +- test/regress/regress0/sygus/let-simp.sy | 2 +- test/regress/regress0/sygus/list-head-x.sy | 2 +- test/regress/regress0/sygus/max.sy | 2 +- test/regress/regress0/sygus/max2-univ.sy | 2 +- test/regress/regress0/sygus/multi-fun-polynomial2.sy | 2 +- test/regress/regress0/sygus/nflat-fwd-3.sy | 2 +- test/regress/regress0/sygus/nflat-fwd.sy | 2 +- test/regress/regress0/sygus/nia-max-square-ns.sy | 2 +- test/regress/regress0/sygus/no-flat-simp.sy | 2 +- test/regress/regress0/sygus/no-mention.sy | 2 +- test/regress/regress0/sygus/no-syntax-test-bool.sy | 2 +- test/regress/regress0/sygus/no-syntax-test-no-si.sy | 2 +- test/regress/regress0/sygus/no-syntax-test.sy | 2 +- test/regress/regress0/sygus/parity-AIG-d0.sy | 2 +- test/regress/regress0/sygus/parse-bv-let.sy | 2 +- test/regress/regress0/sygus/qe.sy | 2 +- test/regress/regress0/sygus/strings-concat-3-args.sy | 2 +- test/regress/regress0/sygus/strings-small.sy | 2 +- test/regress/regress0/sygus/strings-template-infer.sy | 2 +- test/regress/regress0/sygus/strings-trivial-simp.sy | 2 +- test/regress/regress0/sygus/strings-trivial.sy | 2 +- test/regress/regress0/sygus/strings-unconstrained.sy | 2 +- test/regress/regress0/sygus/sygus-dt.sy | 2 +- test/regress/regress0/sygus/tl-type-0.sy | 2 +- test/regress/regress0/sygus/tl-type-4x.sy | 2 +- test/regress/regress0/sygus/tl-type.sy | 2 +- test/regress/regress0/sygus/triv-type-mismatch-si.sy | 2 +- test/regress/regress0/sygus/twolets1.sy | 2 +- test/regress/regress0/sygus/twolets2-orig.sy | 2 +- test/regress/regress0/sygus/uminus_one.sy | 2 +- test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy | 2 +- test/regress/regress1/sygus/MPwL_d1s3.sy | 2 +- test/regress/regress1/sygus/VC22_a.sy | 2 +- test/regress/regress1/sygus/array_sum_dd.sy | 2 +- test/regress/regress1/sygus/hd-sdiv.sy | 2 +- test/regress/regress1/sygus/icfp_easy_mt_ite.sy | 2 +- test/regress/regress1/sygus/inv_gen_fig8.sy | 2 +- test/regress/regress1/sygus/inv_gen_n_c11.sy | 2 +- test/regress/regress1/sygus/mpg_guard1-dd.sy | 2 +- test/regress/regress1/sygus/nia-max-square.sy | 2 +- test/regress/regress1/sygus/stopwatch-bt.sy | 2 +- test/regress/regress1/sygus/three.sy | 2 +- test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy | 2 +- 65 files changed, 65 insertions(+), 65 deletions(-) (limited to 'test/regress') diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy index cf0e37c9f..79b917c7a 100644 --- a/test/regress/regress0/expect/scrub.07.sy +++ b/test/regress/regress0/expect/scrub.07.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (declare-var n Int) diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy index 7f78dbc48..360474f84 100644 --- a/test/regress/regress0/expect/scrub.08.sy +++ b/test/regress/regress0/expect/scrub.08.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy index ee26fac79..1792749e2 100755 --- a/test/regress/regress0/sygus/General_plus10.sy +++ b/test/regress/regress0/sygus/General_plus10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun fb () Int ((Start Int ((Constant Int))))) diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index e6683ced9..41346e655 100644 --- a/test/regress/regress0/sygus/array_search_2.sy +++ b/test/regress/regress0/sygus/array_search_2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy index 387ce9487..84a75d086 100644 --- a/test/regress/regress0/sygus/array_sum_2_5.sy +++ b/test/regress/regress0/sygus/array_sum_2_5.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/cegar1.sy b/test/regress/regress0/sygus/cegar1.sy index dd7f73e27..ee85db88a 100644 --- a/test/regress/regress0/sygus/cegar1.sy +++ b/test/regress/regress0/sygus/cegar1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth +; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status (set-logic LIA) (synth-inv inv-f ((x Int) (y Int))) diff --git a/test/regress/regress0/sygus/cggmp.sy b/test/regress/regress0/sygus/cggmp.sy index 1ae1f53c0..a3247e4f4 100644 --- a/test/regress/regress0/sygus/cggmp.sy +++ b/test/regress/regress0/sygus/cggmp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-inv-templ=pre --no-dump-synth +; COMMAND-LINE: --sygus-inv-templ=pre --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy index 2409b82d2..43fd7c1ac 100644 --- a/test/regress/regress0/sygus/clock-inc-tuple.sy +++ b/test/regress/regress0/sygus/clock-inc-tuple.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic ALL_SUPPORTED) (declare-var m Int) diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy index f675bddad..24201b453 100644 --- a/test/regress/regress0/sygus/commutative.sy +++ b/test/regress/regress0/sygus/commutative.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index b79b7eeec..305f5783a 100644 --- a/test/regress/regress0/sygus/const-var-test.sy +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy index 5c48f5e39..1bb3e59fa 100644 --- a/test/regress/regress0/sygus/constant.sy +++ b/test/regress/regress0/sygus/constant.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy index 0a9fb9112..f4de9b055 100644 --- a/test/regress/regress0/sygus/dt-no-syntax.sy +++ b/test/regress/regress0/sygus/dt-no-syntax.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy index 0c28769b2..a6e8ac5c2 100644 --- a/test/regress/regress0/sygus/dt-test-ns.sy +++ b/test/regress/regress0/sygus/dt-test-ns.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy index bed9972fd..e2c69282e 100644 --- a/test/regress/regress0/sygus/dup-op.sy +++ b/test/regress/regress0/sygus/dup-op.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ Start Start) x)) diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy index 7b59f5f1a..47099eeed 100644 --- a/test/regress/regress0/sygus/enum-test.sy +++ b/test/regress/regress0/sygus/enum-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (define-sort D (Enum (a b))) (define-fun f ((x D)) Int (ite (= x D::a) 3 7)) diff --git a/test/regress/regress0/sygus/fg_polynomial3.sy b/test/regress/regress0/sygus/fg_polynomial3.sy index dab92bb88..d70516bf1 100644 --- a/test/regress/regress0/sygus/fg_polynomial3.sy +++ b/test/regress/regress0/sygus/fg_polynomial3.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy index 2e6c6ef81..1379d4206 100644 --- a/test/regress/regress0/sygus/hd-01-d1-prog.sy +++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --cegqi --sygus-out=status (set-logic BV) diff --git a/test/regress/regress0/sygus/icfp_14.12.sy b/test/regress/regress0/sygus/icfp_14.12.sy index d9c19f8c1..51b86f0f5 100644 --- a/test/regress/regress0/sygus/icfp_14.12.sy +++ b/test/regress/regress0/sygus/icfp_14.12.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic BV) (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy index 74e054159..212ae37f5 100644 --- a/test/regress/regress0/sygus/icfp_28_10.sy +++ b/test/regress/regress0/sygus/icfp_28_10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic BV) diff --git a/test/regress/regress0/sygus/icfp_easy-ite.sy b/test/regress/regress0/sygus/icfp_easy-ite.sy index 248264698..f0cbbdc53 100644 --- a/test/regress/regress0/sygus/icfp_easy-ite.sy +++ b/test/regress/regress0/sygus/icfp_easy-ite.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic BV) (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy index b56425964..ff68bc06c 100644 --- a/test/regress/regress0/sygus/inv-example.sy +++ b/test/regress/regress0/sygus/inv-example.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) (declare-primed-var x Int) diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index d5d40ace4..d26edffd2 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) (synth-fun f ((x Int)) Int diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy index d07f6a717..6f9d9fff9 100644 --- a/test/regress/regress0/sygus/let-simp.sy +++ b/test/regress/regress0/sygus/let-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int ((Start Int (x diff --git a/test/regress/regress0/sygus/list-head-x.sy b/test/regress/regress0/sygus/list-head-x.sy index 8d209a9a0..6c5c1a97b 100644 --- a/test/regress/regress0/sygus/list-head-x.sy +++ b/test/regress/regress0/sygus/list-head-x.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic ALL_SUPPORTED) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index e6e3de5fc..37ed848ef 100644 --- a/test/regress/regress0/sygus/max.sy +++ b/test/regress/regress0/sygus/max.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy index 927148d81..0e00cfd9b 100644 --- a/test/regress/regress0/sygus/max2-univ.sy +++ b/test/regress/regress0/sygus/max2-univ.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status ; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes) (set-logic LIA) (synth-fun max2 ((x Int) (y Int)) Int) diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy index c238de5dd..22a2e0a4b 100644 --- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy +++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy index d3624a731..a1776cf93 100644 --- a/test/regress/regress0/sygus/nflat-fwd-3.sy +++ b/test/regress/regress0/sygus/nflat-fwd-3.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ (+ Con Con) Con) x)) diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy index 3f15d5915..da26a6c93 100644 --- a/test/regress/regress0/sygus/nflat-fwd.sy +++ b/test/regress/regress0/sygus/nflat-fwd.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x)) diff --git a/test/regress/regress0/sygus/nia-max-square-ns.sy b/test/regress/regress0/sygus/nia-max-square-ns.sy index 96baab7fe..6e7f70ff0 100644 --- a/test/regress/regress0/sygus/nia-max-square-ns.sy +++ b/test/regress/regress0/sygus/nia-max-square-ns.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth --nl-ext-tplanes +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --nl-ext-tplanes (set-logic NIA) (synth-fun max ((x Int) (y Int)) Int) diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy index af1284f13..c0f0e4c0f 100644 --- a/test/regress/regress0/sygus/no-flat-simp.sy +++ b/test/regress/regress0/sygus/no-flat-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-mention.sy b/test/regress/regress0/sygus/no-mention.sy index 60efc1b74..f964d6039 100644 --- a/test/regress/regress0/sygus/no-mention.sy +++ b/test/regress/regress0/sygus/no-mention.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun p ((x Int) (y Int)) Int) diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy index ee27b30eb..c6c9383bb 100644 --- a/test/regress/regress0/sygus/no-syntax-test-bool.sy +++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy index bd8da1900..8f333811c 100644 --- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy +++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy index 2b3d5f3e9..f27a07ee7 100644 --- a/test/regress/regress0/sygus/no-syntax-test.sy +++ b/test/regress/regress0/sygus/no-syntax-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy index 3cc577bd8..50c7d39a0 100644 --- a/test/regress/regress0/sygus/parity-AIG-d0.sy +++ b/test/regress/regress0/sygus/parity-AIG-d0.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool diff --git a/test/regress/regress0/sygus/parse-bv-let.sy b/test/regress/regress0/sygus/parse-bv-let.sy index 88ddcf139..1329918fc 100644 --- a/test/regress/regress0/sygus/parse-bv-let.sy +++ b/test/regress/regress0/sygus/parse-bv-let.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic BV) (define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32) diff --git a/test/regress/regress0/sygus/qe.sy b/test/regress/regress0/sygus/qe.sy index eaff0fd9a..5661f4469 100644 --- a/test/regress/regress0/sygus/qe.sy +++ b/test/regress/regress0/sygus/qe.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int) diff --git a/test/regress/regress0/sygus/strings-concat-3-args.sy b/test/regress/regress0/sygus/strings-concat-3-args.sy index 3c93c51d3..6628ff746 100644 --- a/test/regress/regress0/sygus/strings-concat-3-args.sy +++ b/test/regress/regress0/sygus/strings-concat-3-args.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic SLIA) (synth-fun f ((x String)) String ((Start String (ntString)) diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy index 40346bcdf..7d976ff39 100644 --- a/test/regress/regress0/sygus/strings-small.sy +++ b/test/regress/regress0/sygus/strings-small.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic SLIA) (synth-fun f ((firstname String) (lastname String)) String ((Start String (ntString)) diff --git a/test/regress/regress0/sygus/strings-template-infer.sy b/test/regress/regress0/sygus/strings-template-infer.sy index 498e713e8..13c4d7dac 100644 --- a/test/regress/regress0/sygus/strings-template-infer.sy +++ b/test/regress/regress0/sygus/strings-template-infer.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic SLIA) (define-fun cA ((x String) (y String)) String (str.++ (str.++ x "A") y)) diff --git a/test/regress/regress0/sygus/strings-trivial-simp.sy b/test/regress/regress0/sygus/strings-trivial-simp.sy index d37ac8bf4..f5e41a8f5 100644 --- a/test/regress/regress0/sygus/strings-trivial-simp.sy +++ b/test/regress/regress0/sygus/strings-trivial-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic SLIA) (synth-fun f ((name String)) String diff --git a/test/regress/regress0/sygus/strings-trivial.sy b/test/regress/regress0/sygus/strings-trivial.sy index f4847922d..9af0a1bb1 100644 --- a/test/regress/regress0/sygus/strings-trivial.sy +++ b/test/regress/regress0/sygus/strings-trivial.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic SLIA) (synth-fun f ((name String)) String diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy index 38e69e337..39c392487 100644 --- a/test/regress/regress0/sygus/strings-unconstrained.sy +++ b/test/regress/regress0/sygus/strings-unconstrained.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic SLIA) (synth-fun f ((firstname String) (lastname String)) String ((Start String (ntString)) diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy index 59560ed61..d496e3fdc 100644 --- a/test/regress/regress0/sygus/sygus-dt.sy +++ b/test/regress/regress0/sygus/sygus-dt.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/tl-type-0.sy b/test/regress/regress0/sygus/tl-type-0.sy index ef046c8e0..ceda89d78 100644 --- a/test/regress/regress0/sygus/tl-type-0.sy +++ b/test/regress/regress0/sygus/tl-type-0.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Term Term))) diff --git a/test/regress/regress0/sygus/tl-type-4x.sy b/test/regress/regress0/sygus/tl-type-4x.sy index a18d13052..bf8eee5ee 100644 --- a/test/regress/regress0/sygus/tl-type-4x.sy +++ b/test/regress/regress0/sygus/tl-type-4x.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int (Term (+ Start Start))) diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy index a6980425a..6f25a570e 100644 --- a/test/regress/regress0/sygus/tl-type.sy +++ b/test/regress/regress0/sygus/tl-type.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int (Term (+ Start Start))) diff --git a/test/regress/regress0/sygus/triv-type-mismatch-si.sy b/test/regress/regress0/sygus/triv-type-mismatch-si.sy index e2935af51..37c5a7f53 100644 --- a/test/regress/regress0/sygus/triv-type-mismatch-si.sy +++ b/test/regress/regress0/sygus/triv-type-mismatch-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun R ((y Int)) Bool) diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy index b016872b4..06d2ecb71 100644 --- a/test/regress/regress0/sygus/twolets1.sy +++ b/test/regress/regress0/sygus/twolets1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) ;; f1 is x plus 2 ;; f2 is 2x plus 5 diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy index 70d1ffa02..50f7ad544 100644 --- a/test/regress/regress0/sygus/twolets2-orig.sy +++ b/test/regress/regress0/sygus/twolets2-orig.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun f1 ((x Int)) Int ( diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy index e98be942b..94040bf45 100644 --- a/test/regress/regress0/sygus/uminus_one.sy +++ b/test/regress/regress0/sygus/uminus_one.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((- 1))))) (declare-var x Int) diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy index 300b6b65c..d45cec38b 100644 --- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy +++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun inv ((x Int)) Bool diff --git a/test/regress/regress1/sygus/MPwL_d1s3.sy b/test/regress/regress1/sygus/MPwL_d1s3.sy index b5b848848..5178cf86b 100644 --- a/test/regress/regress1/sygus/MPwL_d1s3.sy +++ b/test/regress/regress1/sygus/MPwL_d1s3.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (define-fun get-y ((currPoint Int)) Int diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy index 75bed6a28..32e4723aa 100644 --- a/test/regress/regress1/sygus/VC22_a.sy +++ b/test/regress/regress1/sygus/VC22_a.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun f ((x1 Int) (x2 Int)) Int diff --git a/test/regress/regress1/sygus/array_sum_dd.sy b/test/regress/regress1/sygus/array_sum_dd.sy index dacd7347d..6d3354d2d 100644 --- a/test/regress/regress1/sygus/array_sum_dd.sy +++ b/test/regress/regress1/sygus/array_sum_dd.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun findSum ( (y1 Int) (y2 Int) )Int ( (Start Int ( 0 1 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) diff --git a/test/regress/regress1/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy index 019b48a1c..37e1daf88 100644 --- a/test/regress/regress1/sygus/hd-sdiv.sy +++ b/test/regress/regress1/sygus/hd-sdiv.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=none --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --sygus-out=status (set-logic BV) (define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001)) diff --git a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy b/test/regress/regress1/sygus/icfp_easy_mt_ite.sy index b7428fd51..799633fa3 100644 --- a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy +++ b/test/regress/regress1/sygus/icfp_easy_mt_ite.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic BV) (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) diff --git a/test/regress/regress1/sygus/inv_gen_fig8.sy b/test/regress/regress1/sygus/inv_gen_fig8.sy index 5496f3c0a..19c36e4dc 100644 --- a/test/regress/regress1/sygus/inv_gen_fig8.sy +++ b/test/regress/regress1/sygus/inv_gen_fig8.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun inv ((l Int)) Bool ( diff --git a/test/regress/regress1/sygus/inv_gen_n_c11.sy b/test/regress/regress1/sygus/inv_gen_n_c11.sy index 946f284cb..9e04682a5 100644 --- a/test/regress/regress1/sygus/inv_gen_n_c11.sy +++ b/test/regress/regress1/sygus/inv_gen_n_c11.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun inv ((i Int) (l Int)) Bool ( diff --git a/test/regress/regress1/sygus/mpg_guard1-dd.sy b/test/regress/regress1/sygus/mpg_guard1-dd.sy index e574f7eb6..31800a36f 100644 --- a/test/regress/regress1/sygus/mpg_guard1-dd.sy +++ b/test/regress/regress1/sygus/mpg_guard1-dd.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun eq1 ( (x Int) (y Int) ) Int diff --git a/test/regress/regress1/sygus/nia-max-square.sy b/test/regress/regress1/sygus/nia-max-square.sy index 5858af98a..e023e837b 100644 --- a/test/regress/regress1/sygus/nia-max-square.sy +++ b/test/regress/regress1/sygus/nia-max-square.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth --nl-ext-tplanes +; COMMAND-LINE: --sygus-out=status --nl-ext-tplanes (set-logic NIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress1/sygus/stopwatch-bt.sy b/test/regress/regress1/sygus/stopwatch-bt.sy index 016280521..291ae6099 100644 --- a/test/regress/regress1/sygus/stopwatch-bt.sy +++ b/test/regress/regress1/sygus/stopwatch-bt.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth +; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status (set-logic LIA) (define-fun diff --git a/test/regress/regress1/sygus/three.sy b/test/regress/regress1/sygus/three.sy index 6e2ce3a2c..831e5beb1 100644 --- a/test/regress/regress1/sygus/three.sy +++ b/test/regress/regress1/sygus/three.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy index f840fa519..73d410d51 100644 --- a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy +++ b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --no-dump-synth +; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun inv ((i Int) (y Int) (l Int)) Bool ( -- cgit v1.2.3