Fix some issues with the Python API tests (#8746)

This PR addresses a few issues in the Python API:
    the implementation of defineFunsRec() lacked the call to the C++ function
    a bunch of tests for defineFunsRec() were missing
    the test for getInstantiations() was incorrectly named and thus not valled.
    add missing test for hashing of Sort

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index b46b5f98f76b3728dc2d5c2da0cf1a08e7b409ee..4710c562687b203a898e7e030c7a884dac294b5d 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2069,7 +2069,7 @@ cdef class Solver:
         for bv in bound_vars:
             v.push_back((<Term?> bv).cterm)
 
-        if t is not None:
+        if isinstance(sym_or_fun, str):
             term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
                                                 <const vector[c_Term] &> v,
                                                 (<Sort?> sort_or_term).csort,
@@ -2083,7 +2083,7 @@ cdef class Solver:
 
         return term
 
-    def defineFunsRec(self, funs, bound_vars, terms):
+    def defineFunsRec(self, funs, bound_vars, terms, glb = False):
         """
             Define recursive functions.
 
@@ -2098,9 +2098,8 @@ cdef class Solver:
             :param funs: The sorted functions.
             :param bound_vars: The list of parameters to the functions.
             :param terms: The list of function bodies of the functions.
-            :param global: Determines whether this definition is global (i.e.
-                           persists when popping the context).
-            :return: The function.
+            :param glb: Determines whether this definition is global (i.e.
+                        persists when popping the context).
         """
         cdef vector[c_Term] vf
         cdef vector[vector[c_Term]] vbv
@@ -2117,7 +2116,9 @@ cdef class Solver:
             temp.clear()
 
         for t in terms:
-            vf.push_back((<Term?> t).cterm)
+            vt.push_back((<Term?> t).cterm)
+
+        self.csolver.defineFunsRec(vf, vbv, vt, glb)
 
     def getProof(self):
         """

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 6705a940f8dcbfd6f144379eb9abc0035cd4c2cf..cb7340495d775d1211a3ff153be004d3519aeef1 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -167,19 +167,19 @@ def test_mk_datatype_sorts(solver):
     dtdecl0 = solver.mkDatatypeDecl("dt0", [p0])
     dtdecl1 = solver.mkDatatypeDecl("dt1", [p1])
     ctordecl0 = solver.mkDatatypeConstructorDecl("c0")
-    ctordecl0.addSelector("s0", u1.instantiate({p0}))
+    ctordecl0.addSelector("s0", u1.instantiate([p0]))
     ctordecl1 = solver.mkDatatypeConstructorDecl("c1")
-    ctordecl1.addSelector("s1", u0.instantiate({p1}))
+    ctordecl1.addSelector("s1", u0.instantiate([p1]))
     dtdecl0.addConstructor(ctordecl0)
     dtdecl1.addConstructor(ctordecl1)
     dt_sorts = solver.mkDatatypeSorts([dtdecl0, dtdecl1])
-    isort1 = dt_sorts[1].instantiate({solver.getBooleanSort()})
+    isort1 = dt_sorts[1].instantiate([solver.getBooleanSort()])
     t1 = solver.mkConst(isort1, "t")
     t0 = solver.mkTerm(
         Kind.APPLY_SELECTOR,
         t1.getSort().getDatatype().getSelector("s1").getTerm(),
         t1)
-    assert dt_sorts[0].instantiate({solver.getBooleanSort()}) == t0.getSort()
+    assert dt_sorts[0].instantiate([solver.getBooleanSort()]) == t0.getSort()
 
 def test_mk_function_sort(solver):
     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
@@ -1041,6 +1041,29 @@ def test_define_fun(solver):
         slv.defineFun("ff", [b12, b22], bvSort2, v1)
 
 
+def test_define_fun_global(solver):
+    bSort = solver.getBooleanSort()
+
+    bTrue = solver.mkBoolean(True)
+    # (define-fun f () Bool true)
+    f = solver.defineFun("f", [], bSort, bTrue, True)
+    b = solver.mkVar(bSort, "b")
+    # (define-fun g (b Bool) Bool b)
+    g = solver.defineFun("g", [b], bSort, b, True)
+
+    # (assert (or (not f) (not (g true))))
+    solver.assertFormula(
+        solver.mkTerm(Kind.OR, f.notTerm(),
+                      solver.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
+    assert solver.checkSat().isUnsat()
+    solver.resetAssertions()
+    # (assert (or (not f) (not (g true))))
+    solver.assertFormula(
+        solver.mkTerm(Kind.OR, f.notTerm(),
+                      solver.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
+    assert solver.checkSat().isUnsat()
+
+
 def test_define_fun_rec(solver):
     bvSort = solver.mkBitVectorSort(32)
     funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort)
@@ -1112,6 +1135,126 @@ def test_define_fun_rec_wrong_logic(solver):
         solver.defineFunRec(f, [b, b], v)
 
 
+def test_define_fun_rec_global(solver):
+  bSort = solver.getBooleanSort()
+  fSort = solver.mkFunctionSort([bSort], bSort)
+
+  solver.push()
+  bTrue = solver.mkBoolean(True)
+  # (define-fun f () Bool true)
+  f = solver.defineFunRec("f", [], bSort, bTrue, True)
+  b = solver.mkVar(bSort, "b")
+  gSym = solver.mkConst(fSort, "g")
+  # (define-fun g (b Bool) Bool b)
+  g = solver.defineFunRec(gSym, [b], b, glbl=True)
+
+  # (assert (or (not f) (not (g true))))
+  solver.assertFormula(solver.mkTerm(
+      Kind.OR, f.notTerm(), solver.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
+  assert solver.checkSat().isUnsat()
+  solver.pop()
+  # (assert (or (not f) (not (g true))))
+  solver.assertFormula(solver.mkTerm(
+      Kind.OR, f.notTerm(), solver.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
+  assert solver.checkSat().isUnsat()
+
+
+def test_define_funs_rec(solver):
+  uSort = solver.mkUninterpretedSort("u")
+  bvSort = solver.mkBitVectorSort(32)
+  funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort)
+  funSort2 = solver.mkFunctionSort([uSort], solver.getIntegerSort())
+  b1 = solver.mkVar(bvSort, "b1")
+  b11 = solver.mkVar(bvSort, "b1")
+  b2 = solver.mkVar(solver.getIntegerSort(), "b2")
+  b3 = solver.mkVar(funSort2, "b3")
+  b4 = solver.mkVar(uSort, "b4")
+  v1 = solver.mkConst(bvSort, "v1")
+  v2 = solver.mkConst(solver.getIntegerSort(), "v2")
+  v3 = solver.mkConst(funSort2, "v3")
+  v4 = solver.mkConst(uSort, "v4")
+  f1 = solver.mkConst(funSort1, "f1")
+  f2 = solver.mkConst(funSort2, "f2")
+  f3 = solver.mkConst(bvSort, "f3")
+  solver.defineFunsRec([f1, f2], [[b1, b11], [b4]], [v1, v2])
+  with pytest.raises(RuntimeError):
+    solver.defineFunsRec([f1, f2], [[v1, b11], [b4]], [v1, v2])
+  with pytest.raises(RuntimeError):
+    solver.defineFunsRec([f1, f3], [[b1, b11], [b4]], [v1, v2])
+  with pytest.raises(RuntimeError):
+    solver.defineFunsRec([f1, f2], [[b1], [b4]], [v1, v2])
+  with pytest.raises(RuntimeError):
+    solver.defineFunsRec([f1, f2], [[b1, b2], [b4]], [v1, v2])
+  with pytest.raises(RuntimeError):
+    solver.defineFunsRec([f1, f2], [[b1, b11], [b4]], [v1, v4])
+
+  slv = cvc5.Solver()
+  uSort2 = slv.mkUninterpretedSort("u")
+  bvSort2 = slv.mkBitVectorSort(32)
+  funSort12 = slv.mkFunctionSort([bvSort2, bvSort2], bvSort2)
+  funSort22 = slv.mkFunctionSort([uSort2], slv.getIntegerSort())
+  b12 = slv.mkVar(bvSort2, "b1")
+  b112 = slv.mkVar(bvSort2, "b1")
+  b42 = slv.mkVar(uSort2, "b4")
+  v12 = slv.mkConst(bvSort2, "v1")
+  v22 = slv.mkConst(slv.getIntegerSort(), "v2")
+  f12 = slv.mkConst(funSort12, "f1")
+  f22 = slv.mkConst(funSort22, "f2")
+  
+  slv.defineFunsRec([f12, f22], [[b12, b112], [b42]], [v12, v22])
+  
+  with pytest.raises(RuntimeError):
+    slv.defineFunsRec([f1, f22], [[b12, b112], [b42]], [v12, v22])
+  with pytest.raises(RuntimeError):
+    slv.defineFunsRec([f12, f2], [[b12, b112], [b42]], [v12, v22])
+  with pytest.raises(RuntimeError):
+    slv.defineFunsRec([f12, f22], [[b1, b112], [b42]], [v12, v22])
+  with pytest.raises(RuntimeError):
+    slv.defineFunsRec([f12, f22], [[b12, b11], [b42]], [v12, v22])
+  with pytest.raises(RuntimeError):
+    slv.defineFunsRec([f12, f22], [[b12, b112], [b4]], [v12, v22])
+  with pytest.raises(RuntimeError):
+    slv.defineFunsRec([f12, f22], [[b12, b112], [b42]], [v1, v22])
+  with pytest.raises(RuntimeError):
+    slv.defineFunsRec([f12, f22], [[b12, b112], [b42]], [v12, v2])
+
+
+def test_define_funs_rec_wrong_logic(solver):
+  solver.setLogic("QF_BV")
+  uSort = solver.mkUninterpretedSort("u")
+  bvSort = solver.mkBitVectorSort(32)
+  funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort)
+  funSort2 = solver.mkFunctionSort([uSort], solver.getIntegerSort())
+  b = solver.mkVar(bvSort, "b")
+  u = solver.mkVar(uSort, "u")
+  v1 = solver.mkConst(bvSort, "v1")
+  v2 = solver.mkConst(solver.getIntegerSort(), "v2")
+  f1 = solver.mkConst(funSort1, "f1")
+  f2 = solver.mkConst(funSort2, "f2")
+  with pytest.raises(RuntimeError):
+    solver.defineFunsRec([f1, f2], [[b, b], [u]], [v1, v2])
+
+
+def test_define_funs_rec_global(solver):
+  bSort = solver.getBooleanSort()
+  fSort = solver.mkFunctionSort([bSort], bSort)
+
+  solver.push()
+  bTrue = solver.mkBoolean(True)
+  b = solver.mkVar(bSort, "b")
+  gSym = solver.mkConst(fSort, "g")
+  # (define-funs-rec ((g ((b Bool)) Bool)) (b))
+  solver.defineFunsRec([gSym], [[b]], [b], True)
+
+  # (assert (not (g true)))
+  solver.assertFormula(solver.mkTerm(Kind.APPLY_UF, gSym, bTrue).notTerm())
+  assert solver.checkSat().isUnsat()
+  solver.pop()
+  # (assert (not (g true)))
+  solver.assertFormula(solver.mkTerm(Kind.APPLY_UF, gSym, bTrue).notTerm())
+  assert solver.checkSat().isUnsat()
+
+
 def test_uf_iteration(solver):
     intSort = solver.getIntegerSort()
     funSort = solver.mkFunctionSort([intSort, intSort], intSort)
@@ -1641,17 +1784,17 @@ def test_block_model_values5(solver):
     solver.checkSat()
     solver.blockModelValues([x])
 
-def getInstantiations():
+def test_get_instantiations(solver):
     iSort = solver.getIntegerSort()
     boolSort = solver.getBooleanSort()
     p = solver.declareFun("p", [iSort], boolSort)
     x = solver.mkVar(iSort, "x")
-    bvl = solver.mkTerm(Kind.VARIABLE_LIST, [x])
-    app = solver.mkTerm(Kind.APPLY_UF, [p, x])
-    q = solver.mkTerm(Kind.FORALL, [bvl, app]);
+    bvl = solver.mkTerm(Kind.VARIABLE_LIST, x)
+    app = solver.mkTerm(Kind.APPLY_UF, p, x)
+    q = solver.mkTerm(Kind.FORALL, bvl, app)
     solver.assertFormula(q)
     five = solver.mkInteger(5)
-    app2 = solver.mkTerm(Kind.NOT, [solver.mkTerm(Kind.APPLY_UF, [p, five])])
+    app2 = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.APPLY_UF, p, five))
     solver.assertFormula(app2)
     with pytest.raises(RuntimeError):
         solver.getInstantiations()
@@ -2241,28 +2384,6 @@ def test_declare_pool(solver):
     with pytest.raises(RuntimeError):
         solver.declarePool("i", nullSort, [])
 
-def test_define_fun_global(solver):
-    bSort = solver.getBooleanSort()
-
-    bTrue = solver.mkBoolean(True)
-    # (define-fun f () Bool true)
-    f = solver.defineFun("f", [], bSort, bTrue, True)
-    b = solver.mkVar(bSort, "b")
-    # (define-fun g (b Bool) Bool b)
-    g = solver.defineFun("g", [b], bSort, b, True)
-
-    # (assert (or (not f) (not (g true))))
-    solver.assertFormula(
-        solver.mkTerm(Kind.OR, f.notTerm(),
-                      solver.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
-    assert solver.checkSat().isUnsat()
-    solver.resetAssertions()
-    # (assert (or (not f) (not (g true))))
-    solver.assertFormula(
-        solver.mkTerm(Kind.OR, f.notTerm(),
-                      solver.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
-    assert solver.checkSat().isUnsat()
-
 
 def test_define_sort(solver):
     sortVar0 = solver.mkParamSort("T0")

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index 75384aac41b0ca013d2fc929eb7f21778a017748..41c49227fda3cffad55cbb69632c692a3cc9a9cd 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -51,6 +51,10 @@ def create_param_datatype_sort(solver):
     return paramDtypeSort
 
 
+def test_hash(solver):
+    hash(solver.getIntegerSort())
+
+
 def test_operators_comparison(solver):
     solver.getIntegerSort() == Sort(solver)
     solver.getIntegerSort() != Sort(solver)