diff options
Diffstat (limited to 'test/unit/api')
-rw-r--r-- | test/unit/api/cpp/datatype_api_black.cpp | 11 | ||||
-rw-r--r-- | test/unit/api/cpp/solver_black.cpp | 175 | ||||
-rw-r--r-- | test/unit/api/java/DatatypeTest.java | 8 | ||||
-rw-r--r-- | test/unit/api/java/SolverTest.java | 12 | ||||
-rw-r--r-- | test/unit/api/python/test_datatype_api.py | 11 | ||||
-rw-r--r-- | test/unit/api/python/test_grammar.py | 2 | ||||
-rw-r--r-- | test/unit/api/python/test_op.py | 82 | ||||
-rw-r--r-- | test/unit/api/python/test_result.py | 1 | ||||
-rw-r--r-- | test/unit/api/python/test_solver.py | 336 | ||||
-rw-r--r-- | test/unit/api/python/test_sort.py | 1 | ||||
-rw-r--r-- | test/unit/api/python/test_term.py | 144 | ||||
-rw-r--r-- | test/unit/api/python/test_to_python_obj.py | 14 |
12 files changed, 487 insertions, 310 deletions
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() |