diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-01-20 07:28:29 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-20 09:28:29 -0600 |
commit | e2ec4e5401eba4ef63539ddb7c1f3a54301de4b1 (patch) | |
tree | d17d5a42599eec5699d646e2ffe3150771ff7aff /test/regress/regress0 | |
parent | c8e8acd26b4bd5c47110b9448a74a45913b5518f (diff) |
SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)
This enables more strict handling of operators div, mod and abs
for Integer arithmetic logics.
More strict handling for '/' for Real arithmetic logics is more involved
and should be done in the parser -- instead at solving time, like is
currently done for checking that the application * is in the linear
fragment. The latter should be checked in the parser, too.
This is postponed to a later PR.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/arith/div-chainable.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/arith/issue1399.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/arith/mod-simp.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bug548a.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/expect/scrub.08.sy | 7 | ||||
-rw-r--r-- | test/regress/regress0/parser/linear_arithmetic_err1.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress0/parser/linear_arithmetic_err2.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress0/parser/linear_arithmetic_err3.smt2 | 11 |
8 files changed, 40 insertions, 8 deletions
diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2 index c7771d5c9..90aca07c3 100644 --- a/test/regress/regress0/arith/div-chainable.smt2 +++ b/test/regress/regress0/arith/div-chainable.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: -q ; EXPECT: sat -(set-logic QF_LIA) +(set-logic QF_NIA) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress0/arith/issue1399.smt2 b/test/regress/regress0/arith/issue1399.smt2 index 80305260e..d19addf91 100644 --- a/test/regress/regress0/arith/issue1399.smt2 +++ b/test/regress/regress0/arith/issue1399.smt2 @@ -1,4 +1,4 @@ -(set-logic LIA) +(set-logic NIA) (set-info :status sat) (define-fun findIdx ((y1 Int)(y2 Int)(k1 Int)) Int (div (* (- 7) (mod y1 (- 5))) 2)) diff --git a/test/regress/regress0/arith/mod-simp.smt2 b/test/regress/regress0/arith/mod-simp.smt2 index 1a9c50590..57ccd4652 100644 --- a/test/regress/regress0/arith/mod-simp.smt2 +++ b/test/regress/regress0/arith/mod-simp.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_LIA) +(set-logic QF_NIA) (set-info :status unsat) (declare-fun x () Int) diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2 index 581c34f2d..0c4f1f454 100644 --- a/test/regress/regress0/bug548a.smt2 +++ b/test/regress/regress0/bug548a.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --tlimit 1000 ; EXPECT: unknown -(set-logic AUFLIA) +(set-logic AUFNIA) (declare-fun f (Int) Int) diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy index 592189df2..58a8a3e76 100644 --- a/test/regress/regress0/expect/scrub.08.sy +++ b/test/regress/regress0/expect/scrub.08.sy @@ -1,8 +1,7 @@ +; REQUIRES: no-competition ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --no-sygus-repair-const -; 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 -; EXPECT: ") +; ERROR-SCRUBBER: grep -o "Symbol 'div' not declared as a variable" +; EXPECT-ERROR: Symbol 'div' not declared as a variable ; EXIT: 1 (set-logic LIA) (declare-var n Int) diff --git a/test/regress/regress0/parser/linear_arithmetic_err1.smt2 b/test/regress/regress0/parser/linear_arithmetic_err1.smt2 new file mode 100644 index 000000000..219b59d44 --- /dev/null +++ b/test/regress/regress0/parser/linear_arithmetic_err1.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: no-competition +; SCRUBBER: grep -o "Symbol 'div' not declared as a variable" +; EXPECT: Symbol 'div' not declared as a variable +; EXIT: 1 +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(check-sat-assuming ( (and (= z 0) (>= (+ (- (div 2 x) (* 2 y)) z) 1)) )) diff --git a/test/regress/regress0/parser/linear_arithmetic_err2.smt2 b/test/regress/regress0/parser/linear_arithmetic_err2.smt2 new file mode 100644 index 000000000..893708b61 --- /dev/null +++ b/test/regress/regress0/parser/linear_arithmetic_err2.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: no-competition +; SCRUBBER: grep -o "Symbol 'mod' not declared as a variable" +; EXPECT: Symbol 'mod' not declared as a variable +; EXIT: 1 +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(check-sat-assuming ( (and (= z 0) (>= (+ (- (mod 2 x) (* 2 y)) z) 1)) )) diff --git a/test/regress/regress0/parser/linear_arithmetic_err3.smt2 b/test/regress/regress0/parser/linear_arithmetic_err3.smt2 new file mode 100644 index 000000000..89748b36f --- /dev/null +++ b/test/regress/regress0/parser/linear_arithmetic_err3.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: no-competition +; SCRUBBER: grep -o "Symbol 'abs' not declared as a variable" +; EXPECT: Symbol 'abs' not declared as a variable +; EXIT: 1 +(set-option :incremental false) +(set-info :status sat) +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(check-sat-assuming ( (and (= z 0) (>= (+ (- (abs 2 x) (* 2 y)) z) 1)) )) |