Merge branch 'opt' of https://github.com/Z3Prover/z3 into unstable

src/ast/arith_decl_plugin.cpp

@@ -417,6 +417,7 @@ inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) {
 
 app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
     if (is_int && !val.is_int()) {
+        SASSERT(false);
         m_manager->raise_exception("invalid rational value passed as an integer");
     }
     if (val.is_unsigned()) {

src/ast/ast.cpp

@@ -2078,6 +2078,8 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
     return r;
 }
 
+
+
 func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity, 
                                             sort * const * domain, sort * range) {
     func_decl_info info(null_family_id, null_decl_kind);

src/ast/ast.h

@@ -2006,6 +2006,7 @@ public:
     app * mk_false() { return m_false; }
     app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
 
+
     func_decl* mk_and_decl() { 
         sort* domain[2] = { m_bool_sort, m_bool_sort };
         return mk_func_decl(m_basic_family_id, OP_AND, 0, 0, 2, domain); 

src/ast/ast_smt2_pp.cpp

@@ -77,6 +77,8 @@ bool smt2_pp_environment::is_indexed_fdecl(func_decl * f) const {
     for (i = 0; i < num; i++) {
         if (f->get_parameter(i).is_int())
             continue;
+        if (f->get_parameter(i).is_rational())
+            continue;
         if (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast()))
             continue;
         break;
@@ -105,9 +107,13 @@ format * smt2_pp_environment::pp_fdecl_params(format * fname, func_decl * f) {
     ptr_buffer<format> fs;
     fs.push_back(fname);
     for (unsigned i = 0; i < num; i++) {
-        SASSERT(f->get_parameter(i).is_int() || (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast())));
+        SASSERT(f->get_parameter(i).is_int() || 
+                f->get_parameter(i).is_rational() || 
+                (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast())));
         if (f->get_parameter(i).is_int())
             fs.push_back(mk_int(get_manager(), f->get_parameter(i).get_int()));
+        else if (f->get_parameter(i).is_rational())
+            fs.push_back(mk_string(get_manager(), f->get_parameter(i).get_rational().to_string().c_str()));
         else
             fs.push_back(pp_fdecl_ref(to_func_decl(f->get_parameter(i).get_ast())));
     }
@@ -1159,6 +1165,26 @@ std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p) {
     return out;
 }
 
+std::ostream& operator<<(std::ostream& out, expr_ref const&  e) {
+    return out << mk_ismt2_pp(e.get(), e.get_manager());
+}
+
+std::ostream& operator<<(std::ostream& out, app_ref const&  e) {
+    return out << mk_ismt2_pp(e.get(), e.get_manager());
+}
+
+std::ostream& operator<<(std::ostream& out, expr_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
+
+std::ostream& operator<<(std::ostream& out, app_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
+
 #ifdef Z3DEBUG
 void pp(expr const * n, ast_manager & m) {
     std::cout << mk_ismt2_pp(const_cast<expr*>(n), m) << std::endl;

src/ast/ast_smt2_pp.h

@@ -110,4 +110,10 @@ struct mk_ismt2_pp {
 
 std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p);
 
+std::ostream& operator<<(std::ostream& out, expr_ref const& e);
+std::ostream& operator<<(std::ostream& out, app_ref const& e);
+
+std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e);
+std::ostream& operator<<(std::ostream& out, app_ref_vector const& e);
+
 #endif

src/ast/ast_smt_pp.cpp

@@ -1058,7 +1058,8 @@ void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, u
 
 void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     ptr_vector<quantifier> ql;
-    decl_collector decls(m_manager);
+    ast_manager& m = m_manager;
+    decl_collector decls(m);
     smt_renaming rn;    
 
     for (unsigned i = 0; i < m_assumptions.size(); ++i) {
@@ -1069,7 +1070,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     }
     decls.visit(n);    
 
-    if (m_manager.is_proof(n)) {
+    if (m.is_proof(n)) {
         strm << "(";
     }
     if (m_benchmark_name != symbol::null) {
@@ -1078,7 +1079,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     if (m_source_info != symbol::null && m_source_info != symbol("")) {
         strm << "; :source { " << m_source_info << " }\n";
     }    
-    if (m_manager.is_bool(n)) {
+    if (m.is_bool(n)) {
         strm << "(set-info :status " << m_status << ")\n";
     }
     if (m_category != symbol::null && m_category != symbol("")) {
@@ -1095,7 +1096,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     for (unsigned i = 0; i < decls.get_num_sorts(); ++i) {
         sort* s = decls.get_sorts()[i];
         if (!(*m_is_declared)(s)) {
-            smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
+            smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p.pp_sort_decl(sort_mark, s);
         }        
     }
@@ -1103,7 +1104,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     for (unsigned i = 0; i < decls.get_num_decls(); ++i) {
         func_decl* d = decls.get_func_decls()[i];
         if (!(*m_is_declared)(d)) {
-            smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
+            smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p(d);
             strm << "\n";
         }
@@ -1112,34 +1113,36 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     for (unsigned i = 0; i < decls.get_num_preds(); ++i) {
         func_decl* d = decls.get_pred_decls()[i];
         if (!(*m_is_declared)(d)) {
-            smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
+            smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p(d);
             strm << "\n";
         }
     }
 
     for (unsigned i = 0; i < m_assumptions.size(); ++i) {
-        strm << "(assert\n";
-        smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
-        p(m_assumptions[i].get());   
-        strm << ")\n";     
+        smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
+        strm << "(assert\n ";
+        p(m_assumptions[i].get());
+        strm << ")\n";
     }
 
     for (unsigned i = 0; i < m_assumptions_star.size(); ++i) {        
-        strm << "(assert\n";
-        smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
-        p(m_assumptions_star[i].get());        
+        smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
+        strm << "(assert\n ";
+        p(m_assumptions_star[i].get());
         strm << ")\n";
     }
 
-    smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
-    if (m_manager.is_bool(n)) {
-        strm << "(assert\n";
-        p(n);
-        strm << ")\n";
+    smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 0);
+    if (m.is_bool(n)) {
+        if (!m.is_true(n)) {
+            strm << "(assert\n ";
+            p(n);
+            strm << ")\n";
+        }
         strm << "(check-sat)\n";
     }
-    else if (m_manager.is_proof(n)) {
+    else if (m.is_proof(n)) {
         strm << "(proof\n";
         p(n);
         strm << "))\n";

src/ast/ast_trail.h

@@ -0,0 +1,76 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    ast_trail.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-02.
+
+Revision History:
+
+    Extracted AST specific features from trail.h
+    nbjorner 2014-9-28
+
+--*/
+#ifndef _AST_TRAIL_H_
+#define _AST_TRAIL_H_
+
+#include"ast.h"
+#include"trail.h"
+
+
+template<typename S, typename T>
+class ast2ast_trailmap {
+    ref_vector<S, ast_manager> m_domain;
+    ref_vector<T, ast_manager> m_range;
+    obj_map<S, T*>             m_map;
+public:
+    ast2ast_trailmap(ast_manager& m):
+        m_domain(m),
+        m_range(m), 
+        m_map()
+    {}
+
+    bool find(S* s, T*& t) {
+        return m_map.find(s,t);
+    }
+    
+    void insert(S* s, T* t) {
+        SASSERT(!m_map.contains(s));
+        m_domain.push_back(s);
+        m_range.push_back(t);
+        m_map.insert(s,t);
+    }
+    
+    void pop() {
+        SASSERT(!m_domain.empty());
+        m_map.remove(m_domain.back());
+        m_domain.pop_back();
+        m_range.pop_back();
+    }
+};
+
+template<typename Ctx, typename S, typename T>
+class ast2ast_trail : public trail<Ctx> {
+    ast2ast_trailmap<S,T>& m_map;
+public:
+    ast2ast_trail(ast2ast_trailmap<S,T>& m, S* s, T* t) : 
+        m_map(m) {
+        m.insert(s,t);
+    }
+
+    virtual void undo(Ctx& ctx) {
+        m_map.pop();
+    }    
+};
+
+
+#endif /* _AST_TRAIL_H_ */
+

src/ast/datatype_decl_plugin.cpp

@@ -422,8 +422,55 @@ static sort * get_type(ast_manager & m, family_id datatype_fid, sort * source_da
     }
 }
 
+func_decl * datatype_decl_plugin::mk_update_field(
+    unsigned num_parameters, parameter const * parameters, 
+    unsigned arity, sort * const * domain, sort * range) {
+    decl_kind k = OP_DT_UPDATE_FIELD;
+    ast_manager& m = *m_manager;
+
+    if (num_parameters != 1 || !parameters[0].is_ast()) {
+        m.raise_exception("invalid parameters for datatype field update");
+        return 0;
+    }
+    if (arity != 2) {
+        m.raise_exception("invalid number of arguments for datatype field update");
+        return 0;
+    }
+    func_decl* acc = 0;
+    if (is_func_decl(parameters[0].get_ast())) {
+        acc = to_func_decl(parameters[0].get_ast());
+    }
+    if (acc && !get_util().is_accessor(acc)) {
+        acc = 0;
+    }
+    if (!acc) {
+        m.raise_exception("datatype field update requires a datatype accessor as the second argument");
+        return 0;
+    }
+    sort* dom = acc->get_domain(0);
+    sort* rng = acc->get_range();
+    if (dom != domain[0]) {
+        m.raise_exception("first argument to field update should be a data-type");
+        return 0;
+    }
+    if (rng != domain[1]) {
+        std::ostringstream buffer;
+        buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m) 
+               << " instead of " << mk_ismt2_pp(domain[1], m);
+        m.raise_exception(buffer.str().c_str());
+        return 0;
+    }
+    range = domain[0];
+    func_decl_info info(m_family_id, k, num_parameters, parameters);
+    return m.mk_func_decl(symbol("update_field"), arity, domain, range, info);
+}
+
 func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                              unsigned arity, sort * const * domain, sort * range) {
+
+    if (k == OP_DT_UPDATE_FIELD) {
+        return mk_update_field(num_parameters, parameters, arity, domain, range);
+    }
     if (num_parameters < 2 || !parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) {
         m_manager->raise_exception("invalid parameters for datatype operator");
         return 0;
@@ -521,6 +568,9 @@ func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_paramet
             return m_manager->mk_func_decl(a_name, arity, domain, a_type, info);
         }
         break;
+    case OP_DT_UPDATE_FIELD: 
+        UNREACHABLE();
+        return 0;
     default:
         m_manager->raise_exception("invalid datatype operator kind");
         return 0;
@@ -672,6 +722,13 @@ bool datatype_decl_plugin::is_value(app * e) const {
     return true;
 }
 
+void datatype_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
+    if (logic == symbol::null) {
+        op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD));
+    }
+}
+
+
 datatype_util::datatype_util(ast_manager & m):
     m_manager(m),
     m_family_id(m.mk_family_id("datatype")),

src/ast/datatype_decl_plugin.h

@@ -32,6 +32,7 @@ enum datatype_op_kind {
     OP_DT_CONSTRUCTOR,
     OP_DT_RECOGNISER,
     OP_DT_ACCESSOR,
+    OP_DT_UPDATE_FIELD,
     LAST_DT_OP
 };
 
@@ -149,8 +150,14 @@ public:
 
     virtual bool is_unique_value(app * e) const { return is_value(e); }
 
+    virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
+
 private:
     bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
+
+    func_decl * mk_update_field(
+        unsigned num_parameters, parameter const * parameters, 
+        unsigned arity, sort * const * domain, sort * range);
 };
 
 class datatype_util {
@@ -181,9 +188,11 @@ public:
     bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
     bool is_recognizer(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); }
     bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); }
+    bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
     bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
     bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); }
     bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
+    bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
     ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
     unsigned get_datatype_num_constructors(sort * ty) { 
         SASSERT(is_datatype(ty));

src/ast/expr_map.h

@@ -44,6 +44,10 @@ public:
     void erase(expr * k);
     void reset();
     void flush();
+    void set_store_proofs(bool f) { 
+        if (m_store_proofs != f) flush();
+        m_store_proofs = f; 
+    }
 };
 
 #endif

src/ast/macros/macro_manager.cpp

@@ -255,9 +255,9 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
     app * n = to_app(_n);
     quantifier * q = 0;
     func_decl * d  = n->get_decl(); 
-    TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m_manager) << "\nd:\n" << d->get_name() << "\n";);
+    TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
     if (m_macro_manager.m_decl2macro.find(d, q)) {
-        TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m_manager) << "\n";);
+        TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
         app * head = 0;
         expr * def = 0;
         m_macro_manager.get_head_def(q, d, head, def);
@@ -272,17 +272,17 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
             SASSERT(subst_args[nidx] == 0);
             subst_args[nidx] = n->get_arg(i);
         }
-        var_subst s(m_manager);
+        var_subst s(m);
         s(def, num, subst_args.c_ptr(), r);
-        if (m_manager.proofs_enabled()) {
-            expr_ref instance(m_manager);
+        if (m.proofs_enabled()) {
+            expr_ref instance(m);
             s(q->get_expr(), num, subst_args.c_ptr(), instance);
-            proof * qi_pr = m_manager.mk_quant_inst(m_manager.mk_or(m_manager.mk_not(q), instance), num, subst_args.c_ptr());
+            proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr());
             proof * q_pr  = 0;
             m_macro_manager.m_decl2macro_pr.find(d, q_pr);
             SASSERT(q_pr != 0);
             proof * prs[2] = { qi_pr, q_pr };
-            p = m_manager.mk_unit_resolution(2, prs);
+            p = m.mk_unit_resolution(2, prs);
         }
         else {
             p = 0;

src/ast/macros/macro_util.cpp

@@ -489,7 +489,6 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
                   tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n";
               });
         subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t);
-        SASSERT(is_well_sorted(m_manager, norm_t));
     }
     else {
         norm_t = t;

src/ast/normal_forms/nnf.cpp

@@ -137,7 +137,6 @@ class skolemizer {
             }
         }
         s(body, substitution.size(), substitution.c_ptr(), r);
-        SASSERT(is_well_sorted(m(), r));
         p = 0;
         if (m().proofs_enabled()) {
             if (q->is_forall()) 

src/ast/pattern/pattern_inference.cpp

@@ -116,7 +116,7 @@ void pattern_inference::collect::operator()(expr * n, unsigned num_bindings) {
         n              = e.m_node;
         unsigned delta = e.m_delta;
         TRACE("collect", tout << "processing: " << n->get_id() << " " << delta << " kind: " << n->get_kind() << "\n";);
-        TRACE("collect_info", tout << mk_pp(n, m_manager) << "\n";);
+        TRACE("collect_info", tout << mk_pp(n, m) << "\n";);
         if (visit_children(n, delta)) {
             m_todo.pop_back();
             save_candidate(n, delta);
@@ -170,9 +170,9 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
                 free_vars.insert(idx);
             info * i = 0;
             if (delta == 0)
-                i = alloc(info, m_manager, n, free_vars, 1);
+                i = alloc(info, m, n, free_vars, 1);
             else
-                i = alloc(info, m_manager, m_manager.mk_var(idx, to_var(n)->get_sort()), free_vars, 1);
+                i = alloc(info, m, m.mk_var(idx, to_var(n)->get_sort()), free_vars, 1);
             save(n, delta, i);
         }
         else {
@@ -189,7 +189,7 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
         }
         
         if (c->get_num_args() == 0) {
-            save(n, delta, alloc(info, m_manager, n, uint_set(), 1));
+            save(n, delta, alloc(info, m, n, uint_set(), 1));
             return;
         }
 
@@ -219,10 +219,10 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
             
         app * new_node = 0;
         if (changed)
-            new_node = m_manager.mk_app(decl, buffer.size(), buffer.c_ptr());
+            new_node = m.mk_app(decl, buffer.size(), buffer.c_ptr());
         else
             new_node = to_app(n);
-        save(n, delta, alloc(info, m_manager, new_node, free_vars, size));
+        save(n, delta, alloc(info, m, new_node, free_vars, size));
         // Remark: arithmetic patterns are only used if they are nested inside other terms.
         // That is, we never consider x + 1 as pattern. On the other hand, f(x+1) can be a pattern
         // if arithmetic is not in the forbidden list.
@@ -235,7 +235,7 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
         decl_kind k   = c->get_decl_kind();
         if (!free_vars.empty() && 
             (fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) {
-            TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m_manager) << "\n";);
+            TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";);
             m_owner.add_candidate(new_node, free_vars, size);
         }
         return;
@@ -338,7 +338,7 @@ bool pattern_inference::contains_subpattern::operator()(expr * n) {
                     uint_set const & s2 = e->get_data().m_value.m_free_vars;
                     SASSERT(s2.subset_of(s1));
                     if (s1 == s2) {
-                        TRACE("pattern_inference", tout << mk_pp(n, m_owner.m_manager) << "\nis bigger than\n" << mk_pp(to_app(curr), m_owner.m_manager) << "\n";);
+                        TRACE("pattern_inference", tout << mk_pp(n, m_owner.m) << "\nis bigger than\n" << mk_pp(to_app(curr), m_owner.m) << "\n";);
                         return true;
                     }
                 }
@@ -411,7 +411,7 @@ void pattern_inference::candidates2unary_patterns(ptr_vector<app> const & candid
         expr2info::obj_map_entry * e = m_candidates_info.find_core(candidate);
         info const & i = e->get_data().m_value;
         if (i.m_free_vars.num_elems() == m_num_bindings) {
-            app * new_pattern = m_manager.mk_pattern(candidate);
+            app * new_pattern = m.mk_pattern(candidate);
             result.push_back(new_pattern);
         }
         else {
@@ -435,7 +435,7 @@ void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns,
     for (unsigned j = 0; j < m_pre_patterns.size(); j++) {
         pre_pattern * curr = m_pre_patterns[j];
         if (curr->m_free_vars.num_elems() == m_num_bindings) {
-            app * new_pattern = m_manager.mk_pattern(curr->m_exprs.size(), curr->m_exprs.c_ptr());
+            app * new_pattern = m.mk_pattern(curr->m_exprs.size(), curr->m_exprs.c_ptr());
             result.push_back(new_pattern);
             if (result.size() >= max_num_patterns)
                 return;
@@ -489,7 +489,7 @@ bool pattern_inference::is_forbidden(app * n) const {
     // occur outside of the quantifier. That is, Z3 will never match this kind of 
     // pattern.
     if (m_params.m_pi_avoid_skolems && decl->is_skolem()) {
-        CTRACE("pattern_inference_skolem", decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m_manager) << "\n";);
+        CTRACE("pattern_inference_skolem", decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";);
         return true;
     }
     if (is_forbidden(decl))
@@ -509,8 +509,8 @@ bool pattern_inference::has_preferred_patterns(ptr_vector<app> & candidate_patte
             expr2info::obj_map_entry * e = m_candidates_info.find_core(candidate);
             info const & i = e->get_data().m_value;
             if (i.m_free_vars.num_elems() == m_num_bindings) {
-                TRACE("pattern_inference", tout << "found preferred pattern:\n" << mk_pp(candidate, m_manager) << "\n";);
-                app * p = m_manager.mk_pattern(candidate);
+                TRACE("pattern_inference", tout << "found preferred pattern:\n" << mk_pp(candidate, m) << "\n";);
+                app * p = m.mk_pattern(candidate);
                 result.push_back(p);
                 found = true;
             }
@@ -531,11 +531,11 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
     m_collect(n, num_bindings);
 
     TRACE("pattern_inference", 
-          tout << mk_pp(n, m_manager);
+          tout << mk_pp(n, m);
           tout << "\ncandidates:\n";
           unsigned num = m_candidates.size();
           for (unsigned i = 0; i < num; i++) {
-              tout << mk_pp(m_candidates.get(i), m_manager) << "\n";
+              tout << mk_pp(m_candidates.get(i), m) << "\n";
           });
 
     if (!m_candidates.empty()) {
@@ -543,7 +543,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
         filter_looping_patterns(m_tmp1);
         TRACE("pattern_inference",
               tout << "candidates after removing looping-patterns:\n";
-              dump_app_vector(tout, m_tmp1, m_manager););
+              dump_app_vector(tout, m_tmp1, m););
         SASSERT(!m_tmp1.empty());
         if (!has_preferred_patterns(m_tmp1, result)) {
             // continue if there are no preferred patterns
@@ -552,7 +552,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
             SASSERT(!m_tmp2.empty());
             TRACE("pattern_inference",
                   tout << "candidates after removing bigger patterns:\n";
-                  dump_app_vector(tout, m_tmp2, m_manager););
+                  dump_app_vector(tout, m_tmp2, m););
             m_tmp1.reset();
             candidates2unary_patterns(m_tmp2, m_tmp1, result);
             unsigned num_extra_multi_patterns = m_params.m_pi_max_multi_patterns;
@@ -563,7 +563,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
                 std::stable_sort(m_tmp1.begin(), m_tmp1.end(), m_pattern_weight_lt);
                 TRACE("pattern_inference",
                       tout << "candidates after sorting:\n";
-                      dump_app_vector(tout, m_tmp1, m_manager););
+                      dump_app_vector(tout, m_tmp1, m););
                 candidates2multi_patterns(num_extra_multi_patterns, m_tmp1, result);
             }
         }
@@ -577,7 +577,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
 #include"database.h" // defines g_pattern_database
 
 void pattern_inference::reduce1_quantifier(quantifier * q) {
-    TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m_manager) << "\n";);
+    TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);
     if (!q->is_forall()) {
         simplifier::reduce1_quantifier(q);
         return;
@@ -587,27 +587,27 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
 
     if (m_params.m_pi_use_database) {
         m_database.initialize(g_pattern_database);
-        app_ref_vector new_patterns(m_manager);
+        app_ref_vector new_patterns(m);
         unsigned new_weight;
         if (m_database.match_quantifier(q, new_patterns, new_weight)) {
 #ifdef Z3DEBUG
-            for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m_manager, new_patterns.get(i))); }
+            for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m, new_patterns.get(i))); }
 #endif
-            quantifier_ref new_q(m_manager);
+            quantifier_ref new_q(m);
             if (q->get_num_patterns() > 0) {
                 // just update the weight...
-                TRACE("pattern_inference", tout << "updating weight to: " << new_weight << "\n" << mk_pp(q, m_manager) << "\n";);
-                new_q = m_manager.update_quantifier_weight(q, new_weight);
+                TRACE("pattern_inference", tout << "updating weight to: " << new_weight << "\n" << mk_pp(q, m) << "\n";);
+                new_q = m.update_quantifier_weight(q, new_weight);
             }
             else {
-                quantifier_ref tmp(m_manager);
-                tmp   = m_manager.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr());
-                new_q = m_manager.update_quantifier_weight(tmp, new_weight); 
-                TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m_manager) << "\n";);
+                quantifier_ref tmp(m);
+                tmp   = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr());
+                new_q = m.update_quantifier_weight(tmp, new_weight); 
+                TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";);
             }
             proof * pr = 0;
-            if (m_manager.fine_grain_proofs())
-                pr = m_manager.mk_rewrite(q, new_q);
+            if (m.fine_grain_proofs())
+                pr = m.mk_rewrite(q, new_q);
             cache_result(q, new_q, pr);
             return;
         }
@@ -635,7 +635,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
         new_no_patterns.push_back(new_pattern);
     } 
     
-    app_ref_buffer new_patterns(m_manager);
+    app_ref_buffer new_patterns(m);
     
     if (m_params.m_pi_arith == AP_CONSERVATIVE)
         m_forbidden.push_back(m_afid);
@@ -677,26 +677,26 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
                     warning_msg("using non nested arith. pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=<val>).", 
                                 q->get_qid().str().c_str(), weight);         
                 }
-                // verbose_stream() << mk_pp(q, m_manager) << "\n";
+                // verbose_stream() << mk_pp(q, m) << "\n";
             }
         }
     }
 
-    quantifier_ref new_q(m_manager);
-    new_q = m_manager.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body);
+    quantifier_ref new_q(m);
+    new_q = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body);
     if (weight != q->get_weight())
-        new_q = m_manager.update_quantifier_weight(new_q, weight);
-    proof_ref pr(m_manager);
-    if (m_manager.fine_grain_proofs()) {  
+        new_q = m.update_quantifier_weight(new_q, weight);
+    proof_ref pr(m);
+    if (m.fine_grain_proofs()) {  
         if (new_body_pr == 0)
-            new_body_pr = m_manager.mk_reflexivity(new_body);
-        pr = m_manager.mk_quant_intro(q, new_q, new_body_pr);
+            new_body_pr = m.mk_reflexivity(new_body);
+        pr = m.mk_quant_intro(q, new_q, new_body_pr);
     }
     
     if (new_patterns.empty() && m_params.m_pi_pull_quantifiers) {
-        pull_quant pull(m_manager);
-        expr_ref   new_expr(m_manager);
-        proof_ref  new_pr(m_manager);
+        pull_quant pull(m);
+        expr_ref   new_expr(m);
+        proof_ref  new_pr(m);
         pull(new_q, new_expr, new_pr);
         quantifier * new_new_q = to_quantifier(new_expr);
         if (new_new_q != new_q) {
@@ -705,12 +705,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
                 if (m_params.m_pi_warnings) {
                     warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str());
                 }
-                new_q = m_manager.update_quantifier(new_new_q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_new_q->get_expr());
-                if (m_manager.fine_grain_proofs()) {
-                    pr = m_manager.mk_transitivity(pr, new_pr);
-                    pr = m_manager.mk_transitivity(pr, m_manager.mk_quant_intro(new_new_q, new_q, m_manager.mk_reflexivity(new_q->get_expr())));
+                new_q = m.update_quantifier(new_new_q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_new_q->get_expr());
+                if (m.fine_grain_proofs()) {
+                    pr = m.mk_transitivity(pr, new_pr);
+                    pr = m.mk_transitivity(pr, m.mk_quant_intro(new_new_q, new_q, m.mk_reflexivity(new_q->get_expr())));
                 }
-                TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m_manager) << "\n";);
+                TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m) << "\n";);
             }
         }
     }
@@ -719,7 +719,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
         if (m_params.m_pi_warnings) {
             warning_msg("failed to find a pattern for quantifier (quantifier id: %s)", q->get_qid().str().c_str());
         }
-        TRACE("pi_failed", tout << mk_pp(q, m_manager) << "\n";);
+        TRACE("pi_failed", tout << mk_pp(q, m) << "\n";);
     }
 
     if (new_patterns.empty() && new_body == q->get_expr()) {

src/ast/pattern/pattern_inference.h

@@ -38,7 +38,7 @@ Revision History:
    every instance of f(g(X)) is also an instance of f(X).
 */
 class smaller_pattern {
-    ast_manager &    m_manager;
+    ast_manager &    m;
     ptr_vector<expr> m_bindings;
 
     typedef std::pair<expr *, expr *> expr_pair;
@@ -54,7 +54,7 @@ class smaller_pattern {
 public:
 
     smaller_pattern(ast_manager & m):
-        m_manager(m) {
+        m(m) {
     }
 
     bool operator()(unsigned num_bindings, expr * p1, expr * p2);
@@ -135,7 +135,7 @@ class pattern_inference : public simplifier {
                 m_node(n, m), m_free_vars(vars), m_size(sz) {}
         };
         
-        ast_manager &            m_manager;
+        ast_manager &            m;
         pattern_inference &      m_owner;
         family_id                m_afid;
         unsigned                 m_num_bindings;
@@ -150,7 +150,7 @@ class pattern_inference : public simplifier {
         void save_candidate(expr * n, unsigned delta);
         void reset();
     public:
-        collect(ast_manager & m, pattern_inference & o):m_manager(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
+        collect(ast_manager & m, pattern_inference & o):m(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
         void operator()(expr * n, unsigned num_bindings);
     };
 

src/ast/pb_decl_plugin.cpp

@@ -0,0 +1,282 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_decl_plugin.cpp
+
+Abstract:
+
+    Cardinality Constraints plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-05-11
+
+Revision History:
+
+--*/
+
+#include "pb_decl_plugin.h"
+
+pb_decl_plugin::pb_decl_plugin():
+    m_at_most_sym("at-most"),
+    m_at_least_sym("at-least"),
+    m_pble_sym("pble"),
+    m_pbge_sym("pbge"),
+    m_pbeq_sym("pbeq")
+{}
+
+func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+                                         unsigned arity, sort * const * domain, sort * range) {
+    SASSERT(m_manager);
+    ast_manager& m = *m_manager;
+    for (unsigned i = 0; i < arity; ++i) {
+        if (!m.is_bool(domain[i])) {
+            m.raise_exception("invalid non-Boolean sort applied to 'at-most'");
+        }
+    }
+    symbol sym;
+    switch(k) {
+    case OP_AT_LEAST_K: sym = m_at_least_sym; break;
+    case OP_AT_MOST_K: sym = m_at_most_sym; break;
+    case OP_PB_LE: sym = m_pble_sym; break;
+    case OP_PB_GE: sym = m_pbge_sym; break;
+    case OP_PB_EQ: sym = m_pbeq_sym; break;
+    default: break;
+    }
+    switch(k) {
+    case OP_AT_LEAST_K:
+    case OP_AT_MOST_K: {
+        if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
+            m.raise_exception("function expects one non-negative integer parameter");
+        }
+        func_decl_info info(m_family_id, k, 1, parameters);
+        return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
+    }
+    case OP_PB_GE:
+    case OP_PB_LE: 
+    case OP_PB_EQ: {
+        if (num_parameters != 1 + arity) {
+            m.raise_exception("function expects arity+1 rational parameters");
+        }
+        vector<parameter> params;
+        for (unsigned i = 0; i < num_parameters; ++i) {
+            parameter const& p = parameters[i];
+            if (p.is_int()) {
+                params.push_back(p);
+            }
+            else if (p.is_rational()) {
+                // HACK: ast pretty printer does not work with rationals.
+                rational r = p.get_rational();
+                if (r.is_int32()) {
+                    params.push_back(parameter(r.get_int32()));
+                }
+                else {
+                    params.push_back(p);
+                }
+            }
+            else {
+                m.raise_exception("functions 'pble/pbge/pbeq' expect arity+1 integer parameters");
+            }
+        }
+        func_decl_info info(m_family_id, k, num_parameters, params.c_ptr());
+        return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
+    }
+    default:
+        UNREACHABLE();
+        return 0;
+    }
+}
+
+void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
+    if (logic == symbol::null) {
+        op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
+        op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K));
+        op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
+        op_names.push_back(builtin_name(m_pbge_sym.bare_str(), OP_PB_GE));
+        op_names.push_back(builtin_name(m_pbeq_sym.bare_str(), OP_PB_EQ));
+    }
+}
+
+app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+    vector<parameter> params;
+    params.push_back(parameter(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        params.push_back(parameter(coeffs[i]));
+    }
+    return m.mk_app(m_fid, OP_PB_LE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
+}
+
+app * pb_util::mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+    vector<parameter> params;
+    params.push_back(parameter(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        params.push_back(parameter(coeffs[i]));
+    }
+    return m.mk_app(m_fid, OP_PB_GE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
+}
+
+app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+    vector<parameter> params;
+    params.push_back(parameter(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        params.push_back(parameter(coeffs[i]));
+    }
+    return m.mk_app(m_fid, OP_PB_EQ, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
+}
+
+// ax + by < k
+// <=>
+// -ax - by >= -k + 1
+// <=>
+// a(1-x) + b(1-y) >= -k + a + b + 1
+app * pb_util::mk_lt(unsigned num_args, rational const * _coeffs, expr * const * _args, rational const& _k) {
+    vector<rational> coeffs;
+    rational k(_k);
+    expr_ref_vector args(m);
+    expr* f;
+    rational d(denominator(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        coeffs.push_back(_coeffs[i]);
+        d = lcm(d, denominator(coeffs[i]));
+        if (m.is_not(_args[i], f)) {
+            args.push_back(f);
+        }
+        else {
+            args.push_back(m.mk_not(_args[i]));
+        }
+    }
+    if (!d.is_one()) {
+        k *= d;
+        for (unsigned i = 0; i < num_args; ++i) {
+            coeffs[i] *= d;        
+        }
+    }
+    k.neg();
+    k += rational::one();
+    for (unsigned i = 0; i < num_args; ++i) {
+        k += coeffs[i];
+    }
+    return mk_ge(num_args, coeffs.c_ptr(), args.c_ptr(), k);
+}
+
+
+app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {
+    parameter param(k);
+    return m.mk_app(m_fid, OP_AT_MOST_K, 1, &param, num_args, args, m.mk_bool_sort());
+}
+
+bool pb_util::is_at_most_k(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_AT_MOST_K);
+}
+
+bool pb_util::is_at_most_k(expr *a, rational& k) const {
+    if (is_at_most_k(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+app * pb_util::mk_at_least_k(unsigned num_args, expr * const * args, unsigned k) {
+    parameter param(k);
+    return m.mk_app(m_fid, OP_AT_LEAST_K, 1, &param, num_args, args, m.mk_bool_sort());
+}
+
+bool pb_util::is_at_least_k(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_AT_LEAST_K);
+}
+
+bool pb_util::is_at_least_k(expr *a, rational& k) const {
+    if (is_at_least_k(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+rational pb_util::get_k(func_decl *a) const {
+    parameter const& p = a->get_parameter(0);
+    if (is_at_most_k(a) || is_at_least_k(a)) {
+        return to_rational(p);
+    }
+    else {
+        SASSERT(is_le(a) || is_ge(a) || is_eq(a));
+        return to_rational(p);
+    }
+}
+
+
+bool pb_util::is_le(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_PB_LE);
+}
+
+bool pb_util::is_le(expr* a, rational& k) const {
+    if (is_le(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+bool pb_util::is_ge(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_PB_GE);
+}
+
+bool pb_util::is_ge(expr* a, rational& k) const {
+    if (is_ge(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+
+bool pb_util::is_eq(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_PB_EQ);
+}
+
+bool pb_util::is_eq(expr* a, rational& k) const {
+    if (is_eq(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+rational pb_util::get_coeff(func_decl* a, unsigned index) const {
+    if (is_at_most_k(a) || is_at_least_k(a)) {
+        return rational::one();
+    }
+    SASSERT(is_le(a) || is_ge(a) || is_eq(a));
+    SASSERT(1 + index < a->get_num_parameters());
+    return to_rational(a->get_parameter(index + 1));
+}
+
+rational pb_util::to_rational(parameter const& p) const {
+    if (p.is_int()) {
+        return rational(p.get_int());
+    }
+    SASSERT(p.is_rational());
+    return p.get_rational();
+}
+
+bool pb_util::has_unit_coefficients(func_decl* f) const {
+    if (is_at_most_k(f) || is_at_least_k(f)) return true;
+    unsigned sz = f->get_arity();
+    for (unsigned i = 0; i < sz; ++i) {
+        if (!get_coeff(f, i).is_one()) return false;
+    }
+    return true;
+}

src/ast/pb_decl_plugin.h

@@ -0,0 +1,123 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_decl_plugin.h
+
+Abstract:
+
+    Pseudo-Boolean and Cardinality Constraints plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-05-11
+
+Notes:
+
+
+  (at-most-k x1 .... x_n) means x1 + ... + x_n <= k
+ 
+hence:
+
+  (not (at-most-k x1 .... x_n)) means x1 + ... + x_n >= k + 1
+
+
+--*/
+#ifndef _PB_DECL_PLUGIN_H_
+#define _PB_DECL_PLUGIN_H_
+
+#include"ast.h"
+ 
+enum pb_op_kind {
+    OP_AT_MOST_K,  // at most K Booleans are true.
+    OP_AT_LEAST_K, // at least K Booleans are true.
+    OP_PB_LE,      // pseudo-Boolean <= (generalizes at_most_k)
+    OP_PB_GE,      // pseudo-Boolean >= 
+    OP_PB_EQ,      // equality
+    LAST_PB_OP
+};
+
+
+class pb_decl_plugin : public decl_plugin {
+    symbol m_at_most_sym;
+    symbol m_at_least_sym;
+    symbol m_pble_sym;
+    symbol m_pbge_sym;
+    symbol m_pbeq_sym;
+    func_decl * mk_at_most(unsigned arity, unsigned k);
+    func_decl * mk_at_least(unsigned arity, unsigned k);
+    func_decl * mk_le(unsigned arity, rational const* coeffs, int k);
+    func_decl * mk_ge(unsigned arity, rational const* coeffs, int k);
+    func_decl * mk_eq(unsigned arity, rational const* coeffs, int k);
+public:
+    pb_decl_plugin();
+    virtual ~pb_decl_plugin() {}
+
+    virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
+        UNREACHABLE();
+        return 0;
+    }
+
+    virtual decl_plugin * mk_fresh() {
+        return alloc(pb_decl_plugin);
+    }
+    
+    //
+    // Contract for func_decl:
+    //   parameters[0] - integer (at most k elements)
+    //      all sorts are Booleans
+    //    parameters[1] .. parameters[arity] - coefficients
+    virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+                                     unsigned arity, sort * const * domain, sort * range);
+    virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
+};
+
+
+class pb_util {
+    ast_manager & m;
+    family_id     m_fid;
+public:
+    pb_util(ast_manager& m):m(m), m_fid(m.mk_family_id("pb")) {}
+    ast_manager & get_manager() const { return m; }
+    family_id get_family_id() const { return m_fid; }
+    app * mk_at_most_k(unsigned num_args, expr * const * args, unsigned k);
+    app * mk_at_least_k(unsigned num_args, expr * const * args, unsigned k);
+    app * mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
+    app * mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
+    app * mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
+    app * mk_lt(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
+    bool is_at_most_k(func_decl *a) const;
+    bool is_at_most_k(expr *a) const { return is_app(a) && is_at_most_k(to_app(a)->get_decl()); }
+    bool is_at_most_k(expr *a, rational& k) const;
+    bool is_at_least_k(func_decl *a) const;
+    bool is_at_least_k(expr *a) const { return is_app(a) && is_at_least_k(to_app(a)->get_decl()); }
+    bool is_at_least_k(expr *a, rational& k) const;
+    rational get_k(func_decl *a) const;
+    rational get_k(expr *a) const { return get_k(to_app(a)->get_decl()); }
+    bool is_le(func_decl *a) const;
+    bool is_le(expr *a) const { return is_app(a) && is_le(to_app(a)->get_decl()); }
+    bool is_le(expr* a, rational& k) const;
+    bool is_ge(func_decl* a) const;
+    bool is_ge(expr* a) const { return is_app(a) && is_ge(to_app(a)->get_decl()); }
+    bool is_ge(expr* a, rational& k) const;
+    rational get_coeff(expr* a, unsigned index) const { return get_coeff(to_app(a)->get_decl(), index); }
+    rational get_coeff(func_decl* a, unsigned index) const; 
+    bool has_unit_coefficients(func_decl* f) const;
+    bool has_unit_coefficients(expr* f) const { return is_app(f) && has_unit_coefficients(to_app(f)->get_decl()); }
+
+
+    bool is_eq(func_decl* f) const;
+    bool is_eq(expr* e) const { return is_app(e) && is_eq(to_app(e)->get_decl()); }
+    bool is_eq(expr* e, rational& k) const;
+
+
+private:
+    rational to_rational(parameter const& p) const;
+};
+
+
+
+
+#endif /* _PB_DECL_PLUGIN_H_ */
+

src/ast/pp_params.pyg

@@ -10,7 +10,7 @@ def_module_params('pp',
                           ('decimal', BOOL, False, 'pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise'),
                           ('decimal_precision', UINT, 10, 'maximum number of decimal places to be used when pp.decimal=true'),
                           ('bv_literals', BOOL, True, 'use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing'),
-						  ('fp_real_literals', BOOL, False, 'use real-numbered floating point literals (e.g, +1.0p-1) during pretty printing'),
+                          ('fp_real_literals', BOOL, False, 'use real-numbered floating point literals (e.g, +1.0p-1) during pretty printing'),
                           ('bv_neg', BOOL, False, 'use bvneg when displaying Bit-Vector literals where the most significant bit is 1'),
                           ('flat_assoc', BOOL, True, 'flat associative operators (when pretty printing SMT2 terms/formulas)'),
                           ('fixed_indent', BOOL, False, 'use a fixed indentation for applications'),

src/ast/reg_decl_plugins.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include"datatype_decl_plugin.h"
 #include"dl_decl_plugin.h"
 #include"seq_decl_plugin.h"
+#include"pb_decl_plugin.h"
 #include"fpa_decl_plugin.h"
 
 void reg_decl_plugins(ast_manager & m) {
@@ -48,4 +49,7 @@ void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) {
         m.register_plugin(symbol("fpa"), alloc(fpa_decl_plugin));
     }
+    if (!m.get_plugin(m.mk_family_id(symbol("pb")))) {
+        m.register_plugin(symbol("pb"), alloc(pb_decl_plugin));
+    }
 }

src/ast/rewriter/ast_counter.cpp

@@ -18,12 +18,9 @@ Revision History:
 --*/
 
 #include "ast_counter.h"
-#include "var_subst.h"
 
 void counter::update(unsigned el, int delta) {
     int & counter = get(el);
-    SASSERT(!m_stay_non_negative || counter>=0);
-    SASSERT(!m_stay_non_negative || static_cast<int>(counter)>=-delta);
     counter += delta;
 }
 
@@ -92,16 +89,14 @@ int counter::get_max_counter_value() const {
 void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
     unsigned n = pred->get_num_args();
     for (unsigned i = 0; i < n; i++) {
-        m_sorts.reset();
-        m_todo.reset();
-        m_mark.reset();
-        ::get_free_vars(m_mark, m_todo, pred->get_arg(i), m_sorts);
-        for (unsigned j = 0; j < m_sorts.size(); ++j) {
-            if (m_sorts[j]) {
+        m_fv(pred->get_arg(i));
+        for (unsigned j = 0; j < m_fv.size(); ++j) {
+            if (m_fv[j]) {
                 update(j, coef);
             }
         }
     }
+    m_fv.reset();
 }
 
 

src/ast/rewriter/ast_counter.h

@@ -27,16 +27,16 @@ Revision History:
 #include "ast.h"
 #include "map.h"
 #include "uint_set.h"
+#include "var_subst.h"
 
 class counter {
 protected:
     typedef u_map<int> map_impl;
     map_impl m_data;
-    const bool m_stay_non_negative;
 public:
     typedef map_impl::iterator iterator;
     
-    counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    counter() {}
     
     void reset() { m_data.reset(); }
     iterator begin() const { return m_data.begin(); }
@@ -69,14 +69,13 @@ public:
 
 class var_counter : public counter {
 protected:
-    ptr_vector<sort> m_sorts;
     expr_fast_mark1  m_visited;
+    expr_free_vars   m_fv;
     ptr_vector<expr> m_todo;
-    ast_mark         m_mark;
     unsigned_vector  m_scopes;
     unsigned get_max_var(bool & has_var);    
 public:
-    var_counter(bool stay_non_negative = true): counter(stay_non_negative) {}
+    var_counter() {}
     void count_vars(ast_manager & m, const app * t, int coef = 1);
     unsigned get_max_var(expr* e);
     unsigned get_next_var(expr* e);
@@ -85,11 +84,10 @@ public:
 class ast_counter {
     typedef obj_map<ast, int> map_impl;
     map_impl m_data;
-    bool     m_stay_non_negative;
  public:
     typedef map_impl::iterator iterator;
     
-    ast_counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    ast_counter() {}
     
     iterator begin() const { return m_data.begin(); }
     iterator end() const { return m_data.end(); }
@@ -99,7 +97,6 @@ class ast_counter {
     }
     void update(ast * el, int delta){
         get(el) += delta;
-        SASSERT(!m_stay_non_negative || get(el) >= 0);
     }
     
     void inc(ast * el) { update(el, 1); }

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -1041,6 +1041,11 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
             mk_rotate_right(sz, a_bits, static_cast<unsigned>(k.get_uint64()), out_bits);
     }
     else {
+        //
+        // Review: a better tuned implementation is possible by using shifts by power of two.
+        // e.g., looping over the bits of b_bits, then rotate by a power of two depending
+        // on the bit-position. This would get rid of the mk_urem.
+        //
         expr_ref_vector sz_bits(m());
         expr_ref_vector masked_b_bits(m());
         expr_ref_vector eqs(m());

src/ast/rewriter/datatype_rewriter.cpp

@@ -60,6 +60,32 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
         UNREACHABLE();
         break;
     }
+    case OP_DT_UPDATE_FIELD: {
+        SASSERT(num_args == 2);
+        if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
+            return BR_FAILED;
+        app * a = to_app(args[0]);
+        func_decl * c_decl = a->get_decl();
+        if (c_decl != m_util.get_accessor_constructor(f)) {
+            result = a;
+            return BR_DONE;
+        }
+        ptr_vector<func_decl> const * acc = m_util.get_constructor_accessors(c_decl);
+        SASSERT(acc && acc->size() == a->get_num_args());
+        unsigned num = acc->size();
+        ptr_buffer<expr> new_args;
+        for (unsigned i = 0; i < num; ++i) {
+            
+            if (f == (*acc)[i]) {
+                new_args.push_back(args[1]);
+            }
+            else {
+                new_args.push_back(a->get_arg(i));
+            }
+        }
+        result = m().mk_app(c_decl, num, new_args.c_ptr());
+        return BR_DONE;        
+    }
     default:
         UNREACHABLE();
     }

src/ast/rewriter/expr_safe_replace.cpp

@@ -29,43 +29,39 @@ void expr_safe_replace::insert(expr* src, expr* dst) {
 }
 
 void expr_safe_replace::operator()(expr* e, expr_ref& res) {
-    obj_map<expr,expr*> cache;
-    ptr_vector<expr> todo, args;
-    expr_ref_vector refs(m);
-    todo.push_back(e);
+    m_todo.push_back(e);
     expr* a, *b, *d;
-    todo.push_back(e);
     
-    while (!todo.empty()) {
-        a = todo.back();
-        if (cache.contains(a)) {
-            todo.pop_back();
+    while (!m_todo.empty()) {
+        a = m_todo.back();
+        if (m_cache.contains(a)) {
+            m_todo.pop_back();
         }
         else if (m_subst.find(a, b)) {
-            cache.insert(a, b);
-            todo.pop_back();
+            m_cache.insert(a, b);
+            m_todo.pop_back();
         }
         else if (is_var(a)) {
-            cache.insert(a, a);
-            todo.pop_back();
+            m_cache.insert(a, a);
+            m_todo.pop_back();
         }
         else if (is_app(a)) {
             app* c = to_app(a);
             unsigned n = c->get_num_args();
-            args.reset();
+            m_args.reset();
             for (unsigned i = 0; i < n; ++i) {
-                if (cache.find(c->get_arg(i), d)) {
-                    args.push_back(d);
+                if (m_cache.find(c->get_arg(i), d)) {
+                    m_args.push_back(d);
                 }
                 else {
-                    todo.push_back(c->get_arg(i));
+                    m_todo.push_back(c->get_arg(i));
                 }
             }
-            if (args.size() == n) {
-                b = m.mk_app(c->get_decl(), args.size(), args.c_ptr());
-                refs.push_back(b);
-                cache.insert(a, b);
-                todo.pop_back();
+            if (m_args.size() == n) {
+                b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
+                m_refs.push_back(b);
+                m_cache.insert(a, b);
+                m_todo.pop_back();
             }
         }
         else {
@@ -93,12 +89,16 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
             }
             replace(q->get_expr(), new_body);
             b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body);
-            refs.push_back(b);
-            cache.insert(a, b);
-            todo.pop_back();
+            m_refs.push_back(b);
+            m_cache.insert(a, b);
+            m_todo.pop_back();
         }        
     }
-    res = cache.find(e);
+    res = m_cache.find(e);
+    m_cache.reset();
+    m_todo.reset();
+    m_args.reset();
+    m_refs.reset();    
 }
 
 void expr_safe_replace::reset() {

src/ast/rewriter/expr_safe_replace.h

@@ -29,9 +29,12 @@ class expr_safe_replace {
     expr_ref_vector m_src;
     expr_ref_vector m_dst;
     obj_map<expr, expr*> m_subst;
+    obj_map<expr,expr*> m_cache;
+    ptr_vector<expr> m_todo, m_args;
+    expr_ref_vector m_refs;
 
 public:
-    expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m) {}
+    expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m), m_refs(m) {}
 
     void insert(expr* src, expr* dst);
 
@@ -42,6 +45,8 @@ public:
     void apply_substitution(expr* s, expr* def, expr_ref& t);
 
     void reset();
+
+    bool empty() const { return m_subst.empty(); }
 };
 
 #endif /* __EXPR_SAFE_REPLACE_H__ */

src/ast/rewriter/pb_rewriter.cpp

@@ -0,0 +1,275 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_rewriter.cpp
+
+Abstract:
+
+    Basic rewriting rules for PB constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-14-12
+
+Notes:
+
+--*/
+
+#include "pb_rewriter.h"
+#include "pb_rewriter_def.h"
+#include "ast_pp.h"
+#include "ast_smt_pp.h"
+
+
+class pb_ast_rewriter_util {
+    ast_manager& m;
+    expr_ref_vector m_refs;
+public:
+
+    typedef std::pair<expr*, rational> arg_t;
+    typedef vector<arg_t> args_t;
+    typedef rational numeral;
+
+    pb_ast_rewriter_util(ast_manager& m): m(m), m_refs(m) {}
+
+    expr* negate(expr* e) {
+        if (m.is_true(e)) {
+            return m.mk_false();
+        }
+        if (m.is_false(e)) {
+            return m.mk_true();
+        }
+        if (m.is_not(e, e)) {
+            return e;
+        }
+        m_refs.push_back(m.mk_not(e));
+        return m_refs.back();
+    }
+
+    void display(std::ostream& out, expr* e) {
+        out << mk_pp(e, m);
+    }
+
+    bool is_negated(expr* e) const {
+        return m.is_not(e);
+    }
+
+    bool is_true(expr* e) const {
+        return m.is_true(e);
+    }
+
+    bool is_false(expr* e) const {
+        return m.is_false(e);
+    }
+
+    struct compare {
+        bool operator()(std::pair<expr*,rational> const& a,
+                        std::pair<expr*,rational> const& b) {
+            return a.first->get_id() < b.first->get_id();
+        }
+
+    };
+};
+
+expr_ref pb_rewriter::translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml) {
+    pb_util util(m());
+    arith_util a(m());
+    expr_ref result(m()), tmp(m());
+    expr_ref_vector es(m());
+    expr*const* args = to_app(fml)->get_args();
+    unsigned sz = to_app(fml)->get_num_args();
+    for (unsigned i = 0; i < sz; ++i) {
+        expr* e = args[i];
+        if (m().is_not(e, e)) {
+            es.push_back(a.mk_sub(a.mk_numeral(rational(1),true),vars.find(e)));
+        }
+        else {
+            es.push_back(vars.find(e));
+        }
+    }
+
+    if (util.is_at_most_k(fml) || util.is_at_least_k(fml)) {
+        if (es.empty()) {
+            tmp = a.mk_numeral(rational(0), true);
+        }
+        else {
+            tmp = a.mk_add(es.size(), es.c_ptr());
+        }
+        if (util.is_at_most_k(fml)) {
+            result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+        else {
+            result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+    }
+    else if (util.is_le(fml) || util.is_ge(fml) || util.is_eq(fml)) {
+        for (unsigned i = 0; i < sz; ++i) {
+            es[i] = a.mk_mul(a.mk_numeral(util.get_coeff(fml, i),false), es[i].get());
+        }
+        if (es.empty()) {
+            tmp = a.mk_numeral(rational(0), true);
+        }
+        else {
+            tmp = a.mk_add(es.size(), es.c_ptr());
+        }
+        if (util.is_le(fml)) {
+            result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+        else if (util.is_ge(fml)) {
+            result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+        else {
+            result = m().mk_eq(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+    }
+    else {
+        result = fml;
+    }
+    return result;
+}
+
+expr_ref pb_rewriter::mk_validate_rewrite(app_ref& e1, app_ref& e2) {
+    ast_manager& m = e1.get_manager();
+    arith_util a(m);
+    symbol name;
+    obj_map<expr,expr*> vars;
+    expr_ref_vector trail(m), fmls(m);    
+    unsigned sz = to_app(e1)->get_num_args();
+    expr*const*args = to_app(e1)->get_args();
+    for (unsigned i = 0; i < sz; ++i) {
+        expr* e = args[i];
+        if (m.is_true(e)) {
+            if (!vars.contains(e)) {
+                trail.push_back(a.mk_numeral(rational(1), true));
+                vars.insert(e, trail.back());            
+            }
+            continue;
+        }
+        if (m.is_false(e)) {
+            if (!vars.contains(e)) {
+                trail.push_back(a.mk_numeral(rational(0), true));
+                vars.insert(e, trail.back());            
+            }
+            continue;
+        }
+
+        std::ostringstream strm;
+        strm << "x" << i;
+        name = symbol(strm.str().c_str());
+        trail.push_back(m.mk_const(name, a.mk_int()));
+        expr* x = trail.back();
+        m.is_not(e,e);
+        vars.insert(e, x);
+        fmls.push_back(a.mk_le(a.mk_numeral(rational(0), true), x));
+        fmls.push_back(a.mk_le(x, a.mk_numeral(rational(1), true)));
+    }
+    expr_ref tmp(m);
+    expr_ref fml1 = translate_pb2lia(vars, e1);
+    expr_ref fml2 = translate_pb2lia(vars, e2);    
+    tmp = m.mk_not(m.mk_eq(fml1, fml2));
+    fmls.push_back(tmp);
+    tmp = m.mk_and(fmls.size(), fmls.c_ptr());
+    return tmp;
+}
+
+static unsigned s_lemma = 0;
+
+void pb_rewriter::validate_rewrite(func_decl* f, unsigned sz, expr*const* args, expr_ref& fml) {
+    ast_manager& m = fml.get_manager();
+    app_ref tmp1(m), tmp2(m);
+    tmp1 = m.mk_app(f, sz, args);
+    tmp2 = to_app(fml);
+    expr_ref tmp = mk_validate_rewrite(tmp1, tmp2);
+    dump_pb_rewrite(tmp);
+}
+
+void pb_rewriter::dump_pb_rewrite(expr* fml) {
+    std::ostringstream strm;
+    strm << "pb_rewrite_" << (s_lemma++) << ".smt2";
+    std::ofstream out(strm.str().c_str());    
+    ast_smt_pp pp(m());
+    pp.display_smt2(out, fml);    
+    out.close();
+}
+
+br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    ast_manager& m = result.get_manager();
+    rational sum(0), maxsum(0);
+    for (unsigned i = 0; i < num_args; ++i) {
+        if (m.is_true(args[i])) {
+            sum += m_util.get_coeff(f, i);
+            maxsum += m_util.get_coeff(f, i);
+        }
+        else if (!m.is_false(args[i])) {
+            maxsum += m_util.get_coeff(f, i);            
+        }
+    }
+    rational k = m_util.get_k(f);
+
+    vector<std::pair<expr*,rational> > vec;
+    for (unsigned i = 0; i < num_args; ++i) {
+        vec.push_back(std::make_pair(args[i], m_util.get_coeff(f, i)));
+    }
+    
+    switch(f->get_decl_kind()) {
+    case OP_AT_MOST_K:
+    case OP_PB_LE:
+        for (unsigned i = 0; i < num_args; ++i) {
+            vec[i].second.neg();
+        }
+        k.neg();
+        break;
+    case OP_AT_LEAST_K:
+    case OP_PB_GE:
+    case OP_PB_EQ:
+        break;
+    default:
+        UNREACHABLE();
+        return BR_FAILED;
+    }    
+
+    bool is_eq = f->get_decl_kind() == OP_PB_EQ;
+    
+    pb_ast_rewriter_util pbu(m);
+    pb_rewriter_util<pb_ast_rewriter_util> util(pbu);
+
+    util.unique(vec, k, is_eq);
+    lbool is_sat = util.normalize(vec, k, is_eq);
+    util.prune(vec, k, is_eq);
+    switch (is_sat) {
+    case l_true:
+        result = m.mk_true();
+        break;
+    case l_false:
+        result = m.mk_false();
+        break;
+    default:
+        m_args.reset();
+        m_coeffs.reset();
+        for (unsigned i = 0; i < vec.size(); ++i) {
+            m_args.push_back(vec[i].first);
+            m_coeffs.push_back(vec[i].second);
+        }
+        if (is_eq) {
+            result = m_util.mk_eq(vec.size(), m_coeffs.c_ptr(), m_args.c_ptr(), k);
+        }
+        else {
+            result = m_util.mk_ge(vec.size(), m_coeffs.c_ptr(), m_args.c_ptr(), k);
+        }
+        break;
+    }
+    TRACE("pb",
+          expr_ref tmp(m);
+          tmp = m.mk_app(f, num_args, args);
+          tout << tmp << "\n";
+          tout << result << "\n";
+          );
+    TRACE("pb_validate",
+          validate_rewrite(f, num_args, args, result););
+          
+    return BR_DONE;
+}
+
+

src/ast/rewriter/pb_rewriter.h

@@ -0,0 +1,65 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for PB constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-14-12
+
+Notes:
+
+--*/
+#ifndef _PB_REWRITER_H_
+#define _PB_REWRITER_H_
+
+#include"pb_decl_plugin.h"
+#include"rewriter_types.h"
+#include"params.h"
+#include"lbool.h"
+
+
+template<typename PBU>
+class pb_rewriter_util {    
+    PBU& m_util;
+    void display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
+public:
+    pb_rewriter_util(PBU& u) : m_util(u) {}
+    void unique(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
+    lbool normalize(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
+    void prune(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
+};
+
+/**
+   \brief Cheap rewrite rules for PB constraints
+*/
+class pb_rewriter {
+    pb_util       m_util;
+    vector<rational> m_coeffs;
+    ptr_vector<expr> m_args;
+
+    void validate_rewrite(func_decl* f, unsigned sz, expr*const* args, expr_ref& fml);
+public:    
+    pb_rewriter(ast_manager & m, params_ref const & p = params_ref()):
+        m_util(m) {
+    }
+    ast_manager & m() const { return m_util.get_manager(); }
+    family_id get_fid() const { return m_util.get_family_id(); }
+
+    void updt_params(params_ref const & p) {}
+    static void get_param_descrs(param_descrs & r) {}
+
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+
+    expr_ref translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml);
+    expr_ref mk_validate_rewrite(app_ref& e1, app_ref& e2);
+    void dump_pb_rewrite(expr* fml);
+};
+
+#endif

src/ast/rewriter/pb_rewriter_def.h

@@ -0,0 +1,298 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_rewriter_def.h
+
+Abstract:
+
+    Basic rewriting rules for PB constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-14-12
+
+Notes:
+
+--*/
+#ifndef _PB_REWRITER_DEF_H_
+#define _PB_REWRITER_DEF_H_
+
+#include"pb_rewriter.h"
+
+
+template<typename PBU>
+void pb_rewriter_util<PBU>::display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
+    for (unsigned i = 0; i < args.size(); ++i) {
+        out << args[i].second << " * ";
+        m_util.display(out, args[i].first);
+        out << " ";
+        if (i+1 < args.size()) out << "+ ";
+    }
+    out << (is_eq?" = ":" >= ") << k << "\n";
+}
+
+template<typename PBU>
+void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
+    
+    TRACE("pb_verbose", display(tout << "pre-unique:", args, k, is_eq););
+    for (unsigned i = 0; i < args.size(); ++i) {
+        if (m_util.is_negated(args[i].first)) {
+            args[i].first = m_util.negate(args[i].first);
+            k -= args[i].second;
+            args[i].second = -args[i].second;
+        }
+    }
+    // remove constants
+    for (unsigned i = 0; i < args.size(); ++i) {
+        if (m_util.is_true(args[i].first)) {
+            k -= args[i].second;
+            std::swap(args[i], args[args.size()-1]);
+            args.pop_back();
+            --i;
+        }
+        else if (m_util.is_false(args[i].first)) {
+            std::swap(args[i], args[args.size()-1]);
+            args.pop_back();                
+            --i;
+        }
+    }
+    // sort and coalesce arguments:
+    typename PBU::compare cmp;
+    std::sort(args.begin(), args.end(), cmp);
+
+    // coallesce
+    unsigned i, j;
+    for (i = 0, j = 1; j < args.size(); ++j) {
+        if (args[i].first == args[j].first) {
+            args[i].second += args[j].second;
+        }
+        else {
+            ++i;
+            args[i] = args[j];
+        }
+    }
+    args.resize(i+1);
+
+    // remove 0s.
+    for (i = 0, j = 0; j < args.size(); ++j) {
+        if (!args[j].second.is_zero()) {
+            if (i != j) {
+                args[i] = args[j];
+            }
+            ++i;
+        }
+    }
+    args.resize(i);
+    TRACE("pb_verbose", display(tout << "post-unique:", args, k, is_eq););
+}
+
+template<typename PBU>
+lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
+    TRACE("pb_verbose", display(tout << "pre-normalize:", args, k, is_eq););
+
+    DEBUG_CODE(
+        bool found = false;
+        for (unsigned i = 0; !found && i < args.size(); ++i) {
+            found = args[i].second.is_zero();
+        }
+        if (found) display(verbose_stream(), args, k, is_eq);
+        SASSERT(!found););
+
+    // 
+    // Ensure all coefficients are positive:
+    //    c*l + y >= k 
+    // <=> 
+    //    c*(1-~l) + y >= k
+    // <=>
+    //    c - c*~l + y >= k
+    // <=> 
+    //    -c*~l + y >= k - c
+    // 
+    typename PBU::numeral sum(0);
+    for (unsigned i = 0; i < args.size(); ++i) {
+        typename PBU::numeral c = args[i].second;
+        if (c.is_neg()) {
+            args[i].second = -c;
+            args[i].first = m_util.negate(args[i].first);
+            k -= c;
+        }
+        sum += args[i].second;
+    }
+    // detect tautologies:
+    if (!is_eq && k <= PBU::numeral::zero()) {
+        args.reset();
+        k = PBU::numeral::zero();
+        return l_true;
+    }
+    if (is_eq && k.is_zero() && args.empty()) {
+        return l_true;
+    }
+
+    // detect infeasible constraints:
+    if (sum < k) {
+        args.reset();
+        k = PBU::numeral::one();
+        return l_false;
+    }
+
+    if (is_eq && k == sum) {
+        for (unsigned i = 0; i < args.size(); ++i) {
+            args[i].second = PBU::numeral::one();
+        }
+        typename PBU::numeral num(args.size()); 
+        k = num;
+        return l_undef;
+    }
+    
+    bool all_int = true;
+    for (unsigned i = 0; all_int && i < args.size(); ++i) {
+        all_int = args[i].second.is_int();
+    }
+    
+    if (!all_int) {
+        // normalize to integers.
+        typename PBU::numeral d(denominator(k));
+        for (unsigned i = 0; i < args.size(); ++i) {
+            d = lcm(d, denominator(args[i].second));
+        }
+        SASSERT(!d.is_one());
+        k *= d;
+        for (unsigned i = 0; i < args.size(); ++i) {
+            args[i].second *= d;
+        }            
+    }
+
+    if (is_eq) {
+        TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
+        return l_undef;
+    }
+    
+    // Ensure the largest coefficient is not larger than k:
+    sum = PBU::numeral::zero();
+    for (unsigned i = 0; i < args.size(); ++i) {
+        typename PBU::numeral c = args[i].second;
+        if (c > k) {
+            args[i].second = k;
+        }
+        sum += args[i].second;
+    }
+    SASSERT(!args.empty());
+    
+    // normalize tight inequalities to unit coefficients.
+    if (sum == k) {
+        for (unsigned i = 0; i < args.size(); ++i) {
+            args[i].second = PBU::numeral::one();
+        }
+        typename PBU::numeral num(args.size()); 
+        k = num;
+    }
+    
+    // apply cutting plane reduction:
+    typename PBU::numeral g(0);
+    for (unsigned i = 0; !g.is_one() && i < args.size(); ++i) {
+        typename PBU::numeral c = args[i].second;
+        if (c != k) {
+            if (g.is_zero()) {
+                g = c;
+            }
+            else {
+                g = gcd(g, c);
+            }
+        }
+    }
+    if (g.is_zero()) {
+        // all coefficients are equal to k.
+        for (unsigned i = 0; i < args.size(); ++i) {
+            SASSERT(args[i].second == k);
+            args[i].second = PBU::numeral::one();
+        }
+        k = PBU::numeral::one();
+    }
+    else if (g > PBU::numeral::one()) {
+        
+        //
+        // Example 5x + 5y + 2z + 2u >= 5
+        // becomes 3x + 3y + z + u >= 3
+        // 
+        typename PBU::numeral k_new = div(k, g);    
+        if (!(k % g).is_zero()) {     // k_new is the ceiling of k / g.
+            k_new++;
+        }
+        for (unsigned i = 0; i < args.size(); ++i) {
+            SASSERT(args[i].second.is_pos());
+            typename PBU::numeral c = args[i].second;
+            if (c == k) {
+                c = k_new;
+            }
+            else {
+                c = div(c, g);
+            }
+            args[i].second = c;
+            SASSERT(args[i].second.is_pos());
+        }
+        k = k_new;            
+    }
+    //
+    // normalize coefficients that fall within a range
+    // k/n <= ... < k/(n-1) for some n = 1,2,...
+    //
+    // e.g, k/n <= min <= max < k/(n-1)
+    //      k/min <= n, n-1 < k/max
+    // .    floor(k/max) = ceil(k/min) - 1  
+    // .    floor(k/max) < k/max
+    //
+    // example: k = 5, min = 3, max = 4: 5/3 -> 2   5/4 -> 1, n = 2
+    // replace all coefficients by 1, and k by 2.
+    //
+    if (!k.is_one()) {
+        typename PBU::numeral min = args[0].second, max = args[0].second;
+        for (unsigned i = 1; i < args.size(); ++i) {
+            if (args[i].second < min) min = args[i].second;
+            if (args[i].second > max) max = args[i].second;
+        }            
+        SASSERT(min.is_pos());
+        typename PBU::numeral n0 = k/max;
+        typename PBU::numeral n1 = floor(n0);
+        typename PBU::numeral n2 = ceil(k/min) - PBU::numeral::one();
+        if (n1 == n2 && !n0.is_int()) {
+            IF_VERBOSE(3, display(verbose_stream() << "set cardinality\n", args, k, is_eq););
+            
+            for (unsigned i = 0; i < args.size(); ++i) {
+                args[i].second = PBU::numeral::one();
+            }
+            k = n1 + PBU::numeral::one();
+        }
+    }
+    TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
+    return l_undef;
+}
+
+template<typename PBU>
+void pb_rewriter_util<PBU>::prune(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
+    if (is_eq) {
+        return;
+    }
+    typename PBU::numeral nlt(0);
+    unsigned occ = 0;
+    for (unsigned i = 0; nlt < k && i < args.size(); ++i) {
+        if (args[i].second < k) {
+            nlt += args[i].second;
+            ++occ;
+        }
+    }
+    if (0 < occ && nlt < k) {        
+        for (unsigned i = 0; i < args.size(); ++i) {
+            if (args[i].second < k) {
+                args[i] = args.back();
+                args.pop_back();
+                --i;
+            }
+        }
+        unique(args, k, is_eq);
+        normalize(args, k, is_eq);
+    }    
+}
+
+#endif

src/ast/rewriter/poly_rewriter_def.h

@@ -31,6 +31,8 @@ void poly_rewriter<Config>::updt_params(params_ref const & _p) {
     m_hoist_mul = p.hoist_mul();
     m_hoist_cmul = p.hoist_cmul();
     m_som_blowup = p.som_blowup();
+    if (!m_flat) m_som = false;
+    if (m_som) m_hoist_mul = false;
 }
 
 template<typename Config>

src/ast/rewriter/th_rewriter.cpp

@@ -25,6 +25,7 @@ Notes:
 #include"array_rewriter.h"
 #include"fpa_rewriter.h"
 #include"dl_rewriter.h"
+#include"pb_rewriter.h"
 #include"rewriter_def.h"
 #include"expr_substitution.h"
 #include"ast_smt2_pp.h"
@@ -41,6 +42,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     datatype_rewriter   m_dt_rw;
     fpa_rewriter        m_f_rw;
     dl_rewriter         m_dl_rw;
+    pb_rewriter         m_pb_rw;
     arith_util          m_a_util;
     bv_util             m_bv_util;
     unsigned long long  m_max_memory; // in bytes
@@ -196,6 +198,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             return m_f_rw.mk_app_core(f, num, args, result);
         if (fid == m_dl_rw.get_fid())
             return m_dl_rw.mk_app_core(f, num, args, result);
+        if (fid == m_pb_rw.get_fid())
+            return m_pb_rw.mk_app_core(f, num, args, result);
         return BR_FAILED;
     }
 
@@ -645,6 +649,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_dt_rw(m),
         m_f_rw(m, p),
         m_dl_rw(m),
+        m_pb_rw(m),
         m_a_util(m),
         m_bv_util(m),
         m_used_dependencies(m),

src/ast/rewriter/var_subst.cpp

@@ -164,7 +164,7 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
           tout << "\n----->\n" << mk_ismt2_pp(result, m) << "\n";);
 }
 
-static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
+static void get_free_vars_offset(expr_sparse_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
     todo.push_back(e);
     while (!todo.empty()) {
         e = todo.back();
@@ -176,7 +176,7 @@ static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigne
         switch(e->get_kind()) {
         case AST_QUANTIFIER: {
             quantifier* q = to_quantifier(e);
-            ast_mark mark1;
+            expr_sparse_mark mark1;
             ptr_vector<expr> todo1;
             get_free_vars_offset(mark1, todo1, offset+q->get_num_decls(), q->get_expr(), sorts);
             break;
@@ -210,11 +210,33 @@ static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigne
 
 
 void get_free_vars(expr* e, ptr_vector<sort>& sorts) {
-    ast_mark mark;
+    expr_sparse_mark mark;
     ptr_vector<expr> todo;
     get_free_vars_offset(mark, todo, 0, e, sorts);
 }
 
-void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
+void get_free_vars(expr_sparse_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
     get_free_vars_offset(mark, todo, 0, e, sorts);
 }
+
+void expr_free_vars::reset() {
+    m_mark.reset();
+    m_sorts.reset();
+    SASSERT(m_todo.empty());
+}
+
+void expr_free_vars::set_default_sort(sort *s) {
+    for (unsigned i = 0; i < m_sorts.size(); ++i) {
+        if (!m_sorts[i]) m_sorts[i] = s;
+    }
+}
+
+void expr_free_vars::operator()(expr* e) {
+    reset();
+    get_free_vars_offset(m_mark, m_todo, 0, e, m_sorts);
+}
+
+void expr_free_vars::accumulate(expr* e) {
+    SASSERT(m_todo.empty());
+    get_free_vars_offset(m_mark, m_todo, 0, e, m_sorts);
+}

src/ast/rewriter/var_subst.h

@@ -81,9 +81,23 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
 
    Return the sorts of the free variables.
 */
-void get_free_vars(expr* e, ptr_vector<sort>& sorts);
 
-void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts);
+class expr_free_vars {
+    expr_sparse_mark m_mark;
+    ptr_vector<sort> m_sorts;
+    ptr_vector<expr> m_todo;
+public:    
+    void reset();
+    void operator()(expr* e);
+    void accumulate(expr* e);
+    bool empty() const { return m_sorts.empty(); }
+    unsigned size() const { return m_sorts.size(); }
+    sort* operator[](unsigned idx) const { return m_sorts[idx]; }
+    bool contains(unsigned idx) const { return idx < m_sorts.size() && m_sorts[idx] != 0; }
+    void set_default_sort(sort* s);
+    void reverse() { m_sorts.reverse(); }
+    sort*const* c_ptr() const { return m_sorts.c_ptr(); }  
+};
 
 #endif
 

src/ast/simplifier/array_simplifier_plugin.cpp

@@ -332,6 +332,7 @@ lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned nu
     for (unsigned i = 0; i < num_st; ++i) {
         all_eq  &= (st[i][arity] == def);
         all_diseq &= m_manager.is_unique_value(st[i][arity]) && (st[i][arity] != def);
+        TRACE("array_simplifier", tout << m_manager.is_unique_value(st[i][arity]) << " " << mk_pp(st[i][arity], m_manager) << "\n";);
     }
     if (all_eq) {
         return l_true;
@@ -350,6 +351,12 @@ bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned n
                 return false;
             }
         }
+        TRACE("array_simplifier", tout << "inserting: ";
+              for (unsigned j = 0; j < arity; ++j) {
+                  tout << mk_pp(st[i][j], m_manager) << " ";              
+              }
+            tout << " |-> " << mk_pp(def, m_manager) << "\n";
+            );
         args_entry e(arity, st[i]);
         table.insert_if_not_there(e);
     }
@@ -424,7 +431,8 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul
             lbool eq = eq_stores(c1, arity2, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr());
             TRACE("array_simplifier", 
                   tout << mk_pp(lhs, m_manager) << " = " 
-                  << mk_pp(rhs, m_manager) << " := " << eq << "\n";);
+                  << mk_pp(rhs, m_manager) << " := " << eq << "\n";
+                  tout << "arity: " << arity1 << "\n";);
             switch(eq) {
             case l_false: 
                 result = m_manager.mk_false(); 

src/ast/simplifier/base_simplifier.h

@@ -20,21 +20,32 @@ Notes:
 #define _BASE_SIMPLIFIER_H_
 
 #include"expr_map.h"
+#include"ast_pp.h"
 
 /**
    \brief Implements basic functionality used by expression simplifiers.
 */
 class base_simplifier {
 protected:
-    ast_manager &                  m_manager;
+    ast_manager &                  m;
     expr_map                       m_cache;
     ptr_vector<expr>               m_todo;
 
-    void cache_result(expr * n, expr * r, proof * p) { m_cache.insert(n, r, p); }
+    void cache_result(expr * n, expr * r, proof * p) { 
+        m_cache.insert(n, r, p); 
+        CTRACE("simplifier", !is_rewrite_proof(n, r, p),
+               tout << mk_pp(n, m) << "\n";
+               tout << mk_pp(r, m) << "\n";
+               tout << mk_pp(p, m) << "\n";);
+        SASSERT(is_rewrite_proof(n, r, p));
+    }
     void reset_cache() { m_cache.reset(); }
     void flush_cache() { m_cache.flush(); }
     void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); }
 
+    void reinitialize() { m_cache.set_store_proofs(m.fine_grain_proofs()); }
+
+
     void visit(expr * n, bool & visited) {
         if (!is_cached(n)) {
             m_todo.push_back(n);
@@ -44,11 +55,22 @@ protected:
 
 public:
     base_simplifier(ast_manager & m):
-        m_manager(m),
+        m(m),
         m_cache(m, m.fine_grain_proofs()) {
     }
     bool is_cached(expr * n) const {  return m_cache.contains(n); }
-    ast_manager & get_manager() { return m_manager; }
+    ast_manager & get_manager() { return m; }
+
+    bool is_rewrite_proof(expr* n, expr* r, proof* p) {
+        if (p && 
+            !m.is_undef_proof(p) && 
+            !(m.has_fact(p) && 
+              (m.is_eq(m.get_fact(p)) || m.is_oeq(m.get_fact(p)) || m.is_iff(m.get_fact(p))) && 
+              to_app(m.get_fact(p))->get_arg(0) == n && 
+              to_app(m.get_fact(p))->get_arg(1) == r)) return false;
+        
+        return (!m.fine_grain_proofs() || p || (n == r));
+    }
 };
 
 #endif /* _BASE_SIMPLIFIER_H_ */

src/ast/simplifier/bv_elim.cpp

@@ -100,11 +100,11 @@ bool bv_elim_star::visit_quantifier(quantifier* q) {
 }
 
 void bv_elim_star::reduce1_quantifier(quantifier* q) {
-    quantifier_ref r(m_manager);
-    proof_ref pr(m_manager);
+    quantifier_ref r(m);
+    proof_ref pr(m);
     m_bv_elim.elim(q, r);
-    if (m_manager.fine_grain_proofs()) {
-        pr = m_manager.mk_rewrite(q, r.get());
+    if (m.fine_grain_proofs()) {
+        pr = m.mk_rewrite(q, r.get());
     }
     else {
         pr = 0;

src/ast/simplifier/datatype_simplifier_plugin.cpp

@@ -81,6 +81,8 @@ bool datatype_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr *
         }
         UNREACHABLE();
     }
+    case OP_DT_UPDATE_FIELD:
+        return false;
     default:
         UNREACHABLE();
     }

src/ast/simplifier/elim_bounds.cpp

@@ -203,20 +203,20 @@ void elim_bounds_star::reduce1_quantifier(quantifier * q) {
         cache_result(q, q, 0); 
         return;
     }
-    quantifier_ref new_q(m_manager);
+    quantifier_ref new_q(m);
     expr * new_body = 0;
     proof * new_pr;
     get_cached(q->get_expr(), new_body, new_pr);
-    new_q = m_manager.update_quantifier(q, new_body);
-    expr_ref r(m_manager);
+    new_q = m.update_quantifier(q, new_body);
+    expr_ref r(m);
     m_elim(new_q, r);
     if (q == r.get()) {
         cache_result(q, q, 0);
         return;
     }
-    proof_ref pr(m_manager);
-    if (m_manager.fine_grain_proofs())
-        pr = m_manager.mk_rewrite(q, r); // TODO: improve justification
+    proof_ref pr(m);
+    if (m.fine_grain_proofs())
+        pr = m.mk_rewrite(q, r); // TODO: improve justification
     cache_result(q, r, pr);
 }
 

src/ast/simplifier/pull_ite_tree.cpp

@@ -187,7 +187,7 @@ pull_ite_tree_star::pull_ite_tree_star(ast_manager & m, simplifier & s):
 
 bool pull_ite_tree_star::get_subst(expr * n, expr_ref & r, proof_ref & p) {
     if (is_app(n) && is_target(to_app(n))) {
-        app_ref tmp(m_manager);
+        app_ref tmp(m);
         m_proc(to_app(n), tmp, p);
         r = tmp;
         return true;
@@ -199,10 +199,10 @@ bool pull_cheap_ite_tree_star::is_target(app * n) const {
     bool r = 
         n->get_num_args() == 2 &&
         n->get_family_id() != null_family_id &&
-        m_manager.is_bool(n) &&
-        (m_manager.is_value(n->get_arg(0)) || m_manager.is_value(n->get_arg(1))) &&
-        (m_manager.is_term_ite(n->get_arg(0)) || m_manager.is_term_ite(n->get_arg(1)));
-    TRACE("pull_ite_target", tout << mk_pp(n, m_manager) << "\nresult: " << r << "\n";);
+        m.is_bool(n) &&
+        (m.is_value(n->get_arg(0)) || m.is_value(n->get_arg(1))) &&
+        (m.is_term_ite(n->get_arg(0)) || m.is_term_ite(n->get_arg(1)));
+    TRACE("pull_ite_target", tout << mk_pp(n, m) << "\nresult: " << r << "\n";);
     return r;
 }
 

src/ast/simplifier/push_app_ite.cpp

@@ -34,7 +34,7 @@ push_app_ite::~push_app_ite() {
 
 int push_app_ite::has_ite_arg(unsigned num_args, expr * const * args) {
     for (unsigned i = 0; i < num_args; i++)
-        if (m_manager.is_ite(args[i]))
+        if (m.is_ite(args[i]))
             return i;
     return -1;
 }
@@ -53,10 +53,10 @@ void push_app_ite::apply(func_decl * decl, unsigned num_args, expr * const * arg
     expr ** args_prime      = const_cast<expr**>(args);
     expr * old              = args_prime[ite_arg_idx];
     args_prime[ite_arg_idx] = t;
-    expr_ref t_new(m_manager);
+    expr_ref t_new(m);
     apply(decl, num_args, args_prime, t_new);
     args_prime[ite_arg_idx] = e;
-    expr_ref e_new(m_manager);
+    expr_ref e_new(m);
     apply(decl, num_args, args_prime, e_new);
     args_prime[ite_arg_idx] = old;
     expr * new_args[3] = { c, t_new, e_new };
@@ -67,11 +67,11 @@ void push_app_ite::apply(func_decl * decl, unsigned num_args, expr * const * arg
    \brief Default (conservative) implementation. Return true if there one and only one ite-term argument.
 */
 bool push_app_ite::is_target(func_decl * decl, unsigned num_args, expr * const * args) {
-    if (m_manager.is_ite(decl))
+    if (m.is_ite(decl))
         return false;
     bool found_ite = false;
     for (unsigned i = 0; i < num_args; i++) {
-        if (m_manager.is_ite(args[i]) && !m_manager.is_bool(args[i])) {
+        if (m.is_ite(args[i]) && !m.is_bool(args[i])) {
             if (found_ite) {
                 if (m_conservative)
                     return false;
@@ -83,7 +83,7 @@ bool push_app_ite::is_target(func_decl * decl, unsigned num_args, expr * const *
     }
     CTRACE("push_app_ite", found_ite, tout << "found target for push app ite:\n";
           tout << decl->get_name();
-          for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m_manager);
+          for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m);
           tout << "\n";);
     return found_ite;
 }
@@ -94,19 +94,19 @@ void push_app_ite::operator()(expr * s, expr_ref & r, proof_ref & p) {
     reduce_core(s);
     get_cached(s, result, result_proof);
     r = result;
-    switch (m_manager.proof_mode()) {
+    switch (m.proof_mode()) {
     case PGM_DISABLED:
-        p = m_manager.mk_undef_proof();
+        p = m.mk_undef_proof();
         break;
     case PGM_COARSE:
         if (result == s)
-            p = m_manager.mk_reflexivity(s);
+            p = m.mk_reflexivity(s);
         else
-            p = m_manager.mk_rewrite_star(s, result, 0, 0);
+            p = m.mk_rewrite_star(s, result, 0, 0);
         break;
     case PGM_FINE:
         if (result == s)
-            p = m_manager.mk_reflexivity(s);
+            p = m.mk_reflexivity(s);
         else
             p = result_proof;
         break;
@@ -171,24 +171,24 @@ void push_app_ite::reduce1_app(app * n) {
     m_args.reset();
     
     func_decl * decl = n->get_decl();
-    proof_ref p1(m_manager);
+    proof_ref p1(m);
     get_args(n, m_args, p1);
 
-    expr_ref r(m_manager);
+    expr_ref r(m);
     if (is_target(decl, m_args.size(), m_args.c_ptr()))
         apply(decl, m_args.size(), m_args.c_ptr(), r);
     else
         mk_app(decl, m_args.size(), m_args.c_ptr(), r);
     
-    if (!m_manager.fine_grain_proofs())
+    if (!m.fine_grain_proofs())
         cache_result(n, r, 0);
     else {
-        expr * s = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
+        expr * s = m.mk_app(decl, m_args.size(), m_args.c_ptr());
         proof * p;
         if (n == r)
             p = 0;
         else if (r != s) 
-            p = m_manager.mk_transitivity(p1, m_manager.mk_rewrite(s, r));
+            p = m.mk_transitivity(p1, m.mk_rewrite(s, r));
         else
             p = p1;
         cache_result(n, r, p);
@@ -200,8 +200,8 @@ void push_app_ite::reduce1_quantifier(quantifier * q) {
     proof * new_body_pr;
     get_cached(q->get_expr(), new_body, new_body_pr);
     
-    quantifier * new_q = m_manager.update_quantifier(q, new_body);
-    proof *      p     = q == new_q ? 0 : m_manager.mk_quant_intro(q, new_q, new_body_pr);   
+    quantifier * new_q = m.update_quantifier(q, new_body);
+    proof *      p     = q == new_q ? 0 : m.mk_quant_intro(q, new_q, new_body_pr);   
     cache_result(q, new_q, p);
 }
 

src/ast/simplifier/simplifier.cpp

@@ -61,16 +61,18 @@ void simplifier::enable_ac_support(bool flag) {
 */
 void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
     m_need_reset = true;
+    reinitialize();
+    expr  * s_orig = s;
     expr  * old_s;
     expr  * result;
     proof * result_proof;
-    switch (m_manager.proof_mode()) {
+    switch (m.proof_mode()) {
     case PGM_DISABLED: // proof generation is disabled.
         reduce_core(s); 
         // after executing reduce_core, the result of the simplification is in the cache
         get_cached(s, result, result_proof);
         r = result;
-        p = m_manager.mk_undef_proof();
+        p = m.mk_undef_proof();
         break;
     case PGM_COARSE: // coarse proofs... in this case, we do not produce a step by step (fine grain) proof to show the equivalence (or equisatisfiability) of s an r.
         m_subst_proofs.reset(); // m_subst_proofs is an auxiliary vector that is used to justify substitutions. See comment on method get_subst. 
@@ -78,10 +80,10 @@ void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
         get_cached(s, result, result_proof);
         r = result;
         if (result == s)
-            p = m_manager.mk_reflexivity(s);
+            p = m.mk_reflexivity(s);
         else {
             remove_duplicates(m_subst_proofs);
-            p = m_manager.mk_rewrite_star(s, result, m_subst_proofs.size(), m_subst_proofs.c_ptr());
+            p = m.mk_rewrite_star(s, result, m_subst_proofs.size(), m_subst_proofs.c_ptr());
         }
         break;
     case PGM_FINE: // fine grain proofs... in this mode, every proof step (or most of them) is described.
@@ -90,17 +92,20 @@ void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
         // keep simplyfing until no further simplifications are possible.
         while (s != old_s) {
             TRACE("simplifier", tout << "simplification pass... " << s->get_id() << "\n";);
-            TRACE("simplifier_loop", tout << mk_ll_pp(s, m_manager) << "\n";);
+            TRACE("simplifier_loop", tout << mk_ll_pp(s, m) << "\n";);
             reduce_core(s);
             get_cached(s, result, result_proof);
-            if (result_proof != 0)
+            SASSERT(is_rewrite_proof(s, result, result_proof));
+            if (result_proof != 0) {
                 m_proofs.push_back(result_proof);
+            }
             old_s = s;
             s     = result;
         }
         SASSERT(s != 0);
         r = s;
-        p = m_proofs.empty() ? m_manager.mk_reflexivity(s) : m_manager.mk_transitivity(m_proofs.size(), m_proofs.c_ptr());
+        p = m_proofs.empty() ? m.mk_reflexivity(s) : m.mk_transitivity(m_proofs.size(), m_proofs.c_ptr());
+        SASSERT(is_rewrite_proof(s_orig, r, p));
         break;
     default:
         UNREACHABLE();
@@ -259,9 +264,9 @@ void simplifier::reduce1(expr * n) {
    specific simplifications via plugins.
 */
 void simplifier::reduce1_app(app * n) {
-    expr_ref r(m_manager);
-    proof_ref p(m_manager);
-    TRACE("reduce", tout << "reducing...\n" << mk_pp(n, m_manager) << "\n";);
+    expr_ref r(m);
+    proof_ref p(m);
+    TRACE("reduce", tout << "reducing...\n" << mk_pp(n, m) << "\n";);
     if (get_subst(n, r, p)) {
         TRACE("reduce", tout << "applying substitution...\n";);
         cache_result(n, r, p);
@@ -279,7 +284,7 @@ void simplifier::reduce1_app(app * n) {
 void simplifier::reduce1_app_core(app * n) {
     m_args.reset();
     func_decl * decl = n->get_decl();
-    proof_ref p1(m_manager);
+    proof_ref p1(m);
     // Stores the new arguments of n in m_args.
     // Let n be of the form
     // (decl arg_0 ... arg_{n-1})
@@ -296,23 +301,23 @@ void simplifier::reduce1_app_core(app * n) {
     //   If none of the arguments have been simplified, and n is not a theory symbol,
     //   Then no simplification is possible, and we can cache the result of the simplification of n as n.
     if (has_new_args || decl->get_family_id() != null_family_id) {
-        expr_ref r(m_manager);
-        TRACE("reduce", tout << "reduce1_app\n"; for(unsigned i = 0; i < m_args.size(); i++) tout << mk_ll_pp(m_args[i], m_manager););
+        expr_ref r(m);
+        TRACE("reduce", tout << "reduce1_app\n"; for(unsigned i = 0; i < m_args.size(); i++) tout << mk_ll_pp(m_args[i], m););
         // the method mk_app invokes get_subst and plugins to simplify
         // (decl arg_0' ... arg_{n-1}')
         mk_app(decl, m_args.size(), m_args.c_ptr(), r);
-        if (!m_manager.fine_grain_proofs()) {
+        if (!m.fine_grain_proofs()) {
             cache_result(n, r, 0);
         }
         else {
-            expr * s = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
+            expr * s = m.mk_app(decl, m_args.size(), m_args.c_ptr());
             proof * p;
             if (n == r)
                 p = 0;
             else if (r != s) 
                 // we use a "theory rewrite generic proof" to justify the step
                 // s = (decl arg_0' ... arg_{n-1}') --> r
-                p = m_manager.mk_transitivity(p1, m_manager.mk_rewrite(s, r));
+                p = m.mk_transitivity(p1, m.mk_rewrite(s, r));
             else
                 p = p1;
             cache_result(n, r, p);
@@ -354,11 +359,11 @@ bool is_ac_vector(app * n) {
 }
 
 void simplifier::reduce1_ac_app_core(app * n) {
-    app_ref    n_c(m_manager);
-    proof_ref  p1(m_manager);
+    app_ref    n_c(m);
+    proof_ref  p1(m);
     mk_ac_congruent_term(n, n_c, p1);
-    TRACE("ac", tout << "expr:\n" << mk_pp(n, m_manager) << "\ncongruent term:\n" << mk_pp(n_c, m_manager) << "\n";);
-    expr_ref r(m_manager); 
+    TRACE("ac", tout << "expr:\n" << mk_pp(n, m) << "\ncongruent term:\n" << mk_pp(n_c, m) << "\n";);
+    expr_ref r(m); 
     func_decl * decl = n->get_decl();
     family_id fid    = decl->get_family_id();
     plugin * p       = get_plugin(fid);
@@ -376,7 +381,7 @@ void simplifier::reduce1_ac_app_core(app * n) {
             // done...
         }
         else {
-            r = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
+            r = m.mk_app(decl, m_args.size(), m_args.c_ptr());
         }
     }
     else {
@@ -385,7 +390,7 @@ void simplifier::reduce1_ac_app_core(app * n) {
         get_ac_args(n_c, m_args, m_mults);
         TRACE("ac", tout << "AC args:\n";
               for (unsigned i = 0; i < m_args.size(); i++) {
-                  tout << mk_pp(m_args[i], m_manager) << " * " << m_mults[i] << "\n";
+                  tout << mk_pp(m_args[i], m) << " * " << m_mults[i] << "\n";
               });
         if (p != 0 && p->reduce(decl, m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), r)) {
             // done...
@@ -393,12 +398,12 @@ void simplifier::reduce1_ac_app_core(app * n) {
         else {
             ptr_buffer<expr> new_args;
             expand_args(m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), new_args);
-            r = m_manager.mk_app(decl, new_args.size(), new_args.c_ptr());
+            r = m.mk_app(decl, new_args.size(), new_args.c_ptr());
         }
     }
-    TRACE("ac", tout << "AC result:\n" << mk_pp(r, m_manager) << "\n";);
+    TRACE("ac", tout << "AC result:\n" << mk_pp(r, m) << "\n";);
 
-    if (!m_manager.fine_grain_proofs()) {
+    if (!m.fine_grain_proofs()) {
         cache_result(n, r, 0);
     }
     else {
@@ -406,7 +411,7 @@ void simplifier::reduce1_ac_app_core(app * n) {
         if (n == r.get())
             p = 0;
         else if (r.get() != n_c.get()) 
-            p = m_manager.mk_transitivity(p1, m_manager.mk_rewrite(n_c, r));
+            p = m.mk_transitivity(p1, m.mk_rewrite(n_c, r));
         else
             p = p1;
         cache_result(n, r, p);
@@ -416,8 +421,8 @@ void simplifier::reduce1_ac_app_core(app * n) {
 static unsigned g_rewrite_lemma_id = 0;
 
 void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * const * args, expr* result) {
-    expr_ref arg(m_manager);
-    arg = m_manager.mk_app(decl, num_args, args);
+    expr_ref arg(m);
+    arg = m.mk_app(decl, num_args, args);
     if (arg.get() != result) {
         char buffer[128];
 #ifdef _WINDOWS
@@ -425,11 +430,11 @@ void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr *
 #else
         sprintf(buffer, "rewrite_lemma_%d.smt", g_rewrite_lemma_id);
 #endif        
-        ast_smt_pp pp(m_manager);
+        ast_smt_pp pp(m);
         pp.set_benchmark_name("rewrite_lemma");
         pp.set_status("unsat");
-        expr_ref n(m_manager);
-        n = m_manager.mk_not(m_manager.mk_eq(arg.get(), result));
+        expr_ref n(m);
+        n = m.mk_not(m.mk_eq(arg.get(), result));
         std::ofstream out(buffer);
         pp.display(out, n);
         out.close();
@@ -445,14 +450,14 @@ void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr *
 */
 void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & result) {
     m_need_reset = true;
-    if (m_manager.is_eq(decl)) {
-        sort * s = m_manager.get_sort(args[0]);
+    if (m.is_eq(decl)) {
+        sort * s = m.get_sort(args[0]);
         plugin * p = get_plugin(s->get_family_id());
         if (p != 0 && p->reduce_eq(args[0], args[1], result))
             return;
     }
-    else if (m_manager.is_distinct(decl)) {
-        sort * s = m_manager.get_sort(args[0]);
+    else if (m.is_distinct(decl)) {
+        sort * s = m.get_sort(args[0]);
         plugin * p = get_plugin(s->get_family_id());
         if (p != 0 && p->reduce_distinct(num_args, args, result))
             return;
@@ -464,7 +469,7 @@ void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args
         //dump_rewrite_lemma(decl, num_args, args, result.get());
         return;
     }
-    result = m_manager.mk_app(decl, num_args, args);
+    result = m.mk_app(decl, num_args, args);
 }
 
 /**
@@ -484,7 +489,7 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
         get_cached(arg, new_arg, arg_proof);
 
         CTRACE("simplifier_bug", (arg != new_arg) != (arg_proof != 0), 
-               tout << mk_ll_pp(arg, m_manager) << "\n---->\n" << mk_ll_pp(new_arg, m_manager) << "\n";
+               tout << mk_ll_pp(arg, m) << "\n---->\n" << mk_ll_pp(new_arg, m) << "\n";
                tout << "#" << arg->get_id() << " #" << new_arg->get_id() << "\n";
                tout << arg << " " << new_arg << "\n";);
         
@@ -500,11 +505,11 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
         args.push_back(new_arg);
     }
     if (has_new_args) {
-        r = m_manager.mk_app(n->get_decl(), args.size(), args.c_ptr());
+        r = m.mk_app(n->get_decl(), args.size(), args.c_ptr());
         if (m_use_oeq)
-            p = m_manager.mk_oeq_congruence(n, r, proofs.size(), proofs.c_ptr());
+            p = m.mk_oeq_congruence(n, r, proofs.size(), proofs.c_ptr());
         else
-            p = m_manager.mk_congruence(n, r, proofs.size(), proofs.c_ptr());
+            p = m.mk_congruence(n, r, proofs.size(), proofs.c_ptr());
     }
     else {
         r = n;
@@ -523,8 +528,8 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
 bool simplifier::get_args(app * n, ptr_vector<expr> & result, proof_ref & p) {
     bool has_new_args  = false;
     unsigned num       = n->get_num_args();
-    if (m_manager.fine_grain_proofs()) {
-        app_ref r(m_manager);
+    if (m.fine_grain_proofs()) {
+        app_ref r(m);
         mk_congruent_term(n, r, p);
         result.append(r->get_num_args(), r->get_args());
         SASSERT(n->get_num_args() == result.size());
@@ -582,7 +587,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
                     new_args.push_back(new_arg);
                     if (arg != new_arg)
                         has_new_arg = true;
-                    if (m_manager.fine_grain_proofs()) {
+                    if (m.fine_grain_proofs()) {
                         proof * pr = 0;
                         m_ac_pr_cache.find(to_app(arg), pr);
                         if (pr != 0)
@@ -601,7 +606,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
                 new_args.push_back(new_arg);
                 if (arg != new_arg)
                     has_new_arg = true;
-                if (m_manager.fine_grain_proofs() && pr != 0)
+                if (m.fine_grain_proofs() && pr != 0)
                     new_arg_prs.push_back(pr);
             }
         }
@@ -610,14 +615,14 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
             todo.pop_back();
             if (!has_new_arg) {
                 m_ac_cache.insert(curr, curr);
-                if (m_manager.fine_grain_proofs()) 
+                if (m.fine_grain_proofs()) 
                     m_ac_pr_cache.insert(curr, 0);
             }
             else {
-                app * new_curr = m_manager.mk_app(f, new_args.size(), new_args.c_ptr());
+                app * new_curr = m.mk_app(f, new_args.size(), new_args.c_ptr());
                 m_ac_cache.insert(curr, new_curr);
-                if (m_manager.fine_grain_proofs()) {
-                    proof * p = m_manager.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr());
+                if (m.fine_grain_proofs()) {
+                    proof * p = m.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr());
                     m_ac_pr_cache.insert(curr, p);
                 }
             }
@@ -628,7 +633,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
     app *   new_n = 0;
     m_ac_cache.find(n, new_n);
     r = new_n;
-    if (m_manager.fine_grain_proofs()) {
+    if (m.fine_grain_proofs()) {
         proof * new_pr = 0;
         m_ac_pr_cache.find(n, new_pr);
         p = new_pr;
@@ -719,7 +724,7 @@ void simplifier::get_ac_args(app * n, ptr_vector<expr> & args, vector<rational>
     SASSERT(!sorted_exprs.empty());
     SASSERT(sorted_exprs[sorted_exprs.size()-1] == n);
     
-    TRACE("ac", tout << mk_ll_pp(n, m_manager, true, false) << "#" << n->get_id() << "\nsorted expressions...\n";
+    TRACE("ac", tout << mk_ll_pp(n, m, true, false) << "#" << n->get_id() << "\nsorted expressions...\n";
           for (unsigned i = 0; i < sorted_exprs.size(); i++) {
               tout << "#" << sorted_exprs[i]->get_id() << " ";
           }
@@ -754,10 +759,10 @@ void simplifier::get_ac_args(app * n, ptr_vector<expr> & args, vector<rational>
 void simplifier::reduce1_quantifier(quantifier * q) {
     expr *  new_body;
     proof * new_body_pr;
-    SASSERT(is_well_sorted(m_manager, q));
+    SASSERT(is_well_sorted(m, q));
     get_cached(q->get_expr(), new_body, new_body_pr);
 
-    quantifier_ref q1(m_manager);
+    quantifier_ref q1(m);
     proof * p1 = 0;
     
     if (is_quantifier(new_body) && 
@@ -774,7 +779,7 @@ void simplifier::reduce1_quantifier(quantifier * q) {
         sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts());
         names.append(nested_q->get_num_decls(), nested_q->get_decl_names());
 
-        q1 = m_manager.mk_quantifier(q->is_forall(),
+        q1 = m.mk_quantifier(q->is_forall(),
                                      sorts.size(),
                                      sorts.c_ptr(),
                                      names.c_ptr(),
@@ -783,13 +788,13 @@ void simplifier::reduce1_quantifier(quantifier * q) {
                                      q->get_qid(),
                                      q->get_skid(),
                                      0, 0, 0, 0);
-        SASSERT(is_well_sorted(m_manager, q1));
+        SASSERT(is_well_sorted(m, q1));
         
-        if (m_manager.fine_grain_proofs()) {
-            quantifier * q0 = m_manager.update_quantifier(q, new_body);
-            proof * p0 = q == q0 ? 0 : m_manager.mk_quant_intro(q, q0, new_body_pr);
-            p1 = m_manager.mk_pull_quant(q0, q1);
-            p1 = m_manager.mk_transitivity(p0, p1);
+        if (m.fine_grain_proofs()) {
+            quantifier * q0 = m.update_quantifier(q, new_body);
+            proof * p0 = q == q0 ? 0 : m.mk_quant_intro(q, q0, new_body_pr);
+            p1 = m.mk_pull_quant(q0, q1);
+            p1 = m.mk_transitivity(p0, p1);
         }
     }
     else {
@@ -802,7 +807,7 @@ void simplifier::reduce1_quantifier(quantifier * q) {
         unsigned num = q->get_num_patterns();
         for (unsigned i = 0; i < num; i++) {
             get_cached(q->get_pattern(i), new_pattern, new_pattern_pr);
-            if (m_manager.is_pattern(new_pattern)) {
+            if (m.is_pattern(new_pattern)) {
                 new_patterns.push_back(new_pattern);
             }            
         }
@@ -815,7 +820,7 @@ void simplifier::reduce1_quantifier(quantifier * q) {
         remove_duplicates(new_patterns);
         remove_duplicates(new_no_patterns);
 
-        q1 = m_manager.mk_quantifier(q->is_forall(),
+        q1 = m.mk_quantifier(q->is_forall(),
                                      q->get_num_decls(),
                                      q->get_decl_sorts(),
                                      q->get_decl_names(),
@@ -827,26 +832,26 @@ void simplifier::reduce1_quantifier(quantifier * q) {
                                      new_patterns.c_ptr(),
                                      new_no_patterns.size(),
                                      new_no_patterns.c_ptr());
-        SASSERT(is_well_sorted(m_manager, q1));
+        SASSERT(is_well_sorted(m, q1));
 
-        TRACE("simplifier", tout << mk_pp(q, m_manager) << "\n" << mk_pp(q1, m_manager) << "\n";);
-        if (m_manager.fine_grain_proofs()) {
+        TRACE("simplifier", tout << mk_pp(q, m) << "\n" << mk_pp(q1, m) << "\n";);
+        if (m.fine_grain_proofs()) {
             if (q != q1 && !new_body_pr) {
-                new_body_pr = m_manager.mk_rewrite(q->get_expr(), new_body);
+                new_body_pr = m.mk_rewrite(q->get_expr(), new_body);
             }
-            p1 = q == q1 ? 0 : m_manager.mk_quant_intro(q, q1, new_body_pr);
+            p1 = q == q1 ? 0 : m.mk_quant_intro(q, q1, new_body_pr);
         }
     }
     
-    expr_ref r(m_manager);
-    elim_unused_vars(m_manager, q1, r);
+    expr_ref r(m);
+    elim_unused_vars(m, q1, r);
     
     proof * pr = 0;
-    if (m_manager.fine_grain_proofs()) {
+    if (m.fine_grain_proofs()) {
         proof * p2 = 0;
         if (q1.get() != r.get())
-            p2 = m_manager.mk_elim_unused_vars(q1, r);
-        pr = m_manager.mk_transitivity(p1, p2);
+            p2 = m.mk_elim_unused_vars(q1, r);
+        pr = m.mk_transitivity(p1, p2);
     }
 
     cache_result(q, r, pr);
@@ -892,7 +897,7 @@ bool subst_simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) {
         m_subst_map->get(n, _r, _p);
         r = _r;
         p = _p;
-        if (m_manager.coarse_grain_proofs()) 
+        if (m.coarse_grain_proofs()) 
             m_subst_proofs.push_back(p);
         return true;
     }

src/ast/simplifier/simplifier.h

@@ -210,7 +210,7 @@ public:
 
     plugin * get_plugin(family_id fid) const { return m_plugins.get_plugin(fid); }
 
-    ast_manager & get_manager() { return m_manager; }
+    ast_manager & get_manager() { return m; }
 
     void borrow_plugins(simplifier const & s);
     void release_plugins();

src/ast/substitution/substitution_tree.cpp

@@ -793,8 +793,10 @@ bool substitution_tree::visit(expr * e, st_visitor & st, node * r) {
                 }
                 else {
                     TRACE("st_bug", tout << "found match:\n"; m_subst->display(tout); tout << "m_subst: " << m_subst << "\n";);
-                    if (!st(n->m_expr))
+                    if (!st(n->m_expr)) {
+                        clear_stack();
                         return false;
+                    }
                     if (!backtrack())
                         break;
                 }
@@ -806,12 +808,16 @@ bool substitution_tree::visit(expr * e, st_visitor & st, node * r) {
         else if (!backtrack())
             break;
     }
+    clear_stack();
+    return true;
+}
+
+void substitution_tree::clear_stack() {
     while (!m_bstack.empty()) {
         m_subst->pop_scope();
         m_bstack.pop_back();
     }
     m_subst->pop_scope();
-    return true;
 }
 
 template<substitution_tree::st_visit_mode Mode>

src/ast/substitution/substitution_tree.h

@@ -123,6 +123,8 @@ class substitution_tree {
     template<st_visit_mode Mode>
     void visit(expr * e, st_visitor & st, unsigned in_offset, unsigned st_offset, unsigned reg_offset);
 
+    void clear_stack();
+
 public:
     substitution_tree(ast_manager & m);
     ~substitution_tree();

src/ast/trail.h

@@ -1,404 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    trail.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-06-02.
-
-Revision History:
-
---*/
-#ifndef _TRAIL_H_
-#define _TRAIL_H_
-
-#include"ast.h"
-#include"obj_hashtable.h"
-#include"region.h"
-
-template<typename Ctx>
-class trail {
-public:
-    virtual ~trail() {
-    }
-    virtual void undo(Ctx & ctx) = 0;
-};
-
-template<typename Ctx, typename T>
-class value_trail : public trail<Ctx> {
-    T & m_value;
-    T   m_old_value;
-    
-public:
-    value_trail(T & value):
-        m_value(value),
-        m_old_value(value) {
-    }
-    
-    virtual ~value_trail() {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_value = m_old_value;
-    }
-};
-
-template<typename Ctx>
-class reset_flag_trail : public trail<Ctx> {
-    bool & m_value;
-public:
-    reset_flag_trail(bool & value):
-        m_value(value) {
-    }
-    
-    virtual ~reset_flag_trail() {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_value = false;
-    }
-};
-
-template<typename Ctx, typename T>
-class set_ptr_trail : public trail<Ctx> {
-    T * & m_ptr;
-public:
-    set_ptr_trail(T * & ptr):
-        m_ptr(ptr) {
-        SASSERT(m_ptr == 0);
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_ptr = 0;
-    }
-};
-
-template<typename Ctx, typename T, bool CallDestructors=true>
-class restore_size_trail : public trail<Ctx> {
-    vector<T, CallDestructors> & m_vector;
-    unsigned                     m_old_size;
-public:
-    restore_size_trail(vector<T, CallDestructors> & v, unsigned sz):
-        m_vector(v),
-        m_old_size(sz) {
-    }
-    restore_size_trail(vector<T, CallDestructors> & v):
-        m_vector(v),
-        m_old_size(v.size()) {
-    }
-    virtual ~restore_size_trail() {
-    }
-    virtual void undo(Ctx & ctx) {
-        m_vector.shrink(m_old_size);
-    }
-};    
-        
-template<typename Ctx, typename T, bool CallDestructors=true>
-class vector_value_trail : public trail<Ctx> {
-    vector<T, CallDestructors> & m_vector;
-    unsigned                     m_idx;
-    T                            m_old_value;
-public:
-    vector_value_trail(vector<T, CallDestructors> & v, unsigned idx):
-        m_vector(v),
-        m_idx(idx),
-        m_old_value(v[idx]) {
-    }
-    
-    virtual ~vector_value_trail() {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector[m_idx] = m_old_value;
-    }
-};
-
-
-template<typename Ctx, typename D, typename R>
-class insert_obj_map : public trail<Ctx> {
-    obj_map<D,R>&     m_map;
-    D*                m_obj;
-public:
-    insert_obj_map(obj_map<D,R>& t, D* o) : m_map(t), m_obj(o) {}
-    virtual ~insert_obj_map() {}
-    virtual void undo(Ctx & ctx) { m_map.remove(m_obj); }
-};
-
-template<typename Ctx, typename M, typename D>
-class insert_map : public trail<Ctx> {
-    M&            m_map;
-    D             m_obj;
-public:
-    insert_map(M& t, D o) : m_map(t), m_obj(o) {}
-    virtual ~insert_map() {}
-    virtual void undo(Ctx & ctx) { m_map.remove(m_obj); }
-};
-
-
-
-template<typename Ctx, typename V>
-class push_back_vector : public trail<Ctx> {
-    V & m_vector;
-public:
-    push_back_vector(V & v):
-        m_vector(v) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector.pop_back();
-    }
-};
-
-template<typename Ctx, typename T>
-class set_vector_idx_trail : public trail<Ctx> {
-    ptr_vector<T> & m_vector;
-    unsigned                         m_idx;
-public:
-    set_vector_idx_trail(ptr_vector<T> & v, unsigned idx):
-        m_vector(v),
-        m_idx(idx) {
-    }
-    
-    virtual ~set_vector_idx_trail() {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector[m_idx] = 0;
-    }
-};
-    
-template<typename Ctx, typename T, bool CallDestructors=true>
-class pop_back_trail : public trail<Ctx> {
-    vector<T, CallDestructors> & m_vector;
-    T m_value;
-public:
-    pop_back_trail(vector<T, CallDestructors> & v):
-    m_vector(v),
-    m_value(m_vector.back()) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector.push_back(m_value);
-    }
-};
-
-template<typename Ctx, typename T, bool CallDestructors=true>
-class pop_back2_trail : public trail<Ctx> {
-    vector<T, CallDestructors> & m_vector;
-    typedef vector<vector<T, CallDestructors>, true> vector_t;
-    unsigned m_index;
-    T m_value;
-public:
-    pop_back2_trail(vector<T, CallDestructors> & v, unsigned index):
-    m_vector(v),
-    m_index(index),
-    m_value(m_vector[index].back()) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector[m_index].push_back(m_value);
-    }
-};
-
-
-template<typename S, typename T>
-class ast2ast_trailmap {
-    ref_vector<S, ast_manager> m_domain;
-    ref_vector<T, ast_manager> m_range;
-    obj_map<S, T*>             m_map;
-public:
-    ast2ast_trailmap(ast_manager& m):
-        m_domain(m),
-        m_range(m), 
-        m_map()
-    {}
-
-    bool find(S* s, T*& t) {
-        return m_map.find(s,t);
-    }
-    
-    void insert(S* s, T* t) {
-        SASSERT(!m_map.contains(s));
-        m_domain.push_back(s);
-        m_range.push_back(t);
-        m_map.insert(s,t);
-    }
-    
-    void pop() {
-        SASSERT(!m_domain.empty());
-        m_map.remove(m_domain.back());
-        m_domain.pop_back();
-        m_range.pop_back();
-    }
-};
-
-template<typename Ctx, typename S, typename T>
-class ast2ast_trail : public trail<Ctx> {
-    ast2ast_trailmap<S,T>& m_map;
-public:
-    ast2ast_trail(ast2ast_trailmap<S,T>& m, S* s, T* t) : 
-        m_map(m) {
-        m.insert(s,t);
-    }
-
-    virtual void undo(Ctx& ctx) {
-        m_map.pop();
-    }    
-};
-
-template<typename Ctx, typename T, bool CallDestructors=true>
-class push_back_trail : public trail<Ctx> {
-    vector<T, CallDestructors> & m_vector;
-public:
-    push_back_trail(vector<T, CallDestructors> & v):
-        m_vector(v) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector.pop_back();
-    }
-};
-
-template<typename Ctx, typename T, bool CallDestructors=true>
-class push_back2_trail : public trail<Ctx> {
-    typedef vector<vector<T, CallDestructors>, true> vector_t;
-    vector_t & m_vector;
-    unsigned   m_index;
-public:
-    push_back2_trail(vector_t & v, unsigned index) : 
-    m_vector(v),
-    m_index(index) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector[m_index].pop_back();
-    }
-};
-
-template<typename Ctx>
-class set_bitvector_trail : public trail<Ctx> {
-    svector<bool> & m_vector;
-    unsigned        m_idx;
-public:
-    set_bitvector_trail(svector<bool> & v, unsigned idx):
-        m_vector(v),
-        m_idx(idx) {
-        SASSERT(m_vector[m_idx] == false);
-        m_vector[m_idx] = true;
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector[m_idx] = false;
-    }
-};
-    
-template<typename Ctx, typename T>
-class new_obj_trail : public trail<Ctx> {
-    T * m_obj;
-public:
-    new_obj_trail(T * obj):
-        m_obj(obj) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        dealloc(m_obj);
-    }
-};
-
-template<typename Ctx, typename M, typename T>
-class obj_ref_trail : public trail<Ctx> {
-    obj_ref<T,M> m_obj;
-public:
-    obj_ref_trail(obj_ref<T,M>& obj):
-        m_obj(obj) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_obj.reset();
-    }
-};
-
-template<typename Ctx, typename T>
-class insert_obj_trail : public trail<Ctx> {
-    obj_hashtable<T>& m_table;
-    T*                m_obj;
-public:
-    insert_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
-    virtual ~insert_obj_trail() {}
-    virtual void undo(Ctx & ctx) { m_table.remove(m_obj); }
-};
-
-
-
-template<typename Ctx, typename T>
-class remove_obj_trail : public trail<Ctx> {
-    obj_hashtable<T>& m_table;
-    T*                m_obj;
-public:
-    remove_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
-    virtual ~remove_obj_trail() {}
-    virtual void undo(Ctx & ctx) { m_table.insert(m_obj); } 
-};
-
-
-template<typename Ctx>
-void undo_trail_stack(Ctx & ctx, ptr_vector<trail<Ctx> > & s, unsigned old_size) {
-    SASSERT(old_size <= s.size());
-    typename ptr_vector<trail<Ctx> >::iterator begin = s.begin() + old_size;
-    typename ptr_vector<trail<Ctx> >::iterator it    = s.end();
-    while (it != begin) {
-        --it;
-        (*it)->undo(ctx);
-    }
-    s.shrink(old_size);
-}
-
-template<typename Ctx>
-class trail_stack {
-    Ctx &                   m_ctx;
-    ptr_vector<trail<Ctx> > m_trail_stack;
-    unsigned_vector         m_scopes;
-    region                  m_region;
-public:
-    trail_stack(Ctx & c):m_ctx(c) {}
-
-    ~trail_stack() {}
-    
-    region & get_region() { return m_region; }
-    
-    void reset() { 
-        pop_scope(m_scopes.size()); 
-        // Undo trail objects stored at lvl 0 (avoid memory leaks if lvl 0 contains new_obj_trail objects).
-        undo_trail_stack(m_ctx, m_trail_stack, 0); 
-    }
-
-    void push_ptr(trail<Ctx> * t) { m_trail_stack.push_back(t); }
-
-    template<typename TrailObject>
-    void push(TrailObject const & obj) { m_trail_stack.push_back(new (m_region) TrailObject(obj)); }
-
-    unsigned get_num_scopes() const { return m_scopes.size(); }
-
-    void push_scope() { m_region.push_scope(); m_scopes.push_back(m_trail_stack.size()); }
-
-    void pop_scope(unsigned num_scopes) {
-        if (num_scopes == 0) return;
-        unsigned lvl      = m_scopes.size();
-        SASSERT(num_scopes <= lvl);
-        unsigned new_lvl  = lvl - num_scopes;
-        unsigned old_size = m_scopes[new_lvl];
-        undo_trail_stack(m_ctx, m_trail_stack, old_size);
-        m_scopes.shrink(new_lvl);
-        m_region.pop_scope(num_scopes);
-    }
-};
-
-#endif /* _TRAIL_H_ */
-