From 1e7807069e07a710bafa83fc7412c3ac164249b8 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 10 Jan 2017 17:51:14 -0800 Subject: [PATCH] Adding regression test scrubbing. --- src/printer/cvc/cvc_printer.cpp | 3 + src/theory/arith/arith_rewriter.cpp | 7 +- src/theory/rewriter.cpp | 2 +- src/theory/rewriter.h | 2 +- test/Makefile.am | 1 + test/regress/regress0/Makefile.am | 2 +- test/regress/regress0/arith/Makefile.am | 8 +- test/regress/regress0/arith/bug716.0.smt2 | 662 ++++++++++++++++++ test/regress/regress0/arith/bug716.1.cvc | 6 + test/regress/regress0/arith/div.09.smt2 | 3 +- test/regress/regress0/expect/Makefile.am | 44 ++ test/regress/regress0/expect/README | 1 + test/regress/regress0/expect/scrub.01.smt | 7 + .../regress0/expect/scrub.01.smt.expect | 6 + test/regress/regress0/expect/scrub.02.smt | 13 + test/regress/regress0/expect/scrub.03.smt2 | 9 + .../regress0/expect/scrub.03.smt2.expect | 6 + test/regress/regress0/expect/scrub.04.smt2 | 15 + test/regress/regress0/expect/scrub.06.cvc | 9 + test/regress/regress0/expect/scrub.07.sy | 7 + .../regress0/expect/scrub.07.sy.expect | 6 + test/regress/regress0/expect/scrub.08.sy | 13 + test/regress/regress0/expect/scrub.09.p | 11 + test/regress/run_regression | 25 +- 24 files changed, 854 insertions(+), 14 deletions(-) create mode 100644 test/regress/regress0/arith/bug716.0.smt2 create mode 100644 test/regress/regress0/arith/bug716.1.cvc create mode 100644 test/regress/regress0/expect/Makefile.am create mode 100644 test/regress/regress0/expect/README create mode 100644 test/regress/regress0/expect/scrub.01.smt create mode 100644 test/regress/regress0/expect/scrub.01.smt.expect create mode 100644 test/regress/regress0/expect/scrub.02.smt create mode 100644 test/regress/regress0/expect/scrub.03.smt2 create mode 100644 test/regress/regress0/expect/scrub.03.smt2.expect create mode 100644 test/regress/regress0/expect/scrub.04.smt2 create mode 100644 test/regress/regress0/expect/scrub.06.cvc create mode 100644 test/regress/regress0/expect/scrub.07.sy create mode 100644 test/regress/regress0/expect/scrub.07.sy.expect create mode 100644 test/regress/regress0/expect/scrub.08.sy create mode 100644 test/regress/regress0/expect/scrub.09.p diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 58d0ea6c0..a9eab4a8c 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -507,14 +507,17 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo opType = PREFIX; break; case kind::DIVISION: + case kind::DIVISION_TOTAL: op << '/'; opType = INFIX; break; case kind::INTS_DIVISION: + case kind::INTS_DIVISION_TOTAL: op << "DIV"; opType = INFIX; break; case kind::INTS_MODULUS: + case kind::INTS_MODULUS_TOTAL: op << "MOD"; opType = INFIX; break; diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index e53e2ee97..642216b40 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -19,7 +19,7 @@ #include #include -#include "base/output.h" +#include "smt/logic_exception.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" @@ -31,7 +31,8 @@ namespace arith { bool ArithRewriter::isAtom(TNode n) { Kind k = n.getKind(); - return arith::isRelationOperator(k) || k == kind::IS_INTEGER || k == kind::DIVISIBLE; + return arith::isRelationOperator(k) || k == kind::IS_INTEGER + || k == kind::DIVISIBLE; } RewriteResponse ArithRewriter::rewriteConstant(TNode t){ @@ -211,7 +212,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ ss << "The POW(^) operator can only be used with a natural number "; ss << "in the exponent. Exception occured in:" << std::endl; ss << " " << t; - throw Exception(ss.str()); + throw LogicException(ss.str()); } default: Unreachable(); diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 18ded60a8..87080ec18 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -84,7 +84,7 @@ struct RewriteStackElement { } }; -Node Rewriter::rewrite(TNode node) throw (UnsafeInterruptException){ +Node Rewriter::rewrite(TNode node) { return rewriteTo(theoryOf(node), node); } diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index fc53121e4..aed93a451 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -107,7 +107,7 @@ public: * Rewrites the node using theoryOf() to determine which rewriter to * use on the node. */ - static Node rewrite(TNode node) throw (UnsafeInterruptException); + static Node rewrite(TNode node); /** * Garbage collects the rewrite caches. diff --git a/test/Makefile.am b/test/Makefile.am index b2df85e97..89ac66a3a 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -39,6 +39,7 @@ subdirs_to_check = \ regress/regress0/bv/core \ regress/regress0/datatypes \ regress/regress0/decision \ + regress/regress0/expect \ regress/regress0/fmf \ regress/regress0/lemmas \ regress/regress0/parser \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index d202e78a3..20de7a97c 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets rels parser sygus sep +SUBDIRS = . expect arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets rels parser sygus sep DIST_SUBDIRS = $(SUBDIRS) # don't override a BINARY imported from a personal.mk diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 8a7b19461..048effcf1 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -48,7 +48,10 @@ TESTS = \ miplibtrick.smt \ bug547.1.smt2 \ bug547.2.smt2 \ - bug569.smt2 + bug569.smt2 \ + div.09.smt2 \ + bug716.0.smt2 \ + bug716.1.cvc # problem__003.smt2 EXTRA_DIST = $(TESTS) \ @@ -57,8 +60,7 @@ EXTRA_DIST = $(TESTS) \ miplib-pp08a-3000.smt \ miplib-pp08a-3000.smt2 \ miplib-opt1217--27.smt.expect \ - miplib-pp08a-3000.smt.expect \ - div.09.smt2 + miplib-pp08a-3000.smt.expect #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/arith/bug716.0.smt2 b/test/regress/regress0/arith/bug716.0.smt2 new file mode 100644 index 000000000..20a5ca3f0 --- /dev/null +++ b/test/regress/regress0/arith/bug716.0.smt2 @@ -0,0 +1,662 @@ +; 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: The fact in question: TERM +; EXPECT: ") +; EXIT: 1 +(set-logic AUFBVDTLIRA) +;; produced by cvc4_15.drv ;; +(set-info :source |VC generated by SPARK 2014|) +(set-info :smt-lib-version 2.0) +(set-info :category industrial) +(set-info :status unknown) +;;; generated by SMT-LIB2 driver +;;; SMT-LIB2 driver: bit-vectors, common part +(set-option :produce-models true) +;;; SMT-LIB2: integer arithmetic +;;; SMT-LIB2: real arithmetic +(declare-datatypes () ((tuple0 (Tuple0)))) +(declare-sort us_private 0) + +(declare-fun us_null_ext__ () us_private) + +(declare-sort us_type_of_heap 0) + +(declare-datatypes () +((us_type_of_heap__ref + (mk___type_of_heap__ref (us_type_of_heap__content us_type_of_heap))))) +(declare-sort us_image 0) + +(declare-datatypes () ((int__ref (mk_int__ref (int__content Int))))) +(declare-datatypes () ((bool__ref (mk_bool__ref (bool__content Bool))))) +(declare-datatypes () ((real__ref (mk_real__ref (real__content Real))))) +(declare-datatypes () +((us_private__ref (mk___private__ref (us_private__content us_private))))) +(define-fun int__ref___projection ((a int__ref)) Int (int__content a)) + +(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a)) + +(define-fun real__ref___projection ((a real__ref)) Real (real__content a)) + +(define-fun us_private__ref___projection ((a us_private__ref)) us_private + (us_private__content a)) + +(declare-fun us_compatible_tags (Int Int) Bool) + +;; __compatible_tags_refl + (assert (forall ((tag Int)) (us_compatible_tags tag tag))) + +(define-fun to_int1 ((b Bool)) Int (ite (= b true) 1 0)) + +(define-fun of_int ((i Int)) Bool (ite (= i 0) false true)) + +(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1))) + +(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool) + +(declare-fun power (Real Int) Real) + +;; Power_0 + (assert (forall ((x Real)) (= (power x 0) 1.0))) + +;; Power_s + (assert + (forall ((x Real) (n Int)) + (=> (<= 0 n) (= (power x (+ n 1)) (* x (power x n)))))) + +;; Power_s_alt + (assert + (forall ((x Real) (n Int)) + (=> (< 0 n) (= (power x n) (* x (power x (- n 1))))))) + +;; Power_1 + (assert (forall ((x Real)) (= (power x 1) x))) + +;; Power_sum + (assert + (forall ((x Real) (n Int) (m Int)) + (=> (<= 0 n) + (=> (<= 0 m) (= (power x (+ n m)) (* (power x n) (power x m))))))) + +;; Power_mult + (assert + (forall ((x Real) (n Int) (m Int)) + (=> (<= 0 n) (=> (<= 0 m) (= (power x (* n m)) (power (power x n) m)))))) + +;; Power_mult2 + (assert + (forall ((x Real) (y Real) (n Int)) + (=> (<= 0 n) (= (power (* x y) n) (* (power x n) (power y n)))))) + +;; Pow_ge_one + (assert + (forall ((x Real) (n Int)) + (=> (and (<= 0 n) (<= 1.0 x)) (<= 1.0 (power x n))))) + +(declare-datatypes () +((mode (NearestTiesToEven) (ToZero) (Up) (Down) (NearestTiesToAway)))) +(declare-sort single 0) + +(declare-fun round (mode Real) Real) + +(declare-fun value (single) Real) + +(declare-fun exact (single) Real) + +(declare-fun model (single) Real) + +(define-fun round_error ((x single)) Real (ite (>= (- (value x) (exact x)) 0.0) (- + (value x) (exact x)) (- (- (value x) (exact x))))) + +(define-fun total_error ((x single)) Real (ite (>= (- (value x) (model x)) 0.0) (- + (value x) (model x)) (- (- (value x) (model x))))) + +(define-fun no_overflow ((m mode) + (x Real)) Bool (<= (ite (>= (round m x) 0.0) (round m x) (- (round m x))) 340282346638528859811704183484516925440.0)) + +;; Bounded_real_no_overflow + (assert + (forall ((m mode) (x Real)) + (=> (<= (ite (>= x 0.0) x (- x)) 340282346638528859811704183484516925440.0) + (no_overflow m x)))) + +;; Round_monotonic + (assert + (forall ((m mode) (x Real) (y Real)) + (=> (<= x y) (<= (round m x) (round m y))))) + +;; Round_idempotent + (assert + (forall ((m1 mode) (m2 mode) (x Real)) + (= (round m1 (round m2 x)) (round m2 x)))) + +;; Round_value + (assert (forall ((m mode) (x single)) (= (round m (value x)) (value x)))) + +;; Bounded_value + (assert + (forall ((x single)) + (<= (ite (>= (value x) 0.0) (value x) (- (value x))) 340282346638528859811704183484516925440.0))) + +;; Exact_rounding_for_integers + (assert + (forall ((m mode) (i Int)) + (=> (and (<= (- 16777216) i) (<= i 16777216)) + (= (round m (to_real i)) (to_real i))))) + +;; Round_down_le + (assert (forall ((x Real)) (<= (round Down x) x))) + +;; Round_up_ge + (assert (forall ((x Real)) (<= x (round Up x)))) + +;; Round_down_neg + (assert (forall ((x Real)) (= (round Down (- x)) (- (round Up x))))) + +;; Round_up_neg + (assert (forall ((x Real)) (= (round Up (- x)) (- (round Down x))))) + +(declare-fun round_logic (mode Real) single) + +;; Round_logic_def + (assert + (forall ((m mode) (x Real)) + (=> (no_overflow m x) (= (value (round_logic m x)) (round m x))))) + +(define-fun of_real_post ((m mode) (x Real) + (res single)) Bool (and (= (value res) (round m x)) + (and (= (exact res) x) (= (model res) x)))) + +(define-fun add_post ((m mode) (x single) (y single) + (res single)) Bool (and (= (value res) (round m (+ (value x) (value y)))) + (and (= (exact res) (+ (exact x) (exact y))) + (= (model res) (+ (model x) (model y)))))) + +(define-fun sub_post ((m mode) (x single) (y single) + (res single)) Bool (and (= (value res) (round m (- (value x) (value y)))) + (and (= (exact res) (- (exact x) (exact y))) + (= (model res) (- (model x) (model y)))))) + +(define-fun mul_post ((m mode) (x single) (y single) + (res single)) Bool (and (= (value res) (round m (* (value x) (value y)))) + (and (= (exact res) (* (exact x) (exact y))) + (= (model res) (* (model x) (model y)))))) + +(define-fun div_post ((m mode) (x single) (y single) + (res single)) Bool (and (= (value res) (round m (/ (value x) (value y)))) + (and (= (exact res) (/ (exact x) (exact y))) + (= (model res) (/ (model x) (model y)))))) + +(define-fun neg_post ((x single) + (res single)) Bool (and (= (value res) (- (value x))) + (and (= (exact res) (- (exact x))) + (= (model res) (- (model x)))))) + +(define-fun lt ((x single) (y single)) Bool (< (value x) (value y))) + +(define-fun gt ((x single) (y single)) Bool (< (value y) (value x))) + +(declare-sort double 0) + +(declare-fun round1 (mode Real) Real) + +(declare-fun value1 (double) Real) + +(declare-fun exact1 (double) Real) + +(declare-fun model1 (double) Real) + +(define-fun round_error1 ((x double)) Real (ite (>= (- (value1 x) (exact1 x)) 0.0) (- + (value1 x) (exact1 x)) (- (- (value1 x) (exact1 x))))) + +(define-fun total_error1 ((x double)) Real (ite (>= (- (value1 x) (model1 x)) 0.0) (- + (value1 x) (model1 x)) (- (- (value1 x) (model1 x))))) + +(define-fun no_overflow1 ((m mode) + (x Real)) Bool (<= (ite (>= (round1 m x) 0.0) (round1 m x) (- (round1 m x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)) + +;; Bounded_real_no_overflow + (assert + (forall ((m mode) (x Real)) + (=> + (<= (ite (>= x 0.0) x (- x)) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) + (no_overflow1 m x)))) + +;; Round_monotonic + (assert + (forall ((m mode) (x Real) (y Real)) + (=> (<= x y) (<= (round1 m x) (round1 m y))))) + +;; Round_idempotent + (assert + (forall ((m1 mode) (m2 mode) (x Real)) + (= (round1 m1 (round1 m2 x)) (round1 m2 x)))) + +;; Round_value + (assert + (forall ((m mode) (x double)) (= (round1 m (value1 x)) (value1 x)))) + +;; Bounded_value + (assert + (forall ((x double)) + (<= (ite (>= (value1 x) 0.0) (value1 x) (- (value1 x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))) + +;; Exact_rounding_for_integers + (assert + (forall ((m mode) (i Int)) + (=> (and (<= (- 9007199254740992) i) (<= i 9007199254740992)) + (= (round1 m (to_real i)) (to_real i))))) + +;; Round_down_le + (assert (forall ((x Real)) (<= (round1 Down x) x))) + +;; Round_up_ge + (assert (forall ((x Real)) (<= x (round1 Up x)))) + +;; Round_down_neg + (assert (forall ((x Real)) (= (round1 Down (- x)) (- (round1 Up x))))) + +;; Round_up_neg + (assert (forall ((x Real)) (= (round1 Up (- x)) (- (round1 Down x))))) + +(declare-fun round_logic1 (mode Real) double) + +;; Round_logic_def + (assert + (forall ((m mode) (x Real)) + (=> (no_overflow1 m x) (= (value1 (round_logic1 m x)) (round1 m x))))) + +(define-fun of_real_post1 ((m mode) (x Real) + (res double)) Bool (and (= (value1 res) (round1 m x)) + (and (= (exact1 res) x) (= (model1 res) x)))) + +(define-fun add_post1 ((m mode) (x double) (y double) + (res double)) Bool (and + (= (value1 res) (round1 m (+ (value1 x) (value1 y)))) + (and (= (exact1 res) (+ (exact1 x) (exact1 y))) + (= (model1 res) (+ (model1 x) (model1 y)))))) + +(define-fun sub_post1 ((m mode) (x double) (y double) + (res double)) Bool (and + (= (value1 res) (round1 m (- (value1 x) (value1 y)))) + (and (= (exact1 res) (- (exact1 x) (exact1 y))) + (= (model1 res) (- (model1 x) (model1 y)))))) + +(define-fun mul_post1 ((m mode) (x double) (y double) + (res double)) Bool (and + (= (value1 res) (round1 m (* (value1 x) (value1 y)))) + (and (= (exact1 res) (* (exact1 x) (exact1 y))) + (= (model1 res) (* (model1 x) (model1 y)))))) + +(define-fun div_post1 ((m mode) (x double) (y double) + (res double)) Bool (and + (= (value1 res) (round1 m (/ (value1 x) (value1 y)))) + (and (= (exact1 res) (/ (exact1 x) (exact1 y))) + (= (model1 res) (/ (model1 x) (model1 y)))))) + +(define-fun neg_post1 ((x double) + (res double)) Bool (and (= (value1 res) (- (value1 x))) + (and (= (exact1 res) (- (exact1 x))) + (= (model1 res) (- (model1 x)))))) + +(define-fun lt1 ((x double) (y double)) Bool (< (value1 x) (value1 y))) + +(define-fun gt1 ((x double) (y double)) Bool (< (value1 y) (value1 x))) + +;; round_single_bound + (assert + (forall ((x Real)) + (! (and + (<= (- (- x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0)) + (round NearestTiesToEven x)) + (<= (round NearestTiesToEven x) (+ (+ x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0)))) :pattern ( + (round NearestTiesToEven x)) ))) + +;; round_double_bound + (assert + (forall ((x Real)) + (! (and + (<= (- (- x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0)) + (round1 NearestTiesToEven x)) + (<= (round1 NearestTiesToEven x) (+ (+ x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0)))) :pattern ( + (round1 NearestTiesToEven x)) ))) + +;; round_double_single + (assert + (forall ((x Real)) + (! (= (round1 NearestTiesToEven (round NearestTiesToEven x)) (round + NearestTiesToEven + x)) :pattern ( + (round NearestTiesToEven x)) ))) + +(declare-fun round2 (Real) Int) + +;; Round_down + (assert + (forall ((x Real)) + (=> (< (- x (to_real (to_int x))) (/ 5.0 10.0)) (= (round2 x) (to_int x))))) + +;; Round_up + (assert + (forall ((x Real)) + (=> (< (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0)) + (= (round2 x) (- 1 (to_int (- 1.0 x))))))) + +;; Round_neg_tie + (assert + (forall ((x Real)) + (=> (and (= (- x (to_real (to_int x))) (/ 5.0 10.0)) (< x 0.0)) + (= (round2 x) (to_int x))))) + +;; Round_pos_tie + (assert + (forall ((x Real)) + (=> + (and (= (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0)) (< 0.0 x)) + (= (round2 x) (- 1 (to_int (- 1.0 x))))))) + +;; Round_int + (assert + (forall ((i Int)) + (! (= (round2 (to_real i)) i) :pattern ((round2 (to_real i))) ))) + +;; Round_near_int + (assert + (forall ((i Int)) + (forall ((x Real)) + (=> (and (< (- (/ 5.0 10.0)) x) (< x (/ 5.0 10.0))) + (= (round2 (+ (to_real i) x)) i))))) + +;; Round_monotonic + (assert + (forall ((x Real) (y Real)) (=> (<= x y) (<= (round2 x) (round2 y))))) + +;; Round_monotonic_int1 + (assert + (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (round2 x) i)))) + +;; Round_monotonic_int2 + (assert + (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (round2 x))))) + +;; Round_bound + (assert + (forall ((x Real)) + (and (<= (- x (/ 5.0 10.0)) (to_real (round2 x))) + (<= (to_real (round2 x)) (+ x (/ 5.0 10.0)))))) + +(declare-fun remainder (Real Real) Real) + +(declare-sort float 0) + +(define-fun in_range1 ((x Real)) Bool (and + (<= (- 340282346638528859811704183484516925440.0) x) + (<= x 340282346638528859811704183484516925440.0))) + +(declare-fun to_real1 (float) Real) + +(declare-fun of_real (Real) float) + +(declare-fun user_eq (float float) Bool) + +(declare-fun next_representable (Real) Real) + +(declare-fun prev_representable (Real) Real) + +;; next_representable_def + (assert + (forall ((x Real)) + (! (< x (next_representable x)) :pattern ((next_representable x)) ))) + +;; prev_representable_def + (assert + (forall ((x Real)) + (! (< (prev_representable x) x) :pattern ((prev_representable x)) ))) + +(declare-fun attr__ATTRIBUTE_IMAGE1 (Real) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Real) + +(declare-fun dummy () float) + +;; inversion_axiom + (assert + (forall ((x float)) + (! (= (of_real (to_real1 x)) x) :pattern ((to_real1 x)) ))) + +;; representable_first + (assert + (= (round NearestTiesToEven (- 340282346638528859811704183484516925440.0)) (- 340282346638528859811704183484516925440.0))) + +;; representable_last + (assert + (= (round NearestTiesToEven 340282346638528859811704183484516925440.0) 340282346638528859811704183484516925440.0)) + +;; range_axiom + (assert (forall ((x float)) (in_range1 (to_real1 x)))) + +(declare-datatypes () ((float__ref (mk_float__ref (float__content float))))) +(define-fun float__ref___projection ((a float__ref)) float (float__content a)) + +(declare-sort weapon_kind 0) + +(define-fun in_range2 ((x Int)) Bool (and (<= 0 x) (<= x 2))) + +(define-fun bool_eq ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE2 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE2 (us_image) Int) + +(declare-fun to_rep (weapon_kind) Int) + +(declare-fun of_rep (Int) weapon_kind) + +(declare-fun user_eq1 (weapon_kind weapon_kind) Bool) + +(declare-fun dummy1 () weapon_kind) + +;; inversion_axiom + (assert + (forall ((x weapon_kind)) + (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x)) ))) + +;; range_axiom + (assert + (forall ((x weapon_kind)) (! (in_range2 + (to_rep x)) :pattern ((to_rep x)) ))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range2 x) (= (to_rep (of_rep x)) x)) :pattern ((to_rep + (of_rep x))) ))) + +(declare-datatypes () +((weapon_kind__ref (mk_weapon_kind__ref (weapon_kind__content weapon_kind))))) +(define-fun weapon_kind__ref___projection ((a weapon_kind__ref)) weapon_kind + (weapon_kind__content a)) + +(declare-fun dps (Int) float) + +(declare-fun damage (Int) Int) + +(declare-fun bullet (Int) Int) + +(declare-fun cooldown (Int) Int) + +;; dps__post_axiom + (assert true) + +;; dps__def_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) + (= (to_real1 (dps self)) (round NearestTiesToEven + (/ (round NearestTiesToEven + (to_real (damage (bullet self)))) (round + NearestTiesToEven + (to_real + (cooldown + self))))))) :pattern ( + (dps self)) ))) + +(declare-sort integer 0) + +(define-fun in_range3 ((x Int)) Bool (and (<= (- 2147483648) x) + (<= x 2147483647))) + +(define-fun bool_eq1 ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE3 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Int) + +(declare-fun to_rep1 (integer) Int) + +(declare-fun of_rep1 (Int) integer) + +(declare-fun user_eq2 (integer integer) Bool) + +(declare-fun dummy2 () integer) + +;; inversion_axiom + (assert + (forall ((x integer)) + (! (= (of_rep1 (to_rep1 x)) x) :pattern ((to_rep1 x)) ))) + +;; range_axiom + (assert + (forall ((x integer)) (! (in_range3 (to_rep1 x)) :pattern ((to_rep1 x)) ))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range3 x) (= (to_rep1 (of_rep1 x)) x)) :pattern ((to_rep1 + (of_rep1 x))) ))) + +(declare-datatypes () +((integer__ref (mk_integer__ref (integer__content integer))))) +(define-fun integer__ref___projection ((a integer__ref)) integer (integer__content + a)) + +(define-fun dynamic_invariant ((temp___expr_15 Int) (temp___is_init_12 Bool) + (temp___do_constant_13 Bool) + (temp___do_toplevel_14 Bool)) Bool (=> + (or (= temp___is_init_12 true) + (<= (- 2147483648) 2147483647)) + (in_range3 temp___expr_15))) + +(declare-sort bullet_kind 0) + +(define-fun in_range4 ((x Int)) Bool (and (<= 0 x) (<= x 4))) + +(define-fun bool_eq2 ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE4 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check4 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE4 (us_image) Int) + +(declare-fun to_rep2 (bullet_kind) Int) + +(declare-fun of_rep2 (Int) bullet_kind) + +(declare-fun user_eq3 (bullet_kind bullet_kind) Bool) + +(declare-fun dummy3 () bullet_kind) + +;; inversion_axiom + (assert + (forall ((x bullet_kind)) + (! (= (of_rep2 (to_rep2 x)) x) :pattern ((to_rep2 x)) ))) + +;; range_axiom + (assert + (forall ((x bullet_kind)) (! (in_range4 + (to_rep2 x)) :pattern ((to_rep2 x)) ))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range4 x) (= (to_rep2 (of_rep2 x)) x)) :pattern ((to_rep2 + (of_rep2 x))) ))) + +(declare-datatypes () +((bullet_kind__ref (mk_bullet_kind__ref (bullet_kind__content bullet_kind))))) +(define-fun bullet_kind__ref___projection ((a bullet_kind__ref)) bullet_kind + (bullet_kind__content a)) + +(define-fun dynamic_invariant1 ((temp___expr_180 Int) + (temp___is_init_177 Bool) (temp___do_constant_178 Bool) + (temp___do_toplevel_179 Bool)) Bool (=> + (or (= temp___is_init_177 true) + (<= 0 4)) (in_range4 temp___expr_180))) + +;; damage__post_axiom + (assert + (forall ((self Int)) + (! (=> (in_range4 self) (dynamic_invariant (damage self) true false true)) :pattern ( + (damage self)) ))) + +;; damage__def_axiom + (assert + (forall ((self Int)) + (! (=> (in_range4 self) + (= (damage self) (ite (= self 0) 0 + (ite (= self 1) 1 + (ite (= self 2) 8 (ite (= self 3) 10 1)))))) :pattern ( + (damage self)) ))) + +(define-fun dynamic_invariant2 ((temp___expr_186 Int) + (temp___is_init_183 Bool) (temp___do_constant_184 Bool) + (temp___do_toplevel_185 Bool)) Bool (=> + (or (= temp___is_init_183 true) + (<= 0 2)) (in_range2 temp___expr_186))) + +;; bullet__post_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) (dynamic_invariant1 (bullet self) true false true)) :pattern ( + (bullet self)) ))) + +;; bullet__def_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) + (= (bullet self) (ite (= self 0) 1 (ite (= self 1) 1 2)))) :pattern ( + (bullet self)) ))) + +;; cooldown__post_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) (dynamic_invariant (cooldown self) true false + true)) :pattern ((cooldown self)) ))) + +;; cooldown__def_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) + (= (cooldown self) (ite (= self 0) 4 (ite (= self 1) 1 8)))) :pattern ( + (cooldown self)) ))) + +(assert +;; WP_parameter_def + ;; File "weapons.ads", line 34, characters 0-0 + (not + (forall ((w Int)) + (=> (and (<= 0 w) (<= w 2)) + (or (= w 2) (<= (to_real1 (dps w)) (to_real1 (dps (+ w 1))))))))) +(check-sat) +(get-info :reason-unknown) diff --git a/test/regress/regress0/arith/bug716.1.cvc b/test/regress/regress0/arith/bug716.1.cvc new file mode 100644 index 000000000..3c0e9879a --- /dev/null +++ b/test/regress/regress0/arith/bug716.1.cvc @@ -0,0 +1,6 @@ +% EXPECT: The POW(^) operator can only be used with a natural number in the exponent. Exception occured in: +% EXPECT: 2 ^ x +% EXIT: 1 +x: INT; +ASSERT 2^x = 8; +QUERY x=3; diff --git a/test/regress/regress0/arith/div.09.smt2 b/test/regress/regress0/arith/div.09.smt2 index 9bcb93476..e457734eb 100644 --- a/test/regress/regress0/arith/div.09.smt2 +++ b/test/regress/regress0/arith/div.09.smt2 @@ -1,6 +1,7 @@ +; 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: The fact in question: (>= (+ (* (- 1) (/ n n)) termITE_132) 0) +; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 (set-logic QF_LRA) diff --git a/test/regress/regress0/expect/Makefile.am b/test/regress/regress0/expect/Makefile.am new file mode 100644 index 000000000..e1518d84d --- /dev/null +++ b/test/regress/regress0/expect/Makefile.am @@ -0,0 +1,44 @@ +SUBDIRS = . + +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + scrub.01.smt \ + scrub.02.smt \ + scrub.03.smt2 \ + scrub.04.smt2 \ + scrub.06.cvc \ + scrub.07.sy \ + scrub.08.sy \ + scrub.09.p + +EXTRA_DIST = $(TESTS) \ + scrub.01.smt.expect \ + scrub.03.smt2.expect \ + scrub.07.sy.expect + +# synonyms for "check" in this directory +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 regress4 +regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/expect/README b/test/regress/regress0/expect/README new file mode 100644 index 000000000..756982408 --- /dev/null +++ b/test/regress/regress0/expect/README @@ -0,0 +1 @@ +This directory contains integration tests for the test/regress/run_regression script. \ No newline at end of file diff --git a/test/regress/regress0/expect/scrub.01.smt b/test/regress/regress0/expect/scrub.01.smt new file mode 100644 index 000000000..592a3501f --- /dev/null +++ b/test/regress/regress0/expect/scrub.01.smt @@ -0,0 +1,7 @@ +(benchmark reject_nonlinear +:logic QF_LRA +:extrafuns ((n Real)) +:status unknown +:formula +(= (/ n n) 1) +) diff --git a/test/regress/regress0/expect/scrub.01.smt.expect b/test/regress/regress0/expect/scrub.01.smt.expect new file mode 100644 index 000000000..b21f2d965 --- /dev/null +++ b/test/regress/regress0/expect/scrub.01.smt.expect @@ -0,0 +1,6 @@ +% 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: 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 new file mode 100644 index 000000000..f2e6554b7 --- /dev/null +++ b/test/regress/regress0/expect/scrub.02.smt @@ -0,0 +1,13 @@ +% 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: The fact in question: TERM +% EXPECT: ") +% EXIT: 1 +(benchmark reject_nonlinear +:logic QF_LRA +:extrafuns ((n Real)) +:status unknown +:formula +(= (/ n n) 1) +) diff --git a/test/regress/regress0/expect/scrub.03.smt2 b/test/regress/regress0/expect/scrub.03.smt2 new file mode 100644 index 000000000..a5a2c9be1 --- /dev/null +++ b/test/regress/regress0/expect/scrub.03.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_LRA) +(set-info :status unknown) +(declare-fun n () Real) + +; This example is test that LRA rejects multiplication terms + +(assert (= (/ n n) 1)) + +(check-sat) diff --git a/test/regress/regress0/expect/scrub.03.smt2.expect b/test/regress/regress0/expect/scrub.03.smt2.expect new file mode 100644 index 000000000..b21f2d965 --- /dev/null +++ b/test/regress/regress0/expect/scrub.03.smt2.expect @@ -0,0 +1,6 @@ +% 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: 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 new file mode 100644 index 000000000..e457734eb --- /dev/null +++ b/test/regress/regress0/expect/scrub.04.smt2 @@ -0,0 +1,15 @@ +; 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: The fact in question: TERM +; EXPECT: ") +; EXIT: 1 +(set-logic QF_LRA) +(set-info :status unknown) +(declare-fun n () Real) + +; This example is test that LRA rejects multiplication terms + +(assert (= (/ n n) 1)) + +(check-sat) diff --git a/test/regress/regress0/expect/scrub.06.cvc b/test/regress/regress0/expect/scrub.06.cvc new file mode 100644 index 000000000..b9cb1cd8a --- /dev/null +++ b/test/regress/regress0/expect/scrub.06.cvc @@ -0,0 +1,9 @@ +% 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: The fact in question: TERM +% EXIT: 1 + +n : REAL; + +QUERY (n/n) = 1; \ No newline at end of file diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy new file mode 100644 index 000000000..cf0e37c9f --- /dev/null +++ b/test/regress/regress0/expect/scrub.07.sy @@ -0,0 +1,7 @@ +; COMMAND-LINE: --cegqi-si=all --no-dump-synth +(set-logic LIA) +(declare-var n Int) + +(synth-fun f ((n Int)) Int) +(constraint (= (/ n n) 1)) +(check-synth) diff --git a/test/regress/regress0/expect/scrub.07.sy.expect b/test/regress/regress0/expect/scrub.07.sy.expect new file mode 100644 index 000000000..dfcd45a8a --- /dev/null +++ b/test/regress/regress0/expect/scrub.07.sy.expect @@ -0,0 +1,6 @@ +% 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: 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 new file mode 100644 index 000000000..3b9574cdf --- /dev/null +++ b/test/regress/regress0/expect/scrub.08.sy @@ -0,0 +1,13 @@ +; 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. +; EXPECT: The fact in question: TERM +; EXPECT: ") +; EXIT: 1 +(set-logic LIA) +(declare-var n Int) + +(synth-fun f ((n Int)) Int) +(constraint (= (/ n n) 1)) +(check-synth) \ No newline at end of file diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p new file mode 100644 index 000000000..17eef44fe --- /dev/null +++ b/test/regress/regress0/expect/scrub.09.p @@ -0,0 +1,11 @@ +% 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. +% EXPECT: The fact in question: TERM +% EXPECT: ") +% EXIT: 1 +tff(reject_division,conjecture, + ! [X: $int] : + ( $quotient(X,X) = 1 ) + ). diff --git a/test/regress/run_regression b/test/regress/run_regression index 868a69116..a04e488d8 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -77,6 +77,7 @@ tmpbenchmark= if expr "$benchmark" : '.*\.smt$' &>/dev/null; then lang=smt1 if test -e "$benchmark.expect"; then + scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -84,7 +85,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi - elif grep '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then + elif grep '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then + scrubber=`grep '^% SCRUBBER: ' "$benchmark" | sed 's,^% SCRUBBER: ,,'` expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -92,7 +94,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle # this frustrates our auto-language-detection gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX - grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark" + grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" >"$tmpbenchmark" if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi @@ -111,6 +113,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then lang=smt2 if test -e "$benchmark.expect"; then + scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -118,7 +121,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi - elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then + elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then + scrubber=`grep '^; SCRUBBER: ' "$benchmark" | sed 's,^; SCRUBBER: ,,'` expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'` expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'` @@ -139,6 +143,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then lang=cvc4 + scrubber=`grep '^% SCRUBBER: ' "$benchmark" | sed 's,^% SCRUBBER: ,,'` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then @@ -154,6 +159,7 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then elif expr "$benchmark" : '.*\.p$' &>/dev/null; then lang=tptp command_line=--finite-model-find + scrubber=`grep '^% SCRUBBER: ' "$benchmark" | sed 's,^% SCRUBBER: ,,'` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then @@ -182,6 +188,7 @@ elif expr "$benchmark" : '.*\.p$' &>/dev/null; then elif expr "$benchmark" : '.*\.sy$' &>/dev/null; then lang=sygus if test -e "$benchmark.expect"; then + scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -189,7 +196,8 @@ elif expr "$benchmark" : '.*\.sy$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi - elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then + elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then + scrubber=`grep '^; SCRUBBER: ' "$benchmark" | sed 's,^; SCRUBBER: ,,'` expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'` expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'` @@ -306,6 +314,15 @@ else echo "$actual_error" >"$errfilefix" fi +# Scrub the output file if a scrubber has been specified. +if [ -n "$scrubber" ]; then + echo "About to scrub $outfile using $scrubber" + mv "$outfile" "$outfile.prescrub" + cat "$outfile.prescrub" | eval $scrubber >"$outfile" +else + echo "not scrubbing" +fi + diffs=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"` diffexit=$? diffserr=`diff -u --strip-trailing-cr "$experrfile" "$errfilefix"` -- 2.30.2