Adding python API test part 3 (#6552)

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

1 files changed, 447 insertions, 0 deletions

diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 85594d530..74e3c2b0b 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -884,3 +884,450 @@ def test_get_unsat_core2(solver):
     solver.checkSat()
     with pytest.raises(RuntimeError):
         solver.getUnsatCore()
+
+
+def test_get_unsat_core3(solver):
+    solver.setOption("incremental", "true")
+    solver.setOption("produce-unsat-cores", "true")
+
+    uSort = solver.mkUninterpretedSort("u")
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    uToIntSort = solver.mkFunctionSort(uSort, intSort)
+    intPredSort = solver.mkFunctionSort(intSort, boolSort)
+
+    x = solver.mkConst(uSort, "x")
+    y = solver.mkConst(uSort, "y")
+    f = solver.mkConst(uToIntSort, "f")
+    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))
+    solver.assertFormula(p_0)
+    solver.assertFormula(p_f_y.notTerm())
+    assert solver.checkSat().isUnsat()
+
+    unsat_core = solver.getUnsatCore()
+
+    solver.resetAssertions()
+    for t in unsat_core:
+        solver.assertFormula(t)
+    res = solver.checkSat()
+    assert res.isUnsat()
+
+
+def test_get_value1(solver):
+    solver.setOption("produce-models", "false")
+    t = solver.mkTrue()
+    solver.assertFormula(t)
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.getValue(t)
+
+
+def test_get_value2(solver):
+    solver.setOption("produce-models", "true")
+    t = solver.mkFalse()
+    solver.assertFormula(t)
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.getValue(t)
+
+
+def test_get_value3(solver):
+    solver.setOption("produce-models", "true")
+    uSort = solver.mkUninterpretedSort("u")
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    uToIntSort = solver.mkFunctionSort(uSort, intSort)
+    intPredSort = solver.mkFunctionSort(intSort, boolSort)
+
+    x = solver.mkConst(uSort, "x")
+    y = solver.mkConst(uSort, "y")
+    z = solver.mkConst(uSort, "z")
+    f = solver.mkConst(uToIntSort, "f")
+    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))
+    solver.assertFormula(p_0.notTerm())
+    solver.assertFormula(p_f_y)
+    assert solver.checkSat().isSat()
+    solver.getValue(x)
+    solver.getValue(y)
+    solver.getValue(z)
+    solver.getValue(summ)
+    solver.getValue(p_f_y)
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.getValue(x)
+
+
+def test_declare_separation_heap(solver):
+    solver.setLogic("ALL_SUPPORTED")
+    integer = solver.getIntegerSort()
+    solver.declareSeparationHeap(integer, integer)
+    # cannot declare separation logic heap more than once
+    with pytest.raises(RuntimeError):
+        solver.declareSeparationHeap(integer, integer)
+
+
+# Helper function for test_get_separation_{heap,nil}_termX. Asserts and checks
+# some simple separation logic constraints.
+def checkSimpleSeparationConstraints(slv):
+    integer = slv.getIntegerSort()
+    # declare the separation heap
+    slv.declareSeparationHeap(integer, integer)
+    x = slv.mkConst(integer, "x")
+    p = slv.mkConst(integer, "p")
+    heap = slv.mkTerm(kinds.SepPto, p, x)
+    slv.assertFormula(heap)
+    nil = slv.mkSepNil(integer)
+    slv.assertFormula(nil.eqTerm(slv.mkReal(5)))
+    slv.checkSat()
+
+
+def test_get_separation_heap_term1(solver):
+    solver.setLogic("QF_BV")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "true")
+    t = solver.mkTrue()
+    solver.assertFormula(t)
+    with pytest.raises(RuntimeError):
+        solver.getSeparationHeap()
+
+
+def test_get_separation_heap_term2(solver):
+    solver.setLogic("ALL_SUPPORTED")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "false")
+    checkSimpleSeparationConstraints(solver)
+    with pytest.raises(RuntimeError):
+        solver.getSeparationHeap()
+
+
+def test_get_separation_heap_term3(solver):
+    solver.setLogic("ALL_SUPPORTED")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "true")
+    t = solver.mkFalse()
+    solver.assertFormula(t)
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.getSeparationHeap()
+
+
+def test_get_separation_heap_term4(solver):
+    solver.setLogic("ALL_SUPPORTED")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "true")
+    t = solver.mkTrue()
+    solver.assertFormula(t)
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.getSeparationHeap()
+
+
+def test_get_separation_heap_term5(solver):
+    solver.setLogic("ALL_SUPPORTED")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "true")
+    checkSimpleSeparationConstraints(solver)
+    solver.getSeparationHeap()
+
+
+def test_get_separation_nil_term1(solver):
+    solver.setLogic("QF_BV")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "true")
+    t = solver.mkTrue()
+    solver.assertFormula(t)
+    with pytest.raises(RuntimeError):
+        solver.getSeparationNilTerm()
+
+
+def test_get_separation_nil_term2(solver):
+    solver.setLogic("ALL_SUPPORTED")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "false")
+    checkSimpleSeparationConstraints(solver)
+    with pytest.raises(RuntimeError):
+        solver.getSeparationNilTerm()
+
+
+def test_get_separation_nil_term3(solver):
+    solver.setLogic("ALL_SUPPORTED")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "true")
+    t = solver.mkFalse()
+    solver.assertFormula(t)
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.getSeparationNilTerm()
+
+
+def test_get_separation_nil_term4(solver):
+    solver.setLogic("ALL_SUPPORTED")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "true")
+    t = solver.mkTrue()
+    solver.assertFormula(t)
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.getSeparationNilTerm()
+
+
+def test_get_separation_nil_term5(solver):
+    solver.setLogic("ALL_SUPPORTED")
+    solver.setOption("incremental", "false")
+    solver.setOption("produce-models", "true")
+    checkSimpleSeparationConstraints(solver)
+    solver.getSeparationNilTerm()
+
+
+def test_push1(solver):
+    solver.setOption("incremental", "true")
+    solver.push(1)
+    with pytest.raises(RuntimeError):
+        solver.setOption("incremental", "false")
+    with pytest.raises(RuntimeError):
+        solver.setOption("incremental", "true")
+
+
+def test_push2(solver):
+    solver.setOption("incremental", "false")
+    with pytest.raises(RuntimeError):
+        solver.push(1)
+
+
+def test_pop1(solver):
+    solver.setOption("incremental", "false")
+    with pytest.raises(RuntimeError):
+        solver.pop(1)
+
+
+def test_pop2(solver):
+    solver.setOption("incremental", "true")
+    with pytest.raises(RuntimeError):
+        solver.pop(1)
+
+
+def test_pop3(solver):
+    solver.setOption("incremental", "true")
+    solver.push(1)
+    solver.pop(1)
+    with pytest.raises(RuntimeError):
+        solver.pop(1)
+
+
+def test_setInfo(solver):
+    with pytest.raises(RuntimeError):
+        solver.setInfo("cvc5-lagic", "QF_BV")
+    with pytest.raises(RuntimeError):
+        solver.setInfo("cvc2-logic", "QF_BV")
+    with pytest.raises(RuntimeError):
+        solver.setInfo("cvc5-logic", "asdf")
+
+    solver.setInfo("source", "asdf")
+    solver.setInfo("category", "asdf")
+    solver.setInfo("difficulty", "asdf")
+    solver.setInfo("filename", "asdf")
+    solver.setInfo("license", "asdf")
+    solver.setInfo("name", "asdf")
+    solver.setInfo("notes", "asdf")
+
+    solver.setInfo("smt-lib-version", "2")
+    solver.setInfo("smt-lib-version", "2.0")
+    solver.setInfo("smt-lib-version", "2.5")
+    solver.setInfo("smt-lib-version", "2.6")
+    with pytest.raises(RuntimeError):
+        solver.setInfo("smt-lib-version", ".0")
+
+    solver.setInfo("status", "sat")
+    solver.setInfo("status", "unsat")
+    solver.setInfo("status", "unknown")
+    with pytest.raises(RuntimeError):
+        solver.setInfo("status", "asdf")
+
+
+def test_simplify(solver):
+    with pytest.raises(RuntimeError):
+        solver.simplify(pycvc5.Term(solver))
+
+    bvSort = solver.mkBitVectorSort(32)
+    uSort = solver.mkUninterpretedSort("u")
+    funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort)
+    funSort2 = solver.mkFunctionSort(uSort, solver.getIntegerSort())
+    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)
+
+    x = solver.mkConst(bvSort, "x")
+    solver.simplify(x)
+    a = solver.mkConst(bvSort, "a")
+    solver.simplify(a)
+    b = solver.mkConst(bvSort, "b")
+    solver.simplify(b)
+    x_eq_x = solver.mkTerm(kinds.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)
+    solver.simplify(x_eq_b)
+    assert solver.mkTrue() != x_eq_b
+    assert solver.mkTrue() != solver.simplify(x_eq_b)
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.simplify(x)
+
+    i1 = solver.mkConst(solver.getIntegerSort(), "i1")
+    solver.simplify(i1)
+    i2 = solver.mkTerm(kinds.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))
+    solver.simplify(i3)
+    assert i1 != i3
+    assert i1 == solver.simplify(i3)
+
+    consList = consListSort.getDatatype()
+    dt1 = solver.mkTerm(\
+        kinds.ApplyConstructor,\
+        consList.getConstructorTerm("cons"),\
+        solver.mkInteger(0),\
+        solver.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil")))
+    solver.simplify(dt1)
+    dt2 = solver.mkTerm(\
+      kinds.ApplySelector, consList["cons"].getSelectorTerm("head"), dt1)
+    solver.simplify(dt2)
+
+    b1 = solver.mkVar(bvSort, "b1")
+    solver.simplify(b1)
+    b2 = solver.mkVar(bvSort, "b1")
+    solver.simplify(b2)
+    b3 = solver.mkVar(uSort, "b3")
+    solver.simplify(b3)
+    v1 = solver.mkConst(bvSort, "v1")
+    solver.simplify(v1)
+    v2 = solver.mkConst(solver.getIntegerSort(), "v2")
+    solver.simplify(v2)
+    f1 = solver.mkConst(funSort1, "f1")
+    solver.simplify(f1)
+    f2 = solver.mkConst(funSort2, "f2")
+    solver.simplify(f2)
+    solver.defineFunsRec([f1, f2], [[b1, b2], [b3]], [v1, v2])
+    solver.simplify(f1)
+    solver.simplify(f2)
+
+
+def test_assert_formula(solver):
+    solver.assertFormula(solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.assertFormula(pycvc5.Term(solver))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.assertFormula(solver.mkTrue())
+
+
+def test_check_entailed(solver):
+    solver.setOption("incremental", "false")
+    solver.checkEntailed(solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.checkEntailed(solver.mkTrue())
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.checkEntailed(solver.mkTrue())
+
+
+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)
+    solver.setOption("incremental", "true")
+    solver.checkEntailed(solver.mkTrue())
+    with pytest.raises(RuntimeError):
+        solver.checkEntailed(pycvc5.Term(solver))
+    solver.checkEntailed(solver.mkTrue())
+    solver.checkEntailed(z)
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.checkEntailed(solver.mkTrue())
+
+
+def test_check_entailed2(solver):
+    solver.setOption("incremental", "true")
+
+    uSort = solver.mkUninterpretedSort("u")
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    uToIntSort = solver.mkFunctionSort(uSort, intSort)
+    intPredSort = solver.mkFunctionSort(intSort, boolSort)
+
+    n = pycvc5.Term(solver)
+    # Constants
+    x = solver.mkConst(uSort, "x")
+    y = solver.mkConst(uSort, "y")
+    # Functions
+    f = solver.mkConst(uToIntSort, "f")
+    p = solver.mkConst(intPredSort, "p")
+    # Values
+    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)
+    # 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
+                       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.mkFalse(), solver.mkTerm(kinds.Distinct, x, y)])
+    with pytest.raises(RuntimeError):
+        solver.checkEntailed(n)
+    with pytest.raises(RuntimeError):
+        solver.checkEntailed([n, solver.mkTerm(kinds.Distinct, x, y)])
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.checkEntailed(solver.mkTrue())
+
+
+def test_check_sat(solver):
+    solver.setOption("incremental", "false")
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.checkSat()