bugfix: order of variables in quantified Z3 terms
This fix guarantees that variables are quantified in the right order. This is important for queries otherwise the order of the columns in the answers may be arbitrary. The bug was mostly visible on Python 3 due to dictionnary implementation details. Change-Id: Ida715517a2e1febc64d87b07b54c02c815eabfce
This commit is contained in:
parent
c86a2f5d0c
commit
0be3c4b99e
|
@ -322,6 +322,7 @@ class Z3Context(object):
|
|||
As it is used mainly for rules, the head is distinguished.
|
||||
"""
|
||||
variables = {} # type: Dict[str, z3.Const]
|
||||
z3vars = []
|
||||
|
||||
def compile_expr(expr, translator):
|
||||
"""Compiles an expression to Z3"""
|
||||
|
@ -331,6 +332,7 @@ class Z3Context(object):
|
|||
return variables[name]
|
||||
var = Z3OPT.Const(name, translator.type())
|
||||
variables[name] = var
|
||||
z3vars.append(var)
|
||||
return var
|
||||
elif isinstance(expr, ast.ObjectConstant):
|
||||
return translator.to_z3(expr.name)
|
||||
|
@ -366,7 +368,6 @@ class Z3Context(object):
|
|||
z3body = [compile_atom(atom) for atom in body]
|
||||
# We give back variables explicitely and do not rely on declare_var and
|
||||
# abstract. Otherwise rules are cluttered with useless variables.
|
||||
z3vars = [v for v in six.itervalues(variables)]
|
||||
return (z3vars, z3head, z3body)
|
||||
|
||||
def compile_rule(self, theory, rule):
|
||||
|
|
Loading…
Reference in New Issue