starting on line number tracking in formulas

This commit is contained in:
Ken McMillan 2019-03-01 18:36:15 -08:00
Родитель c046004e48
Коммит 33200da13f
7 изменённых файлов: 76 добавлений и 56 удалений

Просмотреть файл

@ -21,6 +21,8 @@ class AST(object):
if hasattr(self,'lineno'):
res.lineno = self.lineno
return res
def get_lineno(self):
return self.lineno if hasattr(self,'lineno') else None
class Symbol(AST):
def __init__(self,rep,sort):

Просмотреть файл

@ -85,7 +85,7 @@ def compile_args(self):
return [a.compile() for a in self.args]
for fc,tc in op_pairs:
fc.cmpl = lambda self,tc=tc: tc(*compile_args(self))
fc.cmpl = lambda self,tc=tc: tc(*compile_args(self),ref=self.get_lineno())
class Context(object):
@ -304,7 +304,8 @@ def compile_app(self,old=False):
sym = ivy_logic.Symbol(sym.name,variable_sort(self))
if sym is not None:
sym = old_sym(sym,old)
return (sym)(*args)
res = (sym)(*args,ref=self.get_lineno())
return res
res = compile_field_reference(self.rep,args,self.lineno,old=old)
return res
@ -349,12 +350,13 @@ ivy_ast.NativeExpr.cmpl = cmpl_native_expr
ivy_ast.App.cmpl = ivy_ast.Atom.cmpl = compile_app
def compile_isa(self):
lineno = self.get_lineno()
lhs = self.args[0].compile()
rhs = cmpl_sort(self.args[1].relname)
vars = variables_ast(lhs)
rn = UniqueRenamer(used=[v.name for v in vars])
v = ivy_logic.Variable(rn('V'),rhs)
res = ivy_logic.Exists([v],ivy_logic.pto(lhs.sort,rhs)(lhs,v))
v = ivy_logic.Variable(rn('V'),rhs,ref=lineno)
res = ivy_logic.Exists([v],ivy_logic.pto(lhs.sort,rhs)(lhs,v,ref=lineno),ref=lineno)
return res
ivy_ast.Isa.cmpl = compile_isa
@ -367,13 +369,13 @@ def compile_variable(self):
sort = variable_sort(self)
if ivy_logic.is_topsort(sort):
sort = variable_context.map.get(self.rep,sort)
return ivy_logic.Variable(self.rep,sort)
return ivy_logic.Variable(self.rep,sort,ref=self.get_lineno())
ivy_ast.Variable.cmpl = compile_variable
ivy_ast.ConstantSort.cmpl = lambda self,name: ivy_logic.ConstantSort(name)
ivy_ast.ConstantSort.cmpl = lambda self,name: ivy_logic.ConstantSort(name,ref=self.get_lineno())
ivy_ast.EnumeratedSort.cmpl = lambda self,name: ivy_logic.EnumeratedSort(name,self.extension)
ivy_ast.EnumeratedSort.cmpl = lambda self,name: ivy_logic.EnumeratedSort(name,self.extension,ref=self.get_lineno())
SymbolList.cmpl = lambda self: self.clone([find_symbol(s) for s in self.symbols])
@ -383,14 +385,15 @@ def cquant(q):
def compile_quantifier(self):
bounds = [ivy_logic.Variable(v.rep,variable_sort(v)) for v in self.bounds]
with VariableContext(bounds):
return cquant(self)(bounds,self.args[0].compile())
return cquant(self)(bounds,self.args[0].compile(),ref=self.get_lineno())
ivy_ast.Quantifier.cmpl = compile_quantifier
ivy_ast.NamedBinder.cmpl = lambda self: ivy_logic.NamedBinder(
self.name,
[v.compile() for v in self.bounds],
self.args[0].compile()
self.args[0].compile(),
ref = self.get_lineno()
)
ivy_ast.LabeledFormula.cmpl = lambda self: self.clone([self.label,

Просмотреть файл

@ -407,14 +407,14 @@ def get_node_sort(n):
def report_arc(arc):
v,anode,fmla,lineno = arc[0:4]
res = '\n' + str(lineno) + str(fmla)
res = '\n' + str(fmla.ref or lineno) + str(var_uniq.undo(fmla))
if len(arc) > 4:
idx = arc[4]
term = fmla.args[idx]
res += '\n (position {} is a function from '.format(idx) + str(get_node_sort(v)) + ' to ' + str(term.sort) + ')'
if term in skolem_map:
sm = skolem_map[term]
res += '\n ' + str(sm[1].lineno) + 'skolem function defined by:\n ' + str(sm[0])
res += '\n ' + str(sm[0].ref or sm[1].lineno) + 'skolem function defined by:\n ' + str(var_uniq.undo(sm[0]))
return res
def report_cycle(cycle):
@ -434,9 +434,10 @@ def report_interp_over_var(fmla,lineno,node):
if n is node:
if v in universally_quantified_variables:
lf = universally_quantified_variables[v]
var_msg = '\n{}The quantified variable is {}'.format(lf.lineno,var_uniq.undo(v))
var_msg = '\n{}The quantified variable is {}'.format(v.ref or lf.lineno,var_uniq.undo(v))
iu.dbg('fmla.ref')
report_feu_error('An interpreted symbol is applied to a universally quantified variable:\n'+
'{}{}'.format(lineno,var_uniq.undo(fmla))+var_msg)
'{}{}'.format(fmla.ref or lineno,var_uniq.undo(fmla))+var_msg)
def check_feu(assumes,asserts,macros):
""" Take a list of assumes, assert and macros, and determines
@ -536,7 +537,7 @@ def get_assumes_and_asserts(preconds_only):
for ldf in im.module.labeled_axioms:
if not ldf.temporal:
# print 'axiom : {}'.format(ldf.formula)
# print 'axiom : {} {}'.format(ldf.formula.ref,ldf.formula)
assumes.append((ldf.formula,ldf))
for ldf in im.module.labeled_props:

Просмотреть файл

@ -139,23 +139,23 @@ Symbol.relname = property(lambda self: self)
#Symbol.__hash__ = lambda self: hash(self.name)
#Symbol.__eq__ = lambda self,other: (type(self) == type(other) and self.name == other.name)
Symbol.rename = lambda self,rn: Symbol(rn(self.name),self.sort)
Symbol.prefix = lambda self,s: Symbol(s+self.name,self.sort)
Symbol.rename = lambda self,rn: Symbol(rn(self.name),self.sort,ref=self.ref)
Symbol.prefix = lambda self,s: Symbol(s+self.name,self.sort,ref=self.ref)
Symbol.startswith = lambda self,s: self.name.startswith(s)
Symbol.suffix = lambda self,s: Symbol(self.name+s,self.sort)
Symbol.suffix = lambda self,s: Symbol(self.name+s,self.sort,ref=self.ref)
Symbol.endswith = lambda self,s: self.name.endswith(s)
Symbol.drop_prefix = lambda self,s: Symbol(self.name[len(s):],self.sort)
Symbol.drop_suffix = lambda self,s: Symbol(self.name[0,-len(s)],self.sort)
Symbol.drop_prefix = lambda self,s: Symbol(self.name[len(s):],self.sort,ref=self.ref)
Symbol.drop_suffix = lambda self,s: Symbol(self.name[0,-len(s)],self.sort,ref=self.ref)
Symbol.contains = lambda self,s: (s in self.name)
Symbol.skolem = lambda self: self.prefix('__')
Symbol.is_skolem = lambda self: self.contains('__')
Symbol.deskolem = lambda self,s: self.drop_prefix('__')
Symbol.__call__ = lambda self,*args: App(self,*args) if len(args) > 0 or isinstance(self.sort,FunctionSort) else self
Symbol.__call__ = lambda self,*args,**kwargs: App(self,*args,**kwargs) if len(args) > 0 or isinstance(self.sort,FunctionSort) else self
Symbol.is_relation = lambda self: isinstance(self.sort.rng,lg.BooleanSort)
Symbol.args = property(lambda self : [])
Symbol.is_numeral = lambda self : is_numeral_name(self.name)
Symbol.clone = lambda self,args : self
Symbol.resort = lambda self,sort : Symbol(self.name,sort)
Symbol.resort = lambda self,sort : Symbol(self.name,sort,ref=self.ref)
BooleanSort = lg.BooleanSort
@ -164,7 +164,7 @@ class AST(object):
Base class for abstract syntax.
"""
def clone(self,args):
return type(self)(*args)
return type(self)(*args,ref=self.ref)
#
# def __eq__(self,other):
# return type(self) == type(other) and self.args == other.args
@ -187,9 +187,10 @@ class Let(AST):
return res
class Some(AST):
def __init__(self,*args):
def __init__(self,*args,**kwargs):
assert len(args) >= 2
self.args = args
self.ref = kwargs.get('ref',None)
def __str__(self):
res = 'some ' + str(self.args[0]) + '. ' + str(self.args[1])
if len(self.args) >= 3:
@ -209,16 +210,17 @@ class Some(AST):
def variables(self):
return [self.args[0]]
def clone_binder(self,vs,body):
return Some(*(vs+self.args[1:]))
return Some(*(vs+self.args[1:]),ref=self.ref)
class Definition(AST):
"""
Formula of the form p(X,...,Z) <-> fmla[X,...,Z]
"""
def __init__(self,*args):
def __init__(self,*args,**kwargs):
assert len(args) == 2
self.args = args
self.ref = kwargs.get('ref',None)
def __str__(self):
return ' = '.join([repr(x) for x in self.args])
def defines(self):
@ -255,15 +257,15 @@ lg_ops = [lg.Eq, lg.Not, lg.Globally, lg.Eventually, lg.And, lg.Or, lg.Implies,
for cls in lg_ops:
cls.args = property(lambda self: [ a for a in self])
cls.clone = lambda self,args: type(self)(*args)
cls.clone = lambda self,args: type(self)(*args,ref=self.ref)
for cls in [lg.ForAll, lg.Exists, lg.Lambda]:
cls.clone = lambda self,args: type(self)(self.variables,*args)
cls.clone = lambda self,args: type(self)(self.variables,*args,ref=self.ref)
lg.NamedBinder.clone = lambda self,args: lg.NamedBinder(self.name, self.variables, *args)
lg.NamedBinder.clone = lambda self,args: lg.NamedBinder(self.name, self.variables, *args,ref=self.ref)
lg.NamedBinder.rep = property(lambda self: self)
lg.Apply.clone = lambda self,args: type(self)(self.func, *args)
lg.Apply.clone = lambda self,args: type(self)(self.func, *args, ref=self.ref)
lg.Apply.args = property(lambda self: self.terms)
lg.Apply.rep = property(lambda self: self.func)
lg.Apply.relname = property(lambda self: self.func)
@ -596,7 +598,7 @@ def is_binder(term):
return isinstance(term, (lg.ForAll, lg.Exists, lg.Lambda, lg.NamedBinder, Some))
for b in [lg.ForAll,lg.Exists,lg.Lambda]:
b.clone_binder = lambda self, variables, body, b = b: b(variables,body)
b.clone_binder = lambda self, variables, body, b = b: b(variables,body,ref=self.ref)
lg.NamedBinder.clone_binder = lambda self, variables, body: lg.NamedBinder(self.name,variables,body)
@ -682,8 +684,8 @@ Variable.args = property(lambda self: [])
Variable.clone = lambda self,args: self
Variable.rep = property(lambda self: self.name)
Variable.__call__ = lambda self,*args: App(self,*args) if isinstance(self.sort,FunctionSort) else self
Variable.rename = lambda self,name: Variable(name if isinstance(name,str) else name(self.name),self.sort)
Variable.resort = lambda self,sort : Variable(self.name,sort)
Variable.rename = lambda self,name: Variable(name if isinstance(name,str) else name(self.name),self.sort,ref=self.ref)
Variable.resort = lambda self,sort : Variable(self.name,sort,ref=self.ref)
class Literal(AST):
@ -691,10 +693,11 @@ class Literal(AST):
Either a positive or negative atomic formula. Literals are not
formulas! Use Not(Atom(...)) to get a formula.
"""
def __init__(self, polarity, atom):
def __init__(self, polarity, atom, **kwargs):
# assert isinstance(atom,Atom) or isinstance(atom,And) and len(atom.args) == 0
self.polarity = polarity
self.atom = atom
self.ref = kwargs.get('ref',None)
def __repr__(self):
return "Literal({!r},{!r})".format(self.polarity,self.atom)
def __str__(self):
@ -706,7 +709,7 @@ class Literal(AST):
"""
return Literal(1 - self.polarity, self.atom)
def clone(self,args):
return Literal(self.polarity,*args)
return Literal(self.polarity,*args,ref=self.ref)
def __eq__(self,other):
return type(self) == type(other) and self.polarity == other.polarity and self.args == other.args
@property
@ -1084,8 +1087,8 @@ equals = Symbol('=',RelationSort([lg.TopSort(),lg.TopSort()]))
lg.Eq.relname = property(lambda self: equals)
def Equals(x,y):
return lg.Eq(x,y)
def Equals(x,y,**kwargs):
return lg.Eq(x,y,**kwargs)
def is_eq(ast):
return isinstance(ast,lg.Eq)
@ -1546,7 +1549,7 @@ class VariableUniqifier(object):
if is_binder(fmla):
# save the old bindings
obs = [(v,vmap[v]) for v in fmla.variables if v in vmap]
newvars = tuple(Variable(self.rn(v.name),v.sort) for v in fmla.variables)
newvars = tuple(v.rename(self.rn) for v in fmla.variables)
vmap.update(zip(fmla.variables,newvars))
self.invmap.update(zip(newvars,fmla.variables))
try:
@ -1559,14 +1562,20 @@ class VariableUniqifier(object):
return res
if is_variable(fmla):
if fmla not in vmap:
newv = Variable(self.rn(fmla.name),fmla.sort)
newv = fmla.rename(self.rn)
vmap[fmla] = newv
self.invmap[newv] = fmla
return vmap[fmla]
args = [self.rec(f,vmap) for f in fmla.args]
return fmla.clone(args)
def undo(self,fmla):
return lu.substitute(fmla,self.invmap)
if is_binder(fmla):
newvars = tuple(self.invmap.get(v,v) for v in fmla.variables)
return fmla.clone_binder(newvars,self.undo(fmla.body))
if is_variable(fmla):
return self.invmap.get(fmla,fmla)
return fmla.clone(map(self.undo,fmla.args))
def alpha_avoid(fmla,vs):
""" Alpha-convert a formula so that bound variable names do not clash with vs. """

Просмотреть файл

@ -187,7 +187,7 @@ def rename_ast(ast,subs):
"""
args = [rename_ast(x,subs) for x in ast.args]
if is_app(ast) and not is_named_binder(ast):
return subs.get(ast.rep,ast.rep)(*args)
return subs.get(ast.rep,ast.rep)(*args,ref=ast.ref)
return ast.clone(args)
def normalize_free_variables(ast):

Просмотреть файл

@ -157,7 +157,7 @@ def infer_sorts(t, env=None):
else:
s = env[t.name]
unify(s, t.sort)
return s, lambda: type(t)(t.name, convert_from_sortvars(s))
return s, lambda: type(t)(t.name, convert_from_sortvars(s),ref=t.ref)
elif type(t) is Apply:
func_s, func_t = infer_sorts(t.func, env)
@ -168,13 +168,13 @@ def infer_sorts(t, env=None):
unify(func_s, FunctionSort(*sorts))
return sorts[-1], lambda: Apply(func_t(), *(
x() for x in terms_t
))
),ref=t.ref)
elif type(t) is Eq:
s1, t1 = infer_sorts(t.t1, env)
s2, t2 = infer_sorts(t.t2, env)
unify(s1, s2)
return Boolean, lambda: Eq(t1(), t2())
return Boolean, lambda: Eq(t1(), t2(),ref=t.ref)
elif type(t) is Ite:
s_cond, t_cond = infer_sorts(t.cond, env)
@ -182,7 +182,7 @@ def infer_sorts(t, env=None):
s_else, t_else = infer_sorts(t.t_else, env)
unify(s_cond, Boolean)
unify(s_then, s_else)
return s_then, lambda: Ite(t_cond(), t_then(), t_else())
return s_then, lambda: Ite(t_cond(), t_then(), t_else(),ref=t.ref)
elif type(t) in (Not, And, Or, Implies, Iff):
xys = [infer_sorts(tt, env) for tt in t]
@ -192,7 +192,7 @@ def infer_sorts(t, env=None):
unify(s, Boolean)
return Boolean, lambda: type(t)(*[
x() for x in terms_t
])
],ref=t.ref)
elif type(t) in (ForAll, Exists):
# create a copy of the environment and shadow that quantified
@ -204,7 +204,7 @@ def infer_sorts(t, env=None):
unify(body_s, Boolean)
return Boolean, lambda: type(t)(
[x() for x in vars_t],
body_t(),
body_t(),ref=t.ref
)
elif type(t) is NamedBinder:
@ -221,7 +221,7 @@ def infer_sorts(t, env=None):
lambda: NamedBinder(
t.name,
[x() for x in vars_t],
body_t(),
body_t(),ref=t.ref
)
)

Просмотреть файл

@ -34,7 +34,7 @@ def _itemgetter(x):
_class_template = '''\
class {typename}(object):
__slots__ = ('_tup')
__slots__ = ('_tup','_ref')
_meta_fields = {meta_field_names!r}
_sub_fields = {sub_field_names!r}
@ -52,8 +52,9 @@ class {typename}(object):
"""
return args
def __init__(self, {meta_arg_list_with_defaults}{sub_arg_list}):
self._tup = tuple(type(self)._preprocess_({meta_arg_list}{sub_arg_list}))
def __init__(self, {constructor_arg_list}):
self._tup = tuple(type(self)._preprocess_({tuple_arg_list}))
self._ref = kwargs.get('ref',None)
def __repr__(self):
"""Return a nicely formatted representation string"""
@ -108,6 +109,10 @@ class {typename}(object):
def __setstate__(self, state):
self._tup = state['_tup']
@property
def ref(self):
return self._ref
{field_defs}
'''
@ -137,9 +142,9 @@ def recstruct(typename, meta_field_names, sub_field_names, verbose=False):
# Validate the field names.
meta_field_names = _preprocess_names(meta_field_names)
meta_arg_list_with_defaults = ''.join(x + ', ' for x in meta_field_names)
meta_arg_list_with_defaults = tuple(meta_field_names)
meta_field_names = [s.split('=')[0] for s in meta_field_names] #strip off default values
meta_arg_list = ''.join(x + ', ' for x in meta_field_names)
meta_arg_list = tuple(meta_field_names)
sub_field_names = _preprocess_names(sub_field_names)
names = [typename] + meta_field_names
if len(sub_field_names) > 0 and sub_field_names[-1][0] == '*':
@ -168,7 +173,8 @@ def recstruct(typename, meta_field_names, sub_field_names, verbose=False):
# Fill-in the class template
n_meta = len(meta_field_names)
sub_arg_list = ', '.join(sub_field_names)
constructor_arg_list = ', '.join(meta_arg_list_with_defaults+tuple(sub_field_names)+('**kwargs',))
tuple_arg_list = ', '.join(meta_arg_list+tuple(sub_field_names))
field_defs = '\n'.join(
[_meta_field_template.format(index=index, name=name)
for index, name in enumerate(meta_field_names)] +
@ -184,9 +190,8 @@ def recstruct(typename, meta_field_names, sub_field_names, verbose=False):
meta_field_names=meta_field_names,
sub_field_names=sub_field_names,
n_meta=n_meta,
meta_arg_list=meta_arg_list,
meta_arg_list_with_defaults=meta_arg_list_with_defaults,
sub_arg_list=sub_arg_list,
constructor_arg_list = constructor_arg_list,
tuple_arg_list = tuple_arg_list,
field_defs=field_defs,
)