From f278f060c177593a1835422e688fe2a022c40e2f Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 2 Apr 2017 19:29:36 -0700 Subject: Adding a model based axiom instantiation scheme for multiplication. Merge commit for nlAlgMaster. --- test/regress/regress0/arith/bug716.0.smt2 | 3 +-- test/regress/regress0/arith/div.09.smt2 | 3 +-- test/regress/regress0/expect/scrub.01.smt.expect | 3 +-- test/regress/regress0/expect/scrub.02.smt | 3 +-- test/regress/regress0/expect/scrub.03.smt2.expect | 3 +-- test/regress/regress0/expect/scrub.04.smt2 | 3 +-- test/regress/regress0/expect/scrub.06.cvc | 5 ++--- test/regress/regress0/expect/scrub.07.sy.expect | 5 ++--- test/regress/regress0/expect/scrub.08.sy | 7 +++---- test/regress/regress0/expect/scrub.09.p | 5 ++--- 10 files changed, 15 insertions(+), 25 deletions(-) (limited to 'test/regress/regress0') diff --git a/test/regress/regress0/arith/bug716.0.smt2 b/test/regress/regress0/arith/bug716.0.smt2 index 20a5ca3f0..d5df938a7 100644 --- a/test/regress/regress0/arith/bug716.0.smt2 +++ b/test/regress/regress0/arith/bug716.0.smt2 @@ -1,6 +1,5 @@ ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 diff --git a/test/regress/regress0/arith/div.09.smt2 b/test/regress/regress0/arith/div.09.smt2 index e457734eb..1c4bbde2b 100644 --- a/test/regress/regress0/arith/div.09.smt2 +++ b/test/regress/regress0/arith/div.09.smt2 @@ -1,6 +1,5 @@ ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.01.smt.expect b/test/regress/regress0/expect/scrub.01.smt.expect index b21f2d965..4c5aa1491 100644 --- a/test/regress/regress0/expect/scrub.01.smt.expect +++ b/test/regress/regress0/expect/scrub.01.smt.expect @@ -1,6 +1,5 @@ % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXPECT: ") % EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.02.smt b/test/regress/regress0/expect/scrub.02.smt index f2e6554b7..145801619 100644 --- a/test/regress/regress0/expect/scrub.02.smt +++ b/test/regress/regress0/expect/scrub.02.smt @@ -1,6 +1,5 @@ % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXPECT: ") % EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.03.smt2.expect b/test/regress/regress0/expect/scrub.03.smt2.expect index b21f2d965..4c5aa1491 100644 --- a/test/regress/regress0/expect/scrub.03.smt2.expect +++ b/test/regress/regress0/expect/scrub.03.smt2.expect @@ -1,6 +1,5 @@ % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXPECT: ") % EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.04.smt2 b/test/regress/regress0/expect/scrub.04.smt2 index e457734eb..1c4bbde2b 100644 --- a/test/regress/regress0/expect/scrub.04.smt2 +++ b/test/regress/regress0/expect/scrub.04.smt2 @@ -1,6 +1,5 @@ ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.06.cvc b/test/regress/regress0/expect/scrub.06.cvc index b9cb1cd8a..896149334 100644 --- a/test/regress/regress0/expect/scrub.06.cvc +++ b/test/regress/regress0/expect/scrub.06.cvc @@ -1,9 +1,8 @@ % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -e '/^$/d' -% EXPECT: A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXIT: 1 n : REAL; -QUERY (n/n) = 1; \ No newline at end of file +QUERY (n/n) = 1; diff --git a/test/regress/regress0/expect/scrub.07.sy.expect b/test/regress/regress0/expect/scrub.07.sy.expect index dfcd45a8a..4c5aa1491 100644 --- a/test/regress/regress0/expect/scrub.07.sy.expect +++ b/test/regress/regress0/expect/scrub.07.sy.expect @@ -1,6 +1,5 @@ -% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% 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: ") % EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy index 3b9574cdf..7f78dbc48 100644 --- a/test/regress/regress0/expect/scrub.08.sy +++ b/test/regress/regress0/expect/scrub.08.sy @@ -1,7 +1,6 @@ ; COMMAND-LINE: --cegqi-si=all --no-dump-synth -; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; 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: ") ; EXIT: 1 @@ -10,4 +9,4 @@ (synth-fun f ((n Int)) Int) (constraint (= (/ n n) 1)) -(check-synth) \ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p index 17eef44fe..ee765a91a 100644 --- a/test/regress/regress0/expect/scrub.09.p +++ b/test/regress/regress0/expect/scrub.09.p @@ -1,7 +1,6 @@ % COMMAND-LINE: --cegqi-si=all --no-dump-synth -% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% 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: ") % EXIT: 1 -- cgit v1.2.3