From 768462c884f7c22f0d92d3da420b5d6d250b6726 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 16 May 2018 17:39:33 -0700 Subject: [PATCH] handle weird quoting of names in recent z3 --- ivy/ivy_to_cpp.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/ivy/ivy_to_cpp.py b/ivy/ivy_to_cpp.py index 61f516f..10b9350 100755 --- a/ivy/ivy_to_cpp.py +++ b/ivy/ivy_to_cpp.py @@ -371,7 +371,7 @@ thunk_counter = 0 def expr_to_z3(expr): - fmla = '(assert ' + slv.formula_to_z3(expr).sexpr().replace('|!1','!1|').replace('\n',' "\n"') + ')' + fmla = '(assert ' + slv.formula_to_z3(expr).sexpr().replace('|!1','!1|').replace('\\|','').replace('\n',' "\n"') + ')' return 'z3::expr(g.ctx,Z3_parse_smtlib2_string(ctx, "{}", sort_names.size(), &sort_names[0], &sorts[0], decl_names.size(), &decl_names[0], &decls[0]))'.format(fmla) @@ -702,7 +702,7 @@ public: for ldf in im.relevant_definitions(ilu.symbols_asts(constraints)): constraints.append(fix_definition(ldf.formula).to_constraint()) for c in constraints: - fmla = slv.formula_to_z3(c).sexpr().replace('|!1','!1|').replace('\n',' "\n"') + fmla = slv.formula_to_z3(c).sexpr().replace('|!1','!1|').replace('\\|','').replace('\n',' "\n"') indent(impl) impl.append(" {}\\\n".format(fmla)) indent(impl) @@ -835,7 +835,7 @@ def emit_action_gen(header,impl,name,action,classname): emit_decl(impl,sym) indent(impl) - impl.append('add("(assert {})");\n'.format(slv.formula_to_z3(pre).sexpr().replace('|!1','!1|').replace('\n',' "\n"'))) + impl.append('add("(assert {})");\n'.format(slv.formula_to_z3(pre).sexpr().replace('|!1','!1|').replace('\\|','').replace('\n',' "\n"'))) # impl.append('__ivy_modelfile << slvr << std::endl;\n') indent_level -= 1 impl.append("}\n");