import cvc5
import sys
-from cvc5 import Kind
+from cvc5 import Kind, BlockModelsMode, RoundingMode
@pytest.fixture
def test_supports_floating_point(solver):
- solver.mkRoundingMode(cvc5.RoundNearestTiesToEven)
+ solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)
def test_get_boolean_sort(solver):
dtypeSpec2.addConstructor(nil2)
decls = [dtypeSpec1, dtypeSpec2]
- solver.mkDatatypeSorts(decls, set([]))
+ solver.mkDatatypeSorts(decls)
with pytest.raises(RuntimeError):
- slv.mkDatatypeSorts(decls, set([]))
+ slv.mkDatatypeSorts(decls)
throwsDtypeSpec = solver.mkDatatypeDecl("list")
throwsDecls = [throwsDtypeSpec]
with pytest.raises(RuntimeError):
- solver.mkDatatypeSorts(throwsDecls, set([]))
+ solver.mkDatatypeSorts(throwsDecls)
# with unresolved sorts
- unresList = solver.mkUnresolvedSort("ulist")
- unresSorts = set([unresList])
+ unresList = solver.mkUnresolvedDatatypeSort("ulist")
ulist = solver.mkDatatypeDecl("ulist")
ucons = solver.mkDatatypeConstructorDecl("ucons")
ucons.addSelector("car", unresList)
ulist.addConstructor(unil)
udecls = [ulist]
- solver.mkDatatypeSorts(udecls, unresSorts)
+ solver.mkDatatypeSorts(udecls)
with pytest.raises(RuntimeError):
- slv.mkDatatypeSorts(udecls, unresSorts)
+ slv.mkDatatypeSorts(udecls)
# mutually recursive with unresolved parameterized sorts
p0 = solver.mkParamSort("p0")
p1 = solver.mkParamSort("p1")
- u0 = solver.mkUnresolvedSort("dt0", 1)
- u1 = solver.mkUnresolvedSort("dt1", 1)
+ u0 = solver.mkUnresolvedDatatypeSort("dt0", 1)
+ u1 = solver.mkUnresolvedDatatypeSort("dt1", 1)
dtdecl0 = solver.mkDatatypeDecl("dt0", p0)
dtdecl1 = solver.mkDatatypeDecl("dt1", p1)
ctordecl0 = solver.mkDatatypeConstructorDecl("c0")
ctordecl1.addSelector("s1", u0.instantiate({p1}))
dtdecl0.addConstructor(ctordecl0)
dtdecl1.addConstructor(ctordecl1)
- dt_sorts = solver.mkDatatypeSorts([dtdecl0, dtdecl1], {u0, u1})
+ dt_sorts = solver.mkDatatypeSorts([dtdecl0, dtdecl1])
isort1 = dt_sorts[1].instantiate({solver.getBooleanSort()})
t1 = solver.mkConst(isort1, "t")
t0 = solver.mkTerm(
- Kind.ApplySelector,
- t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(),
+ Kind.APPLY_SELECTOR,
+ t1.getSort().getDatatype().getSelector("s1").getTerm(),
t1)
assert dt_sorts[0].instantiate({solver.getBooleanSort()}) == t0.getSort()
def test_mk_predicate_sort(solver):
- solver.mkPredicateSort([solver.getIntegerSort()])
+ solver.mkPredicateSort(solver.getIntegerSort())
with pytest.raises(RuntimeError):
- solver.mkPredicateSort([])
+ solver.mkPredicateSort()
funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
solver.getIntegerSort())
# functions as arguments are allowed
- solver.mkPredicateSort([solver.getIntegerSort(), funSort])
+ solver.mkPredicateSort(solver.getIntegerSort(), funSort)
slv = cvc5.Solver()
with pytest.raises(RuntimeError):
- slv.mkPredicateSort([solver.getIntegerSort()])
+ slv.mkPredicateSort(solver.getIntegerSort())
def test_mk_record_sort(solver):
fields = [("b", solver.getBooleanSort()),\
("bv", solver.mkBitVectorSort(8)),\
("i", solver.getIntegerSort())]
- empty = []
- solver.mkRecordSort(fields)
- solver.mkRecordSort(empty)
- recSort = solver.mkRecordSort(fields)
+ solver.mkRecordSort(*fields)
+ solver.mkRecordSort()
+ recSort = solver.mkRecordSort(*fields)
recSort.getDatatype()
def test_mk_unresolved_sort(solver):
- solver.mkUnresolvedSort("u")
- solver.mkUnresolvedSort("u", 1)
- solver.mkUnresolvedSort("")
- solver.mkUnresolvedSort("", 1)
+ solver.mkUnresolvedDatatypeSort("u")
+ solver.mkUnresolvedDatatypeSort("u", 1)
+ solver.mkUnresolvedDatatypeSort("")
+ solver.mkUnresolvedDatatypeSort("", 1)
def test_mk_sort_constructor_sort(solver):
- solver.mkSortConstructorSort("s", 2)
- solver.mkSortConstructorSort("", 2)
+ solver.mkUninterpretedSortConstructorSort(2, "s")
+ solver.mkUninterpretedSortConstructorSort(2)
with pytest.raises(RuntimeError):
- solver.mkSortConstructorSort("", 0)
+ solver.mkUninterpretedSortConstructorSort(0)
def test_mk_tuple_sort(solver):
- solver.mkTupleSort([solver.getIntegerSort()])
+ solver.mkTupleSort(solver.getIntegerSort())
funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
solver.getIntegerSort())
with pytest.raises(RuntimeError):
- solver.mkTupleSort([solver.getIntegerSort(), funSort])
+ solver.mkTupleSort(solver.getIntegerSort(), funSort)
slv = cvc5.Solver()
with pytest.raises(RuntimeError):
- slv.mkTupleSort([solver.getIntegerSort()])
+ slv.mkTupleSort(solver.getIntegerSort())
def test_mk_bit_vector(solver):
def test_mk_rounding_mode(solver):
- solver.mkRoundingMode(cvc5.RoundTowardZero)
+ assert str(solver.mkRoundingMode(
+ RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)) == "roundNearestTiesToEven"
+ assert str(solver.mkRoundingMode(
+ RoundingMode.ROUND_TOWARD_POSITIVE)) == "roundTowardPositive"
+ assert str(solver.mkRoundingMode(
+ RoundingMode.ROUND_TOWARD_NEGATIVE)) == "roundTowardNegative"
+ assert str(solver.mkRoundingMode(
+ RoundingMode.ROUND_TOWARD_ZERO)) == "roundTowardZero"
+ assert str(solver.mkRoundingMode(
+ RoundingMode.ROUND_NEAREST_TIES_TO_AWAY)) == "roundNearestTiesToAway"
def test_mk_floating_point(solver):
def test_mk_op(solver):
with pytest.raises(ValueError):
- solver.mkOp(Kind.BVExtract, Kind.Equal)
+ solver.mkOp(Kind.BITVECTOR_EXTRACT, Kind.EQUAL)
- solver.mkOp(Kind.Divisible, "2147483648")
+ solver.mkOp(Kind.DIVISIBLE, "2147483648")
with pytest.raises(RuntimeError):
- solver.mkOp(Kind.BVExtract, "asdf")
+ solver.mkOp(Kind.BITVECTOR_EXTRACT, "asdf")
- solver.mkOp(Kind.Divisible, 1)
- solver.mkOp(Kind.BVRotateLeft, 1)
- solver.mkOp(Kind.BVRotateRight, 1)
+ solver.mkOp(Kind.DIVISIBLE, 1)
+ solver.mkOp(Kind.BITVECTOR_ROTATE_LEFT, 1)
+ solver.mkOp(Kind.BITVECTOR_ROTATE_RIGHT, 1)
with pytest.raises(RuntimeError):
- solver.mkOp(Kind.BVExtract, 1)
+ solver.mkOp(Kind.BITVECTOR_EXTRACT, 1)
- solver.mkOp(Kind.BVExtract, 1, 1)
+ solver.mkOp(Kind.BITVECTOR_EXTRACT, 1, 1)
with pytest.raises(RuntimeError):
- solver.mkOp(Kind.Divisible, 1, 2)
+ solver.mkOp(Kind.DIVISIBLE, 1, 2)
args = [1, 2, 2]
- solver.mkOp(Kind.TupleProject, args)
+ solver.mkOp(Kind.TUPLE_PROJECT, *args)
def test_mk_pi(solver):
solver.mkReal(val3, val3)
solver.mkReal(val4, val4)
+ solver.mkReal("1", "2")
+ solver.mkReal("-1", "2")
+ solver.mkReal(-1, "2")
+ solver.mkReal("-1", 2)
+ with pytest.raises(TypeError):
+ solver.mkReal(1, 2, 3)
+ with pytest.raises(RuntimeError):
+ solver.mkReal("1.0", 2)
+ with pytest.raises(RuntimeError):
+ solver.mkReal(1, "asdf")
+
def test_mk_regexp_none(solver):
strSort = solver.getStringSort()
s = solver.mkConst(strSort, "s")
- solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpNone())
+ solver.mkTerm(Kind.STRING_IN_REGEXP, s, solver.mkRegexpNone())
def test_mk_regexp_all(solver):
strSort = solver.getStringSort()
s = solver.mkConst(strSort, "s")
- solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAll())
+ solver.mkTerm(Kind.STRING_IN_REGEXP, s, solver.mkRegexpAll())
def test_mk_regexp_allchar(solver):
strSort = solver.getStringSort()
s = solver.mkConst(strSort, "s")
- solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAllchar())
+ solver.mkTerm(Kind.STRING_IN_REGEXP, s, solver.mkRegexpAllchar())
def test_mk_sep_emp(solver):
bv32 = solver.mkBitVectorSort(32)
a = solver.mkConst(bv32, "a")
b = solver.mkConst(bv32, "b")
- v1 = [a, b]
- v2 = [a, cvc5.Term(solver)]
- v3 = [a, solver.mkTrue()]
- v4 = [solver.mkInteger(1), solver.mkInteger(2)]
- v5 = [solver.mkInteger(1), cvc5.Term(solver)]
- v6 = []
slv = cvc5.Solver()
# mkTerm(Kind kind) const
solver.mkPi()
- solver.mkTerm(Kind.Pi)
- solver.mkTerm(Kind.Pi, v6)
- solver.mkTerm(solver.mkOp(Kind.Pi))
- solver.mkTerm(solver.mkOp(Kind.Pi), v6)
- solver.mkTerm(Kind.RegexpNone)
- solver.mkTerm(Kind.RegexpNone, v6)
- solver.mkTerm(solver.mkOp(Kind.RegexpNone))
- solver.mkTerm(solver.mkOp(Kind.RegexpNone), v6)
- solver.mkTerm(Kind.RegexpAllchar)
- solver.mkTerm(Kind.RegexpAllchar, v6)
- solver.mkTerm(solver.mkOp(Kind.RegexpAllchar))
- solver.mkTerm(solver.mkOp(Kind.RegexpAllchar), v6)
- solver.mkTerm(Kind.SepEmp)
- solver.mkTerm(Kind.SepEmp, v6)
- solver.mkTerm(solver.mkOp(Kind.SepEmp))
- solver.mkTerm(solver.mkOp(Kind.SepEmp), v6)
- with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.ConstBV)
+ solver.mkTerm(Kind.PI)
+ solver.mkTerm(solver.mkOp(Kind.PI))
+ solver.mkTerm(Kind.REGEXP_NONE)
+ solver.mkTerm(solver.mkOp(Kind.REGEXP_NONE))
+ solver.mkTerm(Kind.REGEXP_ALLCHAR)
+ solver.mkTerm(solver.mkOp(Kind.REGEXP_ALLCHAR))
+ solver.mkTerm(Kind.SEP_EMP)
+ solver.mkTerm(solver.mkOp(Kind.SEP_EMP))
+ with pytest.raises(RuntimeError):
+ solver.mkTerm(Kind.CONST_BITVECTOR)
# mkTerm(Kind kind, Term child) const
- solver.mkTerm(Kind.Not, solver.mkTrue())
+ solver.mkTerm(Kind.NOT, solver.mkTrue())
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Not, cvc5.Term(solver))
+ solver.mkTerm(Kind.NOT, cvc5.Term(solver))
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Not, a)
+ solver.mkTerm(Kind.NOT, a)
with pytest.raises(RuntimeError):
- slv.mkTerm(Kind.Not, solver.mkTrue())
+ slv.mkTerm(Kind.NOT, solver.mkTrue())
# mkTerm(Kind kind, Term child1, Term child2) const
- solver.mkTerm(Kind.Equal, a, b)
+ solver.mkTerm(Kind.EQUAL, a, b)
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Equal, cvc5.Term(solver), b)
+ solver.mkTerm(Kind.EQUAL, cvc5.Term(solver), b)
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Equal, a, cvc5.Term(solver))
+ solver.mkTerm(Kind.EQUAL, a, cvc5.Term(solver))
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Equal, a, solver.mkTrue())
+ solver.mkTerm(Kind.EQUAL, a, solver.mkTrue())
with pytest.raises(RuntimeError):
- slv.mkTerm(Kind.Equal, a, b)
+ slv.mkTerm(Kind.EQUAL, a, b)
# mkTerm(Kind kind, Term child1, Term child2, Term child3) const
- solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue())
+ solver.mkTerm(Kind.ITE, solver.mkTrue(), solver.mkTrue(), solver.mkTrue())
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Ite, cvc5.Term(solver), solver.mkTrue(),
+ solver.mkTerm(Kind.ITE, cvc5.Term(solver), solver.mkTrue(),
solver.mkTrue())
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Ite, solver.mkTrue(), cvc5.Term(solver),
+ solver.mkTerm(Kind.ITE, solver.mkTrue(), cvc5.Term(solver),
solver.mkTrue())
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(),
+ solver.mkTerm(Kind.ITE, solver.mkTrue(), solver.mkTrue(),
cvc5.Term(solver))
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), b)
+ solver.mkTerm(Kind.ITE, solver.mkTrue(), solver.mkTrue(), b)
with pytest.raises(RuntimeError):
- slv.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(),
+ slv.mkTerm(Kind.ITE, solver.mkTrue(), solver.mkTrue(),
solver.mkTrue())
- solver.mkTerm(Kind.Equal, v1)
+ solver.mkTerm(Kind.EQUAL, a, b)
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Equal, v2)
+ solver.mkTerm(Kind.EQUAL, a, cvc5.Term(solver))
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Equal, v3)
+ solver.mkTerm(Kind.EQUAL, a, solver.mkTrue())
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.Distinct, v6)
+ solver.mkTerm(Kind.DISTINCT)
# Test cases that are nary via the API but have arity = 2 internally
s_bool = solver.getBooleanSort()
t_bool = solver.mkConst(s_bool, "t_bool")
- solver.mkTerm(Kind.Implies, [t_bool, t_bool, t_bool])
- solver.mkTerm(Kind.Xor, [t_bool, t_bool, t_bool])
- solver.mkTerm(solver.mkOp(Kind.Xor), [t_bool, t_bool, t_bool])
+ solver.mkTerm(Kind.IMPLIES, t_bool, t_bool, t_bool)
+ solver.mkTerm(Kind.XOR, t_bool, t_bool, t_bool)
+ solver.mkTerm(solver.mkOp(Kind.XOR), t_bool, t_bool, t_bool)
t_int = solver.mkConst(solver.getIntegerSort(), "t_int")
- solver.mkTerm(Kind.Division, [t_int, t_int, t_int])
- solver.mkTerm(solver.mkOp(Kind.Division), [t_int, t_int, t_int])
- solver.mkTerm(Kind.IntsDivision, [t_int, t_int, t_int])
- solver.mkTerm(solver.mkOp(Kind.IntsDivision), [t_int, t_int, t_int])
- solver.mkTerm(Kind.Sub, [t_int, t_int, t_int])
- solver.mkTerm(solver.mkOp(Kind.Sub), [t_int, t_int, t_int])
- solver.mkTerm(Kind.Equal, [t_int, t_int, t_int])
- solver.mkTerm(solver.mkOp(Kind.Equal), [t_int, t_int, t_int])
- solver.mkTerm(Kind.Lt, [t_int, t_int, t_int])
- solver.mkTerm(solver.mkOp(Kind.Lt), [t_int, t_int, t_int])
- solver.mkTerm(Kind.Gt, [t_int, t_int, t_int])
- solver.mkTerm(solver.mkOp(Kind.Gt), [t_int, t_int, t_int])
- solver.mkTerm(Kind.Leq, [t_int, t_int, t_int])
- solver.mkTerm(solver.mkOp(Kind.Leq), [t_int, t_int, t_int])
- solver.mkTerm(Kind.Geq, [t_int, t_int, t_int])
- solver.mkTerm(solver.mkOp(Kind.Geq), [t_int, t_int, t_int])
+ solver.mkTerm(Kind.DIVISION, t_int, t_int, t_int)
+ solver.mkTerm(solver.mkOp(Kind.DIVISION), t_int, t_int, t_int)
+ solver.mkTerm(Kind.INTS_DIVISION, t_int, t_int, t_int)
+ solver.mkTerm(solver.mkOp(Kind.INTS_DIVISION), t_int, t_int, t_int)
+ solver.mkTerm(Kind.SUB, t_int, t_int, t_int)
+ solver.mkTerm(solver.mkOp(Kind.SUB), t_int, t_int, t_int)
+ solver.mkTerm(Kind.EQUAL, t_int, t_int, t_int)
+ solver.mkTerm(solver.mkOp(Kind.EQUAL), t_int, t_int, t_int)
+ solver.mkTerm(Kind.LT, t_int, t_int, t_int)
+ solver.mkTerm(solver.mkOp(Kind.LT), t_int, t_int, t_int)
+ solver.mkTerm(Kind.GT, t_int, t_int, t_int)
+ solver.mkTerm(solver.mkOp(Kind.GT), t_int, t_int, t_int)
+ solver.mkTerm(Kind.LEQ, t_int, t_int, t_int)
+ solver.mkTerm(solver.mkOp(Kind.LEQ), t_int, t_int, t_int)
+ solver.mkTerm(Kind.GEQ, t_int, t_int, t_int)
+ solver.mkTerm(solver.mkOp(Kind.GEQ), t_int, t_int, t_int)
t_reg = solver.mkConst(solver.getRegExpSort(), "t_reg")
- solver.mkTerm(Kind.RegexpDiff, [t_reg, t_reg, t_reg])
- solver.mkTerm(solver.mkOp(Kind.RegexpDiff), [t_reg, t_reg, t_reg])
+ solver.mkTerm(Kind.REGEXP_DIFF, t_reg, t_reg, t_reg)
+ solver.mkTerm(solver.mkOp(Kind.REGEXP_DIFF), t_reg, t_reg, t_reg)
t_fun = solver.mkConst(solver.mkFunctionSort(
[s_bool, s_bool, s_bool], s_bool))
- solver.mkTerm(Kind.HoApply, [t_fun, t_bool, t_bool, t_bool])
- solver.mkTerm(solver.mkOp(Kind.HoApply), [t_fun, t_bool, t_bool, t_bool])
+ solver.mkTerm(Kind.HO_APPLY, t_fun, t_bool, t_bool, t_bool)
+ solver.mkTerm(solver.mkOp(Kind.HO_APPLY), t_fun, t_bool, t_bool, t_bool)
def test_mk_term_from_op(solver):
bv32 = solver.mkBitVectorSort(32)
a = solver.mkConst(bv32, "a")
b = solver.mkConst(bv32, "b")
- v1 = [solver.mkInteger(1), solver.mkInteger(2)]
- v2 = [solver.mkInteger(1), cvc5.Term(solver)]
- v3 = []
- v4 = [solver.mkInteger(5)]
slv = cvc5.Solver()
# simple operator terms
- opterm1 = solver.mkOp(Kind.BVExtract, 2, 1)
- opterm2 = solver.mkOp(Kind.Divisible, 1)
+ opterm1 = solver.mkOp(Kind.BITVECTOR_EXTRACT, 2, 1)
+ opterm2 = solver.mkOp(Kind.DIVISIBLE, 1)
# list datatype
sort = solver.mkParamSort("T")
lis = listSort.getDatatype()
# list datatype constructor and selector operator terms
- consTerm1 = lis.getConstructorTerm("cons")
- consTerm2 = lis.getConstructor("cons").getConstructorTerm()
- nilTerm1 = lis.getConstructorTerm("nil")
- nilTerm2 = lis.getConstructor("nil").getConstructorTerm()
- headTerm1 = lis["cons"].getSelectorTerm("head")
- headTerm2 = lis["cons"].getSelector("head").getSelectorTerm()
- tailTerm1 = lis["cons"].getSelectorTerm("tail")
- tailTerm2 = lis["cons"]["tail"].getSelectorTerm()
+ consTerm = lis.getConstructor("cons").getTerm()
+ nilTerm = lis.getConstructor("nil").getTerm()
+ headTerm = lis["cons"].getSelector("head").getTerm()
+ tailTerm = lis["cons"]["tail"].getTerm()
# mkTerm(Op op, Term term) const
- solver.mkTerm(Kind.ApplyConstructor, nilTerm1)
- solver.mkTerm(Kind.ApplyConstructor, nilTerm2)
+ solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
+ solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.ApplySelector, nilTerm1)
+ solver.mkTerm(Kind.APPLY_SELECTOR, nilTerm)
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.ApplySelector, consTerm1)
+ solver.mkTerm(Kind.APPLY_SELECTOR, consTerm)
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.ApplyConstructor, consTerm2)
+ solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm)
with pytest.raises(RuntimeError):
solver.mkTerm(opterm1)
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.ApplySelector, headTerm1)
+ solver.mkTerm(Kind.APPLY_SELECTOR, headTerm)
with pytest.raises(RuntimeError):
solver.mkTerm(opterm1)
with pytest.raises(RuntimeError):
- slv.mkTerm(Kind.ApplyConstructor, nilTerm1)
+ slv.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
# mkTerm(Op op, Term child) const
solver.mkTerm(opterm1, a)
solver.mkTerm(opterm2, solver.mkInteger(1))
- solver.mkTerm(Kind.ApplySelector, headTerm1, c)
- solver.mkTerm(Kind.ApplySelector, tailTerm2, c)
+ solver.mkTerm(Kind.APPLY_SELECTOR, headTerm, c)
+ solver.mkTerm(Kind.APPLY_SELECTOR, tailTerm, c)
with pytest.raises(RuntimeError):
solver.mkTerm(opterm2, a)
with pytest.raises(RuntimeError):
solver.mkTerm(opterm1, cvc5.Term(solver))
with pytest.raises(RuntimeError):
- solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0))
+ solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm, solver.mkInteger(0))
with pytest.raises(RuntimeError):
slv.mkTerm(opterm1, a)
# mkTerm(Op op, Term child1, Term child2) const
- solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0),
- solver.mkTerm(Kind.ApplyConstructor, nilTerm1))
+ solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm, solver.mkInteger(0),
+ solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm))
with pytest.raises(RuntimeError):
solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2))
with pytest.raises(RuntimeError):
with pytest.raises(RuntimeError):
solver.mkTerm(opterm2, cvc5.Term(solver), solver.mkInteger(1))
with pytest.raises(RuntimeError):
- slv.mkTerm(Kind.ApplyConstructor,\
- consTerm1,\
+ slv.mkTerm(Kind.APPLY_CONSTRUCTOR,\
+ consTerm,\
solver.mkInteger(0),\
- solver.mkTerm(Kind.ApplyConstructor, nilTerm1))
+ solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm))
# mkTerm(Op op, Term child1, Term child2, Term child3) const
with pytest.raises(RuntimeError):
solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1),
cvc5.Term(solver))
- solver.mkTerm(opterm2, v4)
+ solver.mkTerm(opterm2, solver.mkInteger(5))
with pytest.raises(RuntimeError):
- solver.mkTerm(opterm2, v1)
+ solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2))
with pytest.raises(RuntimeError):
- solver.mkTerm(opterm2, v2)
+ solver.mkTerm(opterm2, solver.mkInteger(1), cvc5.Term(solver))
with pytest.raises(RuntimeError):
- solver.mkTerm(opterm2, v3)
+ solver.mkTerm(opterm2)
with pytest.raises(RuntimeError):
- slv.mkTerm(opterm2, v4)
+ slv.mkTerm(opterm2, solver.mkInteger(5))
def test_mk_true(solver):
x = solver.mkConst(intSort, "x")
y = solver.mkConst(intSort, "y")
f = solver.mkConst(funSort, "f")
- fxy = solver.mkTerm(Kind.ApplyUf, f, x, y)
+ fxy = solver.mkTerm(Kind.APPLY_UF, f, x, y)
# Expecting the uninterpreted function to be one of the children
expected_children = [f, x, y]
def test_get_op(solver):
bv32 = solver.mkBitVectorSort(32)
a = solver.mkConst(bv32, "a")
- ext = solver.mkOp(Kind.BVExtract, 2, 1)
+ ext = solver.mkOp(Kind.BITVECTOR_EXTRACT, 2, 1)
exta = solver.mkTerm(ext, a)
assert not a.hasOp()
consListSort = solver.mkDatatypeSort(consListSpec)
consList = consListSort.getDatatype()
- consTerm = consList.getConstructorTerm("cons")
- nilTerm = consList.getConstructorTerm("nil")
- headTerm = consList["cons"].getSelectorTerm("head")
+ consTerm = consList.getConstructor("cons").getTerm()
+ nilTerm = consList.getConstructor("nil").getTerm()
+ headTerm = consList["cons"].getSelector("head").getTerm()
- listnil = solver.mkTerm(Kind.ApplyConstructor, nilTerm)
- listcons1 = solver.mkTerm(Kind.ApplyConstructor, consTerm,
+ listnil = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
+ listcons1 = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm,
solver.mkInteger(1), listnil)
- listhead = solver.mkTerm(Kind.ApplySelector, headTerm, listcons1)
+ listhead = solver.mkTerm(Kind.APPLY_SELECTOR, headTerm, listcons1)
assert listnil.hasOp()
assert listcons1.hasOp()
def test_get_option(solver):
- solver.getOption("incremental")
+ solver.setOption("incremental", "true")
+ assert solver.getOption("incremental") == "true"
with pytest.raises(RuntimeError):
solver.getOption("asdf")
+def test_get_option_names(solver):
+ opts = solver.getOptionNames()
+ assert len(opts) > 100
+ assert "verbose" in opts
+ assert "foobar" not in opts
+
+
+def test_get_option_info(solver):
+ with pytest.raises(RuntimeError):
+ solver.getOptionInfo("asdf-invalid")
+
+ info = solver.getOptionInfo("verbose")
+ assert info['name'] == "verbose"
+ assert info['aliases'] == []
+ assert not info['setByUser']
+ assert info['type'] is None
+
+ info = solver.getOptionInfo("print-success")
+ assert info['name'] == "print-success"
+ assert info['aliases'] == []
+ assert not info['setByUser']
+ assert info['type'] is bool
+ assert info['current'] == False
+ assert info['default'] == False
+
+ info = solver.getOptionInfo("verbosity")
+ assert info['name'] == "verbosity"
+ assert info['aliases'] == []
+ assert not info['setByUser']
+ assert info['type'] is int
+ assert info['current'] == 0
+ assert info['default'] == 0
+ assert info['minimum'] is None and info['maximum'] is None
+
+ info = solver.getOptionInfo("rlimit")
+ assert info['name'] == "rlimit"
+ assert info['aliases'] == []
+ assert not info['setByUser']
+ assert info['type'] is int
+ assert info['current'] == 0
+ assert info['default'] == 0
+ assert info['minimum'] is None and info['maximum'] is None
+
+ info = solver.getOptionInfo("random-freq")
+ assert info['name'] == "random-freq"
+ assert info['aliases'] == ["random-frequency"]
+ assert not info['setByUser']
+ assert info['type'] is float
+ assert info['current'] == 0.0
+ assert info['default'] == 0.0
+ assert info['minimum'] == 0.0 and info['maximum'] == 1.0
+
+ info = solver.getOptionInfo("force-logic")
+ assert info['name'] == "force-logic"
+ assert info['aliases'] == []
+ assert not info['setByUser']
+ assert info['type'] is str
+ assert info['current'] == ""
+ assert info['default'] == ""
+
+ info = solver.getOptionInfo("simplification")
+ assert info['name'] == "simplification"
+ assert info['aliases'] == ["simplification-mode"]
+ assert not info['setByUser']
+ assert info['type'] == 'mode'
+ assert info['current'] == 'batch'
+ assert info['default'] == 'batch'
+ assert info['modes'] == ['batch', 'none']
+
+
def test_get_unsat_assumptions1(solver):
solver.setOption("incremental", "false")
solver.checkSatAssuming(solver.mkFalse())
solver.getUnsatCore()
-def test_get_unsat_core3(solver):
+def test_get_unsat_core_and_proof(solver):
solver.setOption("incremental", "true")
solver.setOption("produce-unsat-cores", "true")
+ solver.setOption("produce-proofs", "true");
uSort = solver.mkUninterpretedSort("u")
intSort = solver.getIntegerSort()
p = solver.mkConst(intPredSort, "p")
zero = solver.mkInteger(0)
one = solver.mkInteger(1)
- f_x = solver.mkTerm(Kind.ApplyUf, f, x)
- f_y = solver.mkTerm(Kind.ApplyUf, f, y)
- summ = solver.mkTerm(Kind.Add, f_x, f_y)
- p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
- p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
- solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_x))
- solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_y))
- solver.assertFormula(solver.mkTerm(Kind.Gt, summ, one))
+ f_x = solver.mkTerm(Kind.APPLY_UF, f, x)
+ f_y = solver.mkTerm(Kind.APPLY_UF, f, y)
+ summ = solver.mkTerm(Kind.ADD, f_x, f_y)
+ p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero)
+ p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y)
+ solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_x))
+ solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_y))
+ solver.assertFormula(solver.mkTerm(Kind.GT, summ, one))
solver.assertFormula(p_0)
solver.assertFormula(p_f_y.notTerm())
assert solver.checkSat().isUnsat()
solver.assertFormula(t)
res = solver.checkSat()
assert res.isUnsat()
+ solver.getProof()
def test_learned_literals(solver):
solver.setOption("produce-learned-literals", "true")
y = solver.mkConst(intSort, "y")
zero = solver.mkInteger(0)
ten = solver.mkInteger(10)
- f0 = solver.mkTerm(Kind.Geq, x, ten)
- f1 = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Geq, zero, x), solver.mkTerm(Kind.Geq, y, zero))
+ f0 = solver.mkTerm(Kind.GEQ, x, ten)
+ f1 = solver.mkTerm(
+ Kind.OR,
+ solver.mkTerm(Kind.GEQ, zero, x),
+ solver.mkTerm(Kind.GEQ, y, zero))
solver.assertFormula(f0)
solver.assertFormula(f1)
solver.checkSat()
p = solver.mkConst(intPredSort, "p")
zero = solver.mkInteger(0)
one = solver.mkInteger(1)
- f_x = solver.mkTerm(Kind.ApplyUf, f, x)
- f_y = solver.mkTerm(Kind.ApplyUf, f, y)
- summ = solver.mkTerm(Kind.Add, f_x, f_y)
- p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
- p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
-
- solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_x))
- solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_y))
- solver.assertFormula(solver.mkTerm(Kind.Leq, summ, one))
+ f_x = solver.mkTerm(Kind.APPLY_UF, f, x)
+ f_y = solver.mkTerm(Kind.APPLY_UF, f, y)
+ summ = solver.mkTerm(Kind.ADD, f_x, f_y)
+ p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero)
+ p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y)
+
+ solver.assertFormula(solver.mkTerm(Kind.LEQ, zero, f_x))
+ solver.assertFormula(solver.mkTerm(Kind.LEQ, zero, f_y))
+ solver.assertFormula(solver.mkTerm(Kind.LEQ, summ, one))
solver.assertFormula(p_0.notTerm())
solver.assertFormula(p_f_y)
assert solver.checkSat().isSat()
slv.declareSepHeap(integer, integer)
x = slv.mkConst(integer, "x")
p = slv.mkConst(integer, "p")
- heap = slv.mkTerm(Kind.SepPto, p, x)
+ heap = slv.mkTerm(Kind.SEP_PTO, p, x)
slv.assertFormula(heap)
nil = slv.mkSepNil(integer)
slv.assertFormula(nil.eqTerm(slv.mkReal(5)))
solver.pop(1)
def test_block_model1(solver):
- solver.setOption("produce-models", "true")
x = solver.mkConst(solver.getBooleanSort(), "x")
solver.assertFormula(x.eqTerm(x))
solver.checkSat()
with pytest.raises(RuntimeError):
- solver.blockModel()
+ solver.blockModel(BlockModelsMode.LITERALS)
def test_block_model2(solver):
- solver.setOption("block-models", "literals")
- x = solver.mkConst(solver.getBooleanSort(), "x")
- solver.assertFormula(x.eqTerm(x))
- solver.checkSat()
- with pytest.raises(RuntimeError):
- solver.blockModel()
-
-def test_block_model3(solver):
solver.setOption("produce-models", "true")
- solver.setOption("block-models", "literals")
x = solver.mkConst(solver.getBooleanSort(), "x")
solver.assertFormula(x.eqTerm(x))
with pytest.raises(RuntimeError):
- solver.blockModel()
+ solver.blockModel(BlockModelsMode.LITERALS)
-def test_block_model4(solver):
+def test_block_model3(solver):
solver.setOption("produce-models", "true")
- solver.setOption("block-models", "literals")
x = solver.mkConst(solver.getBooleanSort(), "x");
solver.assertFormula(x.eqTerm(x))
solver.checkSat()
- solver.blockModel()
+ solver.blockModel(BlockModelsMode.LITERALS)
def test_block_model_values1(solver):
solver.setOption("produce-models", "true")
- solver.setOption("block-models", "literals")
x = solver.mkConst(solver.getBooleanSort(), "x");
solver.assertFormula(x.eqTerm(x))
solver.checkSat()
solver.blockModelValues([x])
def test_block_model_values3(solver):
- solver.setOption("block-models", "literals")
x = solver.mkConst(solver.getBooleanSort(), "x")
solver.assertFormula(x.eqTerm(x))
solver.checkSat()
def test_block_model_values4(solver):
solver.setOption("produce-models", "true")
- solver.setOption("block-models", "literals")
x = solver.mkConst(solver.getBooleanSort(), "x")
solver.assertFormula(x.eqTerm(x))
with pytest.raises(RuntimeError):
def test_block_model_values5(solver):
solver.setOption("produce-models", "true")
- solver.setOption("block-models", "literals")
x = solver.mkConst(solver.getBooleanSort(), "x")
solver.assertFormula(x.eqTerm(x))
solver.checkSat()
solver.blockModelValues([x])
+def test_get_statistics(solver):
+ intSort = solver.getIntegerSort()
+ x = solver.mkConst(intSort, "x")
+ y = solver.mkConst(intSort, "y")
+ zero = solver.mkInteger(0)
+ ten = solver.mkInteger(10)
+ f0 = solver.mkTerm(Kind.GEQ, x, ten)
+ f1 = solver.mkTerm(
+ Kind.OR,
+ solver.mkTerm(Kind.GEQ, zero, x),
+ solver.mkTerm(Kind.GEQ, y, zero))
+ solver.assertFormula(f0)
+ solver.assertFormula(f1)
+ solver.checkSat()
+ s = solver.getStatistics()
+ assert s['cvc5::TERM'] == {'defaulted': False, 'internal': False, 'value': {'GEQ': 3, 'OR': 1}}
+ assert s.get(True, False) != {}
+
def test_set_info(solver):
with pytest.raises(RuntimeError):
solver.setInfo("cvc5-lagic", "QF_BV")
solver.simplify(a)
b = solver.mkConst(bvSort, "b")
solver.simplify(b)
- x_eq_x = solver.mkTerm(Kind.Equal, x, x)
+ x_eq_x = solver.mkTerm(Kind.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(Kind.Equal, x, b)
+ x_eq_b = solver.mkTerm(Kind.EQUAL, x, b)
solver.simplify(x_eq_b)
assert solver.mkTrue() != x_eq_b
assert solver.mkTrue() != solver.simplify(x_eq_b)
i1 = solver.mkConst(solver.getIntegerSort(), "i1")
solver.simplify(i1)
- i2 = solver.mkTerm(Kind.Mult, i1, solver.mkInteger("23"))
+ i2 = solver.mkTerm(Kind.MULT, i1, solver.mkInteger("23"))
solver.simplify(i2)
assert i1 != i2
assert i1 != solver.simplify(i2)
- i3 = solver.mkTerm(Kind.Add, i1, solver.mkInteger(0))
+ i3 = solver.mkTerm(Kind.ADD, i1, solver.mkInteger(0))
solver.simplify(i3)
assert i1 != i3
assert i1 == solver.simplify(i3)
consList = consListSort.getDatatype()
- dt1 = solver.mkTerm(\
- Kind.ApplyConstructor,\
- consList.getConstructorTerm("cons"),\
- solver.mkInteger(0),\
- solver.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("nil")))
+ dt1 = solver.mkTerm(
+ Kind.APPLY_CONSTRUCTOR,
+ consList.getConstructor("cons").getTerm(),
+ solver.mkInteger(0),
+ solver.mkTerm(
+ Kind.APPLY_CONSTRUCTOR,
+ consList.getConstructor("nil").getTerm()))
solver.simplify(dt1)
- dt2 = solver.mkTerm(\
- Kind.ApplySelector, consList["cons"].getSelectorTerm("head"), dt1)
+ dt2 = solver.mkTerm(
+ Kind.APPLY_SELECTOR,
+ consList["cons"].getSelector("head").getTerm(),
+ dt1)
solver.simplify(dt2)
b1 = solver.mkVar(bvSort, "b1")
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 = cvc5.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(Kind.And, x, y)
- solver.setOption("incremental", "true")
- solver.checkEntailed(solver.mkTrue())
- with pytest.raises(RuntimeError):
- solver.checkEntailed(cvc5.Term(solver))
- solver.checkEntailed(solver.mkTrue())
- solver.checkEntailed(z)
- slv = cvc5.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 = cvc5.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(Kind.ApplyUf, f, x)
- f_y = solver.mkTerm(Kind.ApplyUf, f, y)
- summ = solver.mkTerm(Kind.Add, f_x, f_y)
- p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
- p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
- # Assertions
- assertions =\
- solver.mkTerm(Kind.And,\
- [solver.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x)
- solver.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y)
- solver.mkTerm(Kind.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(Kind.Distinct, x, y))
- solver.checkEntailed(\
- [solver.mkFalse(), solver.mkTerm(Kind.Distinct, x, y)])
- with pytest.raises(RuntimeError):
- solver.checkEntailed(n)
- with pytest.raises(RuntimeError):
- solver.checkEntailed([n, solver.mkTerm(Kind.Distinct, x, y)])
- slv = cvc5.Solver()
- with pytest.raises(RuntimeError):
- slv.checkEntailed(solver.mkTrue())
-
-
def test_check_sat(solver):
solver.setOption("incremental", "false")
solver.checkSat()
boolSort = solver.getBooleanSort()
x = solver.mkConst(boolSort, "x")
y = solver.mkConst(boolSort, "y")
- z = solver.mkTerm(Kind.And, x, y)
+ z = solver.mkTerm(Kind.AND, x, y)
solver.setOption("incremental", "true")
solver.checkSatAssuming(solver.mkTrue())
with pytest.raises(RuntimeError):
zero = solver.mkInteger(0)
one = solver.mkInteger(1)
# Terms
- f_x = solver.mkTerm(Kind.ApplyUf, f, x)
- f_y = solver.mkTerm(Kind.ApplyUf, f, y)
- summ = solver.mkTerm(Kind.Add, f_x, f_y)
- p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
- p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
+ f_x = solver.mkTerm(Kind.APPLY_UF, f, x)
+ f_y = solver.mkTerm(Kind.APPLY_UF, f, y)
+ summ = solver.mkTerm(Kind.ADD, f_x, f_y)
+ p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero)
+ p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y)
# Assertions
assertions =\
- solver.mkTerm(Kind.And,\
- [solver.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x)
- solver.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y)
- solver.mkTerm(Kind.Leq, summ, one), # f(x) + f(y) <= 1
+ solver.mkTerm(Kind.AND,\
+ solver.mkTerm(Kind.LEQ, zero, f_x), # 0 <= f(x)
+ solver.mkTerm(Kind.LEQ, zero, f_y), # 0 <= f(y)
+ solver.mkTerm(Kind.LEQ, summ, one), # f(x) + f(y) <= 1
p_0.notTerm(), # not p(0)
p_f_y # p(f(y))
- ])
+ )
solver.checkSatAssuming(solver.mkTrue())
solver.assertFormula(assertions)
- solver.checkSatAssuming(solver.mkTerm(Kind.Distinct, x, y))
+ solver.checkSatAssuming(solver.mkTerm(Kind.DISTINCT, x, y))
solver.checkSatAssuming(
- [solver.mkFalse(),
- solver.mkTerm(Kind.Distinct, x, y)])
+ solver.mkFalse(),
+ solver.mkTerm(Kind.DISTINCT, x, y))
with pytest.raises(RuntimeError):
solver.checkSatAssuming(n)
with pytest.raises(RuntimeError):
- solver.checkSatAssuming([n, solver.mkTerm(Kind.Distinct, x, y)])
+ solver.checkSatAssuming(n, solver.mkTerm(Kind.DISTINCT, x, y))
slv = cvc5.Solver()
with pytest.raises(RuntimeError):
slv.checkSatAssuming(solver.mkTrue())
bvSort = solver.mkBitVectorSort(4)
one = solver.mkBitVector(4, 1)
x = solver.mkConst(bvSort, "x")
- ule = solver.mkTerm(Kind.BVUle, x, one)
- srem = solver.mkTerm(Kind.BVSrem, one, x)
+ ule = solver.mkTerm(Kind.BITVECTOR_ULE, x, one)
+ srem = solver.mkTerm(Kind.BITVECTOR_SREM, one, x)
solver.push(4)
- slt = solver.mkTerm(Kind.BVSlt, srem, one)
+ slt = solver.mkTerm(Kind.BITVECTOR_SLT, srem, one)
solver.resetAssertions()
- solver.checkSatAssuming([slt, ule])
+ solver.checkSatAssuming(slt, ule)
def test_mk_sygus_grammar(solver):
def test_synth_inv(solver):
+ solver.setOption("sygus", "true")
boolean = solver.getBooleanSort()
integer = solver.getIntegerSort()
def test_add_sygus_constraint(solver):
+ solver.setOption("sygus", "true")
nullTerm = cvc5.Term(solver)
boolTerm = solver.mkBoolean(True)
intTerm = solver.mkInteger(1)
with pytest.raises(RuntimeError):
slv.addSygusConstraint(boolTerm)
+def test_add_sygus_assume(solver):
+ solver.setOption("sygus", "true")
+ nullTerm = cvc5.Term(solver)
+ boolTerm = solver.mkBoolean(False)
+ intTerm = solver.mkInteger(1)
+ solver.addSygusAssume(boolTerm)
+ with pytest.raises(RuntimeError):
+ solver.addSygusAssume(nullTerm)
+ with pytest.raises(RuntimeError):
+ solver.addSygusAssume(intTerm)
+ slv = cvc5.Solver()
+ with pytest.raises(RuntimeError):
+ slv.addSygusAssume(boolTerm)
+
def test_add_sygus_inv_constraint(solver):
+ solver.setOption("sygus", "true")
boolean = solver.getBooleanSort()
real = solver.getRealSort()
with pytest.raises(RuntimeError):
solver.addSygusInvConstraint(inv, pre, trans, trans)
slv = cvc5.Solver()
+ slv.setOption("sygus", "true")
boolean2 = slv.getBooleanSort()
real2 = slv.getRealSort()
inv22 = slv.declareFun("inv", [real2], boolean2)
slv.addSygusInvConstraint(inv22, pre22, trans22, post)
+def test_check_synth(solver):
+ with pytest.raises(RuntimeError):
+ solver.checkSynth()
+ solver.setOption("sygus", "true")
+ solver.checkSynth()
+
def test_get_synth_solution(solver):
- solver.setOption("lang", "sygus2")
+ solver.setOption("sygus", "true")
solver.setOption("incremental", "false")
nullTerm = cvc5.Term(solver)
with pytest.raises(RuntimeError):
solver.getSynthSolution(f)
- solver.checkSynth()
+ res = solver.checkSynth()
+ assert res.hasSolution()
solver.getSynthSolution(f)
solver.getSynthSolution(f)
slv.getSynthSolution(f)
def test_check_synth_next(solver):
- solver.setOption("lang", "sygus2")
+ solver.setOption("sygus", "true")
solver.setOption("incremental", "true")
f = solver.synthFun("f", [], solver.getBooleanSort())
- solver.checkSynth()
+ res = solver.checkSynth()
+ assert res.hasSolution()
solver.getSynthSolutions([f])
- solver.checkSynthNext()
+ res = solver.checkSynthNext()
+ assert res.hasSolution()
solver.getSynthSolutions([f])
def test_check_synth_next2(solver):
- solver.setOption("lang", "sygus2")
+ solver.setOption("sygus", "true")
solver.setOption("incremental", "false")
f = solver.synthFun("f", [], solver.getBooleanSort())
solver.checkSynthNext()
def test_check_synth_next3(solver):
- solver.setOption("lang", "sygus2")
+ solver.setOption("sygus", "true")
solver.setOption("incremental", "true")
f = solver.synthFun("f", [], solver.getBooleanSort())
with pytest.raises(RuntimeError):
x = solver.mkConst(intSort, "x")
y = solver.mkConst(intSort, "y")
- solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
- conj = solver.mkTerm(Kind.Gt, y, zero)
- output = cvc5.Term(solver)
- assert solver.getAbduct(conj, output)
+ solver.assertFormula(solver.mkTerm(Kind.GT, x, zero))
+ conj = solver.mkTerm(Kind.GT, y, zero)
+ output = solver.getAbduct(conj)
assert not output.isNull() and output.getSort().isBoolean()
boolean = solver.getBooleanSort()
start = solver.mkVar(boolean)
output2 = cvc5.Term(solver)
g = solver.mkSygusGrammar([], [start])
- conj2 = solver.mkTerm(Kind.Gt, x, zero)
+ conj2 = solver.mkTerm(Kind.GT, x, zero)
g.addRule(start, truen)
- assert solver.getAbduct(conj2, g, output2)
+ output2 = solver.getAbduct(conj2, g)
assert output2 == truen
def test_get_abduct2(solver):
zero = solver.mkInteger(0)
x = solver.mkConst(intSort, "x")
y = solver.mkConst(intSort, "y")
- solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
- conj = solver.mkTerm(Kind.Gt, y, zero)
+ solver.assertFormula(solver.mkTerm(Kind.GT, x, zero))
+ conj = solver.mkTerm(Kind.GT, y, zero)
output = cvc5.Term(solver)
with pytest.raises(RuntimeError):
- solver.getAbduct(conj, output)
+ solver.getAbduct(conj)
def test_get_abduct_next(solver):
solver.setLogic("QF_LIA")
x = solver.mkConst(intSort, "x")
y = solver.mkConst(intSort, "y")
- solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
- conj = solver.mkTerm(Kind.Gt, y, zero)
- output = cvc5.Term(solver)
- assert solver.getAbduct(conj, output)
- output2 = cvc5.Term(solver)
- assert solver.getAbductNext(output2)
+ solver.assertFormula(solver.mkTerm(Kind.GT, x, zero))
+ conj = solver.mkTerm(Kind.GT, y, zero)
+ output = solver.getAbduct(conj)
+ output2 = solver.getAbductNext()
assert output != output2
def test_get_interpolant(solver):
solver.setLogic("QF_LIA")
- solver.setOption("produce-interpols", "default")
+ solver.setOption("produce-interpolants", "true")
solver.setOption("incremental", "false")
intSort = solver.getIntegerSort()
z = solver.mkConst(intSort, "z")
solver.assertFormula(solver.mkTerm(
- Kind.Gt, solver.mkTerm(Kind.Add, x, y), zero))
- solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero))
+ Kind.GT, solver.mkTerm(Kind.ADD, x, y), zero))
+ solver.assertFormula(solver.mkTerm(Kind.LT, x, zero))
conj = solver.mkTerm(
- Kind.Or,
- solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero),
- solver.mkTerm(Kind.Lt, z, zero))
- output = cvc5.Term(solver)
- solver.getInterpolant(conj, output)
+ Kind.OR,
+ solver.mkTerm(Kind.GT, solver.mkTerm(Kind.ADD, y, z), zero),
+ solver.mkTerm(Kind.LT, z, zero))
+ output = solver.getInterpolant(conj)
assert output.getSort().isBoolean()
def test_get_interpolant_next(solver):
solver.setLogic("QF_LIA")
- solver.setOption("produce-interpols", "default")
+ solver.setOption("produce-interpolants", "true")
solver.setOption("incremental", "true")
intSort = solver.getIntegerSort()
z = solver.mkConst(intSort, "z")
solver.assertFormula(solver.mkTerm(
- Kind.Gt, solver.mkTerm(Kind.Add, x, y), zero))
- solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero))
+ Kind.GT, solver.mkTerm(Kind.ADD, x, y), zero))
+ solver.assertFormula(solver.mkTerm(Kind.LT, x, zero))
conj = solver.mkTerm(
- Kind.Or,
- solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero),
- solver.mkTerm(Kind.Lt, z, zero))
- output = cvc5.Term(solver)
- solver.getInterpolant(conj, output)
- output2 = cvc5.Term(solver)
- solver.getInterpolantNext(output2)
+ Kind.OR,
+ solver.mkTerm(Kind.GT, solver.mkTerm(Kind.ADD, y, z), zero),
+ solver.mkTerm(Kind.LT, z, zero))
+ output = solver.getInterpolant(conj)
+ output2 = solver.getInterpolantNext()
assert output != output2
# (assert (or (not f) (not (g true))))
solver.assertFormula(
- solver.mkTerm(Kind.Or, f.notTerm(),
- solver.mkTerm(Kind.ApplyUf, g, bTrue).notTerm()))
+ 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.ApplyUf, g, bTrue).notTerm()))
+ solver.mkTerm(Kind.OR, f.notTerm(),
+ solver.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm()))
assert solver.checkSat().isUnsat()
x = solver.mkConst(uSort, "x")
y = solver.mkConst(uSort, "y")
z = solver.mkConst(uSort, "z")
- f = solver.mkTerm(Kind.Distinct, x, y, z)
+ f = solver.mkTerm(Kind.DISTINCT, x, y, z)
solver.assertFormula(f)
solver.checkSat()
solver.getModelDomainElements(uSort)
with pytest.raises(RuntimeError):
solver.getModelDomainElements(intSort)
+def test_get_model_domain_elements2(solver):
+ solver.setOption("produce-models", "true")
+ solver.setOption("finite-model-find", "true")
+ uSort = solver.mkUninterpretedSort("u")
+ x = solver.mkVar(uSort, "x")
+ y = solver.mkVar(uSort, "y")
+ eq = solver.mkTerm(Kind.EQUAL, x, y)
+ bvl = solver.mkTerm(Kind.VARIABLE_LIST, x, y)
+ f = solver.mkTerm(Kind.FORALL, bvl, eq)
+ solver.assertFormula(f)
+ solver.checkSat()
+ solver.getModelDomainElements(uSort)
+ assert len(solver.getModelDomainElements(uSort)) == 1
+
def test_get_synth_solutions(solver):
- solver.setOption("lang", "sygus2")
+ solver.setOption("sygus", "true")
solver.setOption("incremental", "false")
nullTerm = cvc5.Term(solver)
y = solver.mkConst(uSort, "y")
z = solver.mkConst(uSort, "z")
zero = solver.mkInteger(0)
- f = solver.mkTerm(Kind.Not, solver.mkTerm(Kind.Equal, x, y))
+ f = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, x, y))
solver.assertFormula(f)
solver.checkSat()
assert solver.isModelCoreSymbol(x)
solver.isModelCoreSymbol(zero)
+def test_get_model(solver):
+ solver.setOption("produce-models", "true")
+ uSort = solver.mkUninterpretedSort("u")
+ x = solver.mkConst(uSort, "x")
+ y = solver.mkConst(uSort, "y")
+ z = solver.mkConst(uSort, "z")
+ f = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, x, y))
+ solver.assertFormula(f)
+ solver.checkSat()
+ sorts = [uSort]
+ terms = [x, y]
+ solver.getModel(sorts, terms)
+ null = cvc5.Term(solver)
+ terms.append(null)
+ with pytest.raises(RuntimeError):
+ solver.getModel(sorts, terms)
+
+
+def test_get_model2(solver):
+ solver.setOption("produce-models", "true")
+ sorts = []
+ terms = []
+ with pytest.raises(RuntimeError):
+ solver.getModel(sorts, terms)
+
+
+def test_get_model3(solver):
+ solver.setOption("produce-models", "true")
+ sorts = []
+ terms = []
+ solver.checkSat()
+ solver.getModel(sorts, terms)
+ integer = solver.getIntegerSort()
+ sorts.append(integer)
+ with pytest.raises(RuntimeError):
+ solver.getModel(sorts, terms)
+
+
def test_issue5893(solver):
slv = cvc5.Solver()
bvsort4 = solver.mkBitVectorSort(4)
arr = solver.mkConst(arrsort, "arr")
idx = solver.mkConst(bvsort4, "idx")
ten = solver.mkBitVector(8, "10", 10)
- sel = solver.mkTerm(Kind.Select, arr, idx)
- distinct = solver.mkTerm(Kind.Distinct, sel, ten)
+ sel = solver.mkTerm(Kind.SELECT, arr, idx)
+ distinct = solver.mkTerm(Kind.DISTINCT, sel, ten)
distinct.getOp()
t7 = solver.mkConst(s3, "_x5")
t37 = solver.mkConst(s2, "_x32")
t59 = solver.mkConst(s2, "_x51")
- t72 = solver.mkTerm(Kind.Equal, t37, t59)
- t74 = solver.mkTerm(Kind.Gt, t4, t7)
+ t72 = solver.mkTerm(Kind.EQUAL, t37, t59)
+ t74 = solver.mkTerm(Kind.GT, t4, t7)
+ query = solver.mkTerm(Kind.AND, t72, t74, t72, t72)
# throws logic exception since logic is not higher order by default
with pytest.raises(RuntimeError):
- solver.checkEntailed(t72, t74, t72, t72)
+ solver.checkSatAssuming(query.notTerm())
def test_mk_sygus_var(solver):
+ solver.setOption("sygus", "true")
boolSort = solver.getBooleanSort()
intSort = solver.getIntegerSort()
funSort = solver.mkFunctionSort(intSort, boolSort)
- solver.mkSygusVar(boolSort)
- solver.mkSygusVar(funSort)
- solver.mkSygusVar(boolSort, "b")
- solver.mkSygusVar(funSort, "")
+ solver.declareSygusVar("", boolSort)
+ solver.declareSygusVar("", funSort)
+ solver.declareSygusVar("b", boolSort)
with pytest.raises(RuntimeError):
- solver.mkSygusVar(cvc5.Sort(solver))
+ solver.declareSygusVar("", cvc5.Sort(solver))
with pytest.raises(RuntimeError):
- solver.mkSygusVar(solver.getNullSort(), "a")
+ solver.declareSygusVar("a", solver.getNullSort())
slv = cvc5.Solver()
+ solver.setOption("sygus", "true")
with pytest.raises(RuntimeError):
- slv.mkSygusVar(boolSort)
+ slv.declareSygusVar("", boolSort)
def test_synth_fun(solver):
+ solver.setOption("sygus", "true")
null = solver.getNullSort()
boolean = solver.getBooleanSort()
integer = solver.getIntegerSort()
with pytest.raises(RuntimeError):
solver.synthFun("f6", [x], boolean, g2)
slv = cvc5.Solver()
+ slv.setOption("sygus", "true")
x2 = slv.mkVar(slv.getBooleanSort())
slv.synthFun("f1", [x2], slv.getBooleanSort())
with pytest.raises(RuntimeError):
solver.mkBoolean(True), \
solver.mkInteger(3),\
solver.mkString("C"),\
- solver.mkTerm(Kind.SetSingleton, solver.mkString("Z"))]
+ solver.mkTerm(Kind.SET_SINGLETON, solver.mkString("Z"))]
tuple = solver.mkTuple(sorts, elements)
indices5 = [4]
indices6 = [0, 4]
- solver.mkTerm(solver.mkOp(Kind.TupleProject, indices1), tuple)
+ solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices1), tuple)
- solver.mkTerm(solver.mkOp(Kind.TupleProject, indices2), tuple)
+ solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices2), tuple)
- solver.mkTerm(solver.mkOp(Kind.TupleProject, indices3), tuple)
+ solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices3), tuple)
- solver.mkTerm(solver.mkOp(Kind.TupleProject, indices4), tuple)
+ solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices4), tuple)
with pytest.raises(RuntimeError):
- solver.mkTerm(solver.mkOp(Kind.TupleProject, indices5), tuple)
+ solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices5), tuple)
with pytest.raises(RuntimeError):
- solver.mkTerm(solver.mkOp(Kind.TupleProject, indices6), tuple)
+ solver.mkTerm(solver.mkOp(Kind.TUPLE_PROJECT, *indices6), tuple)
indices = [0, 3, 2, 0, 1, 2]
- op = solver.mkOp(Kind.TupleProject, indices)
+ op = solver.mkOp(Kind.TUPLE_PROJECT, *indices)
projection = solver.mkTerm(op, tuple)
datatype = tuple.getSort().getDatatype()
for i in indices:
- selectorTerm = constructor[i].getSelectorTerm()
- selectedTerm = solver.mkTerm(Kind.ApplySelector, selectorTerm, tuple)
+ selectorTerm = constructor[i].getTerm()
+ selectedTerm = solver.mkTerm(Kind.APPLY_SELECTOR, selectorTerm, tuple)
simplifiedTerm = solver.simplify(selectedTerm)
assert elements[i] == simplifiedTerm
- assert "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" == str(
+ assert "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" == str(
projection)
+
+
+
+def test_get_data_type_arity(solver):
+ ctor1 = solver.mkDatatypeConstructorDecl("_x21")
+ ctor2 = solver.mkDatatypeConstructorDecl("_x31")
+ s3 = solver.declareDatatype("_x17", ctor1, ctor2)
+ assert s3.getDatatypeArity() == 0
+
+
+def test_get_difficulty(solver):
+ solver.setOption("produce-difficulty", "true")
+ # cannot ask before a check sat
+ with pytest.raises(RuntimeError):
+ solver.getDifficulty()
+ solver.checkSat()
+ solver.getDifficulty()
+
+def test_get_difficulty2(solver):
+ solver.checkSat()
+ with pytest.raises(RuntimeError):
+ # option is not set
+ solver.getDifficulty()
+
+def test_get_difficulty3(solver):
+ solver.setOption("produce-difficulty", "true")
+ intSort = solver.getIntegerSort()
+ x = solver.mkConst(intSort, "x")
+ zero = solver.mkInteger(0)
+ ten = solver.mkInteger(10)
+ f0 = solver.mkTerm(Kind.GEQ, x, ten)
+ f1 = solver.mkTerm(Kind.GEQ, zero, x)
+ solver.checkSat()
+ dmap = solver.getDifficulty()
+ # difficulty should map assertions to integer values
+ for key, value in dmap.items():
+ assert key == f0 or key == f1
+ assert value.getKind() == Kind.CONST_RATIONAL
+
+def test_get_model(solver):
+ solver.setOption("produce-models", "true")
+ uSort = solver.mkUninterpretedSort("u")
+ x = solver.mkConst(uSort, "x")
+ y = solver.mkConst(uSort, "y")
+ z = solver.mkConst(uSort, "z")
+ f = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, x, y));
+ solver.assertFormula(f)
+ solver.checkSat()
+ sorts = [uSort]
+ terms = [x, y]
+ solver.getModel(sorts, terms)
+ null = cvc5.Term(solver)
+ terms += [null]
+ with pytest.raises(RuntimeError):
+ solver.getModel(sorts, terms)
+
+def test_get_model2(solver):
+ solver.setOption("produce-models", "true")
+ sorts = []
+ terms = []
+ with pytest.raises(RuntimeError):
+ solver.getModel(sorts, terms)
+
+def test_get_model_3(solver):
+ solver.setOption("produce-models", "true")
+ sorts = []
+ terms = []
+ solver.checkSat()
+ solver.getModel(sorts, terms)
+ integer = solver.getIntegerSort()
+ sorts += [integer]
+ with pytest.raises(RuntimeError):
+ solver.getModel(sorts, terms)
+
+def test_get_option_names(solver):
+ names = solver.getOptionNames()
+ assert len(names) > 100
+ assert "verbose" in names
+ assert "foobar" not in names
+
+def test_get_quantifier_elimination(solver):
+ x = solver.mkVar(solver.getBooleanSort(), "x")
+ forall = solver.mkTerm(
+ Kind.FORALL,
+ solver.mkTerm(Kind.VARIABLE_LIST, x),
+ solver.mkTerm(Kind.OR, x, solver.mkTerm(Kind.NOT, x)))
+ with pytest.raises(RuntimeError):
+ solver.getQuantifierElimination(cvc5.Term(solver))
+ with pytest.raises(RuntimeError):
+ solver.getQuantifierElimination(cvc5.Solver().mkBoolean(False))
+ solver.getQuantifierElimination(forall)
+
+def test_get_quantifier_elimination_disjunct(solver):
+ x = solver.mkVar(solver.getBooleanSort(), "x")
+ forall = solver.mkTerm(
+ Kind.FORALL,
+ solver.mkTerm(Kind.VARIABLE_LIST, x),
+ solver.mkTerm(Kind.OR, x, solver.mkTerm(Kind.NOT, x)))
+ with pytest.raises(RuntimeError):
+ solver.getQuantifierEliminationDisjunct(cvc5.Term(solver))
+ with pytest.raises(RuntimeError):
+ solver.getQuantifierEliminationDisjunct(cvc5.Solver().mkBoolean(False))
+ solver.getQuantifierEliminationDisjunct(forall)
projects / cvc5.git / blobdiff