diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-05-12 22:32:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-13 05:32:55 +0000 |
commit | 304064c6bb3bf7ea7a7d54b66e2ad152e8fc4525 (patch) | |
tree | cb33046f6006c7da77ed1b39909ab3148e414bbd /test | |
parent | b837f24d835ce529c749a089ae0e29e471512512 (diff) |
Adding functions to the python API and testing them -- part 2 (#6517)
This PR adds some functions that are missing in the python API, along with unit tests for them.
The unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/term_black.cpp
Diffstat (limited to 'test')
-rw-r--r-- | test/python/unit/api/test_term.py | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py index 91424c905..702634807 100644 --- a/test/python/unit/api/test_term.py +++ b/test/python/unit/api/test_term.py @@ -897,6 +897,83 @@ def test_substitute(solver): 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_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.isInteger() + assert int2.isInteger() + assert int3.isInteger() + assert int4.isInteger() + assert int5.isInteger() + assert int6.isInteger() + assert int7.isInteger() + assert int8.isInteger() + assert int9.isInteger() + assert int10.isInteger() + assert int11.isInteger() + + def test_const_array(solver): intsort = solver.getIntegerSort() arrsort = solver.mkArraySort(intsort, intsort) |