summaryrefslogtreecommitdiff
path: root/test/unit/api
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/api')
-rw-r--r--test/unit/api/cpp/datatype_api_black.cpp11
-rw-r--r--test/unit/api/cpp/solver_black.cpp175
-rw-r--r--test/unit/api/java/DatatypeTest.java8
-rw-r--r--test/unit/api/java/SolverTest.java12
-rw-r--r--test/unit/api/python/test_datatype_api.py11
-rw-r--r--test/unit/api/python/test_grammar.py2
-rw-r--r--test/unit/api/python/test_op.py82
-rw-r--r--test/unit/api/python/test_result.py1
-rw-r--r--test/unit/api/python/test_solver.py336
-rw-r--r--test/unit/api/python/test_sort.py1
-rw-r--r--test/unit/api/python/test_term.py144
-rw-r--r--test/unit/api/python/test_to_python_obj.py14
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()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback