Adding python API test (#6546)

This commit adds unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.

1 files changed, 392 insertions, 6 deletions

diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 74eda63bc..15e669f02 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -1,6 +1,6 @@
 ###############################################################################
 # Top contributors (to current version):
-#   Yoni Zohar
+#   Yoni Zohar, Ying Sheng
 #
 # This file is part of the cvc5 project.
 #
@@ -17,10 +17,12 @@ import sys
 
 from pycvc5 import kinds
 
+
 @pytest.fixture
 def solver():
     return pycvc5.Solver()
 
+
 def test_recoverable_exception(solver):
     solver.setOption("produce-models", "true")
     x = solver.mkConst(solver.getBooleanSort(), "x")
@@ -28,12 +30,396 @@ def test_recoverable_exception(solver):
     with pytest.raises(RuntimeError):
         c = solver.getValue(x)
 
+
 def test_supports_floating_point(solver):
     if solver.supportsFloatingPoint():
-      try:
-          solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
-      except RuntimeError:
-          pytest.fail()
+        solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
+
+
+def test_get_boolean_sort(solver):
+    solver.getBooleanSort()
+
+
+def test_get_integer_sort(solver):
+    solver.getIntegerSort()
+
+
+def test_get_real_sort(solver):
+    solver.getRealSort()
+
+
+def test_get_reg_exp_sort(solver):
+    solver.getRegExpSort()
+
+
+def test_get_string_sort(solver):
+    solver.getStringSort()
+
+
+def test_get_rounding_mode_sort(solver):
+    if solver.supportsFloatingPoint():
+        solver.getRoundingModeSort()
+    else:
+        with pytest.raises(RuntimeError):
+            solver.getRoundingModeSort()
+
+
+def test_mk_array_sort(solver):
+    boolSort = solver.getBooleanSort()
+    intSort = solver.getIntegerSort()
+    realSort = solver.getRealSort()
+    bvSort = solver.mkBitVectorSort(32)
+    solver.mkArraySort(boolSort, boolSort)
+    solver.mkArraySort(intSort, intSort)
+    solver.mkArraySort(realSort, realSort)
+    solver.mkArraySort(bvSort, bvSort)
+    solver.mkArraySort(boolSort, intSort)
+    solver.mkArraySort(realSort, bvSort)
+
+    if (solver.supportsFloatingPoint()):
+        fpSort = solver.mkFloatingPointSort(3, 5)
+        solver.mkArraySort(fpSort, fpSort)
+        solver.mkArraySort(bvSort, fpSort)
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkArraySort(boolSort, boolSort)
+
+
+def test_mk_bit_vector_sort(solver):
+    solver.mkBitVectorSort(32)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVectorSort(0)
+
+
+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.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
+            solver.mkFloatingPointSort(4, 8)
+
+
+def test_mk_datatype_sort(solver):
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    solver.mkDatatypeSort(dtypeSpec)
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkDatatypeSort(dtypeSpec)
+
+    throwsDtypeSpec = solver.mkDatatypeDecl("list")
+    with pytest.raises(RuntimeError):
+        solver.mkDatatypeSort(throwsDtypeSpec)
+
+
+def test_mk_datatype_sorts(solver):
+    slv = pycvc5.Solver()
+
+    dtypeSpec1 = solver.mkDatatypeDecl("list1")
+    cons1 = solver.mkDatatypeConstructorDecl("cons1")
+    cons1.addSelector("head1", solver.getIntegerSort())
+    dtypeSpec1.addConstructor(cons1)
+    nil1 = solver.mkDatatypeConstructorDecl("nil1")
+    dtypeSpec1.addConstructor(nil1)
+
+    dtypeSpec2 = solver.mkDatatypeDecl("list2")
+    cons2 = solver.mkDatatypeConstructorDecl("cons2")
+    cons2.addSelector("head2", solver.getIntegerSort())
+    dtypeSpec2.addConstructor(cons2)
+    nil2 = solver.mkDatatypeConstructorDecl("nil2")
+    dtypeSpec2.addConstructor(nil2)
+
+    decls = [dtypeSpec1, dtypeSpec2]
+    solver.mkDatatypeSorts(decls, [])
+
+    with pytest.raises(RuntimeError):
+        slv.mkDatatypeSorts(decls, [])
+
+    throwsDtypeSpec = solver.mkDatatypeDecl("list")
+    throwsDecls = [throwsDtypeSpec]
+    with pytest.raises(RuntimeError):
+        solver.mkDatatypeSorts(throwsDecls, [])
+
+    # with unresolved sorts
+    unresList = solver.mkUninterpretedSort("ulist")
+    unresSorts = [unresList]
+    ulist = solver.mkDatatypeDecl("ulist")
+    ucons = solver.mkDatatypeConstructorDecl("ucons")
+    ucons.addSelector("car", unresList)
+    ucons.addSelector("cdr", unresList)
+    ulist.addConstructor(ucons)
+    unil = solver.mkDatatypeConstructorDecl("unil")
+    ulist.addConstructor(unil)
+    udecls = [ulist]
+
+    solver.mkDatatypeSorts(udecls, unresSorts)
+    with pytest.raises(RuntimeError):
+        slv.mkDatatypeSorts(udecls, unresSorts)
+
+
+def test_mk_function_sort(solver):
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+            solver.getIntegerSort())
+
+    # function arguments are allowed
+    solver.mkFunctionSort(funSort, solver.getIntegerSort())
+
+    # non-first-class arguments are not allowed
+    reSort = solver.getRegExpSort()
+    with pytest.raises(RuntimeError):
+        solver.mkFunctionSort(reSort, solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        solver.mkFunctionSort(solver.getIntegerSort(), funSort)
+
+    solver.mkFunctionSort([solver.mkUninterpretedSort("u"),\
+            solver.getIntegerSort()],\
+            solver.getIntegerSort())
+    funSort2 = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+            solver.getIntegerSort())
+
+    # function arguments are allowed
+    solver.mkFunctionSort([funSort2, solver.mkUninterpretedSort("u")],\
+            solver.getIntegerSort())
+
+    with pytest.raises(RuntimeError):
+        solver.mkFunctionSort([solver.getIntegerSort(),\
+                solver.mkUninterpretedSort("u")],\
+                funSort2)
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+                solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        slv.mkFunctionSort(slv.mkUninterpretedSort("u"),\
+                solver.getIntegerSort())
+    sorts1 = [solver.getBooleanSort(),\
+            slv.getIntegerSort(),\
+            solver.getIntegerSort()]
+    sorts2 = [slv.getBooleanSort(), slv.getIntegerSort()]
+    slv.mkFunctionSort(sorts2, slv.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        slv.mkFunctionSort(sorts1, slv.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        slv.mkFunctionSort(sorts2, solver.getIntegerSort())
+
+
+def test_mk_param_sort(solver):
+    solver.mkParamSort("T")
+    solver.mkParamSort("")
+
+
+def test_mk_predicate_sort(solver):
+    solver.mkPredicateSort([solver.getIntegerSort()])
+    with pytest.raises(RuntimeError):
+        solver.mkPredicateSort([])
+
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+            solver.getIntegerSort())
+    # functions as arguments are allowed
+    solver.mkPredicateSort([solver.getIntegerSort(), funSort])
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkPredicateSort([solver.getIntegerSort()])
+
+
+def test_mk_record_sort(solver):
+    fields = [("b", solver.getBooleanSort()),\
+              ("bv", solver.mkBitVectorSort(8)),\
+              ("i", solver.getIntegerSort())]
+    empty = []
+    solver.mkRecordSort(fields)
+    solver.mkRecordSort(empty)
+    recSort = solver.mkRecordSort(fields)
+    recSort.getDatatype()
+
+
+def test_mk_set_sort(solver):
+    solver.mkSetSort(solver.getBooleanSort())
+    solver.mkSetSort(solver.getIntegerSort())
+    solver.mkSetSort(solver.mkBitVectorSort(4))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkSetSort(solver.mkBitVectorSort(4))
+
+
+def test_mk_sequence_sort(solver):
+    solver.mkSequenceSort(solver.getBooleanSort())
+    solver.mkSequenceSort(\
+            solver.mkSequenceSort(solver.getIntegerSort()))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkSequenceSort(solver.getIntegerSort())
+
+
+def test_mk_uninterpreted_sort(solver):
+    solver.mkUninterpretedSort("u")
+    solver.mkUninterpretedSort("")
+
+
+def test_mk_sortConstructor_sort(solver):
+    solver.mkSortConstructorSort("s", 2)
+    solver.mkSortConstructorSort("", 2)
+    with pytest.raises(RuntimeError):
+        solver.mkSortConstructorSort("", 0)
+
+
+def test_mk_tuple_sort(solver):
+    solver.mkTupleSort([solver.getIntegerSort()])
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+                                    solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        solver.mkTupleSort([solver.getIntegerSort(), funSort])
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkTupleSort([solver.getIntegerSort()])
+
+
+def test_mk_var(solver):
+    boolSort = solver.getBooleanSort()
+    intSort = solver.getIntegerSort()
+    funSort = solver.mkFunctionSort(intSort, boolSort)
+    solver.mkVar(boolSort)
+    solver.mkVar(funSort)
+    solver.mkVar(boolSort, "b")
+    solver.mkVar(funSort, "")
+    with pytest.raises(RuntimeError):
+        solver.mkVar(pycvc5.Sort(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkVar(pycvc5.Sort(solver), "a")
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkVar(boolSort, "x")
+
+
+def test_mk_boolean(solver):
+    solver.mkBoolean(True)
+    solver.mkBoolean(False)
+
+
+def test_mk_rounding_mode(solver):
+    if solver.supportsFloatingPoint():
+        solver.mkRoundingMode(pycvc5.RoundTowardZero)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkRoundingMode(pycvc5.RoundTowardZero)
+
+
+def test_mk_uninterpreted_const(solver):
+    solver.mkUninterpretedConst(solver.getBooleanSort(), 1)
+    with pytest.raises(RuntimeError):
+        solver.mkUninterpretedConst(pycvc5.Sort(solver), 1)
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkUninterpretedConst(solver.getBooleanSort(), 1)
+
+
+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)
+
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(0, 5, pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(0, 5, t1)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(3, 0, t1)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(3, 5, t2)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(3, 5, t2)
+
+    if (solver.supportsFloatingPoint()):
+        slv = pycvc5.Solver()
+        with pytest.raises(RuntimeError):
+            slv.mkFloatingPoint(3, 5, t1)
+
+
+def test_mk_empty_set(solver):
+    slv = pycvc5.Solver()
+    s = solver.mkSetSort(solver.getBooleanSort())
+    solver.mkEmptySet(pycvc5.Sort(solver))
+    solver.mkEmptySet(s)
+    with pytest.raises(RuntimeError):
+        solver.mkEmptySet(solver.getBooleanSort())
+    with pytest.raises(RuntimeError):
+        slv.mkEmptySet(s)
+
+
+def test_mk_empty_sequence(solver):
+    slv = pycvc5.Solver()
+    s = solver.mkSequenceSort(solver.getBooleanSort())
+    solver.mkEmptySequence(s)
+    solver.mkEmptySequence(solver.getBooleanSort())
+    with pytest.raises(RuntimeError):
+        slv.mkEmptySequence(s)
+
+
+def test_mk_false(solver):
+    solver.mkFalse()
+    solver.mkFalse()
+
+
+def test_mk_nan(solver):
+    if (solver.supportsFloatingPoint()):
+        solver.mkNaN(3, 5)
+    else:
+        with pytest.raises(RuntimeError):
+            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)
+
+
+def test_mk_neg_inf(solver):
+    if (solver.supportsFloatingPoint()):
+        solver.mkNegInf(3, 5)
+    else:
+        with pytest.raises(RuntimeError):
+            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)
+
+
+def test_mk_pos_zero(solver):
+    if (solver.supportsFloatingPoint()):
+        solver.mkPosZero(3, 5)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkPosZero(3, 5)
+
+
+def test_mk_pi(solver):
+    solver.mkPi()