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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
|
# Copyright (C) 2015, University of British Columbia
# Written (originally) by Mark Greenstreet (13th March, 2014)
# Counter-example generation: Carl Kwan (May 2016)
# Edited by Yan Peng (15th Nov 2016)
#
# License: A 3-clause BSD license.
# See the LICENSE file distributed with ACL2
import re
from z3 import *
from functools import reduce # for Python 2/3 compatibility
def sort(x):
if type(x) == bool: return BoolSort()
elif type(x) == int: return IntSort()
elif type(x) == float: return RealSort()
elif hasattr(x, 'sort'):
if x.sort() == BoolSort(): return BoolSort()
if x.sort() == IntSort(): return IntSort()
if x.sort() == RealSort(): return RealSort()
else:
raise Exception('unknown sort for expression')
class ACL22SMT(object):
class Symbol:
# define the Z3Sym type
z3Sym = Datatype('Symbol')
z3Sym.declare('sym', ('ival', IntSort()))
z3Sym = z3Sym.create()
# operations for creating a dictionary of symbols
count = 0
dict = {}
def intern(self, name):
try: return(self.dict[name])
except:
self.dict[name] = self.z3Sym.sym(self.count)
self.count = self.count + 1
return(self.dict[name])
def interns(self, namelist):
return [ self.intern(name) for name in namelist ]
class status:
def __init__(self, value):
self.value = value
def __str__(self):
if(self.value is True): return 'QED'
elif(self.value.__class__ == 'msg'.__class__): return self.value
else: raise Exception('unknown status?')
def isThm(self):
return(self.value is True)
class atom: # added my mrg, 21 May 2015
def __init__(self, string):
self.who_am_i = string.lower()
def __eq__(self, other):
return(self.who_am_i == other.who_am_i)
def __ne__(self, other):
return(self.who_am_i != other.who_am_i)
def __str__(self):
return(self.who_am_i)
def __init__(self, solver=None):
if(solver != None): self.solver = solver
else: self.solver = Solver()
self.nameNumber = 0
# ---------------------------------------------------------
# Basic Functions
#
# Type declarations
def IntSort(self): return IntSort()
def RealSort(self): return RealSort()
def BoolSort(self): return BoolSort()
# type related functions
def integerp(self, x): return sort(x) == IntSort()
def rationalp(self, x): return sort(x) == RealSort()
def booleanp(self, x): return sort(x) == BoolSort()
# manually casting integer sort to real sort
def to_real(self, x):
if(hasattr(x, 'sort') and x.sort() == IntSort()):
return(ToReal(x))
else:
return(x)
def plus(self, *args): return reduce(lambda x, y: x+y, args)
def times(self, *args): return reduce(lambda x, y: x*y, args)
def reciprocal(self, x):
if(type(x) is int): return(Q(1,x))
elif(type(x) is float): return 1.0/x
# Casting variable of IntSort to real
else: return 1.0/self.to_real(x)
def negate(self, x): return -x
def lt(self, x,y): return self.to_real(x) < self.to_real(y)
def equal(self, x,y): return self.to_real(x) == self.to_real(y)
def notx(self, x): return Not(x)
def implies(self, x, y): return Implies(x,y)
def Qx(self, x, y): return Q(x,y)
def ifx(self, condx, thenx, elsex):
try:
return If(condx, thenx, elsex)
except:
print('If failed')
print('If(' + str(condx) + ', ' + str(thenx) + ', ' + str(elsex) + ')')
raise Exception('giving up')
# def hint_okay(self):
# return False
# -------------------------------------------------------------
# Proof functions and counter-example generation
def get_vars(self, asserts):
"""
Return a list of ArithRef objects of variables appeared
in the list of expressions stored in asserts.
"""
acc = []
def get_vars_ast(v):
if(hasattr(v, "children")):
# hopefully, v is a z3 expression
if v.children() == []:
if not(is_int_value(v) or \
is_rational_value(v) or \
is_true(v) or is_false(v) or \
v.sexpr() == 'nil'):
return [v]
else:
return []
else:
children_lst = []
for nu in v.children():
children_lst += get_vars_ast(nu)
return children_lst
else:
return []
for ast in asserts:
acc += get_vars_ast(ast)
return list(set(acc))
def get_model(self, var_lst):
m = self.solver.model()
dontcare_lst = []
model_lst = []
for var in var_lst:
if m.__getitem__(var) == None:
value = m.eval(var, model_completion = True)
dontcare_lst.append([var, value])
else:
value = m.eval(var)
model_lst.append([var, value])
return [model_lst, dontcare_lst]
def translate_to_acl2(self, model_lst, dontcare_lst):
model_acl2 = []
dontcare_acl2 = []
def translate_value(n, v):
translated_v = str(v)
if (is_algebraic_value(v)):
rt_obj = str(v.sexpr())
rt_obj = rt_obj.replace("root-obj", "cex-root-obj " + n + " state")
translated_v = rt_obj
translated_v = translated_v.replace(",", "")
translated_v = re.sub(r"([a-zA-Z0-9_]+?)\(", r"\(\1 ", translated_v)
translated_v = translated_v.replace(".0", "").replace("False", "nil").replace("True","t")
return translated_v
def translate_model(model):
m = model[0]
name = m.decl().name()
value = model[1]
return "(" + name + " " + translate_value(name, value) + ")"
model_acl2 = [translate_model(model) for model in model_lst]
dontcare_acl2 = [translate_model(model) for model in dontcare_lst]
return [model_acl2, dontcare_acl2]
def proof_counterExample(self):
asserts = self.solver.assertions()
var_lst = self.get_vars(asserts)
[model_lst, dontcare_lst] = self.get_model(var_lst)
[model_acl2, dontcare_acl2] = self.translate_to_acl2(model_lst, dontcare_lst)
print('\'(' + ' '.join(model_acl2+dontcare_acl2) + ')')
print('Without dontcares: ' + '\'(' + ' '.join(model_acl2) + ')')
def proof_success(self):
print('proved')
def proof_fail(self):
print('failed to prove')
# usage prove(claim) or prove(hypotheses, conclusion)
def prove(self, hypotheses, conclusion=None):
if(conclusion is None): claim = hypotheses
else: claim = Implies(hypotheses, conclusion)
self.solver.push()
self.solver.add(Not(claim))
res = self.solver.check()
if res == unsat: self.proof_success()
elif res == sat: self.proof_counterExample()
else: self.proof_fail()
self.solver.pop()
return(self.status(res == unsat))
|
