update release notes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

RELEASE_NOTES.md

@@ -20,6 +20,13 @@ Version 4.12.2
   benchmarks created by converting bit-vector semantics to integer 
   reasoning.
 - change API function Z3_mk_real to take two int64 as arguments instead of int.
+- Add _simplifiers_ as optional incremental pre-processing to solvers.
+  They are exposed over the SMTLIB API using the command [`set-simplifier`](https://microsoft.github.io/z3guide/docs/strategies/simplifiers).
+  Simplifiers are similar to tactics, but they operate on solver state that can be incrementally updated. 
+  The exposed simplifiers cover all the pre-processing techniques used internally with some additional simplifiers, such as `solve-eqs`
+  and `elim-predicates` that go beyond incremental pre-processing used internally. The advantage of using `solve-eqs` during pre-processing
+  can be significant. Incremental pre-processing simplification using `solve-eqs` and other simplifiers that change interpretations 
+  was not possible before.
 
 Version 4.12.1
 ==============

doc/mk_tactic_doc.py

@@ -65,7 +65,6 @@ def extract_simplifier_doc(ous, f):
             m = is_simplifier.search(line)
             if m:
                 generate_simplifier_doc(ous, m.group(1), m.group(2))
-                return
 
 def find_tactic_name(path):
     with open(path) as ins:
@@ -76,7 +75,16 @@ def find_tactic_name(path):
     print(f"no tactic in {path}")
     return ""
 
-def presort_files():
+def find_simplifier_name(path):
+    with open(path) as ins:
+        for line in ins:
+            m = is_simplifier.search(line)
+            if m:
+                return m.group(1)
+    print(f"no simplifier in {path}")
+    return ""
+
+def presort_files(find_fn):
     tac_files = []
     for root, dirs, files in os.walk(doc_path("../src")):
         for f in files:
@@ -84,16 +92,16 @@ def presort_files():
                 continue
             if f.endswith("tactic.h") or "simplifiers" in root:
                 tac_files += [(f, os.path.join(root, f))]
-    tac_files = sorted(tac_files, key = lambda x: find_tactic_name(x[1]))
+    tac_files = sorted(tac_files, key = lambda x: find_fn(x[1]))
     return tac_files
     
     
 def help(ous):
     ous.write("---\n")
     ous.write("title: Tactics Summary\n")
-    ous.write("sidebar_position: 5\n")
+    ous.write("sidebar_position: 6\n")
     ous.write("---\n")
-    tac_files = presort_files()
+    tac_files = presort_files(find_tactic_name)
     for file, path in tac_files:
         extract_tactic_doc(ous, path)
 
@@ -101,10 +109,10 @@ def help(ous):
 
 def help_simplifier(ous):
     ous.write("---\n")
-    ous.write("title: Simplifier Summary\n")
+    ous.write("title: Simplifiers Summary\n")
-    ous.write("sidebar_position: 6\n")
+    ous.write("sidebar_position: 7\n")
     ous.write("---\n")
-    tac_files = presort_files()
+    tac_files = presort_files(find_simplifier_name)
     for file, path in tac_files:
         extract_simplifier_doc(ous, path)
 

scripts/mk_genfile_common.py

@@ -743,7 +743,7 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
     # First pass will just generate the tactic factories
     fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, CODE) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, [](ast_manager &m, const params_ref &p) { return CODE; }))\n')
     fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n')
-    fout.write('#define ADD_SIMPLIFIER_CMD(NAME, DESCR, FUNCTION) ctx.insert(alloc(simplifier_cmd, symbol(NAME), DESCR, FUNCTION))\n')
+    fout.write('#define ADD_SIMPLIFIER_CMD(NAME, DESCR, CODE) ctx.insert(alloc(simplifier_cmd, symbol(NAME), DESCR, [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return CODE; }))\n')
     fout.write('void install_tactics(tactic_manager & ctx) {\n')
     for data in ADD_TACTIC_DATA:
         fout.write('  ADD_TACTIC_CMD("%s", "%s", %s);\n' % data)

src/api/api_qe.cpp

@@ -25,7 +25,7 @@ Notes:
 #include "api/api_model.h"
 #include "api/api_ast_map.h"
 #include "api/api_ast_vector.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "muz/spacer/spacer_util.h"
 
 extern "C"

src/ast/simplifiers/CMakeLists.txt

@@ -31,6 +31,11 @@ z3_add_component(simplifiers
     substitution
   TACTIC_HEADERS
     bit_blaster.h
+    bit2int.h
+    elim_bounds.h
+    elim_term_ite.h
+    pull_nested_quantifiers.h
+    push_ite.h
+    refine_inj_axiom.h
     rewriter_simplifier.h
-
 )

src/ast/simplifiers/bit2int.h

@@ -42,3 +42,6 @@ public:
     bool supports_proofs() const override { return true; }
 };
 
+/*
+  ADD_SIMPLIFIER("bit2int", "simplify bit2int expressions.", "alloc(bit2int_simplifier, m, p, s)")
+ */

src/ast/simplifiers/bit_blaster.h

@@ -33,7 +33,7 @@ public:
         m_rewriter(m, p) {
         updt_params(p);
     }
-    char const* name() const override { return "bit-blaster"; }
+    char const* name() const override { return "bit-blast"; }
     void updt_params(params_ref const & p) override;
     void collect_param_descrs(param_descrs & r) override;
     void reduce() override;
@@ -50,5 +50,5 @@ public:
 };
 
 /*
-  ADD_SIMPLIFIER("bit-blaster", "reduce bit-vector expressions into SAT.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bit_blaster_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("bit-blast", "reduce bit-vector expressions into SAT.", "alloc(bit_blaster_simplifier, m, p, s)")
 */

src/ast/simplifiers/elim_bounds.h

@@ -43,3 +43,6 @@ public:
     }
 };
 
+/*
+  ADD_SIMPLIFIER("cheap-fourier-motzkin", "eliminate variables from quantifiers using partial Fourier-Motzkin elimination.", "alloc(elim_bounds_simplifier, m, p, s)")
+ */

src/ast/simplifiers/elim_term_ite.h

@@ -49,3 +49,6 @@ public:
     void pop(unsigned n) override { m_rewriter.pop(n); m_df.pop(n); dependent_expr_simplifier::pop(n); }
 };
 
+/*
+  ADD_SIMPLIFIER("elim-term-ite", "eliminate if-then-else term by hoisting them top top-level.", "alloc(elim_term_ite_simplifier, m, p, s)")
+*/

src/ast/simplifiers/pull_nested_quantifiers.h

@@ -46,3 +46,7 @@ public:
 
     bool supports_proofs() const override { return true; }
 };
+
+/*
+  ADD_SIMPLIFIER("pull-nested-quantifiers", "pull nested quantifiers to top-level.", "alloc(pull_nested_quantifiers_simplifier, m, p, s)")
+*/

src/ast/simplifiers/push_ite.h

@@ -64,3 +64,9 @@ public:
     }
 };
 
+/*
+  ADD_SIMPLIFIER("push-app-ite-conservative", "Push functions over if-then else.", "alloc(push_ite_simplifier, m, p, s, true)")
+  ADD_SIMPLIFIER("push-app-ite", "Push functions over if-then else.", "alloc(push_ite_simplifier, m, p, s, false)")
+  ADD_SIMPLIFIER("ng-push-app-ite-conservative", "Push functions over if-then-else within non-ground terms only.", "alloc(ng_push_ite_simplifier, m, p, s, true)")
+  ADD_SIMPLIFIER("ng-push-app-ite", "Push functions over if-then-else within non-ground terms only.", "alloc(ng_push_ite_simplifier, m, p, s, false)")
+*/

src/ast/simplifiers/refine_inj_axiom.h

@@ -42,3 +42,7 @@ public:
         }
     }
 };
+
+/*
+  ADD_SIMPLIFIER("refine-injectivity", "refine injectivity axioms.", "alloc(refine_inj_axiom_simplifier, m, p, s)")
+*/

src/ast/simplifiers/rewriter_simplifier.h

@@ -55,5 +55,5 @@ public:
 };
 
 /*
-  ADD_SIMPLIFIER("simplify", "apply simplification rules.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(rewriter_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("simplify", "apply simplification rules.", "alloc(rewriter_simplifier, m, p, s)")
  */

src/muz/base/dl_rule.h

@@ -28,7 +28,7 @@ Revision History:
 #include "ast/rewriter/ast_counter.h"
 #include "ast/rewriter/rewriter.h"
 #include "muz/base/hnf.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/rewriter/label_rewriter.h"

src/muz/spacer/spacer_legacy_mbp.cpp

@@ -35,7 +35,7 @@ Notes:
 #include "ast/rewriter/expr_replacer.h"
 #include "model/model_smt2_pp.h"
 #include "ast/scoped_proof.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "muz/spacer/spacer_qe_project.h"
 #include "model/model_pp.h"
 #include "ast/rewriter/expr_safe_replace.h"

src/muz/spacer/spacer_legacy_mev.cpp

@@ -23,7 +23,7 @@ Copyright (c) 2017 Arie Gurfinkel
 #include "ast/rewriter/expr_replacer.h"
 #include "model/model_smt2_pp.h"
 #include "ast/scoped_proof.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "muz/spacer/spacer_qe_project.h"
 #include "model/model_pp.h"
 #include "ast/rewriter/expr_safe_replace.h"

src/muz/spacer/spacer_qe_project.cpp

@@ -36,7 +36,7 @@ Revision History:
 #include "model/model_pp.h"
 
 #include "qe/qe.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 
 #include "muz/spacer/spacer_mev_array.h"
 #include "muz/spacer/spacer_qe_project.h"

src/muz/spacer/spacer_util.cpp

@@ -51,7 +51,7 @@ Notes:
 #include "model/model_smt2_pp.h"
 #include "smt/params/smt_params.h"
 
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "qe/mbp/mbp_plugin.h"
 #include "qe/mbp/mbp_term_graph.h"
 #include "qe/qe_mbp.h"

src/muz/tab/tab_context.cpp

@@ -23,7 +23,7 @@ Revision History:
 #include "muz/base/dl_context.h"
 #include "muz/transforms/dl_mk_rule_inliner.h"
 #include "smt/smt_kernel.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "ast/rewriter/bool_rewriter.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/datatype_decl_plugin.h"

src/qe/lite/CMakeLists.txt

@@ -1,9 +1,9 @@
 z3_add_component(qe_lite
   SOURCES
-    qe_lite.cpp
+    qe_lite_tactic.cpp
   COMPONENT_DEPENDENCIES
     tactic
     mbp
   TACTIC_HEADERS
-    qe_lite.h
+    qe_lite_tactic.h
 )

src/qe/lite/qe_lite_tactic.cpp

@@ -34,7 +34,7 @@ Revision History:
 #include "ast/datatype_decl_plugin.h"
 #include "tactic/tactical.h"
 #include "qe/mbp/mbp_solve_plugin.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "tactic/dependent_expr_state_tactic.h"
 
 
@@ -2444,9 +2444,9 @@ namespace {
 }
 
 tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
-    return alloc(dependent_expr_state_tactic, m, p, mk_qe_lite_simplifer);
+    return alloc(dependent_expr_state_tactic, m, p, mk_qe_lite_simplifier);
 }
 
-dependent_expr_simplifier* mk_qe_lite_simplifer(ast_manager& m, params_ref const& p, dependent_expr_state& st) {
+dependent_expr_simplifier* mk_qe_lite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st) {
     return alloc(qe_lite_simplifier, m, p, st);
 }

src/qe/lite/qe_lite_tactic.h

@@ -68,8 +68,10 @@ public:
 };
 
 tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+dependent_expr_simplifier* mk_qe_lite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st);
+
 /*
   ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)")
+  ADD_SIMPLIFIER("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_simplifier(m, p, s)")
 */
-
-dependent_expr_simplifier* mk_qe_lite_simplifer(ast_manager& m, params_ref const& p, dependent_expr_state& st);

src/qe/qe_mbp.cpp

@@ -30,7 +30,7 @@ Revision History:
 #include "qe/mbp/mbp_arith.h"
 #include "qe/mbp/mbp_arrays.h"
 #include "qe/mbp/mbp_datatypes.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "model/model_pp.h"
 #include "model/model_evaluator.h"
 

src/sat/smt/q_solver.cpp

@@ -23,7 +23,7 @@ Author:
 #include "sat/smt/q_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/sat_th.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include <iostream>
 
 

src/solver/assertions/asserted_formulas.h

@@ -38,7 +38,7 @@ Revision History:
 #include "ast/normal_forms/elim_term_ite.h"
 #include "ast/pattern/pattern_inference.h"
 #include "smt/params/smt_params.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 
 
 class asserted_formulas {

src/solver/solver_preprocess.cpp

@@ -42,7 +42,7 @@ Notes:
 #include "ast/simplifiers/cnf_nnf.h"
 #include "smt/params/smt_params.h"
 #include "solver/solver_preprocess.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 
 void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) {
 
@@ -53,7 +53,7 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep
     if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st));
     if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st));
     if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st));
-    if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st));
+    if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifier(m, p, st));
     if (smtp.m_pull_nested_quantifiers) s.add_simplifier(alloc(pull_nested_quantifiers_simplifier, m, p, st));
     if (smtp.m_max_bv_sharing) s.add_simplifier(mk_max_bv_sharing(m, p, st));
     if (smtp.m_refine_inj_axiom) s.add_simplifier(alloc(refine_inj_axiom_simplifier, m, p, st));

src/tactic/arith/bound_simplifier_tactic.h

@@ -38,5 +38,5 @@ inline tactic* mk_bound_simplifier_tactic(ast_manager& m, params_ref const& p =
 
 /*
   ADD_TACTIC("bound-simplifier", "Simplify arithmetical expressions modulo bounds.", "mk_bound_simplifier_tactic(m, p)")
-  ADD_SIMPLIFIER("bound-simplifier", "Simplify arithmetical expressions modulo bounds.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bound_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("bound-simplifier", "Simplify arithmetical expressions modulo bounds.", "alloc(bound_simplifier, m, p, s)")
 */

src/tactic/arith/card2bv_tactic.h

@@ -69,5 +69,5 @@ inline tactic* mk_card2bv_tactic(ast_manager& m, params_ref const& p = params_re
 
 /*
   ADD_TACTIC("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "mk_card2bv_tactic(m, p)")
-  ADD_SIMPLIFIER("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(card2bv, m, p, s); }")
+  ADD_SIMPLIFIER("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "alloc(card2bv, m, p, s)")
 */

src/tactic/arith/propagate_ineqs_tactic.h

@@ -64,6 +64,6 @@ inline tactic* mk_propagate_ineqs_tactic(ast_manager& m, params_ref const& p = p
 
 /*
   ADD_TACTIC("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", "mk_propagate_ineqs_tactic(m, p)")
-  ADD_SIMPLIFIER("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bound_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", "alloc(bound_simplifier, m, p, s)")
 */
 

src/tactic/bv/CMakeLists.txt

@@ -8,7 +8,6 @@ z3_add_component(bv_tactics
     bv_bound_chk_tactic.cpp
     bv_bounds_tactic.cpp
     bv_size_reduction_tactic.cpp
-    bv_slice_tactic.cpp
     dt2bv_tactic.cpp
     elim_small_bv_tactic.cpp
   COMPONENT_DEPENDENCIES

src/tactic/bv/bv_bounds_tactic.h

@@ -46,7 +46,7 @@ tactic * mk_dom_bv_bounds_tactic(ast_manager & m, params_ref const & p = params_
 /*
   ADD_TACTIC("propagate-bv-bounds", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_bv_bounds_tactic(m, p)")
 
-  ADD_SIMPLIFIER("propagate-bv-bounds", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_bv_bounds_simplifier")
+  ADD_SIMPLIFIER("propagate-bv-bounds", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_bv_bounds_simplifier(m, p, s)")
 
   ADD_TACTIC("propagate-bv-bounds2", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_dom_bv_bounds_tactic(m, p)")
 

src/tactic/bv/bv_slice_tactic.cpp

@@ -15,12 +15,4 @@ Author:
 
 --*/
 
-#include "ast/simplifiers/bv_slice.h"
-#include "tactic/tactic.h"
-#include "tactic/dependent_expr_state_tactic.h"
-#include "tactic/bv/bv_slice_tactic.h"
 
-tactic* mk_bv_slice_tactic(ast_manager& m, params_ref const& p) {
-    return alloc(dependent_expr_state_tactic, m, p,
-                 [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bv::slice, m, s); });
-}

src/tactic/bv/bv_slice_tactic.h

@@ -45,13 +45,22 @@ simplification
 #pragma once
 
 #include "util/params.h"
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/bv_slice.h"
+
 class ast_manager;
 class tactic;
 
-tactic * mk_bv_slice_tactic(ast_manager & m, params_ref const & p = params_ref());
+inline tactic* mk_bv_slice_tactic(ast_manager& m, params_ref const& p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p,
+                 [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bv::slice, m, s); });
+}
+
 
 /*
   ADD_TACTIC("bv-slice", "simplify using bit-vector slices.", "mk_bv_slice_tactic(m, p)")
+  ADD_SIMPLIFIER("bv-slice", "simplify using bit-vector slices.", "alloc(bv::slice, m, s)")
 */
 
 

src/tactic/core/demodulator_tactic.h

@@ -100,5 +100,5 @@ inline tactic * mk_demodulator_tactic(ast_manager& m, params_ref const& p = para
 
 /*
   ADD_TACTIC("demodulator", "extracts equalities from quantifiers and applies them to simplify.", "mk_demodulator_tactic(m, p)")
-  ADD_SIMPLIFIER("demodulator", "extracts equalities from quantifiers and applies them to simplify.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(demodulator_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("demodulator", "extracts equalities from quantifiers and applies them to simplify.", "alloc(demodulator_simplifier, m, p, s)")
 */

src/tactic/core/distribute_forall_tactic.h

@@ -50,6 +50,6 @@ inline tactic * mk_distribute_forall_tactic(ast_manager& m, params_ref const& p
 
 /*
   ADD_TACTIC("distribute-forall", "distribute forall over conjunctions.", "mk_distribute_forall_tactic(m, p)")
-  ADD_SIMPLIFIER("distribute-forall", "distribute forall over conjunctions.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(distribute_forall_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("distribute-forall", "distribute forall over conjunctions.", "alloc(distribute_forall_simplifier, m, p, s)")
 */
 

src/tactic/core/dom_simplify_tactic.h

@@ -56,6 +56,6 @@ inline tactic* mk_dom_simplify_tactic(ast_manager& m, params_ref const& p) {
 
 /*
 ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)")
-ADD_SIMPLIFIER("dom-simplify", "apply dominator simplification rules.", "[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return alloc(dominator_simplifier, m, s, mk_expr_substitution_simplifier(m), p); }")
+ADD_SIMPLIFIER("dom-simplify", "apply dominator simplification rules.", "alloc(dominator_simplifier, m, s, mk_expr_substitution_simplifier(m), p)")
 */
 

src/tactic/core/elim_uncnstr2_tactic.h

@@ -118,5 +118,5 @@ inline tactic * mk_elim_uncnstr2_tactic(ast_manager & m, params_ref const & p =
 
 /*
   ADD_TACTIC("elim-uncnstr2", "eliminate unconstrained variables.", "mk_elim_uncnstr2_tactic(m, p)")
-  ADD_SIMPLIFIER("elim-unconstrained", "eliminate unconstrained variables.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(elim_unconstrained, m, s); }")
+  ADD_SIMPLIFIER("elim-unconstrained", "eliminate unconstrained variables.", "alloc(elim_unconstrained, m, s)")
 */

src/tactic/core/eliminate_predicates_tactic.h

@@ -63,6 +63,6 @@ inline tactic * mk_eliminate_predicates_tactic(ast_manager& m, params_ref const&
 }
 
 /*
-  ADD_TACTIC("elim-predicates", "eliminate predicates.", "mk_eliminate_predicates_tactic(m, p)")
+  ADD_TACTIC("elim-predicates", "eliminate predicates, macros and implicit definitions.", "mk_eliminate_predicates_tactic(m, p)")
-  ADD_SIMPLIFIER("elim-predicates", "eliminate predicates.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(eliminate_predicates, m, s); }")
+  ADD_SIMPLIFIER("elim-predicates", "eliminate predicates, macros and implicit definitions.", "alloc(eliminate_predicates, m, s)")
 */

src/tactic/core/euf_completion_tactic.h

@@ -33,6 +33,9 @@ is extracted.
 #pragma once
 
 #include "util/params.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/euf_completion.h"
+
 class ast_manager;
 class tactic;
 
@@ -40,6 +43,7 @@ tactic * mk_euf_completion_tactic(ast_manager & m, params_ref const & p = params
 
 /*
   ADD_TACTIC("euf-completion", "simplify using equalities.", "mk_euf_completion_tactic(m, p)")
+  ADD_SIMPLIFIER("euf-completion", "simplify modulo congruence closure.", "alloc(euf::completion, m, s)")
 */
 
 

src/tactic/core/propagate_values2_tactic.h

@@ -55,5 +55,5 @@ inline tactic * mk_propagate_values2_tactic(ast_manager & m, params_ref const &
 
 /*
   ADD_TACTIC("propagate-values2", "propagate constants.", "mk_propagate_values2_tactic(m, p)")
-  ADD_SIMPLIFIER("propagate-values", "propagate constants.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(propagate_values, m, p, s); }")
+  ADD_SIMPLIFIER("propagate-values", "propagate constants.", "alloc(propagate_values, m, p, s)")
 */

src/tactic/core/reduce_args_tactic.h

@@ -79,7 +79,7 @@ inline tactic* mk_reduce_args_tactic2(ast_manager& m, params_ref const& p = para
 }
 /*
   ADD_TACTIC("reduce-args2", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "mk_reduce_args_tactic2(m, p)")
-  ADD_SIMPLIFIER("reduce-args", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return mk_reduce_args_simplifier(m, s, p); }")
+  ADD_SIMPLIFIER("reduce-args", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "mk_reduce_args_simplifier(m, s, p)")
 
 */
 

src/tactic/core/solve_eqs_tactic.h

@@ -79,5 +79,5 @@ inline tactic * mk_solve_eqs_tactic(ast_manager& m, params_ref const& p = params
 
 /*
   ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs_tactic(m, p)")
-  ADD_SIMPLIFIER("solve-eqs", "solve for variables.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(euf::solve_eqs, m, s); }")
+  ADD_SIMPLIFIER("solve-eqs", "solve for variables.", "alloc(euf::solve_eqs, m, s)")
 */

src/tactic/smtlogics/nra_tactic.cpp

@@ -24,7 +24,7 @@ Notes:
 #include "tactic/smtlogics/smt_tactic.h"
 #include "qe/qe_tactic.h"
 #include "qe/nlqsat.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "nlsat/tactic/qfnra_nlsat_tactic.h"
 
 tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {

src/tactic/smtlogics/quant_tactics.cpp

@@ -21,7 +21,7 @@ Revision History:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "qe/qsat.h"
 #include "tactic/core/ctx_simplify_tactic.h"
 #include "tactic/core/elim_term_ite_tactic.h"