diff options
Diffstat (limited to 'test/unit/api/python/test_term.py')
-rw-r--r-- | test/unit/api/python/test_term.py | 1267 |
1 files changed, 1267 insertions, 0 deletions
diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py new file mode 100644 index 000000000..34a79d597 --- /dev/null +++ b/test/unit/api/python/test_term.py @@ -0,0 +1,1267 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Makai Mann, Andres Noetzli +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Sort, Term +from fractions import Fraction + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_eq(solver): + uSort = solver.mkUninterpretedSort("u") + x = solver.mkVar(uSort, "x") + y = solver.mkVar(uSort, "y") + z = Term(solver) + + assert x == x + assert not x != x + assert not x == y + assert x != y + assert not (x == z) + assert x != z + + +def test_get_id(solver): + n = Term(solver) + with pytest.raises(RuntimeError): + n.getId() + x = solver.mkVar(solver.getIntegerSort(), "x") + x.getId() + y = x + assert x.getId() == y.getId() + + z = solver.mkVar(solver.getIntegerSort(), "z") + assert x.getId() != z.getId() + + +def test_get_kind(solver): + uSort = solver.mkUninterpretedSort("u") + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(uSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + n = Term(solver) + with pytest.raises(RuntimeError): + n.getKind() + x = solver.mkVar(uSort, "x") + x.getKind() + y = solver.mkVar(uSort, "y") + y.getKind() + + f = solver.mkVar(funSort1, "f") + f.getKind() + p = solver.mkVar(funSort2, "p") + p.getKind() + + zero = solver.mkInteger(0) + zero.getKind() + + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x.getKind() + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y.getKind() + sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum.getKind() + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.getKind() + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y.getKind() + + # Sequence kinds do not exist internally, test that the API properly + # converts them back. + seqSort = solver.mkSequenceSort(intSort) + s = solver.mkConst(seqSort, "s") + ss = solver.mkTerm(kinds.SeqConcat, s, s) + assert ss.getKind() == kinds.SeqConcat + + +def test_get_sort(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + n = Term(solver) + with pytest.raises(RuntimeError): + n.getSort() + x = solver.mkVar(bvSort, "x") + x.getSort() + assert x.getSort() == bvSort + y = solver.mkVar(bvSort, "y") + y.getSort() + assert y.getSort() == bvSort + + f = solver.mkVar(funSort1, "f") + f.getSort() + assert f.getSort() == funSort1 + p = solver.mkVar(funSort2, "p") + p.getSort() + assert p.getSort() == funSort2 + + zero = solver.mkInteger(0) + zero.getSort() + assert zero.getSort() == intSort + + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x.getSort() + assert f_x.getSort() == intSort + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y.getSort() + assert f_y.getSort() == intSort + sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum.getSort() + assert sum.getSort() == intSort + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.getSort() + assert p_0.getSort() == boolSort + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y.getSort() + assert p_f_y.getSort() == boolSort + + +def test_get_op(solver): + intsort = solver.getIntegerSort() + bvsort = solver.mkBitVectorSort(8) + arrsort = solver.mkArraySort(bvsort, intsort) + funsort = solver.mkFunctionSort(intsort, bvsort) + + x = solver.mkConst(intsort, "x") + a = solver.mkConst(arrsort, "a") + b = solver.mkConst(bvsort, "b") + + assert not x.hasOp() + with pytest.raises(RuntimeError): + x.getOp() + + ab = solver.mkTerm(kinds.Select, a, b) + ext = solver.mkOp(kinds.BVExtract, 4, 0) + extb = solver.mkTerm(ext, b) + + assert ab.hasOp() + assert not ab.getOp().isIndexed() + # can compare directly to a Kind (will invoke constructor) + assert extb.hasOp() + assert extb.getOp().isIndexed() + assert extb.getOp() == ext + + f = solver.mkConst(funsort, "f") + fx = solver.mkTerm(kinds.ApplyUf, f, x) + + assert not f.hasOp() + with pytest.raises(RuntimeError): + f.getOp() + assert fx.hasOp() + children = [c for c in fx] + # testing rebuild from op and children + assert fx == solver.mkTerm(fx.getOp(), children) + + # Test Datatypes Ops + sort = solver.mkParamSort("T") + listDecl = solver.mkDatatypeDecl("paramlist", sort) + cons = solver.mkDatatypeConstructorDecl("cons") + nil = solver.mkDatatypeConstructorDecl("nil") + cons.addSelector("head", sort) + cons.addSelectorSelf("tail") + listDecl.addConstructor(cons) + listDecl.addConstructor(nil) + listSort = solver.mkDatatypeSort(listDecl) + intListSort = listSort.instantiate([solver.getIntegerSort()]) + c = solver.mkConst(intListSort, "c") + list1 = listSort.getDatatype() + # list datatype constructor and selector operator terms + consOpTerm = list1.getConstructorTerm("cons") + nilOpTerm = list1.getConstructorTerm("nil") + headOpTerm = list1["cons"].getSelectorTerm("head") + tailOpTerm = list1["cons"].getSelectorTerm("tail") + + nilTerm = solver.mkTerm(kinds.ApplyConstructor, nilOpTerm) + consTerm = solver.mkTerm(kinds.ApplyConstructor, consOpTerm, + solver.mkInteger(0), nilTerm) + headTerm = solver.mkTerm(kinds.ApplySelector, headOpTerm, consTerm) + tailTerm = solver.mkTerm(kinds.ApplySelector, tailOpTerm, consTerm) + + assert nilTerm.hasOp() + assert consTerm.hasOp() + assert headTerm.hasOp() + assert tailTerm.hasOp() + + # Test rebuilding + children = [c for c in headTerm] + assert headTerm == solver.mkTerm(headTerm.getOp(), children) + + +def test_is_null(solver): + x = Term(solver) + assert x.isNull() + x = solver.mkVar(solver.mkBitVectorSort(4), "x") + assert not x.isNull() + + +def test_not_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + with pytest.raises(RuntimeError): + Term(solver).notTerm() + b = solver.mkTrue() + b.notTerm() + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.notTerm() + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.notTerm() + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.notTerm() + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.notTerm() + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.notTerm() + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.notTerm() + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.notTerm() + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.notTerm() + + +def test_and_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).andTerm(b) + with pytest.raises(RuntimeError): + b.andTerm(Term(solver)) + b.andTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.andTerm(b) + with pytest.raises(RuntimeError): + x.andTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.andTerm(b) + with pytest.raises(RuntimeError): + f.andTerm(x) + with pytest.raises(RuntimeError): + f.andTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.andTerm(b) + with pytest.raises(RuntimeError): + p.andTerm(x) + with pytest.raises(RuntimeError): + p.andTerm(f) + with pytest.raises(RuntimeError): + p.andTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.andTerm(b) + with pytest.raises(RuntimeError): + zero.andTerm(x) + with pytest.raises(RuntimeError): + zero.andTerm(f) + with pytest.raises(RuntimeError): + zero.andTerm(p) + with pytest.raises(RuntimeError): + zero.andTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.andTerm(b) + with pytest.raises(RuntimeError): + f_x.andTerm(x) + with pytest.raises(RuntimeError): + f_x.andTerm(f) + with pytest.raises(RuntimeError): + f_x.andTerm(p) + with pytest.raises(RuntimeError): + f_x.andTerm(zero) + with pytest.raises(RuntimeError): + f_x.andTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.andTerm(b) + with pytest.raises(RuntimeError): + sum.andTerm(x) + with pytest.raises(RuntimeError): + sum.andTerm(f) + with pytest.raises(RuntimeError): + sum.andTerm(p) + with pytest.raises(RuntimeError): + sum.andTerm(zero) + with pytest.raises(RuntimeError): + sum.andTerm(f_x) + with pytest.raises(RuntimeError): + sum.andTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.andTerm(b) + with pytest.raises(RuntimeError): + p_0.andTerm(x) + with pytest.raises(RuntimeError): + p_0.andTerm(f) + with pytest.raises(RuntimeError): + p_0.andTerm(p) + with pytest.raises(RuntimeError): + p_0.andTerm(zero) + with pytest.raises(RuntimeError): + p_0.andTerm(f_x) + with pytest.raises(RuntimeError): + p_0.andTerm(sum) + p_0.andTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.andTerm(b) + with pytest.raises(RuntimeError): + p_f_x.andTerm(x) + with pytest.raises(RuntimeError): + p_f_x.andTerm(f) + with pytest.raises(RuntimeError): + p_f_x.andTerm(p) + with pytest.raises(RuntimeError): + p_f_x.andTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.andTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.andTerm(sum) + p_f_x.andTerm(p_0) + p_f_x.andTerm(p_f_x) + + +def test_or_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).orTerm(b) + with pytest.raises(RuntimeError): + b.orTerm(Term(solver)) + b.orTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.orTerm(b) + with pytest.raises(RuntimeError): + x.orTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.orTerm(b) + with pytest.raises(RuntimeError): + f.orTerm(x) + with pytest.raises(RuntimeError): + f.orTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.orTerm(b) + with pytest.raises(RuntimeError): + p.orTerm(x) + with pytest.raises(RuntimeError): + p.orTerm(f) + with pytest.raises(RuntimeError): + p.orTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.orTerm(b) + with pytest.raises(RuntimeError): + zero.orTerm(x) + with pytest.raises(RuntimeError): + zero.orTerm(f) + with pytest.raises(RuntimeError): + zero.orTerm(p) + with pytest.raises(RuntimeError): + zero.orTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.orTerm(b) + with pytest.raises(RuntimeError): + f_x.orTerm(x) + with pytest.raises(RuntimeError): + f_x.orTerm(f) + with pytest.raises(RuntimeError): + f_x.orTerm(p) + with pytest.raises(RuntimeError): + f_x.orTerm(zero) + with pytest.raises(RuntimeError): + f_x.orTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.orTerm(b) + with pytest.raises(RuntimeError): + sum.orTerm(x) + with pytest.raises(RuntimeError): + sum.orTerm(f) + with pytest.raises(RuntimeError): + sum.orTerm(p) + with pytest.raises(RuntimeError): + sum.orTerm(zero) + with pytest.raises(RuntimeError): + sum.orTerm(f_x) + with pytest.raises(RuntimeError): + sum.orTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.orTerm(b) + with pytest.raises(RuntimeError): + p_0.orTerm(x) + with pytest.raises(RuntimeError): + p_0.orTerm(f) + with pytest.raises(RuntimeError): + p_0.orTerm(p) + with pytest.raises(RuntimeError): + p_0.orTerm(zero) + with pytest.raises(RuntimeError): + p_0.orTerm(f_x) + with pytest.raises(RuntimeError): + p_0.orTerm(sum) + p_0.orTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.orTerm(b) + with pytest.raises(RuntimeError): + p_f_x.orTerm(x) + with pytest.raises(RuntimeError): + p_f_x.orTerm(f) + with pytest.raises(RuntimeError): + p_f_x.orTerm(p) + with pytest.raises(RuntimeError): + p_f_x.orTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.orTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.orTerm(sum) + p_f_x.orTerm(p_0) + p_f_x.orTerm(p_f_x) + + +def test_xor_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).xorTerm(b) + with pytest.raises(RuntimeError): + b.xorTerm(Term(solver)) + b.xorTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.xorTerm(b) + with pytest.raises(RuntimeError): + x.xorTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.xorTerm(b) + with pytest.raises(RuntimeError): + f.xorTerm(x) + with pytest.raises(RuntimeError): + f.xorTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.xorTerm(b) + with pytest.raises(RuntimeError): + p.xorTerm(x) + with pytest.raises(RuntimeError): + p.xorTerm(f) + with pytest.raises(RuntimeError): + p.xorTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.xorTerm(b) + with pytest.raises(RuntimeError): + zero.xorTerm(x) + with pytest.raises(RuntimeError): + zero.xorTerm(f) + with pytest.raises(RuntimeError): + zero.xorTerm(p) + with pytest.raises(RuntimeError): + zero.xorTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.xorTerm(b) + with pytest.raises(RuntimeError): + f_x.xorTerm(x) + with pytest.raises(RuntimeError): + f_x.xorTerm(f) + with pytest.raises(RuntimeError): + f_x.xorTerm(p) + with pytest.raises(RuntimeError): + f_x.xorTerm(zero) + with pytest.raises(RuntimeError): + f_x.xorTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.xorTerm(b) + with pytest.raises(RuntimeError): + sum.xorTerm(x) + with pytest.raises(RuntimeError): + sum.xorTerm(f) + with pytest.raises(RuntimeError): + sum.xorTerm(p) + with pytest.raises(RuntimeError): + sum.xorTerm(zero) + with pytest.raises(RuntimeError): + sum.xorTerm(f_x) + with pytest.raises(RuntimeError): + sum.xorTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.xorTerm(b) + with pytest.raises(RuntimeError): + p_0.xorTerm(x) + with pytest.raises(RuntimeError): + p_0.xorTerm(f) + with pytest.raises(RuntimeError): + p_0.xorTerm(p) + with pytest.raises(RuntimeError): + p_0.xorTerm(zero) + with pytest.raises(RuntimeError): + p_0.xorTerm(f_x) + with pytest.raises(RuntimeError): + p_0.xorTerm(sum) + p_0.xorTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.xorTerm(b) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(x) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(f) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(p) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(sum) + p_f_x.xorTerm(p_0) + p_f_x.xorTerm(p_f_x) + + +def test_eq_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).eqTerm(b) + with pytest.raises(RuntimeError): + b.eqTerm(Term(solver)) + b.eqTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.eqTerm(b) + x.eqTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.eqTerm(b) + with pytest.raises(RuntimeError): + f.eqTerm(x) + f.eqTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.eqTerm(b) + with pytest.raises(RuntimeError): + p.eqTerm(x) + with pytest.raises(RuntimeError): + p.eqTerm(f) + p.eqTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.eqTerm(b) + with pytest.raises(RuntimeError): + zero.eqTerm(x) + with pytest.raises(RuntimeError): + zero.eqTerm(f) + with pytest.raises(RuntimeError): + zero.eqTerm(p) + zero.eqTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.eqTerm(b) + with pytest.raises(RuntimeError): + f_x.eqTerm(x) + with pytest.raises(RuntimeError): + f_x.eqTerm(f) + with pytest.raises(RuntimeError): + f_x.eqTerm(p) + f_x.eqTerm(zero) + f_x.eqTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.eqTerm(b) + with pytest.raises(RuntimeError): + sum.eqTerm(x) + with pytest.raises(RuntimeError): + sum.eqTerm(f) + with pytest.raises(RuntimeError): + sum.eqTerm(p) + sum.eqTerm(zero) + sum.eqTerm(f_x) + sum.eqTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.eqTerm(b) + with pytest.raises(RuntimeError): + p_0.eqTerm(x) + with pytest.raises(RuntimeError): + p_0.eqTerm(f) + with pytest.raises(RuntimeError): + p_0.eqTerm(p) + with pytest.raises(RuntimeError): + p_0.eqTerm(zero) + with pytest.raises(RuntimeError): + p_0.eqTerm(f_x) + with pytest.raises(RuntimeError): + p_0.eqTerm(sum) + p_0.eqTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.eqTerm(b) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(x) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(f) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(p) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(sum) + p_f_x.eqTerm(p_0) + p_f_x.eqTerm(p_f_x) + + +def test_imp_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).impTerm(b) + with pytest.raises(RuntimeError): + b.impTerm(Term(solver)) + b.impTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.impTerm(b) + with pytest.raises(RuntimeError): + x.impTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.impTerm(b) + with pytest.raises(RuntimeError): + f.impTerm(x) + with pytest.raises(RuntimeError): + f.impTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.impTerm(b) + with pytest.raises(RuntimeError): + p.impTerm(x) + with pytest.raises(RuntimeError): + p.impTerm(f) + with pytest.raises(RuntimeError): + p.impTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.impTerm(b) + with pytest.raises(RuntimeError): + zero.impTerm(x) + with pytest.raises(RuntimeError): + zero.impTerm(f) + with pytest.raises(RuntimeError): + zero.impTerm(p) + with pytest.raises(RuntimeError): + zero.impTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.impTerm(b) + with pytest.raises(RuntimeError): + f_x.impTerm(x) + with pytest.raises(RuntimeError): + f_x.impTerm(f) + with pytest.raises(RuntimeError): + f_x.impTerm(p) + with pytest.raises(RuntimeError): + f_x.impTerm(zero) + with pytest.raises(RuntimeError): + f_x.impTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.impTerm(b) + with pytest.raises(RuntimeError): + sum.impTerm(x) + with pytest.raises(RuntimeError): + sum.impTerm(f) + with pytest.raises(RuntimeError): + sum.impTerm(p) + with pytest.raises(RuntimeError): + sum.impTerm(zero) + with pytest.raises(RuntimeError): + sum.impTerm(f_x) + with pytest.raises(RuntimeError): + sum.impTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.impTerm(b) + with pytest.raises(RuntimeError): + p_0.impTerm(x) + with pytest.raises(RuntimeError): + p_0.impTerm(f) + with pytest.raises(RuntimeError): + p_0.impTerm(p) + with pytest.raises(RuntimeError): + p_0.impTerm(zero) + with pytest.raises(RuntimeError): + p_0.impTerm(f_x) + with pytest.raises(RuntimeError): + p_0.impTerm(sum) + p_0.impTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.impTerm(b) + with pytest.raises(RuntimeError): + p_f_x.impTerm(x) + with pytest.raises(RuntimeError): + p_f_x.impTerm(f) + with pytest.raises(RuntimeError): + p_f_x.impTerm(p) + with pytest.raises(RuntimeError): + p_f_x.impTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.impTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.impTerm(sum) + p_f_x.impTerm(p_0) + p_f_x.impTerm(p_f_x) + + +def test_ite_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).iteTerm(b, b) + with pytest.raises(RuntimeError): + b.iteTerm(Term(solver), b) + with pytest.raises(RuntimeError): + b.iteTerm(b, Term(solver)) + b.iteTerm(b, b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + b.iteTerm(x, x) + b.iteTerm(b, b) + with pytest.raises(RuntimeError): + b.iteTerm(x, b) + with pytest.raises(RuntimeError): + x.iteTerm(x, x) + with pytest.raises(RuntimeError): + x.iteTerm(x, b) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.iteTerm(b, b) + with pytest.raises(RuntimeError): + x.iteTerm(b, x) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.iteTerm(b, b) + with pytest.raises(RuntimeError): + p.iteTerm(x, b) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.iteTerm(x, x) + with pytest.raises(RuntimeError): + zero.iteTerm(x, b) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.iteTerm(b, b) + with pytest.raises(RuntimeError): + f_x.iteTerm(b, x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.iteTerm(x, x) + with pytest.raises(RuntimeError): + sum.iteTerm(b, x) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.iteTerm(b, b) + p_0.iteTerm(x, x) + with pytest.raises(RuntimeError): + p_0.iteTerm(x, b) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.iteTerm(b, b) + p_f_x.iteTerm(x, x) + with pytest.raises(RuntimeError): + p_f_x.iteTerm(x, b) + + +def test_term_assignment(solver): + t1 = solver.mkInteger(1) + t2 = t1 + t2 = solver.mkInteger(2) + assert t1 == solver.mkInteger(1) + + +def test_substitute(solver): + x = solver.mkConst(solver.getIntegerSort(), "x") + one = solver.mkInteger(1) + ttrue = solver.mkTrue() + xpx = solver.mkTerm(kinds.Plus, x, x) + onepone = solver.mkTerm(kinds.Plus, one, one) + + assert xpx.substitute(x, one) == onepone + assert onepone.substitute(one, x) == xpx + # incorrect due to type + with pytest.raises(RuntimeError): + xpx.substitute(one, ttrue) + + # simultaneous substitution + y = solver.mkConst(solver.getIntegerSort(), "y") + xpy = solver.mkTerm(kinds.Plus, x, y) + xpone = solver.mkTerm(kinds.Plus, y, one) + es = [] + rs = [] + es.append(x) + rs.append(y) + es.append(y) + rs.append(one) + assert xpy.substitute(es, rs) == xpone + + # incorrect substitution due to arity + rs.pop() + with pytest.raises(RuntimeError): + xpy.substitute(es, rs) + + # incorrect substitution due to types + rs.append(ttrue) + with pytest.raises(RuntimeError): + xpy.substitute(es, rs) + + # null cannot substitute + tnull = Term(solver) + with pytest.raises(RuntimeError): + tnull.substitute(one, x) + with pytest.raises(RuntimeError): + xpx.substitute(tnull, x) + with pytest.raises(RuntimeError): + xpx.substitute(x, tnull) + rs.pop() + rs.append(tnull) + with pytest.raises(RuntimeError): + xpy.substitute(es, rs) + es.clear() + rs.clear() + es.append(x) + rs.append(y) + with pytest.raises(RuntimeError): + tnull.substitute(es, rs) + es.append(tnull) + rs.append(one) + with pytest.raises(RuntimeError): + xpx.substitute(es, rs) + + +def test_term_compare(solver): + t1 = solver.mkInteger(1) + t2 = solver.mkTerm(kinds.Plus, solver.mkInteger(2), solver.mkInteger(2)) + t3 = solver.mkTerm(kinds.Plus, solver.mkInteger(2), solver.mkInteger(2)) + assert t2 >= t3 + assert t2 <= t3 + assert (t1 > t2) != (t1 < t2) + assert (t1 > t2 or t1 == t2) == (t1 >= t2) + + +def test_term_children(solver): + # simple term 2+3 + two = solver.mkInteger(2) + t1 = solver.mkTerm(kinds.Plus, two, solver.mkInteger(3)) + assert t1[0] == two + assert t1.getNumChildren() == 2 + tnull = Term(solver) + with pytest.raises(RuntimeError): + tnull.getNumChildren() + + # apply term f(2) + intSort = solver.getIntegerSort() + fsort = solver.mkFunctionSort(intSort, intSort) + f = solver.mkConst(fsort, "f") + t2 = solver.mkTerm(kinds.ApplyUf, f, two) + # due to our higher-order view of terms, we treat f as a child of kinds.ApplyUf + assert t2.getNumChildren() == 2 + assert t2[0] == f + assert t2[1] == two + with pytest.raises(RuntimeError): + tnull[0] + + +def test_get_const_array_base(solver): + intsort = solver.getIntegerSort() + arrsort = solver.mkArraySort(intsort, intsort) + one = solver.mkInteger(1) + constarr = solver.mkConstArray(arrsort, one) + + assert constarr.isConstArray() + assert one == constarr.getConstArrayBase() + + +def test_get_abstract_value(solver): + v1 = solver.mkAbstractValue(1) + v2 = solver.mkAbstractValue("15") + v3 = solver.mkAbstractValue("18446744073709551617") + + assert v1.isAbstractValue() + assert v2.isAbstractValue() + assert v3.isAbstractValue() + assert "1" == v1.getAbstractValue() + assert "15" == v2.getAbstractValue() + assert "18446744073709551617" == v3.getAbstractValue() + + +def test_get_tuple(solver): + s1 = solver.getIntegerSort() + s2 = solver.getRealSort() + s3 = solver.getStringSort() + + t1 = solver.mkInteger(15) + t2 = solver.mkReal(17, 25) + t3 = solver.mkString("abc") + + tup = solver.mkTuple([s1, s2, s3], [t1, t2, t3]) + + assert tup.isTupleValue() + assert [t1, t2, t3] == tup.getTupleValue() + + +def test_get_set(solver): + s = solver.mkSetSort(solver.getIntegerSort()) + + i1 = solver.mkInteger(5) + i2 = solver.mkInteger(7) + + s1 = solver.mkEmptySet(s) + s2 = solver.mkTerm(kinds.SetSingleton, i1) + s3 = solver.mkTerm(kinds.SetSingleton, i1) + s4 = solver.mkTerm(kinds.SetSingleton, i2) + s5 = solver.mkTerm( + kinds.SetUnion, s2, solver.mkTerm(kinds.SetUnion, s3, s4)) + + assert s1.isSetValue() + assert s2.isSetValue() + assert s3.isSetValue() + assert s4.isSetValue() + assert not s5.isSetValue() + s5 = solver.simplify(s5) + assert s5.isSetValue() + + assert set([]) == s1.getSetValue() + assert set([i1]) == s2.getSetValue() + assert set([i1]) == s3.getSetValue() + assert set([i2]) == s4.getSetValue() + assert set([i1, i2]) == s5.getSetValue() + + +def test_get_sequence(solver): + s = solver.mkSequenceSort(solver.getIntegerSort()) + + i1 = solver.mkInteger(5) + i2 = solver.mkInteger(7) + + s1 = solver.mkEmptySequence(s) + s2 = solver.mkTerm(kinds.SeqUnit, i1) + s3 = solver.mkTerm(kinds.SeqUnit, i1) + s4 = solver.mkTerm(kinds.SeqUnit, i2) + s5 = solver.mkTerm(kinds.SeqConcat, s2, + solver.mkTerm(kinds.SeqConcat, s3, s4)) + + assert s1.isSequenceValue() + assert not s2.isSequenceValue() + assert not s3.isSequenceValue() + assert not s4.isSequenceValue() + assert not s5.isSequenceValue() + + s2 = solver.simplify(s2) + s3 = solver.simplify(s3) + s4 = solver.simplify(s4) + s5 = solver.simplify(s5) + + assert [] == s1.getSequenceValue() + assert [i1] == s2.getSequenceValue() + assert [i1] == s3.getSequenceValue() + assert [i2] == s4.getSequenceValue() + assert [i1, i1, i2] == s5.getSequenceValue() + + +def test_get_uninterpreted_const(solver): + s = solver.mkUninterpretedSort("test") + t1 = solver.mkUninterpretedConst(s, 3) + t2 = solver.mkUninterpretedConst(s, 5) + + assert t1.isUninterpretedValue() + assert t2.isUninterpretedValue() + + assert (s, 3) == t1.getUninterpretedValue() + assert (s, 5) == t2.getUninterpretedValue() + + +def test_get_floating_point(solver): + bvval = solver.mkBitVector(16, "0000110000000011", 2) + fp = solver.mkFloatingPoint(5, 11, bvval) + + assert fp.isFloatingPointValue() + assert not fp.isFloatingPointPosZero() + assert not fp.isFloatingPointNegZero() + assert not fp.isFloatingPointPosInf() + assert not fp.isFloatingPointNegInf() + assert not fp.isFloatingPointNaN() + assert (5, 11, bvval) == fp.getFloatingPointValue() + + assert solver.mkPosZero(5, 11).isFloatingPointPosZero() + assert solver.mkNegZero(5, 11).isFloatingPointNegZero() + assert solver.mkPosInf(5, 11).isFloatingPointPosInf() + assert solver.mkNegInf(5, 11).isFloatingPointNegInf() + assert solver.mkNaN(5, 11).isFloatingPointNaN() + + +def test_is_integer(solver): + int1 = solver.mkInteger("-18446744073709551616") + int2 = solver.mkInteger("-18446744073709551615") + int3 = solver.mkInteger("-4294967296") + int4 = solver.mkInteger("-4294967295") + int5 = solver.mkInteger("-10") + int6 = solver.mkInteger("0") + int7 = solver.mkInteger("10") + int8 = solver.mkInteger("4294967295") + int9 = solver.mkInteger("4294967296") + int10 = solver.mkInteger("18446744073709551615") + int11 = solver.mkInteger("18446744073709551616") + int12 = solver.mkInteger("-0") + + with pytest.raises(RuntimeError): + solver.mkInteger("") + with pytest.raises(RuntimeError): + solver.mkInteger("-") + with pytest.raises(RuntimeError): + solver.mkInteger("-1-") + with pytest.raises(RuntimeError): + solver.mkInteger("0.0") + with pytest.raises(RuntimeError): + solver.mkInteger("-0.1") + with pytest.raises(RuntimeError): + solver.mkInteger("012") + with pytest.raises(RuntimeError): + solver.mkInteger("0000") + with pytest.raises(RuntimeError): + solver.mkInteger("-01") + with pytest.raises(RuntimeError): + solver.mkInteger("-00") + + assert int1.isIntegerValue() + assert int2.isIntegerValue() + assert int3.isIntegerValue() + assert int4.isIntegerValue() + assert int5.isIntegerValue() + assert int6.isIntegerValue() + assert int7.isIntegerValue() + assert int8.isIntegerValue() + assert int9.isIntegerValue() + assert int10.isIntegerValue() + assert int11.isIntegerValue() + + assert int1.getIntegerValue() == -18446744073709551616 + assert int2.getIntegerValue() == -18446744073709551615 + assert int3.getIntegerValue() == -4294967296 + assert int4.getIntegerValue() == -4294967295 + assert int5.getIntegerValue() == -10 + assert int6.getIntegerValue() == 0 + assert int7.getIntegerValue() == 10 + assert int8.getIntegerValue() == 4294967295 + assert int9.getIntegerValue() == 4294967296 + assert int10.getIntegerValue() == 18446744073709551615 + assert int11.getIntegerValue() == 18446744073709551616 + + +def test_get_string(solver): + s1 = solver.mkString("abcde") + assert s1.isStringValue() + assert s1.getStringValue() == str("abcde") + + +def test_get_real(solver): + real1 = solver.mkReal("0") + real2 = solver.mkReal(".0") + real3 = solver.mkReal("-17") + real4 = solver.mkReal("-3/5") + real5 = solver.mkReal("12.7") + real6 = solver.mkReal("1/4294967297") + real7 = solver.mkReal("4294967297") + real8 = solver.mkReal("1/18446744073709551617") + real9 = solver.mkReal("18446744073709551617") + + assert real1.isRealValue() + assert real2.isRealValue() + assert real3.isRealValue() + assert real4.isRealValue() + assert real5.isRealValue() + assert real6.isRealValue() + assert real7.isRealValue() + assert real8.isRealValue() + assert real9.isRealValue() + + assert 0 == real1.getRealValue() + assert 0 == real2.getRealValue() + assert -17 == real3.getRealValue() + assert Fraction(-3, 5) == real4.getRealValue() + assert Fraction(127, 10) == real5.getRealValue() + assert Fraction(1, 4294967297) == real6.getRealValue() + assert 4294967297 == real7.getRealValue() + assert Fraction(1, 18446744073709551617) == real8.getRealValue() + assert Fraction(18446744073709551617, 1) == real9.getRealValue() + + # Check denominator too large for float + num = 1 + den = 2 ** 64 + 1 + real_big = solver.mkReal(num, den) + assert real_big.isRealValue() + assert Fraction(num, den) == real_big.getRealValue() + + # Check that we're treating floats as decimal aproximations rather than + # IEEE-754-specified values. + real_decimal = solver.mkReal(0.3) + assert real_decimal.isRealValue() + assert Fraction("0.3") == real_decimal.getRealValue() + assert Fraction(0.3) == Fraction(5404319552844595, 18014398509481984) + assert Fraction(0.3) != real_decimal.getRealValue() + + +def test_get_boolean(solver): + b1 = solver.mkBoolean(True) + b2 = solver.mkBoolean(False) + + assert b1.isBooleanValue() + assert b2.isBooleanValue() + assert b1.getBooleanValue() + assert not b2.getBooleanValue() + + +def test_get_bit_vector(solver): + b1 = solver.mkBitVector(8, 15) + b2 = solver.mkBitVector(8, "00001111", 2) + b3 = solver.mkBitVector(8, "15", 10) + b4 = solver.mkBitVector(8, "0f", 16) + b5 = solver.mkBitVector(9, "00001111", 2); + b6 = solver.mkBitVector(9, "15", 10); + b7 = solver.mkBitVector(9, "0f", 16); + + assert b1.isBitVectorValue() + assert b2.isBitVectorValue() + assert b3.isBitVectorValue() + assert b4.isBitVectorValue() + assert b5.isBitVectorValue() + assert b6.isBitVectorValue() + assert b7.isBitVectorValue() + + assert "00001111" == b1.getBitVectorValue(2) + assert "15" == b1.getBitVectorValue(10) + assert "f" == b1.getBitVectorValue(16) + assert "00001111" == b2.getBitVectorValue(2) + assert "15" == b2.getBitVectorValue(10) + assert "f" == b2.getBitVectorValue(16) + assert "00001111" == b3.getBitVectorValue(2) + assert "15" == b3.getBitVectorValue(10) + assert "f" == b3.getBitVectorValue(16) + assert "00001111" == b4.getBitVectorValue(2) + assert "15" == b4.getBitVectorValue(10) + assert "f" == b4.getBitVectorValue(16) + assert "000001111" == b5.getBitVectorValue(2) + assert "15" == b5.getBitVectorValue(10) + assert "f" == b5.getBitVectorValue(16) + assert "000001111" == b6.getBitVectorValue(2) + assert "15" == b6.getBitVectorValue(10) + assert "f" == b6.getBitVectorValue(16) + assert "000001111" == b7.getBitVectorValue(2) + assert "15" == b7.getBitVectorValue(10) + assert "f" == b7.getBitVectorValue(16) + + +def test_const_array(solver): + intsort = solver.getIntegerSort() + arrsort = solver.mkArraySort(intsort, intsort) + a = solver.mkConst(arrsort, "a") + one = solver.mkInteger(1) + constarr = solver.mkConstArray(arrsort, one) + + assert constarr.getKind() == kinds.ConstArray + assert constarr.getConstArrayBase() == one + with pytest.raises(RuntimeError): + a.getConstArrayBase() + + arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) + zero_array = solver.mkConstArray(arrsort, solver.mkReal(0)) + stores = solver.mkTerm(kinds.Store, zero_array, solver.mkReal(1), + solver.mkReal(2)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), + solver.mkReal(3)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), + solver.mkReal(5)) + + +def test_const_sequence_elements(solver): + realsort = solver.getRealSort() + seqsort = solver.mkSequenceSort(realsort) + s = solver.mkEmptySequence(seqsort) + + assert s.getKind() == kinds.ConstSequence + # empty sequence has zero elements + cs = s.getSequenceValue() + assert len(cs) == 0 + + # A seq.unit app is not a constant sequence (regardless of whether it is + # applied to a constant). + su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1)) + with pytest.raises(RuntimeError): + su.getSequenceValue() + + +def test_term_scoped_to_string(solver): + intsort = solver.getIntegerSort() + x = solver.mkConst(intsort, "x") + assert str(x) == "x" + solver2 = pycvc5.Solver() + assert str(x) == "x" |