From 4929b5dcfaba1e051309a0debfeaf9f8bf8e2d8b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 Oct 2021 15:48:25 -0500 Subject: [PATCH] Add more abduction regressions (#7461) Fixes #5848. This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown. Also introduces subfolder regress/regress1/abduction. --- .../builtin/theory_builtin_type_rules.cpp | 3 ++- test/regress/CMakeLists.txt | 27 +++++++++++-------- .../abd-simple-conj-4.smt2 | 0 .../regress1/{ => abduction}/abduct-dt.smt2 | 0 .../abduction-no-pbe-sym-break.smt2 | 0 .../abduction_1255.corecstrs.readable.smt2 | 0 .../abduction_streq.readable.smt2 | 0 .../regress1/abduction/issue5848-2.smt2 | 6 +++++ .../issue5848-3-trivial-no-abduct.smt2 | 0 .../regress1/abduction/issue5848-4.smt2 | 8 ++++++ .../regress/regress1/abduction/issue5848.smt2 | 7 +++++ .../regress1/abduction/issue6605-1.smt2 | 11 ++++++++ .../sygus-abduct-ex1-grammar.smt2 | 0 .../sygus-abduct-test-ccore.smt2 | 0 .../sygus-abduct-test-user.smt2 | 0 .../{ => abduction}/sygus-abduct-test.smt2 | 0 .../{sygus => abduction}/uf-abduct.smt2 | 0 .../{sygus => abduction}/yoni-true-sol.smt2 | 0 18 files changed, 50 insertions(+), 12 deletions(-) rename test/regress/regress1/{sygus => abduction}/abd-simple-conj-4.smt2 (100%) rename test/regress/regress1/{ => abduction}/abduct-dt.smt2 (100%) rename test/regress/regress1/{sygus => abduction}/abduction-no-pbe-sym-break.smt2 (100%) rename test/regress/regress1/{sygus => abduction}/abduction_1255.corecstrs.readable.smt2 (100%) rename test/regress/regress1/{sygus => abduction}/abduction_streq.readable.smt2 (100%) create mode 100644 test/regress/regress1/abduction/issue5848-2.smt2 rename test/regress/regress1/{sygus => abduction}/issue5848-3-trivial-no-abduct.smt2 (100%) create mode 100644 test/regress/regress1/abduction/issue5848-4.smt2 create mode 100644 test/regress/regress1/abduction/issue5848.smt2 create mode 100644 test/regress/regress1/abduction/issue6605-1.smt2 rename test/regress/regress1/{ => abduction}/sygus-abduct-ex1-grammar.smt2 (100%) rename test/regress/regress1/{ => abduction}/sygus-abduct-test-ccore.smt2 (100%) rename test/regress/regress1/{ => abduction}/sygus-abduct-test-user.smt2 (100%) rename test/regress/regress1/{ => abduction}/sygus-abduct-test.smt2 (100%) rename test/regress/regress1/{sygus => abduction}/uf-abduct.smt2 (100%) rename test/regress/regress1/{sygus => abduction}/yoni-true-sol.smt2 (100%) diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index f3c595720..1888069bc 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -42,7 +42,8 @@ typedef expr::Attribute GroundTermAttribute; Node SortProperties::mkGroundTerm(TypeNode type) { - Assert(type.getKind() == kind::SORT_TYPE); + // we typically use this method for sorts, although there are other types + // where it is used as well, e.g. arrays that are not closed enumerable. GroundTermAttribute gta; if (type.hasAttribute(gta)) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b80fd890b..1c81316c3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1489,7 +1489,22 @@ set(regress_0_tests # Regression level 1 tests set(regress_1_tests - regress1/abduct-dt.smt2 + regress1/abduction/sygus-abduct-test-user.smt2 + regress1/abduction/issue5848-4.smt2 + regress1/abduction/issue5848-2.smt2 + regress1/abduction/issue5848.smt2 + regress1/abduction/issue6605-1.smt2 + regress1/abduction/abduct-dt.smt2 + regress1/abduction/sygus-abduct-test-ccore.smt2 + regress1/abduction/sygus-abduct-test.smt2 + regress1/abduction/abd-simple-conj-4.smt2 + regress1/abduction/abduction_streq.readable.smt2 + regress1/abduction/yoni-true-sol.smt2 + regress1/abduction/uf-abduct.smt2 + regress1/abduction/abduction_1255.corecstrs.readable.smt2 + regress1/abduction/abduction-no-pbe-sym-break.smt2 + regress1/abduction/issue5848-3-trivial-no-abduct.smt2 + regress1/abduction/sygus-abduct-ex1-grammar.smt2 regress1/arith/arith-brab-test.smt2 regress1/arith/arith-int-004.cvc.smt2 regress1/arith/arith-int-011.cvc.smt2 @@ -2322,15 +2337,7 @@ set(regress_1_tests regress1/strings/update-ex1.smt2 regress1/strings/update-ex2.smt2 regress1/strings/username_checker_min.smt2 - regress1/sygus-abduct-ex1-grammar.smt2 - regress1/sygus-abduct-test.smt2 - regress1/sygus-abduct-test-ccore.smt2 - regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy - regress1/sygus/abd-simple-conj-4.smt2 - regress1/sygus/abduction_1255.corecstrs.readable.smt2 - regress1/sygus/abduction_streq.readable.smt2 - regress1/sygus/abduction-no-pbe-sym-break.smt2 regress1/sygus/abv.sy regress1/sygus/array-grammar-store.sy regress1/sygus/array_search_5-Q-easy.sy @@ -2476,10 +2483,8 @@ set(regress_1_tests regress1/sygus/trivial-stream.sy regress1/sygus/twolets1.sy regress1/sygus/twolets2-orig.sy - regress1/sygus/uf-abduct.smt2 regress1/sygus/unbdd_inv_gen_winf1.sy regress1/sygus/univ_2-long-repeat.sy - regress1/sygus/yoni-true-sol.smt2 regress1/sym/q-constant.smt2 regress1/sym/q-function.smt2 regress1/sym/qf-function.smt2 diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/abduction/abd-simple-conj-4.smt2 similarity index 100% rename from test/regress/regress1/sygus/abd-simple-conj-4.smt2 rename to test/regress/regress1/abduction/abd-simple-conj-4.smt2 diff --git a/test/regress/regress1/abduct-dt.smt2 b/test/regress/regress1/abduction/abduct-dt.smt2 similarity index 100% rename from test/regress/regress1/abduct-dt.smt2 rename to test/regress/regress1/abduction/abduct-dt.smt2 diff --git a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 b/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2 similarity index 100% rename from test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 rename to test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2 diff --git a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 similarity index 100% rename from test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 rename to test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 diff --git a/test/regress/regress1/sygus/abduction_streq.readable.smt2 b/test/regress/regress1/abduction/abduction_streq.readable.smt2 similarity index 100% rename from test/regress/regress1/sygus/abduction_streq.readable.smt2 rename to test/regress/regress1/abduction/abduction_streq.readable.smt2 diff --git a/test/regress/regress1/abduction/issue5848-2.smt2 b/test/regress/regress1/abduction/issue5848-2.smt2 new file mode 100644 index 000000000..36716c4c7 --- /dev/null +++ b/test/regress/regress1/abduction/issue5848-2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --produce-abducts +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun v9 () Bool) +(get-abduct A (or true v9)) diff --git a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 b/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 similarity index 100% rename from test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 rename to test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 diff --git a/test/regress/regress1/abduction/issue5848-4.smt2 b/test/regress/regress1/abduction/issue5848-4.smt2 new file mode 100644 index 000000000..93cd8f52b --- /dev/null +++ b/test/regress/regress1/abduction/issue5848-4.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --produce-abducts +; EXPECT: none +(set-logic UFLRA) +(declare-sort S0 0) +(declare-fun S0-0 () S0) +(declare-fun S0-1 () S0) +(declare-fun v87 () Bool) +(get-abduct A (and false (exists ((q117 S0)) (or v87 (and (= S0-1 q117) (= q117 S0-0)))))) diff --git a/test/regress/regress1/abduction/issue5848.smt2 b/test/regress/regress1/abduction/issue5848.smt2 new file mode 100644 index 000000000..7b8761235 --- /dev/null +++ b/test/regress/regress1/abduction/issue5848.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --produce-abducts +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a () Int) +(assert (= (mod 0 a) 0)) +(get-abduct A (= a 1)) diff --git a/test/regress/regress1/abduction/issue6605-1.smt2 b/test/regress/regress1/abduction/issue6605-1.smt2 new file mode 100644 index 000000000..a33fdd905 --- /dev/null +++ b/test/regress/regress1/abduction/issue6605-1.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --produce-abducts +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(set-option :produce-abducts true) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(assert (= (>= b c) (>= 0 a))) +(assert (= c a)) +(get-abduct d (<= a b)) diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2 similarity index 100% rename from test/regress/regress1/sygus-abduct-ex1-grammar.smt2 rename to test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2 diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2 similarity index 100% rename from test/regress/regress1/sygus-abduct-test-ccore.smt2 rename to test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2 diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-user.smt2 similarity index 100% rename from test/regress/regress1/sygus-abduct-test-user.smt2 rename to test/regress/regress1/abduction/sygus-abduct-test-user.smt2 diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/abduction/sygus-abduct-test.smt2 similarity index 100% rename from test/regress/regress1/sygus-abduct-test.smt2 rename to test/regress/regress1/abduction/sygus-abduct-test.smt2 diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/abduction/uf-abduct.smt2 similarity index 100% rename from test/regress/regress1/sygus/uf-abduct.smt2 rename to test/regress/regress1/abduction/uf-abduct.smt2 diff --git a/test/regress/regress1/sygus/yoni-true-sol.smt2 b/test/regress/regress1/abduction/yoni-true-sol.smt2 similarity index 100% rename from test/regress/regress1/sygus/yoni-true-sol.smt2 rename to test/regress/regress1/abduction/yoni-true-sol.smt2 -- 2.30.2