• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Aug 18th, 2019 65 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. from z3 import *
2.
3. def test_list_elt_gt_1():
4.   ll = Datatype('ll')
5.   ll.declare('empty')
6.   ll.declare('cons', ('car', IntSort()), ('cdr', ll))
7.   ll = ll.create()
8.   list_sum = Function('list_sum', ll, IntSort(), BoolSort())
9.   list_len = Function('list_len', ll, IntSort(), BoolSort())
10.   a,e = Consts('a e', ll)
11.   b,c,d = Ints('b c d')
12.
13.   fp = Fixedpoint()
14.   fp.declare_var(a,b,c,d,e)
15.   fp.register_relation(list_sum, list_len)
16.   fp.rule(list_sum(a, 0), a == ll.empty)
17.   fp.rule(list_sum(a, d), [a != ll.empty, b < 1, ll.cons(b, e) == a, list_sum(e, c), b + c == d])
18.   fp.rule(list_len(a, 0), a == ll.empty)
19.   fp.rule(list_len(a, d), [a != ll.empty, b < 1, ll.cons(b, e) == a, list_len(e, c), 1 + c == d])
20.   assert fp.query(And(list_sum(a, b), list_len(a, c), a != ll.empty, b >= c)) == unsat
21.   assert fp.query(And(list_sum(a, b), list_len(a, c), a != ll.empty, b < c)) == sat
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top