testbuilder/solving.py at master · andyg0808/testbuilder · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
from z3 import *
import timeit

set_param("proof", "true")

def run_direct():
    pyname_i = Int("pyname_i")
    ret = Int("ret")
    x = Int("x")
    y = Int("y")
    conditioned = Function("conditioned", IntSort(), IntSort())
    run_func = Function("run_func", IntSort(), IntSort())
    s = Solver()
    s.add(
        ForAll(
            [pyname_i],
            Exists(
                [ret],
                And(
                    conditioned(pyname_i) == ret,
                    Or(And(pyname_i > 4, ret == 6), And(Not(pyname_i > 4), ret == 14)),
                ),
            ),
        )
    )
    # s.add(ForAll([pyname_i], conditioned(pyname_i) == If(pyname_i > 4, 6, 14)))
    # s.add(
    #     ForAll(
    #         [pyname_i],
    #         Exists(
    #             [ret],
    #             And(run_func(pyname_i) == ret, ret == pyname_i * conditioned(pyname_i)),
    #         ),
    #     )
    # )
    s.add(ForAll([pyname_i], run_func(pyname_i) == pyname_i * conditioned(pyname_i)))
    # s.add(conditioned(34) == x)
    s.add(run_func(2) == x)
    s.check()
    # print(s.model())

def run_function():
    pyname_i = Int("pyname_i")
    ret = Int("ret")
    x = Int("x")
    y = Int("y")
    conditioned = Function("conditioned", IntSort(), IntSort())
    run_func = Function("run_func", IntSort(), IntSort())
    s = Solver()

    s.add(ForAll([pyname_i], conditioned(pyname_i) == If(pyname_i > 4, 6, 14)))
    s.add(ForAll([pyname_i], run_func(pyname_i) == pyname_i * conditioned(pyname_i)))
    # s.add(conditioned(34) == x)
    s.add(run_func(2) == x)
    s.check()
    # print(s.model())

print("function")
print(timeit.timeit("run_function()", number=100, globals=globals()))
print("direct")
print(timeit.timeit("run_direct()", number=100, globals=globals()))