Z3: translation validation for dom_simplify

z3_dom_simplify_tv.patch

diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index b5ed1a070..952f61e29 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -47,18 +47,18 @@ def init_project_def():
     add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
     add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
     add_lib('bit_blaster', ['rewriter', 'params'], 'ast/rewriter/bit_blaster')
-    add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
-    add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
     add_lib('mbp', ['model', 'simplex'], 'qe/mbp')
     add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern'], 'sat/smt')
     add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
-    add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
-    add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
 
     add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', 'solver_assertions',
                     'substitution', 'grobner', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp'])
+    add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern', 'smt'], 'tactic/core')
+    add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
+    add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
     add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
+    add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 719de8911..91247bebb 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -22,6 +22,9 @@ Notes:
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "tactic/core/dom_simplify_tactic.h"
+#include "smt_params.h"
+#include "smt_kernel.h"
+
 
 /**
    \brief compute a post-order traversal for e.
@@ -388,6 +391,16 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         change = false;
         ++n;
 
+        expr_ref prev(m);
+        {
+            unsigned sz = g.size();
+            svector<expr*> gs;
+            for (unsigned i = 0; i < sz; ++i) {
+                gs.push_back(g.form(i));
+            }
+            prev = m.mk_and(sz, gs.data());
+        }
+
         // go forwards
         m_forward = true;
         if (!init(g)) return;
@@ -407,6 +420,25 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         }
         pop(scope_level());
 
+        {
+            expr_ref after(m);
+            svector<expr*> gs;
+            unsigned sz = g.size();
+            for (unsigned i = 0; i < sz; ++i) {
+                gs.push_back(g.form(i));
+            }
+            after = m.mk_and(sz, gs.data());
+            smt_params fp;
+            smt::kernel solver(m, fp);
+            expr_ref tmp(m.mk_not(m.mk_eq(prev, after)), m);
+            solver.assert_expr(tmp);
+            if (solver.check() == l_true) {
+                std::cerr << "dom simplify: wrong fwd transformation: " << mk_pp(prev, m) << " -> " << mk_pp(after, m) << std::endl;
+                exit(-1);
+            }
+            prev = std::move(after);
+        }
+
         // go backwards
         m_forward = false;
         if (!init(g)) return;
@@ -427,6 +459,24 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
             g.update(i, r, new_pr, g.dep(i));
         }
         pop(scope_level());
+
+        {
+            expr_ref after(m);
+            svector<expr*> gs;
+            unsigned sz = g.size();
+            for (unsigned i = 0; i < sz; ++i) {
+                gs.push_back(g.form(i));
+            }
+            after = m.mk_and(sz, gs.data());
+            smt_params fp;
+            smt::kernel solver(m, fp);
+            expr_ref tmp(m.mk_not(m.mk_eq(prev, after)), m);
+            solver.assert_expr(tmp);
+            if (solver.check() == l_true) {
+                std::cerr << "dom simplify: wrong bwd transformation: " << mk_pp(prev, m) << " -> " << mk_pp(after, m) << std::endl;
+                exit(-1);
+            }
+        }
     }
     SASSERT(scope_level() == 0);
 }