Merge branch 'master' into rmTearDownIncrementalrmTearDownIncremental

5 files changed, 635 insertions, 80 deletions

diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt
index 54134b510..5b681ca36 100644
--- a/test/python/CMakeLists.txt
+++ b/test/python/CMakeLists.txt
@@ -33,3 +33,5 @@ cvc5_add_python_api_test(pytest_term unit/api/test_term.py)
 cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py)
 cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py)
 cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py)
+cvc5_add_python_api_test(pytest_op unit/api/test_op.py)
+cvc5_add_python_api_test(pytest_result unit/api/test_result.py)
diff --git a/test/python/unit/api/test_op.py b/test/python/unit/api/test_op.py
new file mode 100644
index 000000000..07a57a5c6
--- /dev/null
+++ b/test/python/unit/api/test_op.py
@@ -0,0 +1,178 @@
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# Unit tests for op API.
+#
+# Obtained by translating test/unit/api/op_black.cpp
+##
+
+import pytest
+import pycvc5
+from pycvc5 import kinds
+from pycvc5 import Sort
+from pycvc5 import Op
+
+
+@pytest.fixture
+def solver():
+    return pycvc5.Solver()
+
+
+def test_get_kind(solver):
+    x = solver.mkOp(kinds.BVExtract, 31, 1)
+    x.getKind()
+
+
+def test_is_null(solver):
+    x = Op(solver)
+    assert x.isNull()
+    x = solver.mkOp(kinds.BVExtract, 31, 1)
+    assert not x.isNull()
+
+
+def test_op_from_kind(solver):
+    solver.mkOp(kinds.Plus)
+    with pytest.raises(RuntimeError):
+        solver.mkOp(kinds.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,
+                                                       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)
+
+    assert 0 == plus.getNumIndices()
+    assert 1 == divisible.getNumIndices()
+    assert 1 == bitvector_repeat.getNumIndices()
+    assert 1 == bitvector_zero_extend.getNumIndices()
+    assert 1 == bitvector_sign_extend.getNumIndices()
+    assert 1 == bitvector_rotate_left.getNumIndices()
+    assert 1 == bitvector_rotate_right.getNumIndices()
+    assert 1 == int_to_bitvector.getNumIndices()
+    assert 1 == iand.getNumIndices()
+    assert 1 == floatingpoint_to_ubv.getNumIndices()
+    assert 1 == floatingopint_to_sbv.getNumIndices()
+    assert 2 == floatingpoint_to_fp_ieee_bitvector.getNumIndices()
+    assert 2 == floatingpoint_to_fp_floatingpoint.getNumIndices()
+    assert 2 == floatingpoint_to_fp_real.getNumIndices()
+    assert 2 == floatingpoint_to_fp_signed_bitvector.getNumIndices()
+    assert 2 == floatingpoint_to_fp_unsigned_bitvector.getNumIndices()
+    assert 2 == floatingpoint_to_fp_generic.getNumIndices()
+    assert 2 == regexp_loop.getNumIndices()
+
+
+def test_get_indices_string(solver):
+    x = Op(solver)
+    with pytest.raises(RuntimeError):
+        x.getIndices()
+
+    divisible_ot = solver.mkOp(kinds.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)
+    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_idx = bitvector_zero_extend_ot.getIndices()
+    assert bitvector_zero_extend_idx == 6
+
+    bitvector_sign_extend_ot = solver.mkOp(kinds.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_idx = bitvector_rotate_left_ot.getIndices()
+    assert bitvector_rotate_left_idx == 8
+
+    bitvector_rotate_right_ot = solver.mkOp(kinds.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_idx = int_to_bitvector_ot.getIndices()
+    assert int_to_bitvector_idx == 10
+
+    floatingpoint_to_ubv_ot = solver.mkOp(kinds.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_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)
+    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)
+    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_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_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)
+    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)
+    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_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)
+    op_repr = str(bitvector_repeat_ot)
+    assert str(bitvector_repeat_ot) == op_repr
diff --git a/test/python/unit/api/test_result.py b/test/python/unit/api/test_result.py
new file mode 100644
index 000000000..bd97646f9
--- /dev/null
+++ b/test/python/unit/api/test_result.py
@@ -0,0 +1,115 @@
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# Unit tests for result API.
+#
+# Obtained by translating test/unit/api/result_black.cpp
+##
+
+import pytest
+import pycvc5
+from pycvc5 import kinds
+from pycvc5 import Result
+from pycvc5 import UnknownExplanation
+
+
+@pytest.fixture
+def solver():
+    return pycvc5.Solver()
+
+
+def test_is_null(solver):
+    res_null = Result(solver)
+    assert res_null.isNull()
+    assert not res_null.isSat()
+    assert not res_null.isUnsat()
+    assert not res_null.isSatUnknown()
+    assert not res_null.isEntailed()
+    assert not res_null.isNotEntailed()
+    assert not res_null.isEntailmentUnknown()
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(u_sort, "x")
+    solver.assertFormula(x.eqTerm(x))
+    res = solver.checkSat()
+    assert not res.isNull()
+
+
+def test_eq(solver):
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(u_sort, "x")
+    solver.assertFormula(x.eqTerm(x))
+    res2 = solver.checkSat()
+    res3 = solver.checkSat()
+    res = res2
+    assert res == res2
+    assert res3 == res2
+
+
+def test_is_sat(solver):
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(u_sort, "x")
+    solver.assertFormula(x.eqTerm(x))
+    res = solver.checkSat()
+    assert res.isSat()
+    assert not res.isSatUnknown()
+
+
+def test_is_unsat(solver):
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(u_sort, "x")
+    solver.assertFormula(x.eqTerm(x).notTerm())
+    res = solver.checkSat()
+    assert res.isUnsat()
+    assert not res.isSatUnknown()
+
+
+def test_is_sat_unknown(solver):
+    solver.setLogic("QF_NIA")
+    solver.setOption("incremental", "false")
+    solver.setOption("solve-int-as-bv", "32")
+    int_sort = solver.getIntegerSort()
+    x = solver.mkVar(int_sort, "x")
+    solver.assertFormula(x.eqTerm(x).notTerm())
+    res = solver.checkSat()
+    assert not res.isSat()
+    assert res.isSatUnknown()
+
+
+def test_is_entailed(solver):
+    solver.setOption("incremental", "true")
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkConst(u_sort, "x")
+    y = solver.mkConst(u_sort, "y")
+    a = x.eqTerm(y).notTerm()
+    b = x.eqTerm(y)
+    solver.assertFormula(a)
+    entailed = solver.checkEntailed(a)
+    assert entailed.isEntailed()
+    assert not entailed.isEntailmentUnknown()
+    not_entailed = solver.checkEntailed(b)
+    assert not_entailed.isNotEntailed()
+    assert not not_entailed.isEntailmentUnknown()
+
+
+def test_is_entailment_unknown(solver):
+    solver.setLogic("QF_NIA")
+    solver.setOption("incremental", "false")
+    solver.setOption("solve-int-as-bv", "32")
+    int_sort = solver.getIntegerSort()
+    x = solver.mkVar(int_sort, "x")
+    solver.assertFormula(x.eqTerm(x).notTerm())
+    res = solver.checkEntailed(x.eqTerm(x))
+    assert not res.isEntailed()
+    assert res.isEntailmentUnknown()
+    print(type(pycvc5.RoundTowardZero))
+    print(type(pycvc5.UnknownReason))
+    assert res.getUnknownExplanation() == pycvc5.UnknownReason
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 44ce684dd..8b3ce944e 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -32,11 +32,7 @@ def test_recoverable_exception(solver):
 
 
 def test_supports_floating_point(solver):
-    if solver.supportsFloatingPoint():
-        solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
+    solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
 
 
 def test_get_boolean_sort(solver):
@@ -47,6 +43,10 @@ def test_get_integer_sort(solver):
     solver.getIntegerSort()
 
 
+def test_get_null_sort(solver):
+    solver.getNullSort()
+
+
 def test_get_real_sort(solver):
     solver.getRealSort()
 
@@ -60,11 +60,7 @@ def test_get_string_sort(solver):
 
 
 def test_get_rounding_mode_sort(solver):
-    if solver.supportsFloatingPoint():
-        solver.getRoundingModeSort()
-    else:
-        with pytest.raises(RuntimeError):
-            solver.getRoundingModeSort()
+    solver.getRoundingModeSort()
 
 
 def test_mk_array_sort(solver):
@@ -79,10 +75,9 @@ def test_mk_array_sort(solver):
     solver.mkArraySort(boolSort, intSort)
     solver.mkArraySort(realSort, bvSort)
 
-    if (solver.supportsFloatingPoint()):
-        fpSort = solver.mkFloatingPointSort(3, 5)
-        solver.mkArraySort(fpSort, fpSort)
-        solver.mkArraySort(bvSort, fpSort)
+    fpSort = solver.mkFloatingPointSort(3, 5)
+    solver.mkArraySort(fpSort, fpSort)
+    solver.mkArraySort(bvSort, fpSort)
 
     slv = pycvc5.Solver()
     with pytest.raises(RuntimeError):
@@ -96,15 +91,11 @@ def test_mk_bit_vector_sort(solver):
 
 
 def test_mk_floating_point_sort(solver):
-    if solver.supportsFloatingPoint():
-        solver.mkFloatingPointSort(4, 8)
-        with pytest.raises(RuntimeError):
-            solver.mkFloatingPointSort(0, 8)
-        with pytest.raises(RuntimeError):
-            solver.mkFloatingPointSort(4, 0)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkFloatingPointSort(4, 8)
+    solver.mkFloatingPointSort(4, 8)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPointSort(0, 8)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPointSort(4, 0)
 
 
 def test_mk_datatype_sort(solver):
@@ -257,6 +248,15 @@ def test_mk_set_sort(solver):
         slv.mkSetSort(solver.mkBitVectorSort(4))
 
 
+def test_mk_bag_sort(solver):
+    solver.mkBagSort(solver.getBooleanSort())
+    solver.mkBagSort(solver.getIntegerSort())
+    solver.mkBagSort(solver.mkBitVectorSort(4))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkBagSort(solver.mkBitVectorSort(4))
+
+
 def test_mk_sequence_sort(solver):
     solver.mkSequenceSort(solver.getBooleanSort())
     solver.mkSequenceSort(\
@@ -290,6 +290,42 @@ def test_mk_tuple_sort(solver):
         slv.mkTupleSort([solver.getIntegerSort()])
 
 
+def test_mk_bit_vector(solver):
+    size0 = 0
+    size1 = 8
+    size2 = 32
+    val1 = 2
+    val2 = 2
+    solver.mkBitVector(size1, val1)
+    solver.mkBitVector(size2, val2)
+    solver.mkBitVector("1010", 2)
+    solver.mkBitVector("1010", 10)
+    solver.mkBitVector("1234", 10)
+    solver.mkBitVector("1010", 16)
+    solver.mkBitVector("a09f", 16)
+    solver.mkBitVector(8, "-127", 10)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector(size0, val1)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector(size0, val2)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector("", 2)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector("10", 3)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector("20", 2)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector(8, "101010101", 2)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVector(8, "-256", 10)
+    assert solver.mkBitVector("1010", 2) == solver.mkBitVector("10", 10)
+    assert solver.mkBitVector("1010", 2) == solver.mkBitVector("a", 16)
+    assert str(solver.mkBitVector(8, "01010101", 2)) == "#b01010101"
+    assert str(solver.mkBitVector(8, "F", 16)) == "#b00001111"
+    assert solver.mkBitVector(8, "-1", 10) ==\
+            solver.mkBitVector(8, "FF", 16)
+
+
 def test_mk_var(solver):
     boolSort = solver.getBooleanSort()
     intSort = solver.getIntegerSort()
@@ -313,11 +349,7 @@ def test_mk_boolean(solver):
 
 
 def test_mk_rounding_mode(solver):
-    if solver.supportsFloatingPoint():
-        solver.mkRoundingMode(pycvc5.RoundTowardZero)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkRoundingMode(pycvc5.RoundTowardZero)
+    solver.mkRoundingMode(pycvc5.RoundTowardZero)
 
 
 def test_mk_uninterpreted_const(solver):
@@ -329,15 +361,31 @@ def test_mk_uninterpreted_const(solver):
         slv.mkUninterpretedConst(solver.getBooleanSort(), 1)
 
 
+def test_mk_abstract_value(solver):
+    solver.mkAbstractValue("1")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("0")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("-1")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("1.2")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("1/2")
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue("asdf")
+
+    solver.mkAbstractValue(1)
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue(-1)
+    with pytest.raises(ValueError):
+        solver.mkAbstractValue(0)
+
+
 def test_mk_floating_point(solver):
     t1 = solver.mkBitVector(8)
     t2 = solver.mkBitVector(4)
     t3 = solver.mkInteger(2)
-    if (solver.supportsFloatingPoint()):
-        solver.mkFloatingPoint(3, 5, t1)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkFloatingPoint(3, 5, t1)
+    solver.mkFloatingPoint(3, 5, t1)
 
     with pytest.raises(RuntimeError):
         solver.mkFloatingPoint(0, 5, pycvc5.Term(solver))
@@ -350,10 +398,9 @@ def test_mk_floating_point(solver):
     with pytest.raises(RuntimeError):
         solver.mkFloatingPoint(3, 5, t2)
 
-    if (solver.supportsFloatingPoint()):
-        slv = pycvc5.Solver()
-        with pytest.raises(RuntimeError):
-            slv.mkFloatingPoint(3, 5, t1)
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkFloatingPoint(3, 5, t1)
 
 
 def test_mk_empty_set(solver):
@@ -367,6 +414,17 @@ def test_mk_empty_set(solver):
         slv.mkEmptySet(s)
 
 
+def test_mk_empty_bag(solver):
+    slv = pycvc5.Solver()
+    s = solver.mkBagSort(solver.getBooleanSort())
+    solver.mkEmptyBag(pycvc5.Sort(solver))
+    solver.mkEmptyBag(s)
+    with pytest.raises(RuntimeError):
+        solver.mkEmptyBag(solver.getBooleanSort())
+    with pytest.raises(RuntimeError):
+        slv.mkEmptyBag(s)
+
+
 def test_mk_empty_sequence(solver):
     slv = pycvc5.Solver()
     s = solver.mkSequenceSort(solver.getBooleanSort())
@@ -382,43 +440,50 @@ def test_mk_false(solver):
 
 
 def test_mk_nan(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkNaN(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkNaN(3, 5)
+    solver.mkNaN(3, 5)
 
 
 def test_mk_neg_zero(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkNegZero(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkNegZero(3, 5)
+    solver.mkNegZero(3, 5)
 
 
 def test_mk_neg_inf(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkNegInf(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkNegInf(3, 5)
+    solver.mkNegInf(3, 5)
 
 
 def test_mk_pos_inf(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkPosInf(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkPosInf(3, 5)
+    solver.mkPosInf(3, 5)
 
 
 def test_mk_pos_zero(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkPosZero(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkPosZero(3, 5)
+    solver.mkPosZero(3, 5)
+
+
+def test_mk_op(solver):
+    # mkOp(Kind kind, Kind k)
+    with pytest.raises(ValueError):
+        solver.mkOp(kinds.BVExtract, kinds.Equal)
+
+    # mkOp(Kind kind, const std::string& arg)
+    solver.mkOp(kinds.Divisible, "2147483648")
+    with pytest.raises(RuntimeError):
+        solver.mkOp(kinds.BVExtract, "asdf")
+
+    # mkOp(Kind kind, uint32_t arg)
+    solver.mkOp(kinds.Divisible, 1)
+    solver.mkOp(kinds.BVRotateLeft, 1)
+    solver.mkOp(kinds.BVRotateRight, 1)
+    with pytest.raises(RuntimeError):
+        solver.mkOp(kinds.BVExtract, 1)
+
+    # mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
+    solver.mkOp(kinds.BVExtract, 1, 1)
+    with pytest.raises(RuntimeError):
+        solver.mkOp(kinds.Divisible, 1, 2)
+
+    # mkOp(Kind kind, std::vector<uint32_t> args)
+    args = [1, 2, 2]
+    solver.mkOp(kinds.TupleProject, args)
 
 
 def test_mk_pi(solver):
@@ -568,11 +633,210 @@ def test_mk_sep_nil(solver):
         slv.mkSepNil(solver.getIntegerSort())
 
 
+def test_mk_string(solver):
+    solver.mkString("")
+    solver.mkString("asdfasdf")
+    str(solver.mkString("asdf\\nasdf")) == "\"asdf\\u{5c}nasdf\""
+    str(solver.mkString("asdf\\u{005c}nasdf", True)) ==\
+            "\"asdf\\u{5c}nasdf\""
+
+
+def test_mk_term(solver):
+    bv32 = solver.mkBitVectorSort(32)
+    a = solver.mkConst(bv32, "a")
+    b = solver.mkConst(bv32, "b")
+    v1 = [a, b]
+    v2 = [a, pycvc5.Term(solver)]
+    v3 = [a, solver.mkTrue()]
+    v4 = [solver.mkInteger(1), solver.mkInteger(2)]
+    v5 = [solver.mkInteger(1), pycvc5.Term(solver)]
+    v6 = []
+    slv = pycvc5.Solver()
+
+    # mkTerm(Kind kind) const
+    solver.mkPi()
+    solver.mkTerm(kinds.RegexpEmpty)
+    solver.mkTerm(kinds.RegexpSigma)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ConstBV)
+
+    # mkTerm(Kind kind, Term child) const
+    solver.mkTerm(kinds.Not, solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Not, pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Not, a)
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.Not, solver.mkTrue())
+
+    # mkTerm(Kind kind, Term child1, Term child2) const
+    solver.mkTerm(kinds.Equal, a, b)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, pycvc5.Term(solver), b)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, a, pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, a, solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.Equal, a, b)
+
+    # mkTerm(Kind kind, Term child1, Term child2, Term child3) const
+    solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Ite, pycvc5.Term(solver), solver.mkTrue(),
+                      solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Ite, solver.mkTrue(), pycvc5.Term(solver),
+                      solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(),
+                      pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), b)
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(),
+                   solver.mkTrue())
+
+    # mkTerm(Kind kind, const std::vector<Term>& children) const
+    solver.mkTerm(kinds.Equal, v1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, v2)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Equal, v3)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.Distinct, v6)
+
+
+def test_mk_term_from_op(solver):
+    bv32 = solver.mkBitVectorSort(32)
+    a = solver.mkConst(bv32, "a")
+    b = solver.mkConst(bv32, "b")
+    v1 = [solver.mkInteger(1), solver.mkInteger(2)]
+    v2 = [solver.mkInteger(1), pycvc5.Term(solver)]
+    v3 = []
+    v4 = [solver.mkInteger(5)]
+    slv = pycvc5.Solver()
+
+    # simple operator terms
+    opterm1 = solver.mkOp(kinds.BVExtract, 2, 1)
+    opterm2 = solver.mkOp(kinds.Divisible, 1)
+
+    # list datatype
+    sort = solver.mkParamSort("T")
+    listDecl = solver.mkDatatypeDecl("paramlist", sort)
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    cons.addSelector("head", sort)
+    cons.addSelectorSelf("tail")
+    listDecl.addConstructor(cons)
+    listDecl.addConstructor(nil)
+    listSort = solver.mkDatatypeSort(listDecl)
+    intListSort =\
+        listSort.instantiate([solver.getIntegerSort()])
+    c = solver.mkConst(intListSort, "c")
+    lis = listSort.getDatatype()
+
+    # list datatype constructor and selector operator terms
+    consTerm1 = lis.getConstructorTerm("cons")
+    consTerm2 = lis.getConstructor("cons").getConstructorTerm()
+    nilTerm1 = lis.getConstructorTerm("nil")
+    nilTerm2 = lis.getConstructor("nil").getConstructorTerm()
+    headTerm1 = lis["cons"].getSelectorTerm("head")
+    headTerm2 = lis["cons"].getSelector("head").getSelectorTerm()
+    tailTerm1 = lis["cons"].getSelectorTerm("tail")
+    tailTerm2 = lis["cons"]["tail"].getSelectorTerm()
+
+    # mkTerm(Op op, Term term) const
+    solver.mkTerm(kinds.ApplyConstructor, nilTerm1)
+    solver.mkTerm(kinds.ApplyConstructor, nilTerm2)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ApplySelector, nilTerm1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ApplySelector, consTerm1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ApplyConstructor, consTerm2)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(kinds.ApplySelector, headTerm1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm1)
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.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)
+    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))
+    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))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm1, a, b)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, solver.mkInteger(1), pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1))
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(kinds.ApplyConstructor,\
+                        consTerm1,\
+                        solver.mkInteger(0),\
+                        solver.mkTerm(kinds.ApplyConstructor, nilTerm1))
+
+    # mkTerm(Op op, Term child1, Term child2, Term child3) const
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm1, a, b, a)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1),
+                      pycvc5.Term(solver))
+
+    # mkTerm(Op op, const std::vector<Term>& children) const
+    solver.mkTerm(opterm2, v4)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, v1)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, v2)
+    with pytest.raises(RuntimeError):
+        solver.mkTerm(opterm2, v3)
+    with pytest.raises(RuntimeError):
+        slv.mkTerm(opterm2, v4)
+
+
 def test_mk_true(solver):
     solver.mkTrue()
     solver.mkTrue()
 
 
+def test_mk_tuple(solver):
+    solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)])
+    solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")])
+
+    with pytest.raises(RuntimeError):
+        solver.mkTuple([], [solver.mkBitVector("101", 2)])
+    with pytest.raises(RuntimeError):
+        solver.mkTuple([solver.mkBitVectorSort(4)],
+                       [solver.mkBitVector("101", 2)])
+    with pytest.raises(RuntimeError):
+        solver.mkTuple([solver.getIntegerSort()], [solver.mkReal("5.3")])
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkTuple([solver.mkBitVectorSort(3)], [slv.mkBitVector("101", 2)])
+    with pytest.raises(RuntimeError):
+        slv.mkTuple([slv.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)])
+
+
 def test_mk_universe_set(solver):
     solver.mkUniverseSet(solver.getBooleanSort())
     with pytest.raises(RuntimeError):
diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py
index 5e86382ee..def539cf4 100644
--- a/test/python/unit/api/test_sort.py
+++ b/test/python/unit/api/test_sort.py
@@ -89,9 +89,8 @@ def test_is_reg_exp(solver):
 
 
 def test_is_rounding_mode(solver):
-    if solver.supportsFloatingPoint():
-        assert solver.getRoundingModeSort().isRoundingMode()
-        Sort(solver).isRoundingMode()
+    assert solver.getRoundingModeSort().isRoundingMode()
+    Sort(solver).isRoundingMode()
 
 
 def test_is_bit_vector(solver):
@@ -100,9 +99,8 @@ def test_is_bit_vector(solver):
 
 
 def test_is_floating_point(solver):
-    if solver.supportsFloatingPoint():
-        assert solver.mkFloatingPointSort(8, 24).isFloatingPoint()
-        Sort(solver).isFloatingPoint()
+    assert solver.mkFloatingPointSort(8, 24).isFloatingPoint()
+    Sort(solver).isFloatingPoint()
 
 
 def test_is_datatype(solver):
@@ -447,21 +445,19 @@ def test_get_bv_size(solver):
 
 
 def test_get_fp_exponent_size(solver):
-    if solver.supportsFloatingPoint():
-        fpSort = solver.mkFloatingPointSort(4, 8)
-        fpSort.getFPExponentSize()
-        setSort = solver.mkSetSort(solver.getIntegerSort())
-        with pytest.raises(RuntimeError):
-            setSort.getFPExponentSize()
+    fpSort = solver.mkFloatingPointSort(4, 8)
+    fpSort.getFPExponentSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        setSort.getFPExponentSize()
 
 
 def test_get_fp_significand_size(solver):
-    if solver.supportsFloatingPoint():
-        fpSort = solver.mkFloatingPointSort(4, 8)
-        fpSort.getFPSignificandSize()
-        setSort = solver.mkSetSort(solver.getIntegerSort())
-        with pytest.raises(RuntimeError):
-            setSort.getFPSignificandSize()
+    fpSort = solver.mkFloatingPointSort(4, 8)
+    fpSort.getFPSignificandSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        setSort.getFPSignificandSize()
 
 
 def test_get_datatype_paramsorts(solver):