Merge branch 'master' of https://github.com/z3prover/z3

cmake/git_utils.cmake

@@ -4,23 +4,55 @@
 # of the git directory changes CMake will be forced to re-run. This useful
 # for fetching the current git hash and including it in the build.
 #
-# `GIT_DIR` is the path to the git directory (i.e. the `.git` directory)
+# `GIT_DOT_FILE` is the path to the git directory (i.e. the `.git` directory) or
+# `.git` file used by a git worktree.
 # `SUCCESS_VAR` is the name of the variable to set. It will be set to TRUE
 # if the dependency was successfully added and FALSE otherwise.
-function(add_git_dir_dependency GIT_DIR SUCCESS_VAR)
+function(add_git_dir_dependency GIT_DOT_FILE SUCCESS_VAR)
   if (NOT "${ARGC}" EQUAL 2)
     message(FATAL_ERROR "Invalid number (${ARGC}) of arguments")
   endif()
 
-  if (NOT IS_ABSOLUTE "${GIT_DIR}")
+  if (NOT IS_ABSOLUTE "${GIT_DOT_FILE}")
-    message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not an absolute path")
+    message(FATAL_ERROR "GIT_DOT_FILE (\"${GIT_DOT_FILE}\") is not an absolute path")
   endif()
 
-  if (NOT IS_DIRECTORY "${GIT_DIR}")
+  if (NOT EXISTS "${GIT_DOT_FILE}")
-    message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not a directory")
+    message(FATAL_ERROR "GIT_DOT_FILE (\"${GIT_DOT_FILE}\") does not exist")
   endif()
 
-  set(GIT_HEAD_FILE "${GIT_DIR}/HEAD")
+  if (NOT IS_DIRECTORY "${GIT_DOT_FILE}")
+    # Might be a git worktree. In this case we need parse out the worktree
+    # git directory
+    file(READ "${GIT_DOT_FILE}" GIT_DOT_FILE_DATA LIMIT 512)
+    string(STRIP "${GIT_DOT_FILE_DATA}" GIT_DOT_FILE_DATA_STRIPPED)
+    if ("${GIT_DOT_FILE_DATA_STRIPPED}" MATCHES "^gitdir:[ ]*(.+)$")
+      # Git worktree
+      message(STATUS "Found git worktree")
+      set(GIT_WORKTREE_DIR "${CMAKE_MATCH_1}")
+      set(GIT_HEAD_FILE "${GIT_WORKTREE_DIR}/HEAD")
+      # Figure out where real git directory lives
+      set(GIT_COMMON_DIR_FILE "${GIT_WORKTREE_DIR}/commondir")
+      if (NOT EXISTS "${GIT_COMMON_DIR_FILE}")
+        message(FATAL_ERROR "Found git worktree dir but could not find \"${GIT_COMMON_DIR_FILE}\"")
+      endif()
+      file(READ "${GIT_COMMON_DIR_FILE}" GIT_COMMON_DIR_FILE_DATA LIMIT 512)
+      string(STRIP "${GIT_COMMON_DIR_FILE_DATA}" GIT_COMMON_DIR_FILE_DATA_STRIPPED)
+      get_filename_component(GIT_DIR "${GIT_WORKTREE_DIR}/${GIT_COMMON_DIR_FILE_DATA_STRIPPED}" ABSOLUTE)
+      if (NOT IS_DIRECTORY "${GIT_DIR}")
+        message(FATAL_ERROR "Failed to compute path to git directory from git worktree")
+      endif()
+    else()
+      message(FATAL_ERROR "GIT_DOT_FILE (\"${GIT_DOT_FILE}\") is not a directory or a pointer to git worktree directory")
+    endif()
+  else()
+    # Just a normal `.git` directory
+    message(STATUS "Found simple git working directory")
+    set(GIT_HEAD_FILE "${GIT_DOT_FILE}/HEAD")
+    set(GIT_DIR "${GIT_DOT_FILE}")
+  endif()
+  message(STATUS "Found git directory \"${GIT_DIR}\"")
+
   if (NOT EXISTS "${GIT_HEAD_FILE}")
     message(AUTHOR_WARNING "Git head file \"${GIT_HEAD_FILE}\" cannot be found")
     set(${SUCCESS_VAR} FALSE PARENT_SCOPE)
@@ -79,24 +111,25 @@ function(add_git_dir_dependency GIT_DIR SUCCESS_VAR)
   set(${SUCCESS_VAR} TRUE PARENT_SCOPE)
 endfunction()
 
-# get_git_head_hash(GIT_DIR OUTPUT_VAR)
+# get_git_head_hash(GIT_DOT_FILE OUTPUT_VAR)
 #
-# Retrieve the current commit hash for a git working directory where `GIT_DIR`
+# Retrieve the current commit hash for a git working directory where
-# is the `.git` directory in the root of the git working directory.
+# `GIT_DOT_FILE` is the `.git` directory or `.git` pointer file in a git
+# worktree in the root of the git working directory.
 #
 # `OUTPUT_VAR` should be the name of the variable to put the result in. If this
 # function fails then either a fatal error will be raised or `OUTPUT_VAR` will
 # contain a string with the suffix `NOTFOUND` which can be used in CMake `if()`
 # commands.
-function(get_git_head_hash GIT_DIR OUTPUT_VAR)
+function(get_git_head_hash GIT_DOT_FILE OUTPUT_VAR)
   if (NOT "${ARGC}" EQUAL 2)
     message(FATAL_ERROR "Invalid number of arguments")
   endif()
-  if (NOT IS_DIRECTORY "${GIT_DIR}")
+  if (NOT EXISTS "${GIT_DOT_FILE}")
-    message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory")
+    message(FATAL_ERROR "\"${GIT_DOT_FILE}\" does not exist")
   endif()
-  if (NOT IS_ABSOLUTE "${GIT_DIR}")
+  if (NOT IS_ABSOLUTE "${GIT_DOT_FILE}")
-    message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path")
+    message(FATAL_ERROR \""${GIT_DOT_FILE}\" is not an absolute path")
   endif()
   find_package(Git)
   # NOTE: Use `GIT_FOUND` rather than `Git_FOUND` which was only
@@ -105,7 +138,7 @@ function(get_git_head_hash GIT_DIR OUTPUT_VAR)
     set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE)
     return()
   endif()
-  get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY)
+  get_filename_component(GIT_WORKING_DIR "${GIT_DOT_FILE}" DIRECTORY)
   execute_process(
     COMMAND
       "${GIT_EXECUTABLE}"
@@ -128,24 +161,25 @@ function(get_git_head_hash GIT_DIR OUTPUT_VAR)
   set(${OUTPUT_VAR} "${Z3_GIT_HASH}" PARENT_SCOPE)
 endfunction()
 
-# get_git_head_describe(GIT_DIR OUTPUT_VAR)
+# get_git_head_describe(GIT_DOT_FILE OUTPUT_VAR)
 #
 # Retrieve the output of `git describe` for a git working directory where
-# `GIT_DIR` is the `.git` directory in the root of the git working directory.
+# `GIT_DOT_FILE` is the `.git` directory or `.git` pointer file in a git
+# worktree in the root of the git working directory.
 #
 # `OUTPUT_VAR` should be the name of the variable to put the result in. If this
 # function fails then either a fatal error will be raised or `OUTPUT_VAR` will
 # contain a string with the suffix `NOTFOUND` which can be used in CMake `if()`
 # commands.
-function(get_git_head_describe GIT_DIR OUTPUT_VAR)
+function(get_git_head_describe GIT_DOT_FILE OUTPUT_VAR)
   if (NOT "${ARGC}" EQUAL 2)
     message(FATAL_ERROR "Invalid number of arguments")
   endif()
-  if (NOT IS_DIRECTORY "${GIT_DIR}")
+  if (NOT EXISTS "${GIT_DOT_FILE}")
-    message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory")
+    message(FATAL_ERROR "\"${GIT_DOT_FILE}\" does not exist")
   endif()
-  if (NOT IS_ABSOLUTE "${GIT_DIR}")
+  if (NOT IS_ABSOLUTE "${GIT_DOT_FILE}")
-    message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path")
+    message(FATAL_ERROR \""${GIT_DOT_FILE}\" is not an absolute path")
   endif()
   find_package(Git)
   # NOTE: Use `GIT_FOUND` rather than `Git_FOUND` which was only
@@ -154,7 +188,7 @@ function(get_git_head_describe GIT_DIR OUTPUT_VAR)
     set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE)
     return()
   endif()
-  get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY)
+  get_filename_component(GIT_WORKING_DIR "${GIT_DOT_FILE}" DIRECTORY)
   execute_process(
     COMMAND
       "${GIT_EXECUTABLE}"

scripts/mk_project.py

@@ -23,6 +23,10 @@ def init_project_def():
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
     add_lib('rewriter', ['ast', 'polynomial', 'automata'], 'ast/rewriter')
+    # Simplifier module will be deleted in the future.
+    # It has been replaced with rewriter module.
+    add_lib('simplifier', ['rewriter'], 'ast/simplifier')
+    add_lib('macros', ['simplifier'], 'ast/macros')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
     add_lib('model', ['rewriter'])
     add_lib('tactic', ['ast', 'model'])
@@ -30,7 +34,7 @@ def init_project_def():
     add_lib('parser_util', ['ast'], 'parsers/util')
     add_lib('grobner', ['ast'], 'math/grobner')
     add_lib('euclid', ['util'], 'math/euclid')
-    add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core')
+    add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter'], 'tactic/core')
     add_lib('sat_tactic', ['tactic', 'sat'], 'sat/tactic')
     add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
     add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
@@ -43,11 +47,7 @@ def init_project_def():
     add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
     add_lib('proof_checker', ['rewriter'], 'ast/proof_checker')
-    # Simplifier module will be deleted in the future.
-    # It has been replaced with rewriter module.
-    add_lib('simplifier', ['rewriter'], 'ast/simplifier')
     add_lib('fpa', ['ast', 'util', 'simplifier', 'model'], 'ast/fpa')
-    add_lib('macros', ['simplifier'], 'ast/macros')
     add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern')
     add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster')
     add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params')

src/api/ml/z3.mli

@@ -1912,7 +1912,7 @@ sig
   (* union of regular expressions *)
   val mk_re_union : context -> Expr.expr list -> Expr.expr 
 
-  (* concatenation of regular expressions* )
+  (* concatenation of regular expressions *)
   val mk_re_concat : context -> Expr.expr list -> Expr.expr 
   
   (* regular expression for the range between two characters *)

src/api/z3_api.h

@@ -1530,7 +1530,7 @@ extern "C" {
        In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects
        are determined by the scope level of #Z3_solver_push and #Z3_solver_pop.
        In other words, a Z3_ast object remains valid until there is a
-       call to Z3_pop that takes the current scope below the level where
+       call to Z3_solver_pop that takes the current scope below the level where
        the object was created.
 
        Note that all other reference counted objects, including Z3_model,

src/smt/params/smt_params.h

@@ -31,7 +31,7 @@ Revision History:
 #include "smt/params/preprocessor_params.h"
 #include "cmd_context/context_params.h"
 
-enum phase_selection { 
+enum phase_selection {
     PS_ALWAYS_FALSE,
     PS_ALWAYS_TRUE,
     PS_CACHING,
@@ -52,7 +52,8 @@ enum restart_strategy {
 enum lemma_gc_strategy {
     LGC_FIXED,
     LGC_GEOMETRIC,
-    LGC_AT_RESTART
+    LGC_AT_RESTART,
+    LGC_NONE
 };
 
 enum initial_activity {
@@ -71,11 +72,11 @@ enum case_split_strategy {
     CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity
 };
 
-struct smt_params : public preprocessor_params, 
+struct smt_params : public preprocessor_params,
-                    public dyn_ack_params, 
+                    public dyn_ack_params,
-                    public qi_params, 
+                    public qi_params,
-                    public theory_arith_params, 
+                    public theory_arith_params,
-                    public theory_array_params, 
+                    public theory_array_params,
                     public theory_bv_params,
                     public theory_str_params,
                     public theory_pb_params,
@@ -153,12 +154,12 @@ struct smt_params : public preprocessor_params,
     unsigned          m_lemma_gc_initial;
     double            m_lemma_gc_factor;
     unsigned          m_new_old_ratio;     //!< the ratio of new and old clauses.
-    unsigned          m_new_clause_activity;  
+    unsigned          m_new_clause_activity;
     unsigned          m_old_clause_activity;
     unsigned          m_new_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant.
     unsigned          m_old_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant.
     double            m_inv_clause_decay;     //!< clause activity decay
-    
+
     // -----------------------------------
     //
     // SMT-LIB (debug) pretty printer
@@ -166,7 +167,7 @@ struct smt_params : public preprocessor_params,
     // -----------------------------------
     bool              m_smtlib_dump_lemmas;
     symbol            m_logic;
-    
+
     // -----------------------------------
     //
     // Statistics for Profiling
@@ -179,10 +180,10 @@ struct smt_params : public preprocessor_params,
 
     // -----------------------------------
     //
-    // Model generation 
+    // Model generation
     //
     // -----------------------------------
-    bool             m_model; 
+    bool             m_model;
     bool             m_model_compact;
     bool             m_model_on_timeout;
     bool             m_model_on_final_check;
@@ -213,7 +214,7 @@ struct smt_params : public preprocessor_params,
     unsigned            m_timeout;
     unsigned            m_rlimit;
     bool                m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
-    bool                m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.    
+    bool                m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
     bool                m_dump_goal_as_smt;
     bool                m_auto_config;
 
@@ -237,7 +238,7 @@ struct smt_params : public preprocessor_params,
         m_display_proof(false),
         m_display_dot_proof(false),
         m_display_unsat_core(false),
-        m_check_proof(false), 
+        m_check_proof(false),
         m_eq_propagation(true),
         m_binary_clause_opt(true),
         m_relevancy_lvl(2),
@@ -279,7 +280,7 @@ struct smt_params : public preprocessor_params,
         m_new_old_ratio(16),
         m_new_clause_activity(10),
         m_old_clause_activity(500),
-        m_new_clause_relevancy(45), 
+        m_new_clause_relevancy(45),
         m_old_clause_relevancy(6),
         m_inv_clause_decay(1),
         m_smtlib_dump_lemmas(false),

src/smt/params/smt_params_helper.pyg

@@ -80,5 +80,6 @@ def_module_params(module_name='smt',
                           ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
                           ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
                           ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
-                          ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body')
+                          ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
+                          ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none')
                           ))

src/tactic/core/CMakeLists.txt

@@ -9,6 +9,7 @@ z3_add_component(core_tactics
     distribute_forall_tactic.cpp
     elim_term_ite_tactic.cpp
     elim_uncnstr_tactic.cpp
+    injectivity_tactic.cpp
     nnf_tactic.cpp
     occf_tactic.cpp
     pb_preprocess_tactic.cpp
@@ -22,6 +23,7 @@ z3_add_component(core_tactics
     collect_occs.cpp
   COMPONENT_DEPENDENCIES
     normal_forms
+    rewriter
     tactic
   TACTIC_HEADERS
     blast_term_ite_tactic.h
@@ -32,6 +34,7 @@ z3_add_component(core_tactics
     distribute_forall_tactic.h
     elim_term_ite_tactic.h
     elim_uncnstr_tactic.h
+    injectivity_tactic.h
     nnf_tactic.h
     occf_tactic.h
     pb_preprocess_tactic.h

src/tactic/core/injectivity_tactic.cpp

@@ -0,0 +1,303 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+  injectivity_tactic.cpp
+
+Abstract:
+
+  Injectivity tactics
+  - Discover axioms of the form `forall x. (= (g (f x)) x`
+    Mark `f` as injective
+  - Rewrite (sub)terms of the form `(= (f x) (f y))` to `(= x y)` whenever `f` is injective.
+
+Author:
+
+  Nicolas Braud-Santoni (t-nibrau) 2017-08-10
+
+Notes:
+
+--*/
+#include <algorithm>
+#include <utility>
+#include "tactic/tactical.h"
+#include "ast/rewriter/rewriter_def.h"
+#include "tactic/core/injectivity_tactic.h"
+#include "util/dec_ref_util.h"
+
+
+class injectivity_tactic : public tactic {
+
+    struct InjHelper : public obj_map<func_decl, obj_hashtable<func_decl>*> {
+        ast_manager & m_manager;
+
+        void insert(func_decl* const f, func_decl* const g) {
+            obj_hashtable<func_decl> *m;
+            if (! obj_map::find(f, m)) {
+                m_manager.inc_ref(f);
+                m = alloc(obj_hashtable<func_decl>); // TODO: Check we don't leak memory
+                obj_map::insert(f, m);
+            }
+            if (!m->contains(g)) {
+                m_manager.inc_ref(g);
+                m->insert(g);
+            }
+        }
+
+        bool find(func_decl* const f, func_decl* const g) const {
+            obj_hashtable<func_decl> *m;
+            if(! obj_map::find(f, m))
+                return false;
+
+            return m->contains(g);
+        }
+
+        InjHelper(ast_manager& m) : obj_map<func_decl, obj_hashtable<func_decl>*>(), m_manager(m) {}
+        ~InjHelper() {
+            for(auto m : *this) {
+                for (func_decl* f : *m.get_value())
+                    m_manager.dec_ref(f);
+
+                m_manager.dec_ref(m.m_key);
+                dealloc(m.m_value);
+            }
+        }
+
+    };
+
+    struct finder {
+        ast_manager & m_manager;
+        InjHelper   & inj_map;
+
+        finder(ast_manager & m, InjHelper & map, params_ref const & p) :
+            m_manager(m),
+            inj_map(map) {
+            updt_params(p);
+        }
+
+        ast_manager & m() const { return m_manager; }
+
+        bool is_axiom(expr* n, func_decl* &f, func_decl* &g) {
+            if (!is_quantifier(n))
+                return false;
+
+            quantifier* const q = to_quantifier(n);
+            if (!q->is_forall() || q->get_num_decls() != 1)
+                return false;
+
+            const expr * const body = q->get_expr();
+
+            // n ~= forall x. body
+
+            if (!m().is_eq(body))
+                return false;
+
+            const app * const body_a = to_app(body);
+            if (body_a->get_num_args() != 2)
+                return false;
+
+            const expr* a = body_a->get_arg(0);
+            const expr* b = body_a->get_arg(1);
+
+            // n ~= forall x. (= a b)
+
+            if (is_app(a) && is_var(b)) {
+                // Do nothing
+            }
+            else if (is_app(b) && is_var(a)) {
+                std::swap(a, b);
+            }
+            else
+                return false;
+
+            const app* const a_app = to_app(a);
+            const var* const b_var = to_var(b);
+
+            if (b_var->get_idx() != 0) // idx is the De Bruijn's index
+                return false;
+
+            if (a_app->get_num_args() != 1)
+                return false;
+
+            g = a_app->get_decl();
+            const expr* const a_body = a_app->get_arg(0);
+
+            // n ~= forall x. (= (g a_body) x)
+
+            if (!is_app(a_body))
+                return false;
+            const app* const a_body_app = to_app(a_body);
+            if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions
+                return false;
+
+            f = a_body_app->get_decl();
+            const expr* const a_body_body = a_body_app->get_arg(0);
+
+            // n ~= forall x. (= (g (f a_body_body)) x)
+            if (a_body_body != b_var)
+                return false;
+
+            // n ~= forall x. (= (g (f x)) x)
+
+            return true;
+        }
+
+        void operator()(goal_ref const & goal,
+                        goal_ref_buffer & result,
+                        model_converter_ref & mc,
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
+            SASSERT(goal->is_well_sorted());
+            mc = 0; pc = 0; core = 0;
+            tactic_report report("injectivity", *goal);
+            fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores
+            fail_if_proof_generation("injectivity", goal);
+
+            for (unsigned i = 0; i < goal->size(); ++i) {
+                func_decl *f, *g;
+                if (!is_axiom(goal->form(i), f, g)) continue;
+                TRACE("injectivity", tout << "Marking " << f->get_name() << " as injective" << std::endl;);
+                inj_map.insert(f, g);
+                // TODO: Record that g is f's pseudoinverse
+            }
+        }
+
+        void updt_params(params_ref const & p) {}
+    };
+
+    struct rewriter_eq_cfg : public default_rewriter_cfg {
+        ast_manager              & m_manager;
+        InjHelper                & inj_map;
+//        expr_ref_vector            m_out;
+//        sort_ref_vector            m_bindings;
+
+        ast_manager & m() const { return m_manager; }
+
+        rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) {
+        }
+
+        ~rewriter_eq_cfg() {
+        }
+
+        void cleanup_buffers() {
+//            m_out.finalize();
+        }
+
+        void reset() {
+        }
+
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+            if(num != 2)
+                return BR_FAILED;
+
+            if (!m().is_eq(f))
+                return BR_FAILED;
+
+            // We are rewriting (= a b)
+            if (!is_app(args[0]) || !is_app(args[1]))
+                return BR_FAILED;
+
+            const app* const a = to_app(args[0]);
+            const app* const b = to_app(args[1]);
+
+            // a and b are applications of the same function
+            if (a->get_decl() != b->get_decl())
+                return BR_FAILED;
+
+            // Maybe TODO: Generalize to multi-parameter functions ?
+            if (a->get_num_args() != 1 || b->get_num_args() != 1)
+                return BR_FAILED;
+
+            if (!inj_map.contains(a->get_decl()))
+                return BR_FAILED;
+
+            SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0)));
+            TRACE("injectivity", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) <<
+                                              " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
+            result = m().mk_eq(a->get_arg(0), b->get_arg(0));
+            result_pr = nullptr;
+            return BR_DONE;
+        }
+
+    };
+
+    struct rewriter_eq : public rewriter_tpl<rewriter_eq_cfg> {
+        rewriter_eq_cfg m_cfg;
+        rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) :
+            rewriter_tpl<rewriter_eq_cfg>(m, m.proofs_enabled(), m_cfg),
+            m_cfg(m, map, p) {
+        }
+    };
+
+    struct rewriter_inverse { };
+
+    finder *           m_finder;
+    rewriter_eq *      m_eq;
+    InjHelper *        m_map;
+//    rewriter_inverse * m_inverse;
+
+    params_ref         m_params;
+    ast_manager &      m_manager;
+
+public:
+    injectivity_tactic(ast_manager & m, params_ref const & p):
+        m_params(p),
+        m_manager(m) {
+        TRACE("injectivity", tout << "constructed new tactic" << std::endl;);
+        m_map = alloc(InjHelper, m);
+        m_finder = alloc(finder, m, *m_map, p);
+        m_eq = alloc(rewriter_eq, m, *m_map, p);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(injectivity_tactic, m, m_params);
+    }
+
+    virtual ~injectivity_tactic() {
+        dealloc(m_finder);
+        dealloc(m_eq);
+        dealloc(m_map);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_finder->updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        insert_max_memory(r);
+        insert_produce_models(r);
+    }
+
+    virtual void operator()(goal_ref const & g,
+                            goal_ref_buffer & result,
+                            model_converter_ref & mc,
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_finder)(g, result, mc, pc, core);
+
+        for (unsigned i = 0; i < g->size(); ++i) {
+            expr*     curr = g->form(i);
+            expr_ref  rw(m_manager);
+            proof_ref pr(m_manager);
+            (*m_eq)(curr, rw, pr);
+            g->update(i, rw, pr, g->dep(i));
+        }
+        result.push_back(g.get());
+    }
+
+    virtual void cleanup() {
+        InjHelper * m = alloc(InjHelper, m_manager);
+        finder * f = alloc(finder, m_manager, *m, m_params);
+        rewriter_eq * r = alloc(rewriter_eq, m_manager, *m, m_params);
+        std::swap(m, m_map), std::swap(f, m_finder), std::swap(r, m_eq);
+        dealloc(m), dealloc(f), dealloc(r);
+    }
+
+
+};
+
+tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p) {
+    return alloc(injectivity_tactic, m, p);
+}

src/tactic/core/injectivity_tactic.h

@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    injectivity_tactic.h
+
+Abstract:
+
+    Injectivity tactics
+
+Author:
+
+    Nicolas Braud-Santoni (t-nibrau) 2017-08-10
+
+Notes:
+
+--*/
+#ifndef INJECTIVITY_TACTIC_H_
+#define INJECTIVITY_TACTIC_H_
+
+#include "util/params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+  ADD_TACTIC("injectivity",  "Identifies and applies injectivity axioms.", "mk_injectivity_tactic(m, p)")
+*/
+
+#endif

src/util/obj_hashtable.h

@@ -134,7 +134,7 @@ public:
         return m_table.end();
     }
     
-    void insert(Key * k, Value const & v) {
+    void insert(Key * const k, Value const & v) {
         m_table.insert(key_data(k, v));
     }
     
@@ -150,7 +150,7 @@ public:
         return m_table.find_core(key_data(k));
     }
 
-    bool find(Key * k, Value & v) const {
+    bool find(Key * const k, Value & v) const {
         obj_map_entry * e = find_core(k);
         if (e) {
             v = e->get_data().m_value;