Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- from z3 import *
- def test_list_elt_gt_1():
- ll = Datatype('ll')
- ll.declare('empty')
- ll.declare('cons', ('car', IntSort()), ('cdr', ll))
- ll = ll.create()
- list_sum = Function('list_sum', ll, IntSort(), BoolSort())
- list_len = Function('list_len', ll, IntSort(), BoolSort())
- a,e = Consts('a e', ll)
- b,c,d = Ints('b c d')
- fp = Fixedpoint()
- fp.declare_var(a,b,c,d,e)
- fp.register_relation(list_sum, list_len)
- fp.rule(list_sum(a, 0), a == ll.empty)
- fp.rule(list_sum(a, d), [a != ll.empty, b < 1, ll.cons(b, e) == a, list_sum(e, c), b + c == d])
- fp.rule(list_len(a, 0), a == ll.empty)
- fp.rule(list_len(a, d), [a != ll.empty, b < 1, ll.cons(b, e) == a, list_len(e, c), 1 + c == d])
- assert fp.query(And(list_sum(a, b), list_len(a, c), a != ll.empty, b >= c)) == unsat
- assert fp.query(And(list_sum(a, b), list_len(a, c), a != ll.empty, b < c)) == sat
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement