From e2ec4e5401eba4ef63539ddb7c1f3a54301de4b1 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 20 Jan 2021 07:28:29 -0800 Subject: 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. --- test/regress/CMakeLists.txt | 3 +++ test/regress/regress0/arith/div-chainable.smt2 | 2 +- test/regress/regress0/arith/issue1399.smt2 | 2 +- test/regress/regress0/arith/mod-simp.smt2 | 2 +- test/regress/regress0/bug548a.smt2 | 2 +- test/regress/regress0/expect/scrub.08.sy | 7 +++---- test/regress/regress0/parser/linear_arithmetic_err1.smt2 | 11 +++++++++++ test/regress/regress0/parser/linear_arithmetic_err2.smt2 | 11 +++++++++++ test/regress/regress0/parser/linear_arithmetic_err3.smt2 | 11 +++++++++++ test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 | 2 +- test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 | 2 +- test/regress/regress1/quantifiers/issue5484-qe.smt2 | 3 ++- test/regress/regress1/quantifiers/issue5484b-qe.smt2 | 3 ++- test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 | 2 +- test/regress/regress2/sygus/three.sy | 2 +- 15 files changed, 51 insertions(+), 14 deletions(-) create mode 100644 test/regress/regress0/parser/linear_arithmetic_err1.smt2 create mode 100644 test/regress/regress0/parser/linear_arithmetic_err2.smt2 create mode 100644 test/regress/regress0/parser/linear_arithmetic_err3.smt2 (limited to 'test/regress') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d35758d5c..328f7df8c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -722,6 +722,9 @@ set(regress_0_tests regress0/parser/force_logic_set_logic.smt2 regress0/parser/force_logic_success.smt2 regress0/parser/issue5163.smt2 + regress0/parser/linear_arithmetic_err1.smt2 + regress0/parser/linear_arithmetic_err2.smt2 + regress0/parser/linear_arithmetic_err3.smt2 regress0/parser/shadow_fun_symbol_all.smt2 regress0/parser/shadow_fun_symbol_nirat.smt2 regress0/parser/strings20.smt2 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)) )) diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 index dd9cb6886..efcae64bc 100644 --- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat -(set-logic UFLIA) +(set-logic UFNIA) (set-info :status sat) (define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool ( or diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 index ea5a5e4b7..32e9d4178 100644 --- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat -(set-logic UFLIA) +(set-logic UFNIA) (set-info :status sat) (define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool ( or diff --git a/test/regress/regress1/quantifiers/issue5484-qe.smt2 b/test/regress/regress1/quantifiers/issue5484-qe.smt2 index c2499ed16..9fcc7dcba 100644 --- a/test/regress/regress1/quantifiers/issue5484-qe.smt2 +++ b/test/regress/regress1/quantifiers/issue5484-qe.smt2 @@ -1,7 +1,8 @@ +; COMMAND-LINE: -q ; SCRUBBER: sed 's/(.*)/()/g' ; EXPECT: () ; EXIT: 0 -(set-logic LIA) +(set-logic NIA) (declare-fun v9 () Bool) (declare-fun v18 () Bool) (declare-fun i2 () Int) diff --git a/test/regress/regress1/quantifiers/issue5484b-qe.smt2 b/test/regress/regress1/quantifiers/issue5484b-qe.smt2 index 86f999504..754603135 100644 --- a/test/regress/regress1/quantifiers/issue5484b-qe.smt2 +++ b/test/regress/regress1/quantifiers/issue5484b-qe.smt2 @@ -1,7 +1,8 @@ +; COMMAND-LINE: -q ; SCRUBBER: sed 's/(.*)/()/g' ; EXPECT: () ; EXIT: 0 -(set-logic LIA) +(set-logic NIA) (declare-fun v0 () Bool) (declare-fun v1 () Bool) (declare-fun v2 () Bool) diff --git a/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 b/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 index bd42e3596..62babf518 100644 --- a/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 +++ b/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.6) -(set-logic LIA) +(set-logic NIA) (set-info :status unsat) (declare-fun c_main_~x~0 () Int) (declare-fun c_main_~y~0 () Int) diff --git a/test/regress/regress2/sygus/three.sy b/test/regress/regress2/sygus/three.sy index 44974caf1..239f7f498 100644 --- a/test/regress/regress2/sygus/three.sy +++ b/test/regress/regress2/sygus/three.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -(set-logic LIA) +(set-logic NIA) (synth-fun f ((x Int)) Int ((Start Int)) -- cgit v1.2.3