Adding python API test part 2 (#6551)

This commit (follow #6546) adds more unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.

diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 15e669f02cf38f4a4572de05a780c37b81bc765f..85594d5302eee80af6a3c0a2bafa88925dfbe34c 100644 (file)
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -423,3 +423,464 @@ def test_mk_pos_zero(solver):
 
 def test_mk_pi(solver):
     solver.mkPi()
+
+
+def test_mk_integer(solver):
+    solver.mkInteger("123")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("1.23")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("1/23")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("12/3")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger(".2")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("2.")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("asdf")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("1.2/3")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger(".")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("/")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("2/")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("/2")
+
+    solver.mkReal("123")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("1.23")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("1/23")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("12/3")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger(".2")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("2.")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("asdf")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("1.2/3")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger(".")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("/")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("2/")
+    with pytest.raises(RuntimeError):
+        solver.mkInteger("/2")
+
+    val1 = 1
+    val2 = -1
+    val3 = 1
+    val4 = -1
+    solver.mkInteger(val1)
+    solver.mkInteger(val2)
+    solver.mkInteger(val3)
+    solver.mkInteger(val4)
+    solver.mkInteger(val4)
+
+
+def test_mk_real(solver):
+    solver.mkReal("123")
+    solver.mkReal("1.23")
+    solver.mkReal("1/23")
+    solver.mkReal("12/3")
+    solver.mkReal(".2")
+    solver.mkReal("2.")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("asdf")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("1.2/3")
+    with pytest.raises(RuntimeError):
+        solver.mkReal(".")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("/")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("2/")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("/2")
+
+    solver.mkReal("123")
+    solver.mkReal("1.23")
+    solver.mkReal("1/23")
+    solver.mkReal("12/3")
+    solver.mkReal(".2")
+    solver.mkReal("2.")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("asdf")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("1.2/3")
+    with pytest.raises(RuntimeError):
+        solver.mkReal(".")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("/")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("2/")
+    with pytest.raises(RuntimeError):
+        solver.mkReal("/2")
+
+    val1 = 1
+    val2 = -1
+    val3 = 1
+    val4 = -1
+    solver.mkReal(val1)
+    solver.mkReal(val2)
+    solver.mkReal(val3)
+    solver.mkReal(val4)
+    solver.mkReal(val4)
+    solver.mkReal(val1, val1)
+    solver.mkReal(val2, val2)
+    solver.mkReal(val3, val3)
+    solver.mkReal(val4, val4)
+
+
+def test_mk_regexp_empty(solver):
+    strSort = solver.getStringSort()
+    s = solver.mkConst(strSort, "s")
+    solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpEmpty())
+
+
+def test_mk_regexp_sigma(solver):
+    strSort = solver.getStringSort()
+    s = solver.mkConst(strSort, "s")
+    solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpSigma())
+
+
+def test_mk_sep_nil(solver):
+    solver.mkSepNil(solver.getBooleanSort())
+    with pytest.raises(RuntimeError):
+        solver.mkSepNil(pycvc5.Sort(solver))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkSepNil(solver.getIntegerSort())
+
+
+def test_mk_true(solver):
+    solver.mkTrue()
+    solver.mkTrue()
+
+
+def test_mk_universe_set(solver):
+    solver.mkUniverseSet(solver.getBooleanSort())
+    with pytest.raises(RuntimeError):
+        solver.mkUniverseSet(pycvc5.Sort(solver))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkUniverseSet(solver.getBooleanSort())
+
+
+def test_mk_const(solver):
+    boolSort = solver.getBooleanSort()
+    intSort = solver.getIntegerSort()
+    funSort = solver.mkFunctionSort(intSort, boolSort)
+    solver.mkConst(boolSort)
+    solver.mkConst(funSort)
+    solver.mkConst(boolSort, "b")
+    solver.mkConst(intSort, "i")
+    solver.mkConst(funSort, "f")
+    solver.mkConst(funSort, "")
+    with pytest.raises(RuntimeError):
+        solver.mkConst(pycvc5.Sort(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkConst(pycvc5.Sort(solver), "a")
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkConst(boolSort)
+
+
+def test_mk_const_array(solver):
+    intSort = solver.getIntegerSort()
+    arrSort = solver.mkArraySort(intSort, intSort)
+    zero = solver.mkInteger(0)
+    constArr = solver.mkConstArray(arrSort, zero)
+
+    solver.mkConstArray(arrSort, zero)
+    with pytest.raises(RuntimeError):
+        solver.mkConstArray(pycvc5.Sort(solver), zero)
+    with pytest.raises(RuntimeError):
+        solver.mkConstArray(arrSort, pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkConstArray(arrSort, solver.mkBitVector(1, 1))
+    with pytest.raises(RuntimeError):
+        solver.mkConstArray(intSort, zero)
+    slv = pycvc5.Solver()
+    zero2 = slv.mkInteger(0)
+    arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        slv.mkConstArray(arrSort2, zero)
+    with pytest.raises(RuntimeError):
+        slv.mkConstArray(arrSort, zero2)
+
+
+def test_declare_fun(solver):
+    bvSort = solver.mkBitVectorSort(32)
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+                                    solver.getIntegerSort())
+    solver.declareFun("f1", [], bvSort)
+    solver.declareFun("f3", [bvSort, solver.getIntegerSort()], bvSort)
+    with pytest.raises(RuntimeError):
+        solver.declareFun("f2", [], funSort)
+    # functions as arguments is allowed
+    solver.declareFun("f4", [bvSort, funSort], bvSort)
+    with pytest.raises(RuntimeError):
+        solver.declareFun("f5", [bvSort, bvSort], funSort)
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.declareFun("f1", [], bvSort)
+
+
+def test_declare_sort(solver):
+    solver.declareSort("s", 0)
+    solver.declareSort("s", 2)
+    solver.declareSort("", 2)
+
+
+def test_define_fun(solver):
+    bvSort = solver.mkBitVectorSort(32)
+    funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort)
+    funSort2 = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+                                     solver.getIntegerSort())
+    b1 = solver.mkVar(bvSort, "b1")
+    b11 = solver.mkVar(bvSort, "b1")
+    b2 = solver.mkVar(solver.getIntegerSort(), "b2")
+    b3 = solver.mkVar(funSort2, "b3")
+    v1 = solver.mkConst(bvSort, "v1")
+    v2 = solver.mkConst(solver.getIntegerSort(), "v2")
+    v3 = solver.mkConst(funSort2, "v3")
+    f1 = solver.mkConst(funSort1, "f1")
+    f2 = solver.mkConst(funSort2, "f2")
+    f3 = solver.mkConst(bvSort, "f3")
+    solver.defineFun("f", [], bvSort, v1)
+    solver.defineFun("ff", [b1, b2], bvSort, v1)
+    solver.defineFun(f1, [b1, b11], v1)
+    with pytest.raises(RuntimeError):
+        solver.defineFun("ff", [v1, b2], bvSort, v1)
+    with pytest.raises(RuntimeError):
+        solver.defineFun("fff", [b1], bvSort, v3)
+    with pytest.raises(RuntimeError):
+        solver.defineFun("ffff", [b1], funSort2, v3)
+    # b3 has function sort, which is allowed as an argument
+    solver.defineFun("fffff", [b1, b3], bvSort, v1)
+    with pytest.raises(RuntimeError):
+        solver.defineFun(f1, [v1, b11], v1)
+    with pytest.raises(RuntimeError):
+        solver.defineFun(f1, [b1], v1)
+    with pytest.raises(RuntimeError):
+        solver.defineFun(f1, [b1, b11], v2)
+    with pytest.raises(RuntimeError):
+        solver.defineFun(f1, [b1, b11], v3)
+    with pytest.raises(RuntimeError):
+        solver.defineFun(f2, [b1], v2)
+    with pytest.raises(RuntimeError):
+        solver.defineFun(f3, [b1], v1)
+
+    slv = pycvc5.Solver()
+    bvSort2 = slv.mkBitVectorSort(32)
+    v12 = slv.mkConst(bvSort2, "v1")
+    b12 = slv.mkVar(bvSort2, "b1")
+    b22 = slv.mkVar(slv.getIntegerSort(), "b2")
+    with pytest.raises(RuntimeError):
+        slv.defineFun("f", [], bvSort, v12)
+    with pytest.raises(RuntimeError):
+        slv.defineFun("f", [], bvSort2, v1)
+    with pytest.raises(RuntimeError):
+        slv.defineFun("ff", [b1, b22], bvSort2, v12)
+    with pytest.raises(RuntimeError):
+        slv.defineFun("ff", [b12, b2], bvSort2, v12)
+    with pytest.raises(RuntimeError):
+        slv.defineFun("ff", [b12, b22], bvSort, v12)
+    with pytest.raises(RuntimeError):
+        slv.defineFun("ff", [b12, b22], bvSort2, v1)
+
+
+def test_define_fun_rec(solver):
+    bvSort = solver.mkBitVectorSort(32)
+    funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort)
+    funSort2 = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+                                     solver.getIntegerSort())
+    b1 = solver.mkVar(bvSort, "b1")
+    b11 = solver.mkVar(bvSort, "b1")
+    b2 = solver.mkVar(solver.getIntegerSort(), "b2")
+    b3 = solver.mkVar(funSort2, "b3")
+    v1 = solver.mkConst(bvSort, "v1")
+    v2 = solver.mkConst(solver.getIntegerSort(), "v2")
+    v3 = solver.mkConst(funSort2, "v3")
+    f1 = solver.mkConst(funSort1, "f1")
+    f2 = solver.mkConst(funSort2, "f2")
+    f3 = solver.mkConst(bvSort, "f3")
+    solver.defineFunRec("f", [], bvSort, v1)
+    solver.defineFunRec("ff", [b1, b2], bvSort, v1)
+    solver.defineFunRec(f1, [b1, b11], v1)
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec("fff", [b1], bvSort, v3)
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec("ff", [b1, v2], bvSort, v1)
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec("ffff", [b1], funSort2, v3)
+    # b3 has function sort, which is allowed as an argument
+    solver.defineFunRec("fffff", [b1, b3], bvSort, v1)
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec(f1, [b1], v1)
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec(f1, [b1, b11], v2)
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec(f1, [b1, b11], v3)
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec(f2, [b1], v2)
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec(f3, [b1], v1)
+
+    slv = pycvc5.Solver()
+    bvSort2 = slv.mkBitVectorSort(32)
+    v12 = slv.mkConst(bvSort2, "v1")
+    b12 = slv.mkVar(bvSort2, "b1")
+    b22 = slv.mkVar(slv.getIntegerSort(), "b2")
+    slv.defineFunRec("f", [], bvSort2, v12)
+    slv.defineFunRec("ff", [b12, b22], bvSort2, v12)
+    with pytest.raises(RuntimeError):
+        slv.defineFunRec("f", [], bvSort, v12)
+    with pytest.raises(RuntimeError):
+        slv.defineFunRec("f", [], bvSort2, v1)
+    with pytest.raises(RuntimeError):
+        slv.defineFunRec("ff", [b1, b22], bvSort2, v12)
+    with pytest.raises(RuntimeError):
+        slv.defineFunRec("ff", [b12, b2], bvSort2, v12)
+    with pytest.raises(RuntimeError):
+        slv.defineFunRec("ff", [b12, b22], bvSort, v12)
+    with pytest.raises(RuntimeError):
+        slv.defineFunRec("ff", [b12, b22], bvSort2, v1)
+
+
+def test_define_fun_rec_wrong_logic(solver):
+    solver.setLogic("QF_BV")
+    bvSort = solver.mkBitVectorSort(32)
+    funSort = solver.mkFunctionSort([bvSort, bvSort], bvSort)
+    b = solver.mkVar(bvSort, "b")
+    v = solver.mkConst(bvSort, "v")
+    f = solver.mkConst(funSort, "f")
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec("f", [], bvSort, v)
+    with pytest.raises(RuntimeError):
+        solver.defineFunRec(f, [b, b], v)
+
+
+def test_uf_iteration(solver):
+    intSort = solver.getIntegerSort()
+    funSort = solver.mkFunctionSort([intSort, intSort], intSort)
+    x = solver.mkConst(intSort, "x")
+    y = solver.mkConst(intSort, "y")
+    f = solver.mkConst(funSort, "f")
+    fxy = solver.mkTerm(kinds.ApplyUf, f, x, y)
+
+    # Expecting the uninterpreted function to be one of the children
+    expected_children = [f, x, y]
+    idx = 0
+    for c in fxy:
+        assert idx < 3
+        assert c == expected_children[idx]
+        idx = idx + 1
+
+
+def test_get_info(solver):
+    solver.getInfo("name")
+    with pytest.raises(RuntimeError):
+        solver.getInfo("asdf")
+
+
+def test_get_op(solver):
+    bv32 = solver.mkBitVectorSort(32)
+    a = solver.mkConst(bv32, "a")
+    ext = solver.mkOp(kinds.BVExtract, 2, 1)
+    exta = solver.mkTerm(ext, a)
+
+    assert not a.hasOp()
+    with pytest.raises(RuntimeError):
+        a.getOp()
+    assert exta.hasOp()
+    assert exta.getOp() == ext
+
+    # Test Datatypes -- more complicated
+    consListSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    cons.addSelectorSelf("tail")
+    consListSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    consListSpec.addConstructor(nil)
+    consListSort = solver.mkDatatypeSort(consListSpec)
+    consList = consListSort.getDatatype()
+
+    consTerm = consList.getConstructorTerm("cons")
+    nilTerm = consList.getConstructorTerm("nil")
+    headTerm = consList["cons"].getSelectorTerm("head")
+
+    listnil = solver.mkTerm(kinds.ApplyConstructor, nilTerm)
+    listcons1 = solver.mkTerm(kinds.ApplyConstructor, consTerm,
+                              solver.mkInteger(1), listnil)
+    listhead = solver.mkTerm(kinds.ApplySelector, headTerm, listcons1)
+
+    assert listnil.hasOp()
+    assert listcons1.hasOp()
+    assert listhead.hasOp()
+
+
+def test_get_option(solver):
+    solver.getOption("incremental")
+    with pytest.raises(RuntimeError):
+        solver.getOption("asdf")
+
+
+def test_get_unsat_assumptions1(solver):
+    solver.setOption("incremental", "false")
+    solver.checkSatAssuming(solver.mkFalse())
+    with pytest.raises(RuntimeError):
+        solver.getUnsatAssumptions()
+
+
+def test_get_unsat_assumptions2(solver):
+    solver.setOption("incremental", "true")
+    solver.setOption("produce-unsat-assumptions", "false")
+    solver.checkSatAssuming(solver.mkFalse())
+    with pytest.raises(RuntimeError):
+        solver.getUnsatAssumptions()
+
+
+def test_get_unsat_assumptions3(solver):
+    solver.setOption("incremental", "true")
+    solver.setOption("produce-unsat-assumptions", "true")
+    solver.checkSatAssuming(solver.mkFalse())
+    solver.getUnsatAssumptions()
+    solver.checkSatAssuming(solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.getUnsatAssumptions()
+
+
+def test_get_unsat_core1(solver):
+    solver.setOption("incremental", "false")
+    solver.assertFormula(solver.mkFalse())
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.getUnsatCore()
+
+
+def test_get_unsat_core2(solver):
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-unsat-cores", "false")
+    solver.assertFormula(solver.mkFalse())
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.getUnsatCore()