diff options
Diffstat (limited to 'test')
76 files changed, 1277 insertions, 888 deletions
diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt index eae57f3b9..929c5bef2 100644 --- a/test/api/cpp/CMakeLists.txt +++ b/test/api/cpp/CMakeLists.txt @@ -54,3 +54,5 @@ cvc5_add_api_test(issue4889) cvc5_add_api_test(issue6111) cvc5_add_api_test(proj-issue306) cvc5_add_api_test(proj-issue334) +cvc5_add_api_test(proj-issue344) +cvc5_add_api_test(proj-issue345) diff --git a/test/api/cpp/proj-issue344.cpp b/test/api/cpp/proj-issue344.cpp new file mode 100644 index 000000000..5f486706c --- /dev/null +++ b/test/api/cpp/proj-issue344.cpp @@ -0,0 +1,33 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Test for project issue #345 + * + */ + + +#include "api/cpp/cvc5.h" +#include <cassert> + +using namespace cvc5::api; + +int main(void) +{ + Solver slv; + slv.setOption("solve-bv-as-int", "iand"); + Sort s12 = slv.getIntegerSort(); + Term t13 = slv.mkConst(s12, "_x11"); + Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13}); + Term t66 = slv.mkTerm(Kind::BITVECTOR_ULTBV, {t25, t25}); + Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66}); + slv.checkEntailed({t154, t154, t154, t154}); +} diff --git a/test/api/cpp/proj-issue345.cpp b/test/api/cpp/proj-issue345.cpp new file mode 100644 index 000000000..c33e9e5b8 --- /dev/null +++ b/test/api/cpp/proj-issue345.cpp @@ -0,0 +1,34 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Test for project issue #345 + * + */ + + +#include "api/cpp/cvc5.h" +#include <cassert> + +using namespace cvc5::api; + +int main(void) +{ + Solver slv; + slv.setOption("solve-bv-as-int", "iand"); + Sort s12 = slv.getIntegerSort(); + Term t13 = slv.mkConst(s12, "_x11"); + Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13}); + Term t66 = slv.mkTerm(Kind::BITVECTOR_SLTBV, {t25, t25}); + Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66}); + slv.checkEntailed({t154, t154, t154, t154}); +} + diff --git a/test/api/cpp/sep_log_api.cpp b/test/api/cpp/sep_log_api.cpp index 5795de794..6a2fc9740 100644 --- a/test/api/cpp/sep_log_api.cpp +++ b/test/api/cpp/sep_log_api.cpp @@ -247,8 +247,7 @@ int validate_getters(void) * than the random constant -- if we get a value that is LTE, then * something has gone wrong! */ - if (std::stoll(value.toString()) - <= std::stoll(random_constant.toString())) + if (value.getInt64Value() <= random_constant.getInt64Value()) { return -1; } diff --git a/test/api/python/issue4889.py b/test/api/python/issue4889.py index 538c9f2ca..eae0ecad7 100644 --- a/test/api/python/issue4889.py +++ b/test/api/python/issue4889.py @@ -14,7 +14,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind slv = pycvc5.Solver() sort_int = slv.getIntegerSort() @@ -25,7 +25,7 @@ sort_bool = slv.getBooleanSort() const0 = slv.mkConst(sort_fp32, "_c0") const1 = slv.mkConst(sort_fp32, "_c2") const2 = slv.mkConst(sort_bool, "_c4") -ite = slv.mkTerm(kinds.Ite, const2, const1, const0) -rem = slv.mkTerm(kinds.FPRem, ite, const1) -isnan = slv.mkTerm(kinds.FPIsNan, rem) +ite = slv.mkTerm(Kind.Ite, const2, const1, const0) +rem = slv.mkTerm(Kind.FPRem, ite, const1) +isnan = slv.mkTerm(Kind.FPIsNan, rem) slv.checkSatAssuming(isnan) diff --git a/test/api/python/issue5074.py b/test/api/python/issue5074.py index 05fc84ad6..f07b5c8fa 100644 --- a/test/api/python/issue5074.py +++ b/test/api/python/issue5074.py @@ -14,12 +14,12 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind slv = pycvc5.Solver() c1 = slv.mkConst(slv.getIntegerSort()) -t6 = slv.mkTerm(kinds.StringFromCode, c1) -t12 = slv.mkTerm(kinds.StringToRegexp, t6) -t14 = slv.mkTerm(kinds.StringReplaceRe, [t6, t12, t6]) -t16 = slv.mkTerm(kinds.StringContains, [t14, t14]) +t6 = slv.mkTerm(Kind.StringFromCode, c1) +t12 = slv.mkTerm(Kind.StringToRegexp, t6) +t14 = slv.mkTerm(Kind.StringReplaceRe, [t6, t12, t6]) +t16 = slv.mkTerm(Kind.StringContains, [t14, t14]) slv.checkEntailed(t16) diff --git a/test/api/python/issue6111.py b/test/api/python/issue6111.py index 6a4ec3842..9bbda286c 100644 --- a/test/api/python/issue6111.py +++ b/test/api/python/issue6111.py @@ -14,7 +14,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind solver = pycvc5.Solver() solver.setLogic("QF_BV") @@ -25,7 +25,7 @@ zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10) args1 = [] args1.append(zero) args1.append(input2_1) -bvult_res = solver.mkTerm(kinds.BVUlt, args1) +bvult_res = solver.mkTerm(Kind.BVUlt, args1) solver.assertFormula(bvult_res) bvsort4 = solver.mkBitVectorSort(4) @@ -36,13 +36,13 @@ concat_result_43 = solver.mkConst(bvsort8, "concat_result_43") args2 = [] args2.append(concat_result_42) args2.append( - solver.mkTerm(solver.mkOp(kinds.BVExtract, 7, 4), [concat_result_43])) -solver.assertFormula(solver.mkTerm(kinds.Equal, args2)) + solver.mkTerm(solver.mkOp(Kind.BVExtract, 7, 4), [concat_result_43])) +solver.assertFormula(solver.mkTerm(Kind.Equal, args2)) args3 = [] args3.append(concat_result_42) args3.append( - solver.mkTerm(solver.mkOp(kinds.BVExtract, 3, 0), [concat_result_43])) -solver.assertFormula(solver.mkTerm(kinds.Equal, args3)) + solver.mkTerm(solver.mkOp(Kind.BVExtract, 3, 0), [concat_result_43])) +solver.assertFormula(solver.mkTerm(Kind.Equal, args3)) print(solver.checkSat()) diff --git a/test/api/python/proj-issue306.py b/test/api/python/proj-issue306.py index 5d84f65b6..7dbdd6b41 100644 --- a/test/api/python/proj-issue306.py +++ b/test/api/python/proj-issue306.py @@ -13,7 +13,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind slv = pycvc5.Solver() slv.setOption("check-proofs", "true") @@ -24,8 +24,8 @@ t1 = slv.mkConst(s3, "_x0") t3 = slv.mkConst(s1, "_x2") t11 = slv.mkString("") t14 = slv.mkConst(s3, "_x11") -t42 = slv.mkTerm(kinds.Ite, t3, t14, t1) -t58 = slv.mkTerm(kinds.StringLeq, t14, t11) -t95 = slv.mkTerm(kinds.Equal, t14, t42) +t42 = slv.mkTerm(Kind.Ite, t3, t14, t1) +t58 = slv.mkTerm(Kind.StringLeq, t14, t11) +t95 = slv.mkTerm(Kind.Equal, t14, t42) slv.assertFormula(t95) slv.checkSatAssuming([t58]) diff --git a/test/api/python/reset_assertions.py b/test/api/python/reset_assertions.py index 221f1c884..8c3a4e44c 100644 --- a/test/api/python/reset_assertions.py +++ b/test/api/python/reset_assertions.py @@ -19,7 +19,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind slv = pycvc5.Solver() slv.setOption("incremental", "true") @@ -27,7 +27,7 @@ slv.setOption("incremental", "true") real = slv.getRealSort() x = slv.mkConst(real, "x") four = slv.mkInteger(4) -xEqFour = slv.mkTerm(kinds.Equal, x, four) +xEqFour = slv.mkTerm(Kind.Equal, x, four) slv.assertFormula(xEqFour) print(slv.checkSat()) @@ -37,8 +37,8 @@ elementType = slv.getIntegerSort() indexType = slv.getIntegerSort() arrayType = slv.mkArraySort(indexType, elementType) array = slv.mkConst(arrayType, "array") -arrayAtFour = slv.mkTerm(kinds.Select, array, four) +arrayAtFour = slv.mkTerm(Kind.Select, array, four) ten = slv.mkInteger(10) -arrayAtFour_eq_ten = slv.mkTerm(kinds.Equal, arrayAtFour, ten) +arrayAtFour_eq_ten = slv.mkTerm(Kind.Equal, arrayAtFour, ten) slv.assertFormula(arrayAtFour_eq_ten) print(slv.checkSat()) diff --git a/test/api/python/sep_log_api.py b/test/api/python/sep_log_api.py index 4e2fbb750..8bbef42fa 100644 --- a/test/api/python/sep_log_api.py +++ b/test/api/python/sep_log_api.py @@ -20,7 +20,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind # Test function to validate that we *cannot* obtain the heap/nil expressions @@ -43,7 +43,7 @@ def validate_exception(): y = slv.mkConst(integer, "y") # y > x - y_gt_x = slv.mkTerm(kinds.Gt, y, x) + y_gt_x = slv.mkTerm(Kind.Gt, y, x) # assert it slv.assertFormula(y_gt_x) @@ -124,18 +124,18 @@ def validate_getters(): p2 = slv.mkConst(integer, "p2") # Constraints on x and y - x_equal_const = slv.mkTerm(kinds.Equal, x, random_constant) - y_gt_x = slv.mkTerm(kinds.Gt, y, x) + x_equal_const = slv.mkTerm(Kind.Equal, x, random_constant) + y_gt_x = slv.mkTerm(Kind.Gt, y, x) # Points-to expressions - p1_to_x = slv.mkTerm(kinds.SepPto, p1, x) - p2_to_y = slv.mkTerm(kinds.SepPto, p2, y) + p1_to_x = slv.mkTerm(Kind.SepPto, p1, x) + p2_to_y = slv.mkTerm(Kind.SepPto, p2, y) # Heap -- the points-to have to be "starred"! - heap = slv.mkTerm(kinds.SepStar, p1_to_x, p2_to_y) + heap = slv.mkTerm(Kind.SepStar, p1_to_x, p2_to_y) # Constain "nil" to be something random - fix_nil = slv.mkTerm(kinds.Equal, nil, expr_nil_val) + fix_nil = slv.mkTerm(Kind.Equal, nil, expr_nil_val) # Add it all to the solver! slv.assertFormula(x_equal_const) @@ -157,11 +157,11 @@ def validate_getters(): nil_expr = slv.getValueSepNil() # If the heap is not a separating conjunction, bail-out - if (heap_expr.getKind() != kinds.SepStar): + if (heap_expr.getKind() != Kind.SepStar): return False # If nil is not a direct equality, bail-out - if (nil_expr.getKind() != kinds.Equal): + if (nil_expr.getKind() != Kind.Equal): return False # Obtain the values for our "pointers" @@ -175,7 +175,7 @@ def validate_getters(): # Walk all the children for child in heap_expr: # If we don't have a PTO operator, bail-out - if (child.getKind() != kinds.SepPto): + if (child.getKind() != Kind.SepPto): return False # Find both sides of the PTO operator diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4169036ba..20722a1da 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -257,6 +257,7 @@ set(regress_0_tests regress0/bv/bv_to_int_bvuf_to_intuf.smt2 regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 regress0/bv/bv_to_int_elim_err.smt2 + regress0/bv/bv_to_int_int1.smt2 regress0/bv/bv_to_int_zext.smt2 regress0/bv/bvcomp.cvc.smt2 regress0/bv/bvmul-pow2-only.smt2 @@ -434,6 +435,7 @@ set(regress_0_tests regress0/bv/mult-pow2-negative.smt2 regress0/bv/pr4993-bvugt-bvurem-a.smt2 regress0/bv/pr4993-bvugt-bvurem-b.smt2 + regress0/bv/proj-issue343.smt2 regress0/bv/reset-assertions-assert-input.smt2 regress0/bv/sizecheck.cvc.smt2 regress0/bv/smtcompbug.smtv1.smt2 @@ -510,7 +512,9 @@ set(regress_0_tests regress0/datatypes/mutually-recursive.cvc.smt2 regress0/datatypes/pair-bool-bool.cvc.smt2 regress0/datatypes/pair-real-bool.smt2 + regress0/datatypes/par-updater-type-rule.smt2 regress0/datatypes/parametric-alt-list.cvc.smt2 + regress0/datatypes/proj-issue172.smt2 regress0/datatypes/rec1.cvc.smt2 regress0/datatypes/rec2.cvc.smt2 regress0/datatypes/rec4.cvc.smt2 @@ -557,6 +561,8 @@ set(regress_0_tests regress0/declare-fun-is-match.smt2 regress0/declare-funs.smt2 regress0/define-fun-model.smt2 + regress0/difficulty-simple.smt2 + regress0/difficulty-model-ex.smt2 regress0/distinct.smtv1.smt2 regress0/dump-unsat-core-full.smt2 regress0/echo.smt2 @@ -783,6 +789,7 @@ set(regress_0_tests regress0/options/didyoumean.smt2 regress0/options/help.smt2 regress0/options/interactive-mode.smt2 + regress0/options/named_muted.smt2 regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 regress0/options/statistics.smt2 @@ -1303,6 +1310,7 @@ set(regress_0_tests regress0/sygus/General_plus10.sy regress0/sygus/hd-05-d1-prog-nogrammar.sy regress0/sygus/ho-occ-synth-fun.sy + regress0/sygus/incremental-modify-ex.sy regress0/sygus/inv-different-var-order.sy regress0/sygus/issue3356-syg-inf-usort.smt2 regress0/sygus/issue3624.sy @@ -1597,6 +1605,7 @@ set(regress_1_tests regress1/bug694-Unapply1.scala-0.smt2 regress1/bug800.smt2 regress1/bags/card1.smt2 + regress1/bags/card2.smt2 regress1/bags/choose1.smt2 regress1/bags/choose2.smt2 regress1/bags/choose3.smt2 @@ -1616,10 +1625,12 @@ set(regress_1_tests regress1/bags/intersection_min1.smt2 regress1/bags/intersection_min2.smt2 regress1/bags/issue5759.smt2 - regress1/bags/map-lazy-lam.smt2 regress1/bags/map1.smt2 regress1/bags/map2.smt2 regress1/bags/map3.smt2 + regress1/bags/map-lazy-lam.smt2 + regress1/bags/murxla1.smt2 + regress1/bags/murxla2.smt2 regress1/bags/subbag1.smt2 regress1/bags/subbag2.smt2 regress1/bags/union_disjoint.smt2 @@ -1679,6 +1690,7 @@ set(regress_1_tests regress1/decision/wishue149-2.smt2 regress1/decision/wishue149-3.smt2 regress1/decision/wishue160.smt2 + regress1/difficulty-polarity.smt2 regress1/errorcrash.smt2 regress1/fp/fp_to_real.smt2 regress1/fp/rti_3_5_bug_report.smt2 @@ -1845,6 +1857,7 @@ set(regress_1_tests regress1/nl/tan-rewrite2.smt2 regress1/nl/zero-subset.smt2 regress1/non-fatal-errors.smt2 + regress1/proj-issue175.smt2 regress1/proof00.smt2 regress1/proofs/issue6625-unsat-core-proofs.smt2 regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 @@ -2218,6 +2231,8 @@ set(regress_1_tests regress1/sets/issue5342_difference_version.smt2 regress1/sets/issue5942-witness.smt2 regress1/sets/lemmabug-ListElts317minimized.smt2 + regress1/sets/proj-issue164.smt2 + regress1/sets/proj-issue178.smt2 regress1/sets/remove_check_free_31_6.smt2 regress1/sets/sets-disequal.smt2 regress1/sets/sets-tuple-poly.cvc.smt2 @@ -2510,6 +2525,9 @@ set(regress_1_tests regress1/sygus/phone-1-long.sy regress1/sygus/planning-unif.sy regress1/sygus/process-10-vars.sy + regress1/sygus/proj-issue181.smt2 + regress1/sygus/proj-issue183.smt2 + regress1/sygus/proj-issue185.smt2 regress1/sygus/pLTL_5_trace.sy regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 @@ -2612,6 +2630,7 @@ set(regress_2_tests regress2/bv_to_int_mask_array_2.smt2 regress2/bv_to_int_mask_array_3.smt2 regress2/bv_to_int_shifts.smt2 + regress2/bv_to_int_quantifiers_bvand.smt2 regress2/error1.smtv1.smt2 regress2/fp/issue7056.smt2 regress2/fuzz_2.smtv1.smt2 @@ -2677,7 +2696,7 @@ set(regress_2_tests regress2/strings/replaceall-diffrange.smt2 regress2/strings/replaceall-len-c.smt2 regress2/strings/small-1.smt2 - regress2/strings/strings-alpha-card-129.smt2 + regress2/strings/strings-alpha-card-65.smt2 regress2/strings/update-ex3.smt2 regress2/strings/update-ex4-seq.smt2 regress2/sygus/MPwL_d1s3.sy diff --git a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 index ccb50c55d..b49287c30 100644 --- a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 +++ b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 @@ -1,6 +1,6 @@ ; REQUIRES: poly ; COMMAND-LINE: --theoryof-mode=term --nl-icp -; EXPECT: unknown +; EXPECT: sat (set-logic QF_NRA) (set-option :check-proofs true) (declare-fun x () Real) diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 index 3908cdb16..eb8e75803 100644 --- a/test/regress/regress0/bv/bv_to_int1.smt2 +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: unsat (set-logic QF_BV) (declare-fun x () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 index 91e0c45fd..eced6e0e9 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun T4_180 () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 index 3e545ef03..45d539f04 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_UFBV) (declare-fun a () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 index 0a0ec7b20..ae77380dd 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_UFBV) (declare-sort S 0) diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 index 01ee5dad8..cb7eefbb2 100644 --- a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 +++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 @@ -1,4 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun _substvar_183_ () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_int1.smt2 b/test/regress/regress0/bv/bv_to_int_int1.smt2 new file mode 100644 index 000000000..3295d3481 --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_int1.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; EXPECT: sat +(set-logic QF_ALL) +(declare-fun x () (_ BitVec 4)) +(declare-fun y () (_ BitVec 4)) +(declare-fun z () Int) +(declare-fun w () Int) +(assert (= x (_ bv3 4))) +(assert (= y (_ bv3 4))) +(assert (> z w)) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2 index 8bf4a825d..4fd6109f4 100644 --- a/test/regress/regress0/bv/bv_to_int_zext.smt2 +++ b/test/regress/regress0/bv/bv_to_int_zext.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: unsat (set-logic QF_BV) (declare-fun T1_31078 () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/proj-issue343.smt2 b/test/regress/regress0/bv/proj-issue343.smt2 new file mode 100644 index 000000000..6d2971ad8 --- /dev/null +++ b/test/regress/regress0/bv/proj-issue343.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +; COMMAND-LINE: --no-check-models +(set-logic ALL) +(set-option :solve-bv-as-int bv) +(declare-const _x8 Real) +(assert (distinct real.pi _x8)) +(check-sat) diff --git a/test/regress/regress0/datatypes/par-updater-type-rule.smt2 b/test/regress/regress0/datatypes/par-updater-type-rule.smt2 new file mode 100644 index 000000000..0b4af0287 --- /dev/null +++ b/test/regress/regress0/datatypes/par-updater-type-rule.smt2 @@ -0,0 +1,11 @@ +(set-option :global-declarations true) +(set-logic ALL) +(set-info :status unsat) +(declare-datatype _x0 ( (_x6 (_x1 Bool)))) +(declare-datatype _x36 ( (_x42 (_x37 Bool)))) +(declare-const _x53 Bool) +(declare-const _x56 _x36) +(declare-const _x58 _x0) +(declare-datatype _x176 ( par ( _x178 ) ( (_x186 (_x185 _x178)) (_x184 (_x180 _x0)))) ) +(assert (let ((_let0 ((_ update _x185) (_x184 _x58) _x58)))(distinct _let0 _let0))) +(check-sat) diff --git a/test/regress/regress0/datatypes/proj-issue172.smt2 b/test/regress/regress0/datatypes/proj-issue172.smt2 new file mode 100644 index 000000000..f9f5a2ffc --- /dev/null +++ b/test/regress/regress0/datatypes/proj-issue172.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status sat) +(declare-codatatypes ((a 0)) (((b (c Int) (d a))))) +(declare-fun e () a) +(declare-fun f () a) +(assert (= e f)) +(check-sat) diff --git a/test/regress/regress0/difficulty-model-ex.smt2 b/test/regress/regress0/difficulty-model-ex.smt2 new file mode 100644 index 000000000..0546b5118 --- /dev/null +++ b/test/regress/regress0/difficulty-model-ex.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --produce-difficulty --difficulty-mode=model-check +; SCRUBBER: sed 's/.*//g' +; EXIT: 0 + +(set-logic ALL) +(set-option :produce-difficulty true) +(declare-fun P (Int) Bool) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) + +(assert (= z 78)) + +(assert (! (= (* x x) z) :named a1)) + +(assert (= y 0)) + +(assert (P y)) + +(check-sat) + +(get-difficulty) diff --git a/test/regress/regress0/difficulty-simple.smt2 b/test/regress/regress0/difficulty-simple.smt2 new file mode 100644 index 000000000..a82a96550 --- /dev/null +++ b/test/regress/regress0/difficulty-simple.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --produce-difficulty +; SCRUBBER: sed 's/.*//g' +; EXIT: 0 + +(set-logic ALL) +(set-option :produce-difficulty true) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) + +(assert (or (> a 0) (> b 0) (> c 0))) + +(assert (< (ite (> a b) a b) 0)) + +(check-sat) +(get-difficulty) diff --git a/test/regress/regress0/options/didyoumean.smt2 b/test/regress/regress0/options/didyoumean.smt2 index d95c1bde9..100e1e6fb 100644 --- a/test/regress/regress0/options/didyoumean.smt2 +++ b/test/regress/regress0/options/didyoumean.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: no-competition ; COMMAND-LINE: --input-agnuage ; ERROR-SCRUBBER: grep -o "--[a-zA-Z-]+" ; ERROR-EXPECT: --input-language diff --git a/test/regress/regress0/options/named_muted.smt2 b/test/regress/regress0/options/named_muted.smt2 new file mode 100644 index 000000000..7026298c6 --- /dev/null +++ b/test/regress/regress0/options/named_muted.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --print-success +; EXPECT: success +; EXPECT: success + +(set-logic UF) +(assert (! true :named t)) diff --git a/test/regress/regress0/sygus/incremental-modify-ex.sy b/test/regress/regress0/sygus/incremental-modify-ex.sy new file mode 100644 index 000000000..f453964b0 --- /dev/null +++ b/test/regress/regress0/sygus/incremental-modify-ex.sy @@ -0,0 +1,26 @@ +; COMMAND-LINE: -i --sygus-out=status +;EXPECT: unsat +;EXPECT: unsat +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) + ((Start Int (0 1 x y + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (not StartBool) + (<= Start Start))))) + + +(declare-var x Int) +(declare-var y Int) + +(push 1) +(constraint (>= (f x y) 0)) +(check-synth) +(pop 1) + +(constraint (< (f x y) 0)) +(check-synth) diff --git a/test/regress/regress1/bags/card1.smt2 b/test/regress/regress1/bags/card1.smt2 index 4ea5488d2..3b19fb2cf 100644 --- a/test/regress/regress1/bags/card1.smt2 +++ b/test/regress/regress1/bags/card1.smt2 @@ -1,7 +1,8 @@ -; COMMAND-LINE: --fmf-bound --uf-lazy-ll -; EXPECT: sat -(set-logic HO_ALL) -(define-fun f ((x String)) Int 1) +(set-logic ALL) +(set-option :fmf-bound true) +(set-option :produce-models true) +(set-info :status sat) (declare-fun A () (Bag String)) -(assert (= (bag.card A) 20)) +(assert (= (bag.card A) 10000000)) (check-sat) + diff --git a/test/regress/regress1/bags/card2.smt2 b/test/regress/regress1/bags/card2.smt2 new file mode 100644 index 000000000..260c6927f --- /dev/null +++ b/test/regress/regress1/bags/card2.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-option :fmf-bound true) +(set-option :produce-models true) +(set-info :status sat) +(declare-fun A () (Bag String)) +(declare-fun B () (Bag String)) +(declare-fun C () (Bag String)) +(assert (distinct A B C (as bag.empty (Bag String)))) +(assert (= C (bag.union_disjoint A B))) +(assert (= (bag.card C) 10000000)) +(check-sat) diff --git a/test/regress/regress1/bags/murxla1.smt2 b/test/regress/regress1/bags/murxla1.smt2 new file mode 100644 index 000000000..248f566f0 --- /dev/null +++ b/test/regress/regress1/bags/murxla1.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) +(set-info :status sat) +(declare-const A (Bag Bool)) +(declare-const B (Bag Bool)) +(check-sat-assuming ((distinct A B))) diff --git a/test/regress/regress1/bags/murxla2.smt2 b/test/regress/regress1/bags/murxla2.smt2 new file mode 100644 index 000000000..82ca2e90c --- /dev/null +++ b/test/regress/regress1/bags/murxla2.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :strings-exp true) +(declare-const x Int) +(assert (seq.contains (seq.at (seq.unit (bag false x)) x) (seq.unit (bag false x)))) +(check-sat) diff --git a/test/regress/regress1/difficulty-polarity.smt2 b/test/regress/regress1/difficulty-polarity.smt2 new file mode 100644 index 000000000..ce2388c54 --- /dev/null +++ b/test/regress/regress1/difficulty-polarity.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --produce-difficulty +; SCRUBBER: sed 's/.*//g' +; EXIT: 0 + +(set-logic ALL) +(set-option :finite-model-find true) +(set-option :mbqi none) +(set-option :produce-difficulty true) + +(declare-sort U 0) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(assert (distinct a b c)) +(declare-fun P (U U) Bool) +(declare-fun R (U) Bool) +(declare-fun S (U) Bool) + +(define-fun Q () Bool (forall ((x U) (y U)) (P x y))) + +(assert (or (not Q) (S a))) +(assert (R a)) +(assert (=> (R a) Q)) + +; This example will instantiate the quantified formula 9 times, hence the +; explanation for why it is relevant will be incremented by 9. +; The explanation for why Q is relevant should be (=> (R b) Q) and +; not (or (not Q) (S a)), since the former is the reason it is asserted true. + +(check-sat) +(get-difficulty) diff --git a/test/regress/regress1/nl/cos1-tc.smt2 b/test/regress/regress1/nl/cos1-tc.smt2 index bedc0209b..ba49f23fe 100644 --- a/test/regress/regress1/nl/cos1-tc.smt2 +++ b/test/regress/regress1/nl/cos1-tc.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --nl-ext=full --no-nl-ext-tf-tplanes --no-nl-ext-inc-prec -; EXPECT: unknown +; EXPECT: sat (set-logic UFNRAT) (declare-fun f (Real) Real) diff --git a/test/regress/regress1/proj-issue175.smt2 b/test/regress/regress1/proj-issue175.smt2 new file mode 100644 index 000000000..2df1e21e6 --- /dev/null +++ b/test/regress/regress1/proj-issue175.smt2 @@ -0,0 +1,83 @@ +(set-logic QF_AUFNIA) +(set-info :status sat) +(declare-fun |#offset~STRUCT#?type~INT?length~UINT?off~UINT?data~$Pointer$?input~$Pointer$?comp~$Pointer$#~data| () Int) +(declare-fun |ssl3_accept_#t~mem38_491| () Int) +(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state| () Int) +(declare-fun ssl3_accept_~s.offset_12 () Int) +(declare-fun ssl3_accept_~s.base_12 () Int) +(declare-fun |#memory_int_136| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~mem35_173| () Int) +(declare-fun |ssl3_accept_#t~mem49_513| () Int) +(declare-fun |ssl3_accept_#t~mem29_161| () Int) +(declare-fun |#memory_int_53| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~mem24_68| () Int) +(declare-fun |#memory_int_601| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~mem31_631| () Int) +(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~init_num| () Int) +(declare-fun |#memory_$Pointer$.base_53| () (Array Int (Array Int Int))) +(declare-fun |#memory_$Pointer$.base_52| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~nondet159_515| () Int) +(declare-fun ssl3_accept_~ret~10_753 () Int) +(declare-fun ssl3_accept_~ret~10_314 () Int) +(declare-fun |ssl3_accept_#t~mem22_459| () Int) +(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~s3| () Int) +(declare-fun |#memory_$Pointer$.offset_521| () (Array Int (Array Int Int))) +(declare-fun |ssl3_accept_#t~mem165.offset_593| () Int) +(declare-fun |ssl3_accept_#t~mem23_461| () Int) +(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~packet| () Int) +(assert + (let (($x220 (= |#offset~STRUCT#?type~INT?length~UINT?off~UINT?data~$Pointer$?input~$Pointer$?comp~$Pointer$#~data| 12))) + (let (($x2621 (= |ssl3_accept_#t~mem38_491| 8544))) + (let (($x2622 (not $x2621))) + (let (($x10875 (not $x2622))) + (let (($x23085 (and $x10875 $x220))) + (not $x23085))))))) +(assert + (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|))) + (let ((?x1399 (select |#memory_int_136| ssl3_accept_~s.base_12))) + (let ((?x1400 (select ?x1399 ?x806))) + (let (($x1478 (>= |ssl3_accept_#t~mem35_173| ?x1400))) + (not $x1478)))))) +(assert + (let (($x2678 (>= |ssl3_accept_#t~mem49_513| 8640))) + (not $x2678))) +(assert + (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|))) + (let ((?x1399 (select |#memory_int_136| ssl3_accept_~s.base_12))) + (let ((?x1400 (select ?x1399 ?x806))) + (let (($x1447 (<= |ssl3_accept_#t~mem29_161| ?x1400))) + (let ((?x1089 (select |#memory_int_53| ssl3_accept_~s.base_12))) + (let ((?x1090 (select ?x1089 ?x806))) + (let (($x1113 (>= |ssl3_accept_#t~mem24_68| ?x1090))) + (let (($x19982 (and $x1113 $x1447))) + (not $x19982)))))))))) +(assert + (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|))) + (let ((?x3029 (select |#memory_int_601| ssl3_accept_~s.base_12))) + (let ((?x3030 (select ?x3029 ?x806))) + (let (($x3088 (>= |ssl3_accept_#t~mem31_631| ?x3030))) + (let ((?x1050 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~init_num|))) + (let ((?x1051 (select |#memory_$Pointer$.base_53| ssl3_accept_~s.base_12))) + (let ((?x1032 (select |#memory_$Pointer$.base_52| ssl3_accept_~s.base_12))) + (let ((?x1054 (store |#memory_$Pointer$.base_52| ssl3_accept_~s.base_12 (store ?x1032 ?x1050 (select ?x1051 ?x1050))))) + (let (($x1055 (= |#memory_$Pointer$.base_53| ?x1054))) + (let (($x11490 (and $x1055 $x3088))) + (not $x11490)))))))))))) +(assert + (let (($x3458 (>= ssl3_accept_~ret~10_753 |ssl3_accept_#t~nondet159_515|))) + (let (($x2065 (not (<= ssl3_accept_~ret~10_314 0)))) + (let (($x50182 (and $x2065 $x3458))) + (not $x50182))))) +(assert + (let (($x2542 (not (= |ssl3_accept_#t~mem22_459| 16384)))) + (let ((?x1068 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~s3|))) + (let ((?x2719 (select |#memory_$Pointer$.offset_521| ssl3_accept_~s.base_12))) + (let ((?x2734 (select ?x2719 ?x1068))) + (let (($x2925 (<= |ssl3_accept_#t~mem165.offset_593| ?x2734))) + (and $x2925 $x2542))))))) +(assert + (let (($x2547 (not (= |ssl3_accept_#t~mem23_461| 8192)))) + (let (($x73 (= |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~packet| 72))) + (let (($x11452 (and $x73 $x2547))) + (not $x11452))))) +(check-sat) diff --git a/test/regress/regress1/sets/proj-issue164.smt2 b/test/regress/regress1/sets/proj-issue164.smt2 new file mode 100644 index 000000000..5e343156e --- /dev/null +++ b/test/regress/regress1/sets/proj-issue164.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun b () (Set String)) +(declare-fun c () (Set (Tuple Int Int))) +(declare-fun d () (Set (Tuple Int Int))) +(declare-fun e () Int) +(assert (distinct c (set.insert (tuple 0 0) (set.singleton (tuple 1 1))))) +(assert (distinct d (rel.tclosure c))) +(assert (distinct e (set.card b))) +(check-sat) diff --git a/test/regress/regress1/sets/proj-issue178.smt2 b/test/regress/regress1/sets/proj-issue178.smt2 new file mode 100644 index 000000000..2b95f43c9 --- /dev/null +++ b/test/regress/regress1/sets/proj-issue178.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :sygus-inference true) +(set-option :sets-infer-as-lemmas false) +(declare-fun a () (Set Int)) +(declare-fun b () (Set Int)) +(declare-fun c () (Set Int)) +(declare-fun d () Int) +(assert (> (set.card (set.minus a (set.inter (set.minus a b) (set.minus a c)))) d)) +(check-sat) diff --git a/test/regress/regress1/sygus/proj-issue181.smt2 b/test/regress/regress1/sygus/proj-issue181.smt2 new file mode 100644 index 000000000..656d1e757 --- /dev/null +++ b/test/regress/regress1/sygus/proj-issue181.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :sygus-inference true) +(set-info :status sat) +(declare-fun a (Int) Int) +(assert (exists ((b Int)) (distinct (a b) (- b 29)))) +(assert (distinct (a 0) (- 4))) +(assert (= (a (- 99)) (- 107))) +(check-sat) diff --git a/test/regress/regress1/sygus/proj-issue183.smt2 b/test/regress/regress1/sygus/proj-issue183.smt2 new file mode 100644 index 000000000..e50e035f3 --- /dev/null +++ b/test/regress/regress1/sygus/proj-issue183.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(set-option :sygus-inference true) +(set-info :status sat) +(declare-fun a () String) +(declare-fun b () String) +(declare-const c String) +(declare-const d String) +(declare-fun g () Bool) +(declare-fun e () Bool) +(declare-fun f () String) +(assert (str.in_re (str.substr a 0 (str.len (str.substr a 0 (str.len (str.substr a 0 (str.len c)))))) (re.* (re.++ (str.to_re "") (re.* (str.to_re "aa")))))) +(assert (str.in_re (str.substr b 0 (str.len d)) (re.* (re.++ (re.* (str.to_re "")) (str.to_re "bb"))))) +(assert (= 4 (str.len d))) +(assert (not (= (str.substr a 0 (str.len c)) d))) +(assert (= g (not (= "file" (str.substr a (str.len c) (str.len f)))))) +(assert (= e (not g))) +(assert e) +(check-sat) diff --git a/test/regress/regress1/sygus/proj-issue185.smt2 b/test/regress/regress1/sygus/proj-issue185.smt2 new file mode 100644 index 000000000..a3e4b8205 --- /dev/null +++ b/test/regress/regress1/sygus/proj-issue185.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: -q +; EXPECT: unsat +(set-logic ALL) +(set-option :sygus-inference true) +(set-info :status unsat) +(declare-codatatypes ((a 0)) (((b (c Int) (d a))))) +(declare-fun e () a) +(declare-fun f () a) +(assert (= e (b 0 (b 0 e)))) +(assert (distinct f (b 0 f))) +(assert (not (distinct e f))) +(check-sat) diff --git a/test/regress/regress2/bv_to_int2.smt2 b/test/regress/regress2/bv_to_int2.smt2 index 424e95b27..b9c27c6b8 100644 --- a/test/regress/regress2/bv_to_int2.smt2 +++ b/test/regress/regress2/bv_to_int2.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2 index 0c6768546..1f5df2c31 100644 --- a/test/regress/regress2/bv_to_int_ashr.smt2 +++ b/test/regress/regress2/bv_to_int_ashr.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_bitwise.smt2 b/test/regress/regress2/bv_to_int_bitwise.smt2 index 23624e12c..4dc37a94c 100644 --- a/test/regress/regress2/bv_to_int_bitwise.smt2 +++ b/test/regress/regress2/bv_to_int_bitwise.smt2 @@ -1,8 +1,10 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 -; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value -; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum -; COMMAND-LINE: --solve-bv-as-int=bv +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=5 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress2/bv_to_int_bvmul1.smt2 b/test/regress/regress2/bv_to_int_bvmul1.smt2 index 232959f33..bf6f2cfc4 100644 --- a/test/regress/regress2/bv_to_int_bvmul1.smt2 +++ b/test/regress/regress2/bv_to_int_bvmul1.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 index babf9af32..2ecd0fe6c 100644 --- a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 +++ b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 @@ -1,4 +1,5 @@ -;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-unsat-cores +;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +;COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores ;EXPECT: unsat (set-logic QF_UFBV) (declare-fun z$n0s32 () (_ BitVec 32)) diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2 index 4b22c8ed8..28fb86f76 100644 --- a/test/regress/regress2/bv_to_int_inc1.smt2 +++ b/test/regress/regress2/bv_to_int_inc1.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --incremental --solve-bv-as-int=sum +; COMMAND-LINE: --incremental --solve-bv-as-int=bitwise ; COMMAND-LINE: --incremental --solve-bv-as-int=iand ; COMMAND-LINE: --incremental --solve-bv-as-int=bv ; EXPECT sat diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2 index 3b55c035d..c12138091 100644 --- a/test/regress/regress2/bv_to_int_mask_array_1.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2 @@ -1,5 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 -; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores ; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores ; EXPECT: unsat diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2 index edcc14149..17a113f85 100644 --- a/test/regress/regress2/bv_to_int_mask_array_2.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum ; COMMAND-LINE: --solve-bv-as-int=bv diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2 index 74e5ca95a..2b411209d 100644 --- a/test/regress/regress2/bv_to_int_mask_array_3.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic ALL) (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4))) diff --git a/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 new file mode 100644 index 000000000..d454ad630 --- /dev/null +++ b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores +; EXPECT: (error "Error in option parsing: --solve-bv-as-int=bitwise does not support quantifiers") +; EXIT: 1 +(set-logic BV) +(declare-const x (_ BitVec 8)) +(assert (forall ((y (_ BitVec 8))) + (distinct #b00000000 + (bvand x y)))) +(check-sat) diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2 index bcc31c38c..173f1a552 100644 --- a/test/regress/regress2/bv_to_int_shifts.smt2 +++ b/test/regress/regress2/bv_to_int_shifts.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress2/strings/strings-alpha-card-129.smt2 b/test/regress/regress2/strings/strings-alpha-card-129.smt2 deleted file mode 100644 index c0b4ae0a2..000000000 --- a/test/regress/regress2/strings/strings-alpha-card-129.smt2 +++ /dev/null @@ -1,393 +0,0 @@ -; COMMAND-LINE: --strings-alpha-card=128 --simplification=none -; EXPECT: unsat -(set-logic QF_SLIA) -(declare-fun s1 () String) -(assert (= (str.len s1) 1)) -(declare-fun s2 () String) -(assert (= (str.len s2) 1)) -(declare-fun s3 () String) -(assert (= (str.len s3) 1)) -(declare-fun s4 () String) -(assert (= (str.len s4) 1)) -(declare-fun s5 () String) -(assert (= (str.len s5) 1)) -(declare-fun s6 () String) -(assert (= (str.len s6) 1)) -(declare-fun s7 () String) -(assert (= (str.len s7) 1)) -(declare-fun s8 () String) -(assert (= (str.len s8) 1)) -(declare-fun s9 () String) -(assert (= (str.len s9) 1)) -(declare-fun s10 () String) -(assert (= (str.len s10) 1)) -(declare-fun s11 () String) -(assert (= (str.len s11) 1)) -(declare-fun s12 () String) -(assert (= (str.len s12) 1)) -(declare-fun s13 () String) -(assert (= (str.len s13) 1)) -(declare-fun s14 () String) -(assert (= (str.len s14) 1)) -(declare-fun s15 () String) -(assert (= (str.len s15) 1)) -(declare-fun s16 () String) -(assert (= (str.len s16) 1)) -(declare-fun s17 () String) -(assert (= (str.len s17) 1)) -(declare-fun s18 () String) -(assert (= (str.len s18) 1)) -(declare-fun s19 () String) -(assert (= (str.len s19) 1)) -(declare-fun s20 () String) -(assert (= (str.len s20) 1)) -(declare-fun s21 () String) -(assert (= (str.len s21) 1)) -(declare-fun s22 () String) -(assert (= (str.len s22) 1)) -(declare-fun s23 () String) -(assert (= (str.len s23) 1)) -(declare-fun s24 () String) -(assert (= (str.len s24) 1)) -(declare-fun s25 () String) -(assert (= (str.len s25) 1)) -(declare-fun s26 () String) -(assert (= (str.len s26) 1)) -(declare-fun s27 () String) -(assert (= (str.len s27) 1)) -(declare-fun s28 () String) -(assert (= (str.len s28) 1)) -(declare-fun s29 () String) -(assert (= (str.len s29) 1)) -(declare-fun s30 () String) -(assert (= (str.len s30) 1)) -(declare-fun s31 () String) -(assert (= (str.len s31) 1)) -(declare-fun s32 () String) -(assert (= (str.len s32) 1)) -(declare-fun s33 () String) -(assert (= (str.len s33) 1)) -(declare-fun s34 () String) -(assert (= (str.len s34) 1)) -(declare-fun s35 () String) -(assert (= (str.len s35) 1)) -(declare-fun s36 () String) -(assert (= (str.len s36) 1)) -(declare-fun s37 () String) -(assert (= (str.len s37) 1)) -(declare-fun s38 () String) -(assert (= (str.len s38) 1)) -(declare-fun s39 () String) -(assert (= (str.len s39) 1)) -(declare-fun s40 () String) -(assert (= (str.len s40) 1)) -(declare-fun s41 () String) -(assert (= (str.len s41) 1)) -(declare-fun s42 () String) -(assert (= (str.len s42) 1)) -(declare-fun s43 () String) -(assert (= (str.len s43) 1)) -(declare-fun s44 () String) -(assert (= (str.len s44) 1)) -(declare-fun s45 () String) -(assert (= (str.len s45) 1)) -(declare-fun s46 () String) -(assert (= (str.len s46) 1)) -(declare-fun s47 () String) -(assert (= (str.len s47) 1)) -(declare-fun s48 () String) -(assert (= (str.len s48) 1)) -(declare-fun s49 () String) -(assert (= (str.len s49) 1)) -(declare-fun s50 () String) -(assert (= (str.len s50) 1)) -(declare-fun s51 () String) -(assert (= (str.len s51) 1)) -(declare-fun s52 () String) -(assert (= (str.len s52) 1)) -(declare-fun s53 () String) -(assert (= (str.len s53) 1)) -(declare-fun s54 () String) -(assert (= (str.len s54) 1)) -(declare-fun s55 () String) -(assert (= (str.len s55) 1)) -(declare-fun s56 () String) -(assert (= (str.len s56) 1)) -(declare-fun s57 () String) -(assert (= (str.len s57) 1)) -(declare-fun s58 () String) -(assert (= (str.len s58) 1)) -(declare-fun s59 () String) -(assert (= (str.len s59) 1)) -(declare-fun s60 () String) -(assert (= (str.len s60) 1)) -(declare-fun s61 () String) -(assert (= (str.len s61) 1)) -(declare-fun s62 () String) -(assert (= (str.len s62) 1)) -(declare-fun s63 () String) -(assert (= (str.len s63) 1)) -(declare-fun s64 () String) -(assert (= (str.len s64) 1)) -(declare-fun s65 () String) -(assert (= (str.len s65) 1)) -(declare-fun s66 () String) -(assert (= (str.len s66) 1)) -(declare-fun s67 () String) -(assert (= (str.len s67) 1)) -(declare-fun s68 () String) -(assert (= (str.len s68) 1)) -(declare-fun s69 () String) -(assert (= (str.len s69) 1)) -(declare-fun s70 () String) -(assert (= (str.len s70) 1)) -(declare-fun s71 () String) -(assert (= (str.len s71) 1)) -(declare-fun s72 () String) -(assert (= (str.len s72) 1)) -(declare-fun s73 () String) -(assert (= (str.len s73) 1)) -(declare-fun s74 () String) -(assert (= (str.len s74) 1)) -(declare-fun s75 () String) -(assert (= (str.len s75) 1)) -(declare-fun s76 () String) -(assert (= (str.len s76) 1)) -(declare-fun s77 () String) -(assert (= (str.len s77) 1)) -(declare-fun s78 () String) -(assert (= (str.len s78) 1)) -(declare-fun s79 () String) -(assert (= (str.len s79) 1)) -(declare-fun s80 () String) -(assert (= (str.len s80) 1)) -(declare-fun s81 () String) -(assert (= (str.len s81) 1)) -(declare-fun s82 () String) -(assert (= (str.len s82) 1)) -(declare-fun s83 () String) -(assert (= (str.len s83) 1)) -(declare-fun s84 () String) -(assert (= (str.len s84) 1)) -(declare-fun s85 () String) -(assert (= (str.len s85) 1)) -(declare-fun s86 () String) -(assert (= (str.len s86) 1)) -(declare-fun s87 () String) -(assert (= (str.len s87) 1)) -(declare-fun s88 () String) -(assert (= (str.len s88) 1)) -(declare-fun s89 () String) -(assert (= (str.len s89) 1)) -(declare-fun s90 () String) -(assert (= (str.len s90) 1)) -(declare-fun s91 () String) -(assert (= (str.len s91) 1)) -(declare-fun s92 () String) -(assert (= (str.len s92) 1)) -(declare-fun s93 () String) -(assert (= (str.len s93) 1)) -(declare-fun s94 () String) -(assert (= (str.len s94) 1)) -(declare-fun s95 () String) -(assert (= (str.len s95) 1)) -(declare-fun s96 () String) -(assert (= (str.len s96) 1)) -(declare-fun s97 () String) -(assert (= (str.len s97) 1)) -(declare-fun s98 () String) -(assert (= (str.len s98) 1)) -(declare-fun s99 () String) -(assert (= (str.len s99) 1)) -(declare-fun s100 () String) -(assert (= (str.len s100) 1)) -(declare-fun s101 () String) -(assert (= (str.len s101) 1)) -(declare-fun s102 () String) -(assert (= (str.len s102) 1)) -(declare-fun s103 () String) -(assert (= (str.len s103) 1)) -(declare-fun s104 () String) -(assert (= (str.len s104) 1)) -(declare-fun s105 () String) -(assert (= (str.len s105) 1)) -(declare-fun s106 () String) -(assert (= (str.len s106) 1)) -(declare-fun s107 () String) -(assert (= (str.len s107) 1)) -(declare-fun s108 () String) -(assert (= (str.len s108) 1)) -(declare-fun s109 () String) -(assert (= (str.len s109) 1)) -(declare-fun s110 () String) -(assert (= (str.len s110) 1)) -(declare-fun s111 () String) -(assert (= (str.len s111) 1)) -(declare-fun s112 () String) -(assert (= (str.len s112) 1)) -(declare-fun s113 () String) -(assert (= (str.len s113) 1)) -(declare-fun s114 () String) -(assert (= (str.len s114) 1)) -(declare-fun s115 () String) -(assert (= (str.len s115) 1)) -(declare-fun s116 () String) -(assert (= (str.len s116) 1)) -(declare-fun s117 () String) -(assert (= (str.len s117) 1)) -(declare-fun s118 () String) -(assert (= (str.len s118) 1)) -(declare-fun s119 () String) -(assert (= (str.len s119) 1)) -(declare-fun s120 () String) -(assert (= (str.len s120) 1)) -(declare-fun s121 () String) -(assert (= (str.len s121) 1)) -(declare-fun s122 () String) -(assert (= (str.len s122) 1)) -(declare-fun s123 () String) -(assert (= (str.len s123) 1)) -(declare-fun s124 () String) -(assert (= (str.len s124) 1)) -(declare-fun s125 () String) -(assert (= (str.len s125) 1)) -(declare-fun s126 () String) -(assert (= (str.len s126) 1)) -(declare-fun s127 () String) -(assert (= (str.len s127) 1)) -(declare-fun s128 () String) -(assert (= (str.len s128) 1)) -(declare-fun s129 () String) -(assert (= (str.len s129) 1)) -(assert (distinct -s1 -s2 -s3 -s4 -s5 -s6 -s7 -s8 -s9 -s10 -s11 -s12 -s13 -s14 -s15 -s16 -s17 -s18 -s19 -s20 -s21 -s22 -s23 -s24 -s25 -s26 -s27 -s28 -s29 -s30 -s31 -s32 -s33 -s34 -s35 -s36 -s37 -s38 -s39 -s40 -s41 -s42 -s43 -s44 -s45 -s46 -s47 -s48 -s49 -s50 -s51 -s52 -s53 -s54 -s55 -s56 -s57 -s58 -s59 -s60 -s61 -s62 -s63 -s64 -s65 -s66 -s67 -s68 -s69 -s70 -s71 -s72 -s73 -s74 -s75 -s76 -s77 -s78 -s79 -s80 -s81 -s82 -s83 -s84 -s85 -s86 -s87 -s88 -s89 -s90 -s91 -s92 -s93 -s94 -s95 -s96 -s97 -s98 -s99 -s100 -s101 -s102 -s103 -s104 -s105 -s106 -s107 -s108 -s109 -s110 -s111 -s112 -s113 -s114 -s115 -s116 -s117 -s118 -s119 -s120 -s121 -s122 -s123 -s124 -s125 -s126 -s127 -s128 -s129 -)) -(check-sat) diff --git a/test/regress/regress2/strings/strings-alpha-card-65.smt2 b/test/regress/regress2/strings/strings-alpha-card-65.smt2 new file mode 100644 index 000000000..82ab06ea9 --- /dev/null +++ b/test/regress/regress2/strings/strings-alpha-card-65.smt2 @@ -0,0 +1,201 @@ +; COMMAND-LINE: --strings-alpha-card=64 --simplification=none +; EXPECT: unsat +(set-logic QF_SLIA) +(declare-fun s1 () String) +(assert (= (str.len s1) 1)) +(declare-fun s2 () String) +(assert (= (str.len s2) 1)) +(declare-fun s3 () String) +(assert (= (str.len s3) 1)) +(declare-fun s4 () String) +(assert (= (str.len s4) 1)) +(declare-fun s5 () String) +(assert (= (str.len s5) 1)) +(declare-fun s6 () String) +(assert (= (str.len s6) 1)) +(declare-fun s7 () String) +(assert (= (str.len s7) 1)) +(declare-fun s8 () String) +(assert (= (str.len s8) 1)) +(declare-fun s9 () String) +(assert (= (str.len s9) 1)) +(declare-fun s10 () String) +(assert (= (str.len s10) 1)) +(declare-fun s11 () String) +(assert (= (str.len s11) 1)) +(declare-fun s12 () String) +(assert (= (str.len s12) 1)) +(declare-fun s13 () String) +(assert (= (str.len s13) 1)) +(declare-fun s14 () String) +(assert (= (str.len s14) 1)) +(declare-fun s15 () String) +(assert (= (str.len s15) 1)) +(declare-fun s16 () String) +(assert (= (str.len s16) 1)) +(declare-fun s17 () String) +(assert (= (str.len s17) 1)) +(declare-fun s18 () String) +(assert (= (str.len s18) 1)) +(declare-fun s19 () String) +(assert (= (str.len s19) 1)) +(declare-fun s20 () String) +(assert (= (str.len s20) 1)) +(declare-fun s21 () String) +(assert (= (str.len s21) 1)) +(declare-fun s22 () String) +(assert (= (str.len s22) 1)) +(declare-fun s23 () String) +(assert (= (str.len s23) 1)) +(declare-fun s24 () String) +(assert (= (str.len s24) 1)) +(declare-fun s25 () String) +(assert (= (str.len s25) 1)) +(declare-fun s26 () String) +(assert (= (str.len s26) 1)) +(declare-fun s27 () String) +(assert (= (str.len s27) 1)) +(declare-fun s28 () String) +(assert (= (str.len s28) 1)) +(declare-fun s29 () String) +(assert (= (str.len s29) 1)) +(declare-fun s30 () String) +(assert (= (str.len s30) 1)) +(declare-fun s31 () String) +(assert (= (str.len s31) 1)) +(declare-fun s32 () String) +(assert (= (str.len s32) 1)) +(declare-fun s33 () String) +(assert (= (str.len s33) 1)) +(declare-fun s34 () String) +(assert (= (str.len s34) 1)) +(declare-fun s35 () String) +(assert (= (str.len s35) 1)) +(declare-fun s36 () String) +(assert (= (str.len s36) 1)) +(declare-fun s37 () String) +(assert (= (str.len s37) 1)) +(declare-fun s38 () String) +(assert (= (str.len s38) 1)) +(declare-fun s39 () String) +(assert (= (str.len s39) 1)) +(declare-fun s40 () String) +(assert (= (str.len s40) 1)) +(declare-fun s41 () String) +(assert (= (str.len s41) 1)) +(declare-fun s42 () String) +(assert (= (str.len s42) 1)) +(declare-fun s43 () String) +(assert (= (str.len s43) 1)) +(declare-fun s44 () String) +(assert (= (str.len s44) 1)) +(declare-fun s45 () String) +(assert (= (str.len s45) 1)) +(declare-fun s46 () String) +(assert (= (str.len s46) 1)) +(declare-fun s47 () String) +(assert (= (str.len s47) 1)) +(declare-fun s48 () String) +(assert (= (str.len s48) 1)) +(declare-fun s49 () String) +(assert (= (str.len s49) 1)) +(declare-fun s50 () String) +(assert (= (str.len s50) 1)) +(declare-fun s51 () String) +(assert (= (str.len s51) 1)) +(declare-fun s52 () String) +(assert (= (str.len s52) 1)) +(declare-fun s53 () String) +(assert (= (str.len s53) 1)) +(declare-fun s54 () String) +(assert (= (str.len s54) 1)) +(declare-fun s55 () String) +(assert (= (str.len s55) 1)) +(declare-fun s56 () String) +(assert (= (str.len s56) 1)) +(declare-fun s57 () String) +(assert (= (str.len s57) 1)) +(declare-fun s58 () String) +(assert (= (str.len s58) 1)) +(declare-fun s59 () String) +(assert (= (str.len s59) 1)) +(declare-fun s60 () String) +(assert (= (str.len s60) 1)) +(declare-fun s61 () String) +(assert (= (str.len s61) 1)) +(declare-fun s62 () String) +(assert (= (str.len s62) 1)) +(declare-fun s63 () String) +(assert (= (str.len s63) 1)) +(declare-fun s64 () String) +(assert (= (str.len s64) 1)) +(declare-fun s65 () String) +(assert (= (str.len s65) 1)) +(assert (distinct +s1 +s2 +s3 +s4 +s5 +s6 +s7 +s8 +s9 +s10 +s11 +s12 +s13 +s14 +s15 +s16 +s17 +s18 +s19 +s20 +s21 +s22 +s23 +s24 +s25 +s26 +s27 +s28 +s29 +s30 +s31 +s32 +s33 +s34 +s35 +s36 +s37 +s38 +s39 +s40 +s41 +s42 +s43 +s44 +s45 +s46 +s47 +s48 +s49 +s50 +s51 +s52 +s53 +s54 +s55 +s56 +s57 +s58 +s59 +s60 +s61 +s62 +s63 +s64 +s65 +)) +(check-sat) diff --git a/test/regress/regress2/sygus/multi-udiv.sy b/test/regress/regress2/sygus/multi-udiv.sy index d9deb28a3..65e5d428f 100644 --- a/test/regress/regress2/sygus/multi-udiv.sy +++ b/test/regress/regress2/sygus/multi-udiv.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum (set-logic BV) (define-fun hd05 ((x (_ BitVec 32))) (_ BitVec 32) (bvor x (bvsub x #x00000001))) diff --git a/test/regress/regress2/sygus/sets-fun-test.sy b/test/regress/regress2/sygus/sets-fun-test.sy index 43a8b36a9..23abc5c7e 100644 --- a/test/regress/regress2/sygus/sets-fun-test.sy +++ b/test/regress/regress2/sygus/sets-fun-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum (set-logic ALL) (synth-fun f ((x Int)) (Set Int)) diff --git a/test/regress/regress2/sygus/three.sy b/test/regress/regress2/sygus/three.sy index 239f7f498..9bed1e667 100644 --- a/test/regress/regress2/sygus/three.sy +++ b/test/regress/regress2/sygus/three.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum (set-logic NIA) diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2 index 2c728417d..8ae10a04f 100644 --- a/test/regress/regress3/bv_to_int_and_or.smt2 +++ b/test/regress/regress3/bv_to_int_and_or.smt2 @@ -1,5 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=2 --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 4)) diff --git a/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 index aeacda35e..3a0320119 100644 --- a/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 +++ b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 @@ -1,5 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=bv -; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum +; COMMAND-LINE: --solve-bv-as-int=bv +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=bitwise ; EXPECT: sat (set-logic QF_BV) (declare-fun _substvar_1171_ () (_ BitVec 32)) diff --git a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 index c4988e3c6..3c50acc1c 100644 --- a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 +++ b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=bv -; COMMAND-LINE: --solve-bv-as-int=sum -; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum +; COMMAND-LINE: --solve-bv-as-int=bv +; COMMAND-LINE: --solve-bv-as-int=sum +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=bitwise ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value ; EXPECT: unsat diff --git a/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 index dd7e11a50..b37dc371d 100644 --- a/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 +++ b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --solve-bv-as-int=bv --no-check-models -; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --full-saturate-quant --cegqi-all --no-check-models +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --full-saturate-quant --cegqi-all --no-check-models ;EXPECT: sat (set-logic BV) (assert (exists ((c__detect__main__1__i_36_C (_ BitVec 32))) (bvslt ((_ sign_extend 32) c__detect__main__1__i_36_C) (_ bv0 64)))) diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index 745abc17c..fecf228a5 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -231,6 +231,7 @@ TEST_F(TestApiBlackDatatype, datatypeNames) dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); Datatype dt = dtypeSort.getDatatype(); + ASSERT_THROW(dt.getParameters(), CVC5ApiException); ASSERT_EQ(dt.getName(), std::string("list")); ASSERT_NO_THROW(dt.getConstructor("nil")); ASSERT_NO_THROW(dt["cons"]); @@ -274,6 +275,8 @@ TEST_F(TestApiBlackDatatype, parametricDatatype) Sort pairType = d_solver.mkDatatypeSort(pairSpec); ASSERT_TRUE(pairType.getDatatype().isParametric()); + std::vector<Sort> dparams = pairType.getDatatype().getParameters(); + ASSERT_TRUE(dparams[0] == t1 && dparams[1] == t2); v.clear(); v.push_back(d_solver.getIntegerSort()); @@ -576,12 +579,16 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) iargs.push_back(isort); Sort listInt = dtsorts[0].instantiate(iargs); + std::vector<Sort> liparams = listInt.getDatatype().getParameters(); + // the parameter of the datatype is not instantiated + ASSERT_TRUE(liparams.size() == 1 && liparams[0] == x); + Term testConsTerm; // get the specialized constructor term for list[Int] - ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt)); + ASSERT_NO_THROW(testConsTerm = nilc.getInstantiatedConstructorTerm(listInt)); ASSERT_NE(testConsTerm, nilc.getConstructorTerm()); // error to get the specialized constructor term for Int - ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC5ApiException); + ASSERT_THROW(nilc.getInstantiatedConstructorTerm(isort), CVC5ApiException); } } // namespace test } // namespace cvc5 diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 36b669bca..b17054637 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -929,22 +929,35 @@ TEST_F(TestApiBlackSolver, mkConstArray) TEST_F(TestApiBlackSolver, declareDatatype) { + DatatypeConstructorDecl lin = d_solver.mkDatatypeConstructorDecl("lin"); + std::vector<DatatypeConstructorDecl> ctors0 = {lin}; + ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors0)); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); std::vector<DatatypeConstructorDecl> ctors1 = {nil}; ASSERT_NO_THROW(d_solver.declareDatatype(std::string("a"), ctors1)); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil"); std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2}; ASSERT_NO_THROW(d_solver.declareDatatype(std::string("b"), ctors2)); + DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons"); DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil"); std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3}; ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors3)); + + // must have at least one constructor std::vector<DatatypeConstructorDecl> ctors4; ASSERT_THROW(d_solver.declareDatatype(std::string("c"), ctors4), CVC5ApiException); - ASSERT_THROW(d_solver.declareDatatype(std::string(""), ctors4), + // constructors may not be reused + DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21"); + DatatypeConstructorDecl ctor2 = d_solver.mkDatatypeConstructorDecl("_x31"); + Sort s3 = d_solver.declareDatatype(std::string("_x17"), {ctor1, ctor2}); + ASSERT_THROW(d_solver.declareDatatype(std::string("_x86"), {ctor1, ctor2}), CVC5ApiException); + // constructor belongs to different solver instance Solver slv; ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC5ApiException); } @@ -1443,13 +1456,16 @@ TEST_F(TestApiBlackSolver, getOptionInfo) } { // mode option - api::OptionInfo info = d_solver.getOptionInfo("output"); - EXPECT_EQ("output", info.name); - EXPECT_EQ(std::vector<std::string>{}, info.aliases); + api::OptionInfo info = d_solver.getOptionInfo("simplification"); + EXPECT_EQ("simplification", info.name); + EXPECT_EQ(std::vector<std::string>{"simplification-mode"}, info.aliases); EXPECT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo)); auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo); - EXPECT_EQ("none", modeInfo.defaultValue); - EXPECT_EQ("none", modeInfo.currentValue); + EXPECT_EQ("batch", modeInfo.defaultValue); + EXPECT_EQ("batch", modeInfo.currentValue); + EXPECT_EQ(2, modeInfo.modes.size()); + EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "batch") + != modeInfo.modes.end()); EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "none") != modeInfo.modes.end()); } @@ -2639,5 +2655,152 @@ TEST_F(TestApiBlackSolver, issue5893) ASSERT_NO_FATAL_FAILURE(distinct.getOp()); } +TEST_F(TestApiBlackSolver, proj_issue373) +{ + Sort s1 = d_solver.getRealSort(); + + DatatypeConstructorDecl ctor13 = d_solver.mkDatatypeConstructorDecl("_x115"); + ctor13.addSelector("_x109", s1); + Sort s4 = d_solver.declareDatatype("_x86", {ctor13}); + + Term t452 = d_solver.mkVar(s1, "_x281"); + Term bvl = d_solver.mkTerm(d_solver.mkOp(VARIABLE_LIST), {t452}); + Term acons = + d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR), + {s4.getDatatype().getConstructorTerm("_x115"), t452}); + // type exception + ASSERT_THROW( + d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR), {bvl, acons, t452}), + CVC5ApiException); +} + +TEST_F(TestApiBlackSolver, proj_issue378) +{ + DatatypeDecl dtdecl; + DatatypeConstructorDecl cdecl; + + Sort s1 = d_solver.getBooleanSort(); + + dtdecl = d_solver.mkDatatypeDecl("_x0"); + cdecl = d_solver.mkDatatypeConstructorDecl("_x6"); + cdecl.addSelector("_x1", s1); + dtdecl.addConstructor(cdecl); + Sort s2 = d_solver.mkDatatypeSort(dtdecl); + + dtdecl = d_solver.mkDatatypeDecl("_x36"); + cdecl = d_solver.mkDatatypeConstructorDecl("_x42"); + cdecl.addSelector("_x37", s1); + dtdecl.addConstructor(cdecl); + Sort s4 = d_solver.mkDatatypeSort(dtdecl); + + Term t1 = d_solver.mkConst(s1, "_x53"); + Term t4 = d_solver.mkConst(s4, "_x56"); + Term t7 = d_solver.mkConst(s2, "_x58"); + + Sort sp = d_solver.mkParamSort("_x178"); + dtdecl = d_solver.mkDatatypeDecl("_x176", sp); + cdecl = d_solver.mkDatatypeConstructorDecl("_x184"); + cdecl.addSelector("_x180", s2); + dtdecl.addConstructor(cdecl); + cdecl = d_solver.mkDatatypeConstructorDecl("_x186"); + cdecl.addSelector("_x185", sp); + dtdecl.addConstructor(cdecl); + Sort s7 = d_solver.mkDatatypeSort(dtdecl); + Sort s9 = s7.instantiate({s2}); + Term t1507 = d_solver.mkTerm( + APPLY_CONSTRUCTOR, s9.getDatatype().getConstructorTerm("_x184"), t7); + ASSERT_NO_THROW(d_solver.mkTerm( + APPLY_UPDATER, + s9.getDatatype().getConstructor("_x186").getSelectorTerm("_x185"), + t1507, + t7)); +} + +TEST_F(TestApiBlackSolver, proj_issue379) +{ + Sort bsort = d_solver.getBooleanSort(); + Sort psort = d_solver.mkParamSort("_x1"); + DatatypeConstructorDecl cdecl; + DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("x_0", psort); + cdecl = d_solver.mkDatatypeConstructorDecl("_x8"); + cdecl.addSelector("_x7", bsort); + dtdecl.addConstructor(cdecl); + cdecl = d_solver.mkDatatypeConstructorDecl("_x6"); + cdecl.addSelector("_x2", psort); + cdecl.addSelectorSelf("_x3"); + cdecl.addSelector("_x4", psort); + cdecl.addSelector("_x5", bsort); + Sort s2 = d_solver.mkDatatypeSort(dtdecl); + Sort s6 = s2.instantiate({bsort}); + Term t317 = d_solver.mkConst(bsort, "_x345"); + Term t843 = d_solver.mkConst(s6, "_x346"); + Term t879 = d_solver.mkTerm(APPLY_UPDATER, + t843.getSort() + .getDatatype() + .getConstructor("_x8") + .getSelector("_x7") + .getUpdaterTerm(), + t843, + t317); + ASSERT_EQ(t879.getSort(), s6); +} + +TEST_F(TestApiBlackSolver, getDatatypeArity) +{ + DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21"); + DatatypeConstructorDecl ctor2 = d_solver.mkDatatypeConstructorDecl("_x31"); + Sort s3 = d_solver.declareDatatype(std::string("_x17"), {ctor1, ctor2}); + ASSERT_EQ(s3.getDatatypeArity(), 0); +} + +TEST_F(TestApiBlackSolver, proj_issue381) +{ + Sort s1 = d_solver.getBooleanSort(); + + Sort psort = d_solver.mkParamSort("_x9"); + DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x8", psort); + DatatypeConstructorDecl ctor = d_solver.mkDatatypeConstructorDecl("_x22"); + ctor.addSelector("_x19", s1); + dtdecl.addConstructor(ctor); + Sort s3 = d_solver.mkDatatypeSort(dtdecl); + Sort s6 = s3.instantiate({s1}); + Term t26 = d_solver.mkConst(s6, "_x63"); + Term t5 = d_solver.mkTrue(); + Term t187 = d_solver.mkTerm(APPLY_UPDATER, + t26.getSort() + .getDatatype() + .getConstructor("_x22") + .getSelector("_x19") + .getUpdaterTerm(), + t26, + t5); + ASSERT_NO_THROW(d_solver.simplify(t187)); +} + +TEST_F(TestApiBlackSolver, proj_issue383) +{ + d_solver.setOption("produce-models", "true"); + + Sort s1 = d_solver.getBooleanSort(); + + DatatypeConstructorDecl ctordecl = d_solver.mkDatatypeConstructorDecl("_x5"); + DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x0"); + dtdecl.addConstructor(ctordecl); + Sort s2 = d_solver.mkDatatypeSort(dtdecl); + + ctordecl = d_solver.mkDatatypeConstructorDecl("_x23"); + ctordecl.addSelectorSelf("_x21"); + dtdecl = d_solver.mkDatatypeDecl("_x12"); + dtdecl.addConstructor(ctordecl); + Sort s4 = d_solver.mkDatatypeSort(dtdecl); + ASSERT_FALSE(s4.getDatatype().isWellFounded()); + + Term t3 = d_solver.mkConst(s4, "_x25"); + Term t13 = d_solver.mkConst(s1, "_x34"); + + d_solver.checkEntailed(t13); + ASSERT_THROW(d_solver.getValue(t3), CVC5ApiException); +} + } // namespace test } // namespace cvc5 diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index fb23ea515..e94785b08 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -248,6 +248,8 @@ class DatatypeTest Sort pairType = d_solver.mkDatatypeSort(pairSpec); assertTrue(pairType.getDatatype().isParametric()); + Sort[] dparams = pairType.getDatatype().getParameters(); + assertTrue(dparams[0].equals(t1) && dparams[1].equals(t2)); v.clear(); v.add(d_solver.getIntegerSort()); @@ -562,10 +564,12 @@ class DatatypeTest AtomicReference<Term> atomicTerm = new AtomicReference<>(); // get the specialized constructor term for list[Int] - assertDoesNotThrow(() -> atomicTerm.set(nilc.getSpecializedConstructorTerm(listInt))); + assertDoesNotThrow( + () -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt))); Term testConsTerm = atomicTerm.get(); assertNotEquals(testConsTerm, nilc.getConstructorTerm()); // error to get the specialized constructor term for Int - assertThrows(CVC5ApiException.class, () -> nilc.getSpecializedConstructorTerm(isort)); + assertThrows(CVC5ApiException.class, + () -> nilc.getInstantiatedConstructorTerm(isort)); } } diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index ed2f7491d..5d651e82a 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1428,15 +1428,17 @@ class SolverTest } { // mode option - OptionInfo info = d_solver.getOptionInfo("output"); + OptionInfo info = d_solver.getOptionInfo("simplification"); assertions.clear(); - assertions.add(() -> assertEquals("output", info.getName())); + assertions.add(() -> assertEquals("simplification", info.getName())); assertions.add( - () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases()))); + () -> assertEquals(Arrays.asList(new String[] {"simplification-mode"}), Arrays.asList(info.getAliases()))); assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ModeInfo.class)); OptionInfo.ModeInfo modeInfo = (OptionInfo.ModeInfo) info.getBaseInfo(); - assertions.add(() -> assertEquals("none", modeInfo.getDefaultValue())); - assertions.add(() -> assertEquals("none", modeInfo.getCurrentValue())); + assertions.add(() -> assertEquals("batch", modeInfo.getDefaultValue())); + assertions.add(() -> assertEquals("batch", modeInfo.getCurrentValue())); + assertions.add(() -> assertEquals(2, modeInfo.getModes().length)); + assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("batch"))); assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("none"))); } assertAll(assertions); diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index d8a4c26f7..af34e098e 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -13,7 +13,6 @@ import pytest import pycvc5 -from pycvc5 import kinds from pycvc5 import Sort, Term from pycvc5 import DatatypeDecl from pycvc5 import Datatype @@ -156,6 +155,8 @@ def test_datatype_structs(solver): dtypeSpec.addConstructor(nil) dtypeSort = solver.mkDatatypeSort(dtypeSpec) dt = dtypeSort.getDatatype() + # not parametric datatype + with pytest.raises(RuntimeError): dt.getParameters() assert not dt.isCodatatype() assert not dt.isTuple() assert not dt.isRecord() @@ -263,7 +264,7 @@ def test_parametric_datatype(solver): v.append(t1) v.append(t2) pairSpec = solver.mkDatatypeDecl("pair", v) - + mkpair = solver.mkDatatypeConstructorDecl("mk-pair") mkpair.addSelector("first", t1) mkpair.addSelector("second", t2) @@ -272,6 +273,8 @@ def test_parametric_datatype(solver): pairType = solver.mkDatatypeSort(pairSpec) assert pairType.getDatatype().isParametric() + dparams = pairType.getDatatype().getParameters() + assert dparams[0]==t1 and dparams[1]==t2 v.clear() v.append(solver.getIntegerSort()) @@ -559,8 +562,8 @@ def test_datatype_specialized_cons(solver): testConsTerm = Term(solver) # get the specialized constructor term for list[Int] - testConsTerm = nilc.getSpecializedConstructorTerm(listInt) + testConsTerm = nilc.getInstantiatedConstructorTerm(listInt) assert testConsTerm != nilc.getConstructorTerm() # error to get the specialized constructor term for Int with pytest.raises(RuntimeError): - nilc.getSpecializedConstructorTerm(isort) + nilc.getInstantiatedConstructorTerm(isort) diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py index db567a6ba..6225844e3 100644 --- a/test/unit/api/python/test_grammar.py +++ b/test/unit/api/python/test_grammar.py @@ -16,7 +16,7 @@ import pytest import pycvc5 -from pycvc5 import kinds, Term +from pycvc5 import Term @pytest.fixture diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index 5126a481d..a79fd0426 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -17,7 +17,7 @@ import pytest import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind from pycvc5 import Sort from pycvc5 import Op @@ -28,44 +28,44 @@ def solver(): def test_get_kind(solver): - x = solver.mkOp(kinds.BVExtract, 31, 1) + x = solver.mkOp(Kind.BVExtract, 31, 1) x.getKind() def test_is_null(solver): x = Op(solver) assert x.isNull() - x = solver.mkOp(kinds.BVExtract, 31, 1) + x = solver.mkOp(Kind.BVExtract, 31, 1) assert not x.isNull() def test_op_from_kind(solver): - solver.mkOp(kinds.Plus) + solver.mkOp(Kind.Plus) with pytest.raises(RuntimeError): - solver.mkOp(kinds.BVExtract) + solver.mkOp(Kind.BVExtract) def test_get_num_indices(solver): - plus = solver.mkOp(kinds.Plus) - divisible = solver.mkOp(kinds.Divisible, 4) - bitvector_repeat = solver.mkOp(kinds.BVRepeat, 5) - bitvector_zero_extend = solver.mkOp(kinds.BVZeroExtend, 6) - bitvector_sign_extend = solver.mkOp(kinds.BVSignExtend, 7) - bitvector_rotate_left = solver.mkOp(kinds.BVRotateLeft, 8) - bitvector_rotate_right = solver.mkOp(kinds.BVRotateRight, 9) - int_to_bitvector = solver.mkOp(kinds.IntToBV, 10) - iand = solver.mkOp(kinds.Iand, 3) - floatingpoint_to_ubv = solver.mkOp(kinds.FPToUbv, 11) - floatingopint_to_sbv = solver.mkOp(kinds.FPToSbv, 13) - floatingpoint_to_fp_ieee_bitvector = solver.mkOp(kinds.FPToFpIeeeBV, 4, 25) - floatingpoint_to_fp_floatingpoint = solver.mkOp(kinds.FPToFpFP, 4, 25) - floatingpoint_to_fp_real = solver.mkOp(kinds.FPToFpReal, 4, 25) - floatingpoint_to_fp_signed_bitvector = solver.mkOp(kinds.FPToFpSignedBV, 4, + plus = solver.mkOp(Kind.Plus) + divisible = solver.mkOp(Kind.Divisible, 4) + bitvector_repeat = solver.mkOp(Kind.BVRepeat, 5) + bitvector_zero_extend = solver.mkOp(Kind.BVZeroExtend, 6) + bitvector_sign_extend = solver.mkOp(Kind.BVSignExtend, 7) + bitvector_rotate_left = solver.mkOp(Kind.BVRotateLeft, 8) + bitvector_rotate_right = solver.mkOp(Kind.BVRotateRight, 9) + int_to_bitvector = solver.mkOp(Kind.IntToBV, 10) + iand = solver.mkOp(Kind.Iand, 3) + floatingpoint_to_ubv = solver.mkOp(Kind.FPToUbv, 11) + floatingopint_to_sbv = solver.mkOp(Kind.FPToSbv, 13) + floatingpoint_to_fp_ieee_bitvector = solver.mkOp(Kind.FPToFpIeeeBV, 4, 25) + floatingpoint_to_fp_floatingpoint = solver.mkOp(Kind.FPToFpFP, 4, 25) + floatingpoint_to_fp_real = solver.mkOp(Kind.FPToFpReal, 4, 25) + floatingpoint_to_fp_signed_bitvector = solver.mkOp(Kind.FPToFpSignedBV, 4, 25) floatingpoint_to_fp_unsigned_bitvector = solver.mkOp( - kinds.FPToFpUnsignedBV, 4, 25) - floatingpoint_to_fp_generic = solver.mkOp(kinds.FPToFpGeneric, 4, 25) - regexp_loop = solver.mkOp(kinds.RegexpLoop, 2, 3) + Kind.FPToFpUnsignedBV, 4, 25) + floatingpoint_to_fp_generic = solver.mkOp(Kind.FPToFpGeneric, 4, 25) + regexp_loop = solver.mkOp(Kind.RegexpLoop, 2, 3) assert 0 == plus.getNumIndices() assert 1 == divisible.getNumIndices() @@ -87,7 +87,7 @@ def test_get_num_indices(solver): assert 2 == regexp_loop.getNumIndices() def test_op_indices_list(solver): - with_list = solver.mkOp(kinds.TupleProject, [4, 25]) + with_list = solver.mkOp(Kind.TupleProject, [4, 25]) assert 2 == with_list.getNumIndices() def test_get_indices_string(solver): @@ -95,87 +95,87 @@ def test_get_indices_string(solver): with pytest.raises(RuntimeError): x.getIndices() - divisible_ot = solver.mkOp(kinds.Divisible, 4) + divisible_ot = solver.mkOp(Kind.Divisible, 4) assert divisible_ot.isIndexed() divisible_idx = divisible_ot.getIndices() assert divisible_idx == "4" def test_get_indices_uint(solver): - bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + bitvector_repeat_ot = solver.mkOp(Kind.BVRepeat, 5) assert bitvector_repeat_ot.isIndexed() bitvector_repeat_idx = bitvector_repeat_ot.getIndices() assert bitvector_repeat_idx == 5 - bitvector_zero_extend_ot = solver.mkOp(kinds.BVZeroExtend, 6) + bitvector_zero_extend_ot = solver.mkOp(Kind.BVZeroExtend, 6) bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices() assert bitvector_zero_extend_idx == 6 - bitvector_sign_extend_ot = solver.mkOp(kinds.BVSignExtend, 7) + bitvector_sign_extend_ot = solver.mkOp(Kind.BVSignExtend, 7) bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIndices() assert bitvector_sign_extend_idx == 7 - bitvector_rotate_left_ot = solver.mkOp(kinds.BVRotateLeft, 8) + bitvector_rotate_left_ot = solver.mkOp(Kind.BVRotateLeft, 8) bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIndices() assert bitvector_rotate_left_idx == 8 - bitvector_rotate_right_ot = solver.mkOp(kinds.BVRotateRight, 9) + bitvector_rotate_right_ot = solver.mkOp(Kind.BVRotateRight, 9) bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIndices() assert bitvector_rotate_right_idx == 9 - int_to_bitvector_ot = solver.mkOp(kinds.IntToBV, 10) + int_to_bitvector_ot = solver.mkOp(Kind.IntToBV, 10) int_to_bitvector_idx = int_to_bitvector_ot.getIndices() assert int_to_bitvector_idx == 10 - floatingpoint_to_ubv_ot = solver.mkOp(kinds.FPToUbv, 11) + floatingpoint_to_ubv_ot = solver.mkOp(Kind.FPToUbv, 11) floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIndices() assert floatingpoint_to_ubv_idx == 11 - floatingpoint_to_sbv_ot = solver.mkOp(kinds.FPToSbv, 13) + floatingpoint_to_sbv_ot = solver.mkOp(Kind.FPToSbv, 13) floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices() assert floatingpoint_to_sbv_idx == 13 def test_get_indices_pair_uint(solver): - bitvector_extract_ot = solver.mkOp(kinds.BVExtract, 4, 0) + bitvector_extract_ot = solver.mkOp(Kind.BVExtract, 4, 0) assert bitvector_extract_ot.isIndexed() bitvector_extract_indices = bitvector_extract_ot.getIndices() assert bitvector_extract_indices == (4, 0) floatingpoint_to_fp_ieee_bitvector_ot = solver.mkOp( - kinds.FPToFpIeeeBV, 4, 25) + Kind.FPToFpIeeeBV, 4, 25) floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot.getIndices( ) assert floatingpoint_to_fp_ieee_bitvector_indices == (4, 25) - floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(kinds.FPToFpFP, 4, 25) + floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(Kind.FPToFpFP, 4, 25) floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot.getIndices( ) assert floatingpoint_to_fp_floatingpoint_indices == (4, 25) - floatingpoint_to_fp_real_ot = solver.mkOp(kinds.FPToFpReal, 4, 25) + floatingpoint_to_fp_real_ot = solver.mkOp(Kind.FPToFpReal, 4, 25) floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices() assert floatingpoint_to_fp_real_indices == (4, 25) floatingpoint_to_fp_signed_bitvector_ot = solver.mkOp( - kinds.FPToFpSignedBV, 4, 25) + Kind.FPToFpSignedBV, 4, 25) floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot.getIndices( ) assert floatingpoint_to_fp_signed_bitvector_indices == (4, 25) floatingpoint_to_fp_unsigned_bitvector_ot = solver.mkOp( - kinds.FPToFpUnsignedBV, 4, 25) + Kind.FPToFpUnsignedBV, 4, 25) floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot.getIndices( ) assert floatingpoint_to_fp_unsigned_bitvector_indices == (4, 25) - floatingpoint_to_fp_generic_ot = solver.mkOp(kinds.FPToFpGeneric, 4, 25) + floatingpoint_to_fp_generic_ot = solver.mkOp(Kind.FPToFpGeneric, 4, 25) floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIndices( ) assert floatingpoint_to_fp_generic_indices == (4, 25) def test_op_scoping_to_string(solver): - bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + bitvector_repeat_ot = solver.mkOp(Kind.BVRepeat, 5) op_repr = str(bitvector_repeat_ot) assert str(bitvector_repeat_ot) == op_repr diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py index bd97646f9..e6ca3cf1e 100644 --- a/test/unit/api/python/test_result.py +++ b/test/unit/api/python/test_result.py @@ -17,7 +17,6 @@ import pytest import pycvc5 -from pycvc5 import kinds from pycvc5 import Result from pycvc5 import UnknownExplanation diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index b6520e0d3..d9d6a6c36 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -15,7 +15,7 @@ import pytest import pycvc5 import sys -from pycvc5 import kinds +from pycvc5 import Kind @pytest.fixture @@ -495,24 +495,24 @@ def test_mk_pos_zero(solver): def test_mk_op(solver): with pytest.raises(ValueError): - solver.mkOp(kinds.BVExtract, kinds.Equal) + solver.mkOp(Kind.BVExtract, Kind.Equal) - solver.mkOp(kinds.Divisible, "2147483648") + solver.mkOp(Kind.Divisible, "2147483648") with pytest.raises(RuntimeError): - solver.mkOp(kinds.BVExtract, "asdf") + solver.mkOp(Kind.BVExtract, "asdf") - solver.mkOp(kinds.Divisible, 1) - solver.mkOp(kinds.BVRotateLeft, 1) - solver.mkOp(kinds.BVRotateRight, 1) + solver.mkOp(Kind.Divisible, 1) + solver.mkOp(Kind.BVRotateLeft, 1) + solver.mkOp(Kind.BVRotateRight, 1) with pytest.raises(RuntimeError): - solver.mkOp(kinds.BVExtract, 1) + solver.mkOp(Kind.BVExtract, 1) - solver.mkOp(kinds.BVExtract, 1, 1) + solver.mkOp(Kind.BVExtract, 1, 1) with pytest.raises(RuntimeError): - solver.mkOp(kinds.Divisible, 1, 2) + solver.mkOp(Kind.Divisible, 1, 2) args = [1, 2, 2] - solver.mkOp(kinds.TupleProject, args) + solver.mkOp(Kind.TupleProject, args) def test_mk_pi(solver): @@ -644,19 +644,19 @@ def test_mk_real(solver): def test_mk_regexp_none(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpNone()) + solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpNone()) def test_mk_regexp_all(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAll()) + solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAll()) def test_mk_regexp_allchar(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAllchar()) + solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAllchar()) def test_mk_sep_emp(solver): @@ -694,100 +694,100 @@ def test_mk_term(solver): # mkTerm(Kind kind) const solver.mkPi() - solver.mkTerm(kinds.Pi) - solver.mkTerm(kinds.Pi, v6) - solver.mkTerm(solver.mkOp(kinds.Pi)) - solver.mkTerm(solver.mkOp(kinds.Pi), v6) - solver.mkTerm(kinds.RegexpNone) - solver.mkTerm(kinds.RegexpNone, v6) - solver.mkTerm(solver.mkOp(kinds.RegexpNone)) - solver.mkTerm(solver.mkOp(kinds.RegexpNone), v6) - solver.mkTerm(kinds.RegexpAllchar) - solver.mkTerm(kinds.RegexpAllchar, v6) - solver.mkTerm(solver.mkOp(kinds.RegexpAllchar)) - solver.mkTerm(solver.mkOp(kinds.RegexpAllchar), v6) - solver.mkTerm(kinds.SepEmp) - solver.mkTerm(kinds.SepEmp, v6) - solver.mkTerm(solver.mkOp(kinds.SepEmp)) - solver.mkTerm(solver.mkOp(kinds.SepEmp), v6) - with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ConstBV) + solver.mkTerm(Kind.Pi) + solver.mkTerm(Kind.Pi, v6) + solver.mkTerm(solver.mkOp(Kind.Pi)) + solver.mkTerm(solver.mkOp(Kind.Pi), v6) + solver.mkTerm(Kind.RegexpNone) + solver.mkTerm(Kind.RegexpNone, v6) + solver.mkTerm(solver.mkOp(Kind.RegexpNone)) + solver.mkTerm(solver.mkOp(Kind.RegexpNone), v6) + solver.mkTerm(Kind.RegexpAllchar) + solver.mkTerm(Kind.RegexpAllchar, v6) + solver.mkTerm(solver.mkOp(Kind.RegexpAllchar)) + solver.mkTerm(solver.mkOp(Kind.RegexpAllchar), v6) + solver.mkTerm(Kind.SepEmp) + solver.mkTerm(Kind.SepEmp, v6) + solver.mkTerm(solver.mkOp(Kind.SepEmp)) + solver.mkTerm(solver.mkOp(Kind.SepEmp), v6) + with pytest.raises(RuntimeError): + solver.mkTerm(Kind.ConstBV) # mkTerm(Kind kind, Term child) const - solver.mkTerm(kinds.Not, solver.mkTrue()) + solver.mkTerm(Kind.Not, solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Not, pycvc5.Term(solver)) + solver.mkTerm(Kind.Not, pycvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Not, a) + solver.mkTerm(Kind.Not, a) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.Not, solver.mkTrue()) + slv.mkTerm(Kind.Not, solver.mkTrue()) # mkTerm(Kind kind, Term child1, Term child2) const - solver.mkTerm(kinds.Equal, a, b) + solver.mkTerm(Kind.Equal, a, b) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, pycvc5.Term(solver), b) + solver.mkTerm(Kind.Equal, pycvc5.Term(solver), b) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, a, pycvc5.Term(solver)) + solver.mkTerm(Kind.Equal, a, pycvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, a, solver.mkTrue()) + solver.mkTerm(Kind.Equal, a, solver.mkTrue()) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.Equal, a, b) + slv.mkTerm(Kind.Equal, a, b) # mkTerm(Kind kind, Term child1, Term child2, Term child3) const - solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) + solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Ite, pycvc5.Term(solver), solver.mkTrue(), + solver.mkTerm(Kind.Ite, pycvc5.Term(solver), solver.mkTrue(), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Ite, solver.mkTrue(), pycvc5.Term(solver), + solver.mkTerm(Kind.Ite, solver.mkTrue(), pycvc5.Term(solver), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), pycvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), b) + solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), b) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + slv.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) - solver.mkTerm(kinds.Equal, v1) + solver.mkTerm(Kind.Equal, v1) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, v2) + solver.mkTerm(Kind.Equal, v2) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, v3) + solver.mkTerm(Kind.Equal, v3) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Distinct, v6) + solver.mkTerm(Kind.Distinct, v6) # Test cases that are nary via the API but have arity = 2 internally s_bool = solver.getBooleanSort() t_bool = solver.mkConst(s_bool, "t_bool") - solver.mkTerm(kinds.Implies, [t_bool, t_bool, t_bool]) - solver.mkTerm(kinds.Xor, [t_bool, t_bool, t_bool]) - solver.mkTerm(solver.mkOp(kinds.Xor), [t_bool, t_bool, t_bool]) + solver.mkTerm(Kind.Implies, [t_bool, t_bool, t_bool]) + solver.mkTerm(Kind.Xor, [t_bool, t_bool, t_bool]) + solver.mkTerm(solver.mkOp(Kind.Xor), [t_bool, t_bool, t_bool]) t_int = solver.mkConst(solver.getIntegerSort(), "t_int") - solver.mkTerm(kinds.Division, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Division), [t_int, t_int, t_int]) - solver.mkTerm(kinds.IntsDivision, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.IntsDivision), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Minus, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Minus), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Equal, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Equal), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Lt, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Lt), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Gt, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Gt), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Leq, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Leq), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Geq, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Geq), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Division, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Division), [t_int, t_int, t_int]) + solver.mkTerm(Kind.IntsDivision, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.IntsDivision), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Minus, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Minus), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Equal, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Equal), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Lt, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Lt), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Gt, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Gt), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Leq, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Leq), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Geq, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Geq), [t_int, t_int, t_int]) t_reg = solver.mkConst(solver.getRegExpSort(), "t_reg") - solver.mkTerm(kinds.RegexpDiff, [t_reg, t_reg, t_reg]) - solver.mkTerm(solver.mkOp(kinds.RegexpDiff), [t_reg, t_reg, t_reg]) + solver.mkTerm(Kind.RegexpDiff, [t_reg, t_reg, t_reg]) + solver.mkTerm(solver.mkOp(Kind.RegexpDiff), [t_reg, t_reg, t_reg]) t_fun = solver.mkConst(solver.mkFunctionSort( [s_bool, s_bool, s_bool], s_bool)) - solver.mkTerm(kinds.HoApply, [t_fun, t_bool, t_bool, t_bool]) - solver.mkTerm(solver.mkOp(kinds.HoApply), [t_fun, t_bool, t_bool, t_bool]) + solver.mkTerm(Kind.HoApply, [t_fun, t_bool, t_bool, t_bool]) + solver.mkTerm(solver.mkOp(Kind.HoApply), [t_fun, t_bool, t_bool, t_bool]) def test_mk_term_from_op(solver): bv32 = solver.mkBitVectorSort(32) @@ -800,8 +800,8 @@ def test_mk_term_from_op(solver): slv = pycvc5.Solver() # simple operator terms - opterm1 = solver.mkOp(kinds.BVExtract, 2, 1) - opterm2 = solver.mkOp(kinds.Divisible, 1) + opterm1 = solver.mkOp(Kind.BVExtract, 2, 1) + opterm2 = solver.mkOp(Kind.Divisible, 1) # list datatype sort = solver.mkParamSort("T") @@ -829,40 +829,40 @@ def test_mk_term_from_op(solver): tailTerm2 = lis["cons"]["tail"].getSelectorTerm() # mkTerm(Op op, Term term) const - solver.mkTerm(kinds.ApplyConstructor, nilTerm1) - solver.mkTerm(kinds.ApplyConstructor, nilTerm2) + solver.mkTerm(Kind.ApplyConstructor, nilTerm1) + solver.mkTerm(Kind.ApplyConstructor, nilTerm2) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplySelector, nilTerm1) + solver.mkTerm(Kind.ApplySelector, nilTerm1) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplySelector, consTerm1) + solver.mkTerm(Kind.ApplySelector, consTerm1) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplyConstructor, consTerm2) + solver.mkTerm(Kind.ApplyConstructor, consTerm2) with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplySelector, headTerm1) + solver.mkTerm(Kind.ApplySelector, headTerm1) with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.ApplyConstructor, nilTerm1) + slv.mkTerm(Kind.ApplyConstructor, nilTerm1) # mkTerm(Op op, Term child) const solver.mkTerm(opterm1, a) solver.mkTerm(opterm2, solver.mkInteger(1)) - solver.mkTerm(kinds.ApplySelector, headTerm1, c) - solver.mkTerm(kinds.ApplySelector, tailTerm2, c) + solver.mkTerm(Kind.ApplySelector, headTerm1, c) + solver.mkTerm(Kind.ApplySelector, tailTerm2, c) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, a) with pytest.raises(RuntimeError): solver.mkTerm(opterm1, pycvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0)) + solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0)) with pytest.raises(RuntimeError): slv.mkTerm(opterm1, a) # mkTerm(Op op, Term child1, Term child2) const - solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0), - solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0), + solver.mkTerm(Kind.ApplyConstructor, nilTerm1)) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2)) with pytest.raises(RuntimeError): @@ -872,10 +872,10 @@ def test_mk_term_from_op(solver): with pytest.raises(RuntimeError): solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1)) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.ApplyConstructor,\ + slv.mkTerm(Kind.ApplyConstructor,\ consTerm1,\ solver.mkInteger(0),\ - solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + solver.mkTerm(Kind.ApplyConstructor, nilTerm1)) # mkTerm(Op op, Term child1, Term child2, Term child3) const with pytest.raises(RuntimeError): @@ -1113,7 +1113,7 @@ def test_uf_iteration(solver): x = solver.mkConst(intSort, "x") y = solver.mkConst(intSort, "y") f = solver.mkConst(funSort, "f") - fxy = solver.mkTerm(kinds.ApplyUf, f, x, y) + fxy = solver.mkTerm(Kind.ApplyUf, f, x, y) # Expecting the uninterpreted function to be one of the children expected_children = [f, x, y] @@ -1133,7 +1133,7 @@ def test_get_info(solver): def test_get_op(solver): bv32 = solver.mkBitVectorSort(32) a = solver.mkConst(bv32, "a") - ext = solver.mkOp(kinds.BVExtract, 2, 1) + ext = solver.mkOp(Kind.BVExtract, 2, 1) exta = solver.mkTerm(ext, a) assert not a.hasOp() @@ -1157,10 +1157,10 @@ def test_get_op(solver): nilTerm = consList.getConstructorTerm("nil") headTerm = consList["cons"].getSelectorTerm("head") - listnil = solver.mkTerm(kinds.ApplyConstructor, nilTerm) - listcons1 = solver.mkTerm(kinds.ApplyConstructor, consTerm, + listnil = solver.mkTerm(Kind.ApplyConstructor, nilTerm) + listcons1 = solver.mkTerm(Kind.ApplyConstructor, consTerm, solver.mkInteger(1), listnil) - listhead = solver.mkTerm(kinds.ApplySelector, headTerm, listcons1) + listhead = solver.mkTerm(Kind.ApplySelector, headTerm, listcons1) assert listnil.hasOp() assert listcons1.hasOp() @@ -1231,14 +1231,14 @@ def test_get_unsat_core3(solver): p = solver.mkConst(intPredSort, "p") zero = solver.mkInteger(0) one = solver.mkInteger(1) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) - f_y = solver.mkTerm(kinds.ApplyUf, f, y) - summ = solver.mkTerm(kinds.Plus, f_x, f_y) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) - solver.assertFormula(solver.mkTerm(kinds.Gt, zero, f_x)) - solver.assertFormula(solver.mkTerm(kinds.Gt, zero, f_y)) - solver.assertFormula(solver.mkTerm(kinds.Gt, summ, one)) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) + summ = solver.mkTerm(Kind.Plus, f_x, f_y) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) + solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_x)) + solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_y)) + solver.assertFormula(solver.mkTerm(Kind.Gt, summ, one)) solver.assertFormula(p_0) solver.assertFormula(p_f_y.notTerm()) assert solver.checkSat().isUnsat() @@ -1285,15 +1285,15 @@ def test_get_value3(solver): p = solver.mkConst(intPredSort, "p") zero = solver.mkInteger(0) one = solver.mkInteger(1) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) - f_y = solver.mkTerm(kinds.ApplyUf, f, y) - summ = solver.mkTerm(kinds.Plus, f_x, f_y) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) - - solver.assertFormula(solver.mkTerm(kinds.Leq, zero, f_x)) - solver.assertFormula(solver.mkTerm(kinds.Leq, zero, f_y)) - solver.assertFormula(solver.mkTerm(kinds.Leq, summ, one)) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) + summ = solver.mkTerm(Kind.Plus, f_x, f_y) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) + + solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_x)) + solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_y)) + solver.assertFormula(solver.mkTerm(Kind.Leq, summ, one)) solver.assertFormula(p_0.notTerm()) solver.assertFormula(p_f_y) assert solver.checkSat().isSat() @@ -1325,7 +1325,7 @@ def checkSimpleSeparationConstraints(slv): slv.declareSepHeap(integer, integer) x = slv.mkConst(integer, "x") p = slv.mkConst(integer, "p") - heap = slv.mkTerm(kinds.SepPto, p, x) + heap = slv.mkTerm(Kind.SepPto, p, x) slv.assertFormula(heap) nil = slv.mkSepNil(integer) slv.assertFormula(nil.eqTerm(slv.mkReal(5))) @@ -1518,11 +1518,11 @@ def test_simplify(solver): solver.simplify(a) b = solver.mkConst(bvSort, "b") solver.simplify(b) - x_eq_x = solver.mkTerm(kinds.Equal, x, x) + x_eq_x = solver.mkTerm(Kind.Equal, x, x) solver.simplify(x_eq_x) assert solver.mkTrue() != x_eq_x assert solver.mkTrue() == solver.simplify(x_eq_x) - x_eq_b = solver.mkTerm(kinds.Equal, x, b) + x_eq_b = solver.mkTerm(Kind.Equal, x, b) solver.simplify(x_eq_b) assert solver.mkTrue() != x_eq_b assert solver.mkTrue() != solver.simplify(x_eq_b) @@ -1532,24 +1532,24 @@ def test_simplify(solver): i1 = solver.mkConst(solver.getIntegerSort(), "i1") solver.simplify(i1) - i2 = solver.mkTerm(kinds.Mult, i1, solver.mkInteger("23")) + i2 = solver.mkTerm(Kind.Mult, i1, solver.mkInteger("23")) solver.simplify(i2) assert i1 != i2 assert i1 != solver.simplify(i2) - i3 = solver.mkTerm(kinds.Plus, i1, solver.mkInteger(0)) + i3 = solver.mkTerm(Kind.Plus, i1, solver.mkInteger(0)) solver.simplify(i3) assert i1 != i3 assert i1 == solver.simplify(i3) consList = consListSort.getDatatype() dt1 = solver.mkTerm(\ - kinds.ApplyConstructor,\ + Kind.ApplyConstructor,\ consList.getConstructorTerm("cons"),\ solver.mkInteger(0),\ - solver.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil"))) + solver.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("nil"))) solver.simplify(dt1) dt2 = solver.mkTerm(\ - kinds.ApplySelector, consList["cons"].getSelectorTerm("head"), dt1) + Kind.ApplySelector, consList["cons"].getSelectorTerm("head"), dt1) solver.simplify(dt2) b1 = solver.mkVar(bvSort, "b1") @@ -1594,7 +1594,7 @@ def test_check_entailed1(solver): boolSort = solver.getBooleanSort() x = solver.mkConst(boolSort, "x") y = solver.mkConst(boolSort, "y") - z = solver.mkTerm(kinds.And, x, y) + z = solver.mkTerm(Kind.And, x, y) solver.setOption("incremental", "true") solver.checkEntailed(solver.mkTrue()) with pytest.raises(RuntimeError): @@ -1626,30 +1626,30 @@ def test_check_entailed2(solver): zero = solver.mkInteger(0) one = solver.mkInteger(1) # Terms - f_x = solver.mkTerm(kinds.ApplyUf, f, x) - f_y = solver.mkTerm(kinds.ApplyUf, f, y) - summ = solver.mkTerm(kinds.Plus, f_x, f_y) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) + summ = solver.mkTerm(Kind.Plus, f_x, f_y) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) # Assertions assertions =\ - solver.mkTerm(kinds.And,\ - [solver.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) - solver.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) - solver.mkTerm(kinds.Leq, summ, one), # f(x) + f(y) <= 1 + solver.mkTerm(Kind.And,\ + [solver.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x) + solver.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y) + solver.mkTerm(Kind.Leq, summ, one), # f(x) + f(y) <= 1 p_0.notTerm(), # not p(0) p_f_y # p(f(y)) ]) solver.checkEntailed(solver.mkTrue()) solver.assertFormula(assertions) - solver.checkEntailed(solver.mkTerm(kinds.Distinct, x, y)) + solver.checkEntailed(solver.mkTerm(Kind.Distinct, x, y)) solver.checkEntailed(\ - [solver.mkFalse(), solver.mkTerm(kinds.Distinct, x, y)]) + [solver.mkFalse(), solver.mkTerm(Kind.Distinct, x, y)]) with pytest.raises(RuntimeError): solver.checkEntailed(n) with pytest.raises(RuntimeError): - solver.checkEntailed([n, solver.mkTerm(kinds.Distinct, x, y)]) + solver.checkEntailed([n, solver.mkTerm(Kind.Distinct, x, y)]) slv = pycvc5.Solver() with pytest.raises(RuntimeError): slv.checkEntailed(solver.mkTrue()) @@ -1676,7 +1676,7 @@ def test_check_sat_assuming1(solver): boolSort = solver.getBooleanSort() x = solver.mkConst(boolSort, "x") y = solver.mkConst(boolSort, "y") - z = solver.mkTerm(kinds.And, x, y) + z = solver.mkTerm(Kind.And, x, y) solver.setOption("incremental", "true") solver.checkSatAssuming(solver.mkTrue()) with pytest.raises(RuntimeError): @@ -1708,31 +1708,31 @@ def test_check_sat_assuming2(solver): zero = solver.mkInteger(0) one = solver.mkInteger(1) # Terms - f_x = solver.mkTerm(kinds.ApplyUf, f, x) - f_y = solver.mkTerm(kinds.ApplyUf, f, y) - summ = solver.mkTerm(kinds.Plus, f_x, f_y) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) + summ = solver.mkTerm(Kind.Plus, f_x, f_y) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) # Assertions assertions =\ - solver.mkTerm(kinds.And,\ - [solver.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) - solver.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) - solver.mkTerm(kinds.Leq, summ, one), # f(x) + f(y) <= 1 + solver.mkTerm(Kind.And,\ + [solver.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x) + solver.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y) + solver.mkTerm(Kind.Leq, summ, one), # f(x) + f(y) <= 1 p_0.notTerm(), # not p(0) p_f_y # p(f(y)) ]) solver.checkSatAssuming(solver.mkTrue()) solver.assertFormula(assertions) - solver.checkSatAssuming(solver.mkTerm(kinds.Distinct, x, y)) + solver.checkSatAssuming(solver.mkTerm(Kind.Distinct, x, y)) solver.checkSatAssuming( [solver.mkFalse(), - solver.mkTerm(kinds.Distinct, x, y)]) + solver.mkTerm(Kind.Distinct, x, y)]) with pytest.raises(RuntimeError): solver.checkSatAssuming(n) with pytest.raises(RuntimeError): - solver.checkSatAssuming([n, solver.mkTerm(kinds.Distinct, x, y)]) + solver.checkSatAssuming([n, solver.mkTerm(Kind.Distinct, x, y)]) slv = pycvc5.Solver() with pytest.raises(RuntimeError): slv.checkSatAssuming(solver.mkTrue()) @@ -1762,10 +1762,10 @@ def test_reset_assertions(solver): bvSort = solver.mkBitVectorSort(4) one = solver.mkBitVector(4, 1) x = solver.mkConst(bvSort, "x") - ule = solver.mkTerm(kinds.BVUle, x, one) - srem = solver.mkTerm(kinds.BVSrem, one, x) + ule = solver.mkTerm(Kind.BVUle, x, one) + srem = solver.mkTerm(Kind.BVSrem, one, x) solver.push(4) - slt = solver.mkTerm(kinds.BVSlt, srem, one) + slt = solver.mkTerm(Kind.BVSlt, srem, one) solver.resetAssertions() solver.checkSatAssuming([slt, ule]) @@ -1970,14 +1970,14 @@ def test_define_fun_global(solver): # (assert (or (not f) (not (g true)))) solver.assertFormula( - solver.mkTerm(kinds.Or, f.notTerm(), - solver.mkTerm(kinds.ApplyUf, g, bTrue).notTerm())) + solver.mkTerm(Kind.Or, f.notTerm(), + solver.mkTerm(Kind.ApplyUf, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() solver.resetAssertions() # (assert (or (not f) (not (g true)))) solver.assertFormula( - solver.mkTerm(kinds.Or, f.notTerm(), - solver.mkTerm(kinds.ApplyUf, g, bTrue).notTerm())) + solver.mkTerm(Kind.Or, f.notTerm(), + solver.mkTerm(Kind.ApplyUf, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() @@ -2001,7 +2001,7 @@ def test_get_model_domain_elements(solver): x = solver.mkConst(uSort, "x") y = solver.mkConst(uSort, "y") z = solver.mkConst(uSort, "z") - f = solver.mkTerm(kinds.Distinct, x, y, z) + f = solver.mkTerm(Kind.Distinct, x, y, z) solver.assertFormula(f) solver.checkSat() solver.getModelDomainElements(uSort) @@ -2146,7 +2146,7 @@ def test_is_model_core_symbol(solver): y = solver.mkConst(uSort, "y") z = solver.mkConst(uSort, "z") zero = solver.mkInteger(0) - f = solver.mkTerm(kinds.Not, solver.mkTerm(kinds.Equal, x, y)) + f = solver.mkTerm(Kind.Not, solver.mkTerm(Kind.Equal, x, y)) solver.assertFormula(f) solver.checkSat() assert solver.isModelCoreSymbol(x) @@ -2164,8 +2164,8 @@ def test_issue5893(solver): arr = solver.mkConst(arrsort, "arr") idx = solver.mkConst(bvsort4, "idx") ten = solver.mkBitVector(8, "10", 10) - sel = solver.mkTerm(kinds.Select, arr, idx) - distinct = solver.mkTerm(kinds.Distinct, sel, ten) + sel = solver.mkTerm(Kind.Select, arr, idx) + distinct = solver.mkTerm(Kind.Distinct, sel, ten) distinct.getOp() @@ -2177,8 +2177,8 @@ def test_issue7000(solver): t7 = solver.mkConst(s3, "_x5") t37 = solver.mkConst(s2, "_x32") t59 = solver.mkConst(s2, "_x51") - t72 = solver.mkTerm(kinds.Equal, t37, t59) - t74 = solver.mkTerm(kinds.Gt, t4, t7) + t72 = solver.mkTerm(Kind.Equal, t37, t59) + t74 = solver.mkTerm(Kind.Gt, t4, t7) # throws logic exception since logic is not higher order by default with pytest.raises(RuntimeError): solver.checkEntailed(t72, t74, t72, t72) @@ -2247,7 +2247,7 @@ def test_tuple_project(solver): solver.mkBoolean(True), \ solver.mkInteger(3),\ solver.mkString("C"),\ - solver.mkTerm(kinds.SetSingleton, solver.mkString("Z"))] + solver.mkTerm(Kind.SetSingleton, solver.mkString("Z"))] tuple = solver.mkTuple(sorts, elements) @@ -2258,22 +2258,22 @@ def test_tuple_project(solver): indices5 = [4] indices6 = [0, 4] - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices1), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices1), tuple) - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices2), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices2), tuple) - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices3), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices3), tuple) - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices4), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices4), tuple) with pytest.raises(RuntimeError): - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices5), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices5), tuple) with pytest.raises(RuntimeError): - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices6), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices6), tuple) indices = [0, 3, 2, 0, 1, 2] - op = solver.mkOp(kinds.TupleProject, indices) + op = solver.mkOp(Kind.TupleProject, indices) projection = solver.mkTerm(op, tuple) datatype = tuple.getSort().getDatatype() @@ -2282,7 +2282,7 @@ def test_tuple_project(solver): for i in indices: selectorTerm = constructor[i].getSelectorTerm() - selectedTerm = solver.mkTerm(kinds.ApplySelector, selectorTerm, tuple) + selectedTerm = solver.mkTerm(Kind.ApplySelector, selectorTerm, tuple) simplifiedTerm = solver.simplify(selectedTerm) assert elements[i] == simplifiedTerm diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index 98cf76d76..9c9458792 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -17,7 +17,6 @@ import pytest import pycvc5 -from pycvc5 import kinds from pycvc5 import Sort diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 49314638f..27702bd23 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -13,7 +13,7 @@ import pytest import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind from pycvc5 import Sort, Term from fractions import Fraction @@ -73,23 +73,23 @@ def test_get_kind(solver): zero = solver.mkInteger(0) zero.getKind() - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) f_x.getKind() - f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) f_y.getKind() - sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum = solver.mkTerm(Kind.Plus, f_x, f_y) sum.getKind() - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.getKind() - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) p_f_y.getKind() # Sequence kinds do not exist internally, test that the API properly # converts them back. seqSort = solver.mkSequenceSort(intSort) s = solver.mkConst(seqSort, "s") - ss = solver.mkTerm(kinds.SeqConcat, s, s) - assert ss.getKind() == kinds.SeqConcat + ss = solver.mkTerm(Kind.SeqConcat, s, s) + assert ss.getKind() == Kind.SeqConcat def test_get_sort(solver): @@ -120,19 +120,19 @@ def test_get_sort(solver): zero.getSort() assert zero.getSort() == intSort - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) f_x.getSort() assert f_x.getSort() == intSort - f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) f_y.getSort() assert f_y.getSort() == intSort - sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum = solver.mkTerm(Kind.Plus, f_x, f_y) sum.getSort() assert sum.getSort() == intSort - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.getSort() assert p_0.getSort() == boolSort - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) p_f_y.getSort() assert p_f_y.getSort() == boolSort @@ -151,8 +151,8 @@ def test_get_op(solver): with pytest.raises(RuntimeError): x.getOp() - ab = solver.mkTerm(kinds.Select, a, b) - ext = solver.mkOp(kinds.BVExtract, 4, 0) + ab = solver.mkTerm(Kind.Select, a, b) + ext = solver.mkOp(Kind.BVExtract, 4, 0) extb = solver.mkTerm(ext, b) assert ab.hasOp() @@ -163,7 +163,7 @@ def test_get_op(solver): assert extb.getOp() == ext f = solver.mkConst(funsort, "f") - fx = solver.mkTerm(kinds.ApplyUf, f, x) + fx = solver.mkTerm(Kind.ApplyUf, f, x) assert not f.hasOp() with pytest.raises(RuntimeError): @@ -192,11 +192,11 @@ def test_get_op(solver): headOpTerm = list1["cons"].getSelectorTerm("head") tailOpTerm = list1["cons"].getSelectorTerm("tail") - nilTerm = solver.mkTerm(kinds.ApplyConstructor, nilOpTerm) - consTerm = solver.mkTerm(kinds.ApplyConstructor, consOpTerm, + nilTerm = solver.mkTerm(Kind.ApplyConstructor, nilOpTerm) + consTerm = solver.mkTerm(Kind.ApplyConstructor, consOpTerm, solver.mkInteger(0), nilTerm) - headTerm = solver.mkTerm(kinds.ApplySelector, headOpTerm, consTerm) - tailTerm = solver.mkTerm(kinds.ApplySelector, tailOpTerm, consTerm) + headTerm = solver.mkTerm(Kind.ApplySelector, headOpTerm, consTerm) + tailTerm = solver.mkTerm(Kind.ApplySelector, tailOpTerm, consTerm) assert nilTerm.hasOp() assert consTerm.hasOp() @@ -255,15 +255,15 @@ def test_not_term(solver): zero = solver.mkInteger(0) with pytest.raises(RuntimeError): zero.notTerm() - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.notTerm() - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.notTerm() - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.notTerm() - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.notTerm() @@ -312,7 +312,7 @@ def test_and_term(solver): zero.andTerm(p) with pytest.raises(RuntimeError): zero.andTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.andTerm(b) with pytest.raises(RuntimeError): @@ -325,7 +325,7 @@ def test_and_term(solver): f_x.andTerm(zero) with pytest.raises(RuntimeError): f_x.andTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.andTerm(b) with pytest.raises(RuntimeError): @@ -340,7 +340,7 @@ def test_and_term(solver): sum.andTerm(f_x) with pytest.raises(RuntimeError): sum.andTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.andTerm(b) with pytest.raises(RuntimeError): p_0.andTerm(x) @@ -355,7 +355,7 @@ def test_and_term(solver): with pytest.raises(RuntimeError): p_0.andTerm(sum) p_0.andTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.andTerm(b) with pytest.raises(RuntimeError): p_f_x.andTerm(x) @@ -418,7 +418,7 @@ def test_or_term(solver): zero.orTerm(p) with pytest.raises(RuntimeError): zero.orTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.orTerm(b) with pytest.raises(RuntimeError): @@ -431,7 +431,7 @@ def test_or_term(solver): f_x.orTerm(zero) with pytest.raises(RuntimeError): f_x.orTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.orTerm(b) with pytest.raises(RuntimeError): @@ -446,7 +446,7 @@ def test_or_term(solver): sum.orTerm(f_x) with pytest.raises(RuntimeError): sum.orTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.orTerm(b) with pytest.raises(RuntimeError): p_0.orTerm(x) @@ -461,7 +461,7 @@ def test_or_term(solver): with pytest.raises(RuntimeError): p_0.orTerm(sum) p_0.orTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.orTerm(b) with pytest.raises(RuntimeError): p_f_x.orTerm(x) @@ -524,7 +524,7 @@ def test_xor_term(solver): zero.xorTerm(p) with pytest.raises(RuntimeError): zero.xorTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.xorTerm(b) with pytest.raises(RuntimeError): @@ -537,7 +537,7 @@ def test_xor_term(solver): f_x.xorTerm(zero) with pytest.raises(RuntimeError): f_x.xorTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.xorTerm(b) with pytest.raises(RuntimeError): @@ -552,7 +552,7 @@ def test_xor_term(solver): sum.xorTerm(f_x) with pytest.raises(RuntimeError): sum.xorTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.xorTerm(b) with pytest.raises(RuntimeError): p_0.xorTerm(x) @@ -567,7 +567,7 @@ def test_xor_term(solver): with pytest.raises(RuntimeError): p_0.xorTerm(sum) p_0.xorTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.xorTerm(b) with pytest.raises(RuntimeError): p_f_x.xorTerm(x) @@ -626,7 +626,7 @@ def test_eq_term(solver): with pytest.raises(RuntimeError): zero.eqTerm(p) zero.eqTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.eqTerm(b) with pytest.raises(RuntimeError): @@ -637,7 +637,7 @@ def test_eq_term(solver): f_x.eqTerm(p) f_x.eqTerm(zero) f_x.eqTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.eqTerm(b) with pytest.raises(RuntimeError): @@ -649,7 +649,7 @@ def test_eq_term(solver): sum.eqTerm(zero) sum.eqTerm(f_x) sum.eqTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.eqTerm(b) with pytest.raises(RuntimeError): p_0.eqTerm(x) @@ -664,7 +664,7 @@ def test_eq_term(solver): with pytest.raises(RuntimeError): p_0.eqTerm(sum) p_0.eqTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.eqTerm(b) with pytest.raises(RuntimeError): p_f_x.eqTerm(x) @@ -727,7 +727,7 @@ def test_imp_term(solver): zero.impTerm(p) with pytest.raises(RuntimeError): zero.impTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.impTerm(b) with pytest.raises(RuntimeError): @@ -740,7 +740,7 @@ def test_imp_term(solver): f_x.impTerm(zero) with pytest.raises(RuntimeError): f_x.impTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.impTerm(b) with pytest.raises(RuntimeError): @@ -755,7 +755,7 @@ def test_imp_term(solver): sum.impTerm(f_x) with pytest.raises(RuntimeError): sum.impTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.impTerm(b) with pytest.raises(RuntimeError): p_0.impTerm(x) @@ -770,7 +770,7 @@ def test_imp_term(solver): with pytest.raises(RuntimeError): p_0.impTerm(sum) p_0.impTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.impTerm(b) with pytest.raises(RuntimeError): p_f_x.impTerm(x) @@ -827,22 +827,22 @@ def test_ite_term(solver): zero.iteTerm(x, x) with pytest.raises(RuntimeError): zero.iteTerm(x, b) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.iteTerm(b, b) with pytest.raises(RuntimeError): f_x.iteTerm(b, x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.iteTerm(x, x) with pytest.raises(RuntimeError): sum.iteTerm(b, x) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.iteTerm(b, b) p_0.iteTerm(x, x) with pytest.raises(RuntimeError): p_0.iteTerm(x, b) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.iteTerm(b, b) p_f_x.iteTerm(x, x) with pytest.raises(RuntimeError): @@ -860,8 +860,8 @@ def test_substitute(solver): x = solver.mkConst(solver.getIntegerSort(), "x") one = solver.mkInteger(1) ttrue = solver.mkTrue() - xpx = solver.mkTerm(kinds.Plus, x, x) - onepone = solver.mkTerm(kinds.Plus, one, one) + xpx = solver.mkTerm(Kind.Plus, x, x) + onepone = solver.mkTerm(Kind.Plus, one, one) assert xpx.substitute(x, one) == onepone assert onepone.substitute(one, x) == xpx @@ -871,8 +871,8 @@ def test_substitute(solver): # simultaneous substitution y = solver.mkConst(solver.getIntegerSort(), "y") - xpy = solver.mkTerm(kinds.Plus, x, y) - xpone = solver.mkTerm(kinds.Plus, y, one) + xpy = solver.mkTerm(Kind.Plus, x, y) + xpone = solver.mkTerm(Kind.Plus, y, one) es = [] rs = [] es.append(x) @@ -917,8 +917,8 @@ def test_substitute(solver): def test_term_compare(solver): t1 = solver.mkInteger(1) - t2 = solver.mkTerm(kinds.Plus, solver.mkInteger(2), solver.mkInteger(2)) - t3 = solver.mkTerm(kinds.Plus, solver.mkInteger(2), solver.mkInteger(2)) + t2 = solver.mkTerm(Kind.Plus, solver.mkInteger(2), solver.mkInteger(2)) + t3 = solver.mkTerm(Kind.Plus, solver.mkInteger(2), solver.mkInteger(2)) assert t2 >= t3 assert t2 <= t3 assert (t1 > t2) != (t1 < t2) @@ -928,7 +928,7 @@ def test_term_compare(solver): def test_term_children(solver): # simple term 2+3 two = solver.mkInteger(2) - t1 = solver.mkTerm(kinds.Plus, two, solver.mkInteger(3)) + t1 = solver.mkTerm(Kind.Plus, two, solver.mkInteger(3)) assert t1[0] == two assert t1.getNumChildren() == 2 tnull = Term(solver) @@ -939,8 +939,8 @@ def test_term_children(solver): intSort = solver.getIntegerSort() fsort = solver.mkFunctionSort(intSort, intSort) f = solver.mkConst(fsort, "f") - t2 = solver.mkTerm(kinds.ApplyUf, f, two) - # due to our higher-order view of terms, we treat f as a child of kinds.ApplyUf + t2 = solver.mkTerm(Kind.ApplyUf, f, two) + # due to our higher-order view of terms, we treat f as a child of Kind.ApplyUf assert t2.getNumChildren() == 2 assert t2[0] == f assert t2[1] == two @@ -993,11 +993,11 @@ def test_get_set(solver): i2 = solver.mkInteger(7) s1 = solver.mkEmptySet(s) - s2 = solver.mkTerm(kinds.SetSingleton, i1) - s3 = solver.mkTerm(kinds.SetSingleton, i1) - s4 = solver.mkTerm(kinds.SetSingleton, i2) + s2 = solver.mkTerm(Kind.SetSingleton, i1) + s3 = solver.mkTerm(Kind.SetSingleton, i1) + s4 = solver.mkTerm(Kind.SetSingleton, i2) s5 = solver.mkTerm( - kinds.SetUnion, s2, solver.mkTerm(kinds.SetUnion, s3, s4)) + Kind.SetUnion, s2, solver.mkTerm(Kind.SetUnion, s3, s4)) assert s1.isSetValue() assert s2.isSetValue() @@ -1021,11 +1021,11 @@ def test_get_sequence(solver): i2 = solver.mkInteger(7) s1 = solver.mkEmptySequence(s) - s2 = solver.mkTerm(kinds.SeqUnit, i1) - s3 = solver.mkTerm(kinds.SeqUnit, i1) - s4 = solver.mkTerm(kinds.SeqUnit, i2) - s5 = solver.mkTerm(kinds.SeqConcat, s2, - solver.mkTerm(kinds.SeqConcat, s3, s4)) + s2 = solver.mkTerm(Kind.SeqUnit, i1) + s3 = solver.mkTerm(Kind.SeqUnit, i1) + s4 = solver.mkTerm(Kind.SeqUnit, i2) + s5 = solver.mkTerm(Kind.SeqConcat, s2, + solver.mkTerm(Kind.SeqConcat, s3, s4)) assert s1.isSequenceValue() assert not s2.isSequenceValue() @@ -1244,18 +1244,18 @@ def test_const_array(solver): one = solver.mkInteger(1) constarr = solver.mkConstArray(arrsort, one) - assert constarr.getKind() == kinds.ConstArray + assert constarr.getKind() == Kind.ConstArray assert constarr.getConstArrayBase() == one with pytest.raises(RuntimeError): a.getConstArrayBase() arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) zero_array = solver.mkConstArray(arrsort, solver.mkReal(0)) - stores = solver.mkTerm(kinds.Store, zero_array, solver.mkReal(1), + stores = solver.mkTerm(Kind.Store, zero_array, solver.mkReal(1), solver.mkReal(2)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), + stores = solver.mkTerm(Kind.Store, stores, solver.mkReal(2), solver.mkReal(3)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), + stores = solver.mkTerm(Kind.Store, stores, solver.mkReal(4), solver.mkReal(5)) @@ -1264,14 +1264,14 @@ def test_const_sequence_elements(solver): seqsort = solver.mkSequenceSort(realsort) s = solver.mkEmptySequence(seqsort) - assert s.getKind() == kinds.ConstSequence + assert s.getKind() == Kind.ConstSequence # empty sequence has zero elements cs = s.getSequenceValue() assert len(cs) == 0 # A seq.unit app is not a constant sequence (regardless of whether it is # applied to a constant). - su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1)) + su = solver.mkTerm(Kind.SeqUnit, solver.mkReal(1)) with pytest.raises(RuntimeError): su.getSequenceValue() diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py index bb30fae8f..bef7e78c0 100644 --- a/test/unit/api/python/test_to_python_obj.py +++ b/test/unit/api/python/test_to_python_obj.py @@ -15,7 +15,7 @@ from fractions import Fraction import pytest import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind def testGetBool(): @@ -54,9 +54,9 @@ def testGetArray(): solver = pycvc5.Solver() arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0)) - stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5)) + stores = solver.mkTerm(Kind.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) + stores = solver.mkTerm(Kind.Store, stores, solver.mkInteger(2), solver.mkInteger(3)) + stores = solver.mkTerm(Kind.Store, stores, solver.mkInteger(4), solver.mkInteger(5)) array_dict = stores.toPythonObj() @@ -90,7 +90,7 @@ def testGetValueInt(): intsort = solver.getIntegerSort() x = solver.mkConst(intsort, "x") - solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkInteger(6))) + solver.assertFormula(solver.mkTerm(Kind.Equal, x, solver.mkInteger(6))) r = solver.checkSat() assert r.isSat() @@ -106,8 +106,8 @@ def testGetValueReal(): realsort = solver.getRealSort() x = solver.mkConst(realsort, "x") y = solver.mkConst(realsort, "y") - solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkReal("6"))) - solver.assertFormula(solver.mkTerm(kinds.Equal, y, solver.mkReal("8.33"))) + solver.assertFormula(solver.mkTerm(Kind.Equal, x, solver.mkReal("6"))) + solver.assertFormula(solver.mkTerm(Kind.Equal, y, solver.mkReal("8.33"))) r = solver.checkSat() assert r.isSat() diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp index a8d9f952b..6bc48f9d0 100644 --- a/test/unit/context/cdlist_black.cpp +++ b/test/unit/context/cdlist_black.cpp @@ -20,7 +20,6 @@ #include "base/exception.h" #include "context/cdlist.h" -#include "memory.h" #include "test_context.h" namespace cvc5 { @@ -135,25 +134,6 @@ TEST_F(TestContextBlackCDList, empty_iterator) list->deleteSelf(); } -TEST_F(TestContextBlackCDList, out_of_memory) -{ -#ifndef CVC5_MEMORY_LIMITING_DISABLED - CDList<uint32_t> list(d_context.get()); - test::WithLimitedMemory wlm(1); - - ASSERT_THROW( - { - // We cap it at UINT32_MAX, preferring to terminate with a - // failure than run indefinitely. - for (uint32_t i = 0; i < UINT32_MAX; ++i) - { - list.push_back(i); - } - }, - std::bad_alloc); -#endif -} - TEST_F(TestContextBlackCDList, pop_below_level_created) { d_context->push(); diff --git a/test/unit/memory.h b/test/unit/memory.h deleted file mode 100644 index 574488e21..000000000 --- a/test/unit/memory.h +++ /dev/null @@ -1,93 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Morgan Deters, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Utility class to help testing out-of-memory conditions. - * - * Use it like this (for example): - * - * cvc5::test::WithLimitedMemory wlm(amount); - * ASSERT_THROW( foo(), bad_alloc ); - * - * The WithLimitedMemory destructor will re-establish the previous limit. - * - * This class does not exist in CVC5_MEMORY_LIMITING_DISABLED is defined. - * This can be disabled for a variety of reasons. - */ - -#include "test.h" - -#ifndef __CVC5__TEST__UNIT__MEMORY_H -#define __CVC5__TEST__UNIT__MEMORY_H - -#include <string> -#include <sys/resource.h> -#include <sys/time.h> - -#include "base/check.h" -#include "base/configuration_private.h" - -// Conditionally define CVC5_MEMORY_LIMITING_DISABLED. -#ifdef __APPLE__ -#define CVC5_MEMORY_LIMITING_DISABLED 1 -#define CVC5_MEMORY_LIMITING_DISABLED_REASON "setrlimit() is broken on Mac." -#else /* __APPLE__ */ - -// Tests cannot expect bad_alloc to be thrown due to limit memory using -// setrlimit when ASAN is enable. ASAN instead aborts on mmap failures. -# if IS_ASAN_BUILD -#define CVC5_MEMORY_LIMITING_DISABLED 1 -#define CVC5_MEMORY_LIMITING_DISABLED_REASON "ASAN's mmap failures abort." -# endif -#endif - -namespace cvc5 { -namespace test { - -#ifndef CVC5_MEMORY_LIMITING_DISABLED -class WithLimitedMemory { - public: - WithLimitedMemory() { remember(); } - - WithLimitedMemory(rlim_t amount) { - remember(); - set(amount); - } - - ~WithLimitedMemory() { set(d_prevAmount); } - - void set(rlim_t amount) { - struct rlimit rlim; - rlim.rlim_cur = amount; - rlim.rlim_max = RLIM_INFINITY; - ASSERT_EQ(setrlimit(RLIMIT_AS, &rlim), 0); - } - - private: - void remember() { - struct rlimit rlim; - ASSERT_EQ(getrlimit(RLIMIT_AS, &rlim), 0); - d_prevAmount = rlim.rlim_cur; - } - - rlim_t d_prevAmount; -}; /* class WithLimitedMemory */ -#endif - -} // namespace test -} // namespace cvc5 - -// Remove CVC5_MEMORY_LIMITING_DISABLED_REASON if it is defined. -#ifdef CVC5_MEMORY_LIMITING_DISABLED_REASON -#undef CVC5_MEMORY_LIMITING_DISABLED_REASON -#endif /* CVC5_MEMORY_LIMITING_DISABLED_REASON */ - -#endif /* __CVC5__TEST__MEMORY_H */ diff --git a/test/unit/options/options_black.cpp b/test/unit/options/options_black.cpp index 1ab4bce23..0aa160677 100644 --- a/test/unit/options/options_black.cpp +++ b/test/unit/options/options_black.cpp @@ -92,11 +92,13 @@ TEST_F(TestBlackOptions, set) } EXPECT_NO_THROW(d_solver.setOption( name, std::to_string((range.first + range.second) / 2))); + EXPECT_THROW(d_solver.setOption(name, "0123abc"), CVC5ApiOptionException); }, [this, &name](const OptionInfo::NumberInfo<uint64_t>& v) { std::pair<uint64_t, uint64_t> range{ std::numeric_limits<uint64_t>::min(), std::numeric_limits<uint64_t>::max()}; + EXPECT_THROW(d_solver.setOption(name, "-1"), CVC5ApiOptionException); if (v.minimum) { EXPECT_THROW( @@ -117,6 +119,7 @@ TEST_F(TestBlackOptions, set) } EXPECT_NO_THROW(d_solver.setOption( name, std::to_string((range.first + range.second) / 2))); + EXPECT_THROW(d_solver.setOption(name, "0123abc"), CVC5ApiOptionException); }, [this, &name](const OptionInfo::NumberInfo<double>& v) { std::pair<double, double> range{ @@ -149,7 +152,9 @@ TEST_F(TestBlackOptions, set) for (const auto& m : v.modes) { d_solver.setOption(name, m); + EXPECT_EQ(d_solver.getOption(name), m); } + EXPECT_DEATH(d_solver.setOption(name, "help"), ""); }, }, info.valueInfo); diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index 2ad8695de..e8238ecbb 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -61,7 +61,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) Env env(d_nodeManager, &opts); env.d_logic.setLogicString("QF_UFBV"); env.d_logic.lock(); - IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, false); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems); Node seven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)); ASSERT_EQ(seven, result); @@ -86,7 +86,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant) Env env(d_nodeManager, &opts); env.d_logic.setLogicString("QF_UFBV"); env.d_logic.lock(); - IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, true); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(bv, lemmas, skolems); ASSERT_TRUE(result.isVar() && result.getType().isInteger()); @@ -116,7 +116,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf) Env env(d_nodeManager, &opts); env.d_logic.setLogicString("QF_UFBV"); env.d_logic.lock(); - IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, true); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(f, lemmas, skolems); TypeNode resultType = result.getType(); std::vector<TypeNode> resultDomain = resultType.getArgTypes(); @@ -130,7 +130,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf) } /** Check all cases of the translation. - * This is a sanity check, that noly verifies + * This is a sanity check, that only verifies * the expected type, and that there were no * failures. */ @@ -143,7 +143,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) Env env(d_nodeManager, &opts); env.d_logic.setLogicString("QF_UFBV"); env.d_logic.lock(); - IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, true); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); // bit-vector variables TypeNode bvType = d_nodeManager->mkBitVectorType(4); @@ -280,5 +280,45 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children) ASSERT_TRUE(result.getType().isInteger()); } +/** Check AND translation for bitwise option. + * This is a sanity check, that only verifies + * the expected kind, and that there were no + * failures. + */ +TEST_F(TestTheoryWhiteBvIntblaster, intblaster_bitwise) +{ + // place holders for lemmas and skolem + std::vector<Node> lemmas; + std::map<Node, Node> skolems; + Options opts; + Env env(d_nodeManager, &opts); + env.d_logic.setLogicString("QF_UFBV"); + env.d_logic.lock(); + IntBlaster intBlaster(env, options::SolveBVAsIntMode::BITWISE, 1); + + // bit-vector variables + TypeNode bvType = d_nodeManager->mkBitVectorType(4); + Node v1 = d_nodeManager->mkVar("v1", bvType); + Node v2 = d_nodeManager->mkVar("v2", bvType); + + // translated integer variables + Node i1 = intBlaster.translateNoChildren(v1, lemmas, skolems); + Node i2 = intBlaster.translateNoChildren(v2, lemmas, skolems); + + // if original is BV, result should be Int. + // Otherwise, they should have the same type. + Node original; + Node result; + + // bvand + original = d_nodeManager->mkNode(BITVECTOR_AND, v1, v2); + size_t orig_num_lemmas = lemmas.size(); + result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas); + // should have kind skolem, would use bitwise comparisons to refine + ASSERT_TRUE(result.getKind() == kind::SKOLEM); + // check that a lemma was added + ASSERT_TRUE(lemmas.size() > orig_num_lemmas); +} + } // namespace test } // namespace cvc5 diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp index 368f12222..2be2515eb 100644 --- a/test/unit/util/integer_black.cpp +++ b/test/unit/util/integer_black.cpp @@ -333,18 +333,69 @@ TEST_F(TestUtilBlackInteger, pow) ASSERT_EQ(Integer(-1000), Integer(-10).pow(3)); } -TEST_F(TestUtilBlackInteger, overly_long) +TEST_F(TestUtilBlackInteger, overly_long_signed) +{ + int64_t sl = std::numeric_limits<int64_t>::max(); + Integer i(sl); + if constexpr (sizeof(unsigned long) == sizeof(uint64_t)) + { + ASSERT_EQ(i.getLong(), sl); + } + ASSERT_NO_THROW(i.getSigned64()); + ASSERT_EQ(i.getSigned64(), sl); + i = i + 1; + ASSERT_THROW(i.getSigned64(), IllegalArgumentException); +} + +TEST_F(TestUtilBlackInteger, overly_long_unsigned) { uint64_t ul = std::numeric_limits<uint64_t>::max(); Integer i(ul); - ASSERT_EQ(i.getUnsignedLong(), ul); + if constexpr (sizeof(unsigned long) == sizeof(uint64_t)) + { + ASSERT_EQ(i.getUnsignedLong(), ul); + } ASSERT_THROW(i.getLong(), IllegalArgumentException); + ASSERT_NO_THROW(i.getUnsigned64()); + ASSERT_EQ(i.getUnsigned64(), ul); uint64_t ulplus1 = ul + 1; ASSERT_EQ(ulplus1, 0); i = i + 1; ASSERT_THROW(i.getUnsignedLong(), IllegalArgumentException); } +TEST_F(TestUtilBlackInteger, getSigned64) +{ + { + int64_t i = std::numeric_limits<int64_t>::max(); + Integer a(i); + EXPECT_EQ(a.getSigned64(), i); + EXPECT_THROW((a + 1).getSigned64(), IllegalArgumentException); + } + { + int64_t i = std::numeric_limits<int64_t>::min(); + Integer a(i); + EXPECT_EQ(a.getSigned64(), i); + EXPECT_THROW((a - 1).getSigned64(), IllegalArgumentException); + } +} + +TEST_F(TestUtilBlackInteger, getUnsigned64) +{ + { + uint64_t i = std::numeric_limits<uint64_t>::max(); + Integer a(i); + EXPECT_EQ(a.getUnsigned64(), i); + EXPECT_THROW((a + 1).getUnsigned64(), IllegalArgumentException); + } + { + uint64_t i = std::numeric_limits<uint64_t>::min(); + Integer a(i); + EXPECT_EQ(a.getUnsigned64(), i); + EXPECT_THROW((a - 1).getUnsigned64(), IllegalArgumentException); + } +} + TEST_F(TestUtilBlackInteger, testBit) { ASSERT_FALSE(Integer(0).testBit(6)); |