From 0be3c4b99ee63793b0b3342dd3a5aed32d639391 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre=20Cr=C3=A9gut?= Date: Tue, 31 Jul 2018 08:50:13 +0200 Subject: [PATCH] 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 --- congress/z3/z3theory.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/congress/z3/z3theory.py b/congress/z3/z3theory.py index 8481f55c7..c4c257edb 100644 --- a/congress/z3/z3theory.py +++ b/congress/z3/z3theory.py @@ -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):