From: Gereon Kremer Date: Tue, 10 May 2022 17:47:52 +0000 (-0700) Subject: Fix some issues with the Python API tests (#8746) X-Git-Tag: cvc5-1.0.1~149 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fe939c31bd286675298990d7d1865d275d982679;p=cvc5.git 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 b46b5f98f..4710c5626 100644 --- 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(( bv).cterm) - if t is not None: + if isinstance(sym_or_fun, str): term.cterm = self.csolver.defineFunRec(( sym_or_fun).encode(), v, ( 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(( t).cterm) + vt.push_back(( 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 6705a940f..cb7340495 100644 --- 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 75384aac4..41c49227f 100644 --- 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)