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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
|
# This script illustrates uses of proof logs over the Python interface.
from z3 import *
example1 = """
(declare-sort T)
(declare-fun subtype (T T) Bool)
;; subtype is reflexive
(assert (forall ((x T)) (subtype x x)))
;; subtype is antisymmetric
(assert (forall ((x T) (y T)) (=> (and (subtype x y)
(subtype y x))
(= x y))))
;; subtype is transitive
(assert (forall ((x T) (y T) (z T)) (=> (and (subtype x y)
(subtype y z))
(subtype x z))))
;; subtype has the tree-property
(assert (forall ((x T) (y T) (z T)) (=> (and (subtype x z)
(subtype y z))
(or (subtype x y)
(subtype y x)))))
;; now we define a simple example using the axiomatization above.
(declare-const obj-type T)
(declare-const int-type T)
(declare-const real-type T)
(declare-const complex-type T)
(declare-const string-type T)
;; we have an additional axiom: every type is a subtype of obj-type
(assert (forall ((x T)) (subtype x obj-type)))
(assert (subtype int-type real-type))
(assert (subtype real-type complex-type))
(assert (not (subtype string-type real-type)))
(declare-const root-type T)
(assert (subtype obj-type root-type))
"""
def monitor_plain():
print("Monitor all inferred clauses")
s = Solver()
s.from_string(example1)
onc = OnClause(s, lambda pr, clause : print(pr, clause))
print(s.check())
def log_instance(pr, clause):
if pr.decl().name() == "inst":
q = pr.arg(0).arg(0) # first argument is Not(q)
for ch in pr.children():
if ch.decl().name() == "bind":
print("Binding")
print(q)
print(ch.children())
break
def monitor_instances():
print("Monitor just quantifier bindings")
s = Solver()
s.from_string(example1)
onc = OnClause(s, log_instance)
print(s.check())
def monitor_with_proofs():
print("Monitor clauses annotated with detailed justifications")
set_param(proof=True)
s = Solver()
s.from_string(example1)
onc = OnClause(s, lambda pr, clause : print(pr, clause))
print(s.check())
def monitor_new_core():
print("Monitor proof objects from the new core")
set_param("sat.euf", True)
set_param("tactic.default_tactic", "sat")
s = Solver()
s.from_string(example1)
onc = OnClause(s, lambda pr, clause : print(pr, clause))
print(s.check())
if __name__ == "__main__":
monitor_plain()
monitor_instances()
monitor_new_core()
# Monitoring with proofs cannot be done in the same session
# monitor_with_proofs()
|
