From 982282eed2b02c1ca4aec2a335e460e622c4e963 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 11 Feb 2020 23:33:21 -0800 Subject: run_regression: Distinguish between timeout and failure. (#3750) If --use-skip-return-code is enabled and a regression test times out it will return EXIT_SKIP instead of EXIT_FAILURE. --- test/regress/run_regression.py | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 2a0144c13..f2246c40b 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -29,7 +29,7 @@ REQUIRES = 'REQUIRES:' EXIT_OK = 0 EXIT_FAILURE = 1 EXIT_SKIP = 77 - +STATUS_TIMEOUT = 124 def run_process(args, cwd, timeout, s_input=None): """Runs a process with a timeout `timeout` in seconds. `args` are the @@ -47,7 +47,7 @@ def run_process(args, cwd, timeout, s_input=None): out = '' err = '' - exit_status = 124 + exit_status = STATUS_TIMEOUT try: if timeout: timer = threading.Timer(timeout, lambda p: p.kill(), [proc]) @@ -56,6 +56,9 @@ def run_process(args, cwd, timeout, s_input=None): exit_status = proc.returncode finally: if timeout: + # The timer killed the process and is not active anymore. + if exit_status == -9 and not timer.is_alive(): + exit_status = STATUS_TIMEOUT timer.cancel() return out, err, exit_status @@ -344,7 +347,10 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, command_line_args, benchmark_dir, benchmark_basename, timeout) output = re.sub(r'^[ \t]*', '', output, flags=re.MULTILINE) error = re.sub(r'^[ \t]*', '', error, flags=re.MULTILINE) - if output != expected_output: + if exit_status == STATUS_TIMEOUT: + exit_code = EXIT_SKIP if use_skip_return_code else EXIT_FAILURE + print('Timeout - Flags: {}'.format(command_line_args)) + elif output != expected_output: exit_code = EXIT_FAILURE print( 'not ok - Differences between expected and actual output on stdout - Flags: {}' -- cgit v1.2.3 From f38cd31ddfd3d5caa2ffe3a0ffafbb2b0394391b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 12 Feb 2020 16:24:13 -0600 Subject: Ensure ext rewrites for associative ops dont throw assertions for kind arities (#3681) --- src/theory/quantifiers/extended_rewrite.cpp | 10 ++++++++++ test/regress/CMakeLists.txt | 3 ++- test/regress/regress1/bv/issue3654.smt2 | 24 ++++++++++++++++++++++++ test/regress/regress1/sygus/issue3649.sy | 24 ++++++++++++++++++++++++ test/regress/regress1/sygus/issue3654.sy | 24 ------------------------ 5 files changed, 60 insertions(+), 25 deletions(-) create mode 100644 test/regress/regress1/bv/issue3654.smt2 create mode 100644 test/regress/regress1/sygus/issue3649.sy delete mode 100644 test/regress/regress1/sygus/issue3654.sy diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 05e789ce2..9e924f34d 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -155,6 +155,16 @@ Node ExtendedRewriter::extendedRewrite(Node n) // we may have subsumed children down to one ret = children[0]; } + else if (isAssoc && children.size() > kind::metakind::getUpperBoundForKind(k)) + { + Assert(kind::metakind::getUpperBoundForKind(k) >= 2); + // kind may require binary construction + ret = children[0]; + for (unsigned i = 1, nchild = children.size(); i < nchild; i++) + { + ret = nm->mkNode(k, ret, children[i]); + } + } else { ret = nm->mkNode(k, children); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index aaabd2301..150983187 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1191,6 +1191,7 @@ set(regress_1_tests regress1/bv/divtest.smt2 regress1/bv/fuzz34.smtv1.smt2 regress1/bv/fuzz38.smtv1.smt2 + regress1/bv/issue3654.smt2 regress1/bv/test-bv-abstraction.smt2 regress1/bv/unsound1.smt2 regress1/bvdiv2.smt2 @@ -1819,7 +1820,7 @@ set(regress_1_tests regress1/sygus/issue3635.smt2 regress1/sygus/issue3644.smt2 regress1/sygus/issue3648.smt2 - regress1/sygus/issue3654.sy + regress1/sygus/issue3649.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy diff --git a/test/regress/regress1/bv/issue3654.smt2 b/test/regress/regress1/bv/issue3654.smt2 new file mode 100644 index 000000000..59c11456f --- /dev/null +++ b/test/regress/regress1/bv/issue3654.smt2 @@ -0,0 +1,24 @@ +; COMMAND_LINE: --ext-rew-prep +; EXPECT: sat +(set-logic QF_BV) +(declare-fun a () (_ BitVec 4)) +(assert (let ((a!1 ((_ sign_extend 3) + (ite (bvult ((_ sign_extend 15) #b0) #x2b7e) #b1 #b0))) + (a!2 ((_ zero_extend 15) + (ite (distinct #x2b7e ((_ sign_extend 12) a)) #b1 #b0))) + (a!4 (bvsgt (bvlshr (bvadd #x2b7e ((_ sign_extend 12) a)) + ((_ sign_extend 12) a)) + ((_ zero_extend 12) a))) + (a!5 (bvugt (ite (bvult ((_ sign_extend 15) #b0) #x2b7e) #b1 #b0) #b0)) + (a!6 (bvugt (bvlshr (bvadd #x2b7e ((_ sign_extend 12) a)) + ((_ sign_extend 12) a)) + #x2b7e))) +(let ((a!3 (bvslt a!2 + (bvlshr (bvadd #x2b7e ((_ sign_extend 12) a)) + ((_ sign_extend 12) a)))) + (a!7 (xor (ite a!4 a!5 a!4) + a!6 + (= (bvxnor #x2b7e ((_ zero_extend 12) a)) + (bvadd #x2b7e ((_ sign_extend 12) a)))))) + (ite (bvule a!1 a) a!3 a!7)))) +(check-sat) diff --git a/test/regress/regress1/sygus/issue3649.sy b/test/regress/regress1/sygus/issue3649.sy new file mode 100644 index 000000000..12949c55a --- /dev/null +++ b/test/regress/regress1/sygus/issue3649.sy @@ -0,0 +1,24 @@ +; EXPECT: unknown +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) +(synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool) + +(define-fun init-fn ((i Int) (x (Array Int Int)) (c Int)) Bool + (and (= i 0) + (= (select x 10) c))) + +(define-fun post-fn ((i Int) (x (Array Int Int))(c Int)) Bool + (exists ((index Int)) (and (= (select x index) c) + (forall ((index2 Int)) (=> (< index2 index) (not (= (select x index) c)))) + ))) + +(declare-var x (Array Int Int)) +(declare-var x! (Array Int Int)) +(declare-var i Int) +(declare-var i! Int) +(declare-var c Int) + + +(constraint (=> (init-fn i x c) (inv-fn i x c))) +(constraint (=> (inv-fn i x c) (post-fn i x c))) +(check-synth) diff --git a/test/regress/regress1/sygus/issue3654.sy b/test/regress/regress1/sygus/issue3654.sy deleted file mode 100644 index 12949c55a..000000000 --- a/test/regress/regress1/sygus/issue3654.sy +++ /dev/null @@ -1,24 +0,0 @@ -; EXPECT: unknown -; COMMAND-LINE: --sygus-out=status -(set-logic ALL) -(synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool) - -(define-fun init-fn ((i Int) (x (Array Int Int)) (c Int)) Bool - (and (= i 0) - (= (select x 10) c))) - -(define-fun post-fn ((i Int) (x (Array Int Int))(c Int)) Bool - (exists ((index Int)) (and (= (select x index) c) - (forall ((index2 Int)) (=> (< index2 index) (not (= (select x index) c)))) - ))) - -(declare-var x (Array Int Int)) -(declare-var x! (Array Int Int)) -(declare-var i Int) -(declare-var i! Int) -(declare-var c Int) - - -(constraint (=> (init-fn i x c) (inv-fn i x c))) -(constraint (=> (inv-fn i x c) (post-fn i x c))) -(check-synth) -- cgit v1.2.3