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:
Pierre Crégut 2018-07-31 08:50:13 +02:00
parent c86a2f5d0c
commit 0be3c4b99e
1 changed files with 2 additions and 1 deletions

View File

@ -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):