update new assertions

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

src/ast/ast.h

@@ -2470,6 +2470,42 @@ public:
     void operator()(AST * n) { m_manager.inc_ref(n); }
 };
 
+class justified_expr {
+    ast_manager& m;
+    expr*        m_fml;
+    proof*       m_proof;
+ public:
+ justified_expr(ast_manager& m, expr* fml, proof* p):
+    m(m),
+    m_fml(fml),
+    m_proof(p) {
+        m.inc_ref(fml);
+        m.inc_ref(p);
+    }
+
+    justified_expr& operator=(justified_expr& other) {
+        SASSERT(&m == &other.m);
+        if (this != &other) {
+            m.dec_ref(m_fml);
+            m.dec_ref(m_proof);
+            m_fml = other.get_fml();
+            m_proof = other.get_proof();
+            m.inc_ref(m_fml);
+            m.inc_ref(m_proof);
+        }
+        return *this;
+    }
+    
+    ~justified_expr() {
+        m.dec_ref(m_fml);
+        m.dec_ref(m_proof);
+    }
+    
+    expr* get_fml() const { return m_fml; }
+    proof* get_proof() const { return m_proof; }        
+};
+
+
 #endif /* AST_H_ */
 
 

src/ast/macros/macro_finder.cpp

@@ -111,6 +111,71 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
     return true;
 }
 
+bool macro_finder::is_arith_macro(expr * n, proof * pr, vector<justified_expr>& new_fmls) {
+    if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
+        return false;
+    expr * body        = to_quantifier(n)->get_expr();
+    unsigned num_decls = to_quantifier(n)->get_num_decls();
+    
+    if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m_manager.is_eq(body))
+        return false;
+    if (!m_autil.is_add(to_app(body)->get_arg(0)))
+        return false;
+    app_ref head(m_manager);
+    expr_ref def(m_manager);
+    bool inv = false;
+    if (!m_util.is_arith_macro(body, num_decls, head, def, inv))
+        return false;
+    app_ref new_body(m_manager);
+    
+    if (!inv || m_manager.is_eq(body))
+        new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def);
+    else if (m_autil.is_le(body))
+        new_body = m_autil.mk_ge(head, def);
+    else
+        new_body = m_autil.mk_le(head, def);
+
+    quantifier_ref new_q(m_manager); 
+    new_q = m_manager.update_quantifier(to_quantifier(n), new_body);
+    proof * new_pr      = 0;
+    if (m_manager.proofs_enabled()) {
+        proof * rw  = m_manager.mk_rewrite(n, new_q);
+        new_pr      = m_manager.mk_modus_ponens(pr, rw);
+    }
+    if (m_manager.is_eq(body)) {
+        return m_macro_manager.insert(head->get_decl(), new_q, new_pr);
+    }
+    // is ge or le
+    // 
+    TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";);
+    func_decl * f   = head->get_decl();
+    func_decl * k   = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
+    app * k_app     = m_manager.mk_app(k, head->get_num_args(), head->get_args());
+    expr_ref_buffer new_rhs_args(m_manager);
+    expr_ref new_rhs2(m_autil.mk_add(def, k_app), m_manager);
+    expr * body1    = m_manager.mk_eq(head, new_rhs2);
+    expr * body2    = m_manager.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0));
+    quantifier * q1 = m_manager.update_quantifier(new_q, body1);
+    expr * patterns[1] = { m_manager.mk_pattern(k_app) };
+    quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2);
+    proof* pr1 = 0, *pr2 = 0;
+    if (m_manager.proofs_enabled()) {
+        // new_pr  : new_q
+        // rw  : [rewrite] new_q ~ q1 & q2
+        // mp  : [modus_pones new_pr rw] q1 & q2
+        // pr1 : [and-elim mp] q1
+        // pr2 : [and-elim mp] q2
+        app * q1q2  = m_manager.mk_and(q1,q2);
+        proof * rw  = m_manager.mk_oeq_rewrite(new_q, q1q2);
+        proof * mp  = m_manager.mk_modus_ponens(new_pr, rw);
+        pr1 = m_manager.mk_and_elim(mp, 0);
+        pr2 = m_manager.mk_and_elim(mp, 1);
+    }
+    new_fmls.push_back(justified_expr(m_manager, q1, pr1));
+    new_fmls.push_back(justified_expr(m_manager, q2, pr2));
+    return true;
+}
+
 /**
    n is of the form: (forall (X) (iff (= (f X) t) def[X]))
 
@@ -152,6 +217,34 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
     }
 }
 
+static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, 
+                                         vector<justified_expr>& new_fmls) {
+    func_decl * f = head->get_decl();
+    func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
+    app * k_app   = m.mk_app(k, head->get_num_args(), head->get_args());
+    app * ite     = m.mk_ite(def, t, k_app);
+    app * body_1  = m.mk_eq(head, ite); 
+    app * body_2  = m.mk_not(m.mk_eq(k_app, t));
+    quantifier * q1 = m.update_quantifier(q, body_1);
+    proof * pr1 = 0, *pr2 = 0;
+    expr * pats[1] = { m.mk_pattern(k_app) };
+    quantifier * q2 = m.update_quantifier(q, 1, pats, body_2); // erase patterns
+    if (m.proofs_enabled()) {
+        // r  : [rewrite] q ~ q1 & q2
+        // pr : q
+        // mp : [modus_pones pr pr1] q1 & q2
+        // pr1 : [and-elim mp] q1
+        // pr2 : [and-elim mp] q2
+        app * q1q2  = m.mk_and(q1,q2);
+        proof * r   = m.mk_oeq_rewrite(q, q1q2);
+        proof * mp  = m.mk_modus_ponens(pr, r);
+        pr1 = m.mk_and_elim(mp, 0);
+        pr2 = m.mk_and_elim(mp, 1);
+    }
+    new_fmls.push_back(justified_expr(m, q1, pr1));
+    new_fmls.push_back(justified_expr(m, q2, pr2));
+}
+
 macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
     m_manager(m),
     m_macro_manager(mm),
@@ -216,3 +309,51 @@ void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const
 }
 
 
+
+bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vector<justified_expr>& new_fmls) {
+    TRACE("macro_finder", tout << "starting expand_macros:\n";
+          m_macro_manager.display(tout););
+    bool found_new_macro = false;
+    for (unsigned i = 0; i < num; i++) {
+        expr * n       = fmls[i].get_fml();
+        proof * pr     = m_manager.proofs_enabled() ? fmls[i].get_proof() : 0;
+        expr_ref new_n(m_manager), def(m_manager);
+        proof_ref new_pr(m_manager);
+        m_macro_manager.expand_macros(n, pr, new_n, new_pr);
+        app_ref head(m_manager), t(m_manager);
+        if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) {
+            TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
+            found_new_macro = true;
+        }
+        else if (is_arith_macro(new_n, new_pr, new_fmls)) {
+            TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";);
+            found_new_macro = true;
+        }
+        else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { 
+            TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
+            pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_fmls);
+            found_new_macro = true;
+        }
+        else {
+            new_fmls.push_back(justified_expr(m_manager, new_n, new_pr));
+        }
+    }
+    return found_new_macro;
+}
+
+void macro_finder::operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {
+    TRACE("macro_finder", tout << "processing macros...\n";);
+    vector<justified_expr> _new_fmls;
+    if (expand_macros(n, fmls, _new_fmls)) {
+        while (true) {
+            vector<justified_expr> old_fmls;
+            _new_fmls.swap(old_fmls);
+            SASSERT(_new_fmls.empty());
+            if (!expand_macros(old_fmls.size(), old_fmls.c_ptr(), _new_fmls))
+                break;
+        }
+    }
+    new_fmls.append(_new_fmls);
+}
+
+

src/ast/macros/macro_finder.h

@@ -38,7 +38,9 @@ class macro_finder {
     macro_util &                m_util;
     arith_util                  m_autil;
     bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    bool expand_macros(unsigned n, justified_expr const * fmls, vector<justified_expr>& new_fmls);
     bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    bool is_arith_macro(expr * n, proof * pr, vector<justified_expr>& new_fmls);
 
     bool is_macro(expr * n, app_ref & head, expr_ref & def);
     bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
@@ -48,6 +50,7 @@ public:
     macro_finder(ast_manager & m, macro_manager & mm);
     ~macro_finder();
     void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    void operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
 };
 
 #endif /* MACRO_FINDER_H_ */

src/ast/macros/macro_manager.cpp

@@ -152,6 +152,14 @@ void macro_manager::mark_forbidden(unsigned n, expr * const * exprs) {
         for_each_expr(p, visited, exprs[i]);
 }
 
+void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) {
+    expr_mark visited;
+    macro_manager_ns::proc p(m_forbidden_set, m_forbidden);
+    for (unsigned i = 0; i < n; i++)
+        for_each_expr(p, visited, exprs[i].get_fml());
+}
+
+
 void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const {
     app * body = to_app(q->get_expr());
     SASSERT(m.is_eq(body) || m.is_iff(body));

src/ast/macros/macro_manager.h

@@ -71,6 +71,7 @@ public:
     void pop_scope(unsigned num_scopes);
     void reset();
     void mark_forbidden(unsigned n, expr * const * exprs);
+    void mark_forbidden(unsigned n, justified_expr const * exprs);
     void mark_forbidden(expr * e) { mark_forbidden(1, &e); }
     bool is_forbidden(func_decl * d) const { return m_forbidden_set.contains(d); }
     obj_hashtable<func_decl> const & get_forbidden_set() const { return m_forbidden_set; }

src/ast/macros/quasi_macros.cpp

@@ -293,6 +293,44 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
     return res;
 }
 
+bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
+    TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl;
+                          for (unsigned i = 0 ; i < n ; i++) 
+                              tout << i << ": " << mk_pp(exprs[i].get_fml(), m_manager) << std::endl; );
+    bool res = false;
+    m_occurrences.reset();
+    
+
+    // Find out how many non-ground appearences for each uninterpreted function there are    
+    for ( unsigned i = 0 ; i < n ; i++ )
+        find_occurrences(exprs[i].get_fml());
+
+    TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
+    for (occurrences_map::iterator it = m_occurrences.begin(); 
+         it != m_occurrences.end(); 
+         it++)
+        tout << it->m_key->get_name() << ": " << it->m_value << std::endl; );
+   
+    // Find all macros
+    for ( unsigned i = 0 ; i < n ; i++ ) {
+        app_ref a(m_manager);
+        expr_ref t(m_manager);
+        if (is_quasi_macro(exprs[i].get_fml(), a, t)) {
+            quantifier_ref macro(m_manager);
+            quasi_macro_to_macro(to_quantifier(exprs[i].get_fml()), a, t, macro);
+            TRACE("quasi_macros", tout << "Found quasi macro: " << mk_pp(exprs[i].get_fml(), m_manager) << std::endl;
+                                  tout << "Macro: " << mk_pp(macro, m_manager) << std::endl; );
+            proof * pr = 0;
+            if (m_manager.proofs_enabled())
+                pr = m_manager.mk_def_axiom(macro);
+            if (m_macro_manager.insert(a->get_decl(), macro, pr))
+                res = true;
+        }
+    }
+
+    return res;
+}
+
 void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {     
     for ( unsigned i = 0 ; i < n ; i++ ) {
         expr_ref r(m_manager), rs(m_manager);
@@ -319,3 +357,27 @@ bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const *
         return false;
     }    
 }
+
+void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {     
+    for ( unsigned i = 0 ; i < n ; i++ ) {
+        expr_ref r(m_manager), rs(m_manager);
+        proof_ref pr(m_manager), ps(m_manager);
+        proof * p = m_manager.proofs_enabled() ? fmls[i].get_proof() : 0;
+        m_macro_manager.expand_macros(fmls[i].get_fml(), p, r, pr);
+        m_rewriter(r);
+        new_fmls.push_back(justified_expr(m_manager, r, pr));
+    }
+}
+
+bool quasi_macros::operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {
+    if (find_macros(n, fmls)) {
+        apply_macros(n, fmls, new_fmls);
+        return true;
+    } else {
+        // just copy them over
+        for ( unsigned i = 0 ; i < n ; i++ ) {
+            new_fmls.push_back(fmls[i]);
+        }
+        return false;
+    }    
+}

src/ast/macros/quasi_macros.h

@@ -53,7 +53,9 @@ class quasi_macros {
 
     void find_occurrences(expr * e);
     bool find_macros(unsigned n, expr * const * exprs);
+    bool find_macros(unsigned n, justified_expr const* expr);
     void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    void apply_macros(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
 
 public:
     quasi_macros(ast_manager & m, macro_manager & mm);
@@ -63,6 +65,7 @@ public:
        \brief Find pure function macros and apply them.
     */
     bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);    
+    bool operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
 };
 
 #endif

src/ast/rewriter/CMakeLists.txt

@@ -15,6 +15,7 @@ z3_add_component(rewriter
     expr_safe_replace.cpp
     factor_rewriter.cpp
     fpa_rewriter.cpp
+    inj_axiom.cpp
     label_rewriter.cpp
     mk_simplified_app.cpp
     pb_rewriter.cpp

src/ast/simplifier/CMakeLists.txt

@@ -12,7 +12,6 @@ z3_add_component(simplifier
     datatype_simplifier_plugin.cpp
     elim_bounds.cpp
     fpa_simplifier_plugin.cpp
-    inj_axiom.cpp
     maximise_ac_sharing.cpp
     poly_simplifier_plugin.cpp
     seq_simplifier_plugin.cpp

src/ast/simplifier/bv_elim.cpp

@@ -12,16 +12,16 @@ Copyright (c) 2015 Microsoft Corporation
 void bv_elim::elim(quantifier* q, quantifier_ref& r) {
 
     svector<symbol>  names, _names;
-    sort_ref_buffer  sorts(m_manager), _sorts(m_manager);
+    sort_ref_buffer  sorts(m), _sorts(m);
-    expr_ref_buffer  pats(m_manager);
+    expr_ref_buffer  pats(m);
-    expr_ref_buffer  no_pats(m_manager);
+    expr_ref_buffer  no_pats(m);
-    expr_ref_buffer  subst_map(m_manager), _subst_map(m_manager);
+    expr_ref_buffer  subst_map(m), _subst_map(m);
-    var_subst        subst(m_manager);
+    var_subst        subst(m);
-    bv_util          bv(m_manager);
+    bv_util          bv(m);
-    expr_ref         new_body(m_manager);
+    expr_ref         new_body(m);
     expr*            old_body = q->get_expr();
     unsigned num_decls = q->get_num_decls();
-    family_id bfid = m_manager.mk_family_id("bv");
+    family_id bfid = m.mk_family_id("bv");
 
     //
     // Traverse sequence of bound variables to eliminate
@@ -37,23 +37,23 @@ void bv_elim::elim(quantifier* q, quantifier_ref& r) {
         if (bv.is_bv_sort(s)) {
             // convert n-bit bit-vector variable into sequence of n-Booleans.
             unsigned num_bits = bv.get_bv_size(s);
-            expr_ref_buffer args(m_manager);
+            expr_ref_buffer args(m);
-            expr_ref bv(m_manager);
+            expr_ref bv(m);
             for (unsigned j = 0; j < num_bits; ++j) {
                 std::ostringstream new_name;
                 new_name << nm.str();
                 new_name << "_";
                 new_name << j;
-                var* v = m_manager.mk_var(var_idx++, m_manager.mk_bool_sort());                
+                var* v = m.mk_var(var_idx++, m.mk_bool_sort());                
                 args.push_back(v);
-                _sorts.push_back(m_manager.mk_bool_sort());
+                _sorts.push_back(m.mk_bool_sort());
                 _names.push_back(symbol(new_name.str().c_str()));
             }
-            bv = m_manager.mk_app(bfid, OP_MKBV, 0, 0, args.size(), args.c_ptr());
+            bv = m.mk_app(bfid, OP_MKBV, 0, 0, args.size(), args.c_ptr());
             _subst_map.push_back(bv.get());
         }
         else {
-            _subst_map.push_back(m_manager.mk_var(var_idx++, s));
+            _subst_map.push_back(m.mk_var(var_idx++, s));
             _sorts.push_back(s);
             _names.push_back(nm);
         }
@@ -78,26 +78,26 @@ void bv_elim::elim(quantifier* q, quantifier_ref& r) {
     subst(old_body, sub_size, sub, new_body);
 
     for (unsigned j = 0; j < q->get_num_patterns(); j++) {
-        expr_ref pat(m_manager);        
+        expr_ref pat(m);        
         subst(q->get_pattern(j), sub_size, sub, pat);
         pats.push_back(pat);
     }
     for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
-        expr_ref nopat(m_manager);
+        expr_ref nopat(m);
         subst(q->get_no_pattern(j), sub_size, sub, nopat);
         no_pats.push_back(nopat);
     }
 
-    r = m_manager.mk_quantifier(true, 
+    r = m.mk_quantifier(true, 
-                                names.size(),
+                        names.size(),
-                                sorts.c_ptr(),
+                        sorts.c_ptr(),
-                                names.c_ptr(),
+                        names.c_ptr(),
-                                new_body.get(),
+                        new_body.get(),
-                                q->get_weight(),
+                        q->get_weight(),
-                                q->get_qid(),
+                        q->get_qid(),
-                                q->get_skid(),
+                        q->get_skid(),
-                                pats.size(), pats.c_ptr(),
+                        pats.size(), pats.c_ptr(),
-                                no_pats.size(), no_pats.c_ptr());
+                        no_pats.size(), no_pats.c_ptr());
 }
 
 bool bv_elim_star::visit_quantifier(quantifier* q) {

src/ast/simplifier/bv_elim.h

@@ -24,9 +24,9 @@ Revision History:
 #include "ast/simplifier/simplifier.h"
 
 class bv_elim {
-    ast_manager& m_manager;
+    ast_manager& m;
 public:
-    bv_elim(ast_manager& m) : m_manager(m) {};
+    bv_elim(ast_manager& m) : m(m) {};
 
     void elim(quantifier* q, quantifier_ref& r);
 };

src/ast/simplifier/inj_axiom.cpp

@@ -1,142 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    inj_axiom.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-06-23.
-
-Revision History:
-
---*/
-#include "ast/simplifier/inj_axiom.h"
-#include "ast/ast_pp.h"
-#include "ast/ast_ll_pp.h"
-#include "ast/has_free_vars.h"
-#include "ast/well_sorted.h"
-
-/**
-   \brief Little HACK for simplifying injectivity axioms
-   
-   \remark It is not covering all possible cases.
-*/
-bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
-    expr * n = q->get_expr();
-    if (q->is_forall() && m.is_or(n) && to_app(n)->get_num_args() == 2) {
-        expr * arg1 = to_app(n)->get_arg(0);
-        expr * arg2 = to_app(n)->get_arg(1);
-        if (m.is_not(arg2)) 
-            std::swap(arg1, arg2);
-        if (m.is_not(arg1) && 
-            m.is_eq(to_app(arg1)->get_arg(0)) && 
-            m.is_eq(arg2)) {
-            expr * app1 = to_app(to_app(arg1)->get_arg(0))->get_arg(0);
-            expr * app2 = to_app(to_app(arg1)->get_arg(0))->get_arg(1);
-            expr * var1 = to_app(arg2)->get_arg(0);
-            expr * var2 = to_app(arg2)->get_arg(1);
-            if (is_app(app1) &&
-                is_app(app2) && 
-                to_app(app1)->get_decl() == to_app(app2)->get_decl() &&
-                to_app(app1)->get_num_args() == to_app(app2)->get_num_args() &&
-                to_app(app1)->get_family_id() == null_family_id &&
-                to_app(app1)->get_num_args() > 0 &&
-                is_var(var1) && 
-                is_var(var2) && 
-                var1 != var2) {
-                app * f1          = to_app(app1);
-                app * f2          = to_app(app2);
-                bool found_vars   = false;
-                unsigned num      = f1->get_num_args();
-                unsigned idx      = UINT_MAX;
-                unsigned num_vars = 1;
-                for (unsigned i = 0; i < num; i++) {
-                    expr  * c1 = f1->get_arg(i);
-                    expr  * c2 = f2->get_arg(i);
-                    if (!is_var(c1) && !is_uninterp_const(c1))
-                        return false;
-                    if ((c1 == var1 && c2 == var2) || (c1 == var2 && c2 == var1)) {
-                        if (found_vars)
-                            return false;
-                        found_vars = true;
-                        idx = i;
-                    }
-                    else if (c1 == c2 && c1 != var1 && c1 != var2) {
-                        if (is_var(c1)) {
-                            ++num_vars;
-                        }
-                    }
-                    else {
-                        return false;
-                    }
-                }
-                if (found_vars && !has_free_vars(q)) {
-                    TRACE("inj_axiom", 
-                          tout << "Cadidate for simplification:\n" << mk_ll_pp(q, m) << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n" <<
-                          mk_pp(var1, m) << "\n" << mk_pp(var2, m) << "\nnum_vars: " << num_vars << "\n";);
-                    // Building new (optimized) axiom
-                    func_decl * decl      = f1->get_decl();
-                    unsigned var_idx      = 0;
-                    ptr_buffer<expr> f_args, inv_vars;
-                    ptr_buffer<sort> decls;
-                    buffer<symbol>   names;
-                    
-                    expr * var            = 0;
-                    for (unsigned i = 0; i < num; i++) {
-                        expr * c = f1->get_arg(i);
-                        if (is_var(c)) {
-                            names.push_back(symbol(i));
-                            sort * s = decl->get_domain(i);
-                            decls.push_back(s);
-                            expr * new_c = m.mk_var(var_idx, s);
-                            var_idx++;
-                            f_args.push_back(new_c);
-                            if (i == idx) {
-                                var = new_c;
-                            }
-                            else {
-                                inv_vars.push_back(new_c);
-                            }
-                        }
-                        else {
-                            SASSERT(is_uninterp_const(c));
-                            f_args.push_back(c);
-                        }
-                    }
-                    SASSERT(var != 0);
-                    app * f    = m.mk_app(decl, f_args.size(), f_args.c_ptr());
-
-                    ptr_vector<sort>  domain;
-                    inv_vars.push_back(f);
-                    for (unsigned i = 0; i < inv_vars.size(); ++i) {
-                        domain.push_back(m.get_sort(inv_vars[i]));
-                    }
-                    sort * d              = decl->get_domain(idx);
-                    func_decl * inv_decl  = m.mk_fresh_func_decl("inj", domain.size(), domain.c_ptr(), d);
-                    
-                    expr * proj = m.mk_app(inv_decl, inv_vars.size(), inv_vars.c_ptr());
-                    expr * eq   = m.mk_eq(proj, var);
-                    expr * p    = m.mk_pattern(f);
-                    
-                    // decls are in the wrong order...
-                    // Remark: the sort of the var 0 must be in the last position.
-                    std::reverse(decls.begin(), decls.end());
-                    
-                    result = m.mk_forall(decls.size(), decls.c_ptr(), names.c_ptr(), eq,
-                                         0, symbol(), symbol(), 1, &p);
-                    TRACE("inj_axiom", tout << "new axiom:\n" << mk_pp(result, m) << "\n";);
-                    SASSERT(is_well_sorted(m, result));
-                    return true;
-                }
-            }
-        }
-    }
-    return false;
-}
-

src/ast/simplifier/inj_axiom.h

@@ -1,27 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    inj_axiom.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-06-23.
-
-Revision History:
-
---*/
-#ifndef INJ_AXIOM_H_
-#define INJ_AXIOM_H_
-
-#include "ast/ast.h"
-
-bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result);
-
-#endif /* INJ_AXIOM_H_ */
-

src/smt/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(smt
     arith_eq_adapter.cpp
     arith_eq_solver.cpp
     asserted_formulas.cpp
+    asserted_formulas_new.cpp
     cached_var_subst.cpp
     cost_evaluator.cpp
     dyn_ack.cpp

src/smt/asserted_formulas.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/rewriter/pull_ite_tree.h"
 #include "ast/rewriter/push_app_ite.h"
+#include "ast/rewriter/inj_axiom.h"
 #include "ast/simplifier/arith_simplifier_plugin.h"
 #include "ast/simplifier/array_simplifier_plugin.h"
 #include "ast/simplifier/datatype_simplifier_plugin.h"
@@ -31,7 +32,6 @@ Revision History:
 #include "ast/simplifier/seq_simplifier_plugin.h"
 #include "ast/simplifier/bv_simplifier_plugin.h"
 #include "ast/simplifier/bv_elim.h"
-#include "ast/simplifier/inj_axiom.h"
 #include "ast/simplifier/elim_bounds.h"
 #include "ast/simplifier/bit2int.h"
 #include "ast/normal_forms/pull_quant.h"

src/smt/elim_term_ite.cpp

@@ -157,4 +157,22 @@ void elim_term_ite::reduce1_quantifier(quantifier * q) {
 }
 
 
+br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr) {
+    if (!m.is_term_ite(f)) {
+        return BR_FAILED;
+    }
+
+    expr_ref   new_def(m);
+    proof_ref  new_def_pr(m);
+    app_ref   r(m.mk_app(f, n, args), m);
+    app_ref    new_r(m);
+    if (!m_defined_names.mk_name(r, new_def, new_def_pr, new_r, result_pr)) {
+        return BR_FAILED;
+    }
+    result = new_r;
+     
+    CTRACE("elim_term_ite_bug", new_def.get() == 0, tout << mk_ismt2_pp(r, m) << "\n";);
+    m_new_defs.push_back(justified_expr(m, new_def, new_def_pr));
+    return BR_DONE;
+}
 

src/smt/elim_term_ite.h

@@ -21,6 +21,7 @@ Revision History:
 
 #include "ast/simplifier/simplifier.h"
 #include "ast/normal_forms/defined_names.h"
+#include "ast/rewriter/rewriter.h"
 
 class elim_term_ite : public simplifier {
     defined_names &    m_defined_names;
@@ -46,5 +47,32 @@ public:
                     );
 };
 
+
+
+class elim_term_ite_cfg : public default_rewriter_cfg {
+    ast_manager&           m;
+    defined_names &        m_defined_names;
+    vector<justified_expr> m_new_defs;
+public:
+    elim_term_ite_cfg(ast_manager & m, defined_names & d): m(m), m_defined_names(d) { 
+        // TBD enable_ac_support(false);
+    }
+    virtual ~elim_term_ite_cfg() {}
+    vector<justified_expr> const& new_defs() const { return m_new_defs; }
+    br_status reduce_app(func_decl* f, unsigned n, expr *const* args, expr_ref& result, proof_ref& result_pr);
+};
+
+class elim_term_ite_rw : public rewriter_tpl<elim_term_ite_cfg> {
+    elim_term_ite_cfg m_cfg;
+public:
+    elim_term_ite_rw(ast_manager& m, defined_names & dn):
+        rewriter_tpl<elim_term_ite_cfg>(m, m.proofs_enabled(), m_cfg),
+        m_cfg(m, dn) 
+    {}
+    vector<justified_expr> const& new_defs() const { return m_cfg.new_defs(); }
+};
+
+
+
 #endif /* ELIM_TERM_ITE_H_ */