sync

src/ast/CMakeLists.txt

@@ -41,6 +41,7 @@ z3_add_component(ast
     reg_decl_plugins.cpp
     seq_decl_plugin.cpp
     shared_occs.cpp
+    special_relations_decl_plugin.cpp
     static_features.cpp
     used_vars.cpp
     well_sorted.cpp

src/ast/array_decl_plugin.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include "util/warning.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/arith_decl_plugin.h"
 
 array_decl_plugin::array_decl_plugin():
     m_store_sym("store"),
@@ -34,7 +35,8 @@ array_decl_plugin::array_decl_plugin():
     m_set_complement_sym("complement"),
     m_set_subset_sym("subset"),
     m_array_ext_sym("array-ext"),
-    m_as_array_sym("as-array") {
+    m_as_array_sym("as-array"),
+    m_set_has_size_sym("set-has-size") {
 }
 
 #define ARRAY_SORT_STR "Array"
@@ -141,7 +143,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
         std::ostringstream buffer;
         buffer << "map expects to take as many arguments as the function being mapped, "
                << "it was given " << arity << " but expects " << f->get_arity();
-        m_manager->raise_exception(buffer.str().c_str());
+        m_manager->raise_exception(buffer.str());
         return nullptr;
     }
     if (arity == 0) {
@@ -158,14 +160,14 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
         if (!is_array_sort(domain[i])) {
             std::ostringstream buffer;
             buffer << "map expects an array sort as argument at position " << i;
-            m_manager->raise_exception(buffer.str().c_str());
+            m_manager->raise_exception(buffer.str());
             return nullptr;
         }
         if (get_array_arity(domain[i]) != dom_arity) {
             std::ostringstream buffer;
             buffer << "map expects all arguments to have the same array domain,  "
                    << "this is not the case for argument " << i;
-            m_manager->raise_exception(buffer.str().c_str());
+            m_manager->raise_exception(buffer.str());
             return nullptr;
         }
         for (unsigned j = 0; j < dom_arity; ++j) {
@@ -173,7 +175,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
                 std::ostringstream buffer;
                 buffer << "map expects all arguments to have the same array domain, "
                        << "this is not the case for argument " << i;
-                m_manager->raise_exception(buffer.str().c_str());
+                m_manager->raise_exception(buffer.str());
                 return nullptr;
             }
         }
@@ -181,7 +183,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
             std::ostringstream buffer;
             buffer << "map expects the argument at position " << i 
                    << " to have the array range the same as the function";
-            m_manager->raise_exception(buffer.str().c_str());
+            m_manager->raise_exception(buffer.str());
             return nullptr;
         }
     }
@@ -244,7 +246,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
     if (num_parameters != arity) {
         std::stringstream strm;
         strm << "select requires " << num_parameters << " arguments, but was provided with " << arity << " arguments";
-        m_manager->raise_exception(strm.str().c_str());
+        m_manager->raise_exception(strm.str());
         return nullptr;
     }
     ptr_buffer<sort> new_domain; // we need this because of coercions.
@@ -256,7 +258,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
             std::stringstream strm;
             strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter ";
             strm << parameter_pp(parameters[i], *m_manager) << " do not match";
-            m_manager->raise_exception(strm.str().c_str());
+            m_manager->raise_exception(strm.str());
             UNREACHABLE();
             return nullptr;
         }
@@ -284,7 +286,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
         std::ostringstream buffer;
         buffer << "store expects the first argument to be an array taking " << num_parameters+1 
                << ", instead it was passed " << (arity - 1) << "arguments";
-        m_manager->raise_exception(buffer.str().c_str());
+        m_manager->raise_exception(buffer.str());
         UNREACHABLE();
         return nullptr;
     }
@@ -299,7 +301,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
         sort* srt2 = domain[i+1];
         if (!m_manager->compatible_sorts(srt1, srt2)) {
             std::stringstream strm;
-            strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt2, *m_manager) << " do not match";
+            strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt1, *m_manager) << " do not match";
             m_manager->raise_exception(strm.str());
             UNREACHABLE();
             return nullptr;
@@ -438,6 +440,25 @@ func_decl * array_decl_plugin::mk_set_subset(unsigned arity, sort * const * doma
                                    func_decl_info(m_family_id, OP_SET_SUBSET));
 }
 
+func_decl * array_decl_plugin::mk_set_has_size(unsigned arity, sort * const* domain) {
+    if (arity != 2) {
+        m_manager->raise_exception("set-has-size takes two arguments");
+        return nullptr;
+    }    
+    // domain[0] is a Boolean array,
+    // domain[1] is Int
+    arith_util arith(*m_manager);
+    if (!arith.is_int(domain[1])) {
+        m_manager->raise_exception("set-has-size expects second argument to be an integer");
+    }
+    if (!is_array_sort(domain[0]) || !m_manager->is_bool(get_array_range(domain[0]))) {
+        m_manager->raise_exception("set-has-size expects first argument to be an array of Booleans");
+    }
+    sort * bool_sort = m_manager->mk_bool_sort();
+    return m_manager->mk_func_decl(m_set_has_size_sym, arity, domain, bool_sort,
+                                   func_decl_info(m_family_id, OP_SET_HAS_SIZE));
+}
+
 func_decl * array_decl_plugin::mk_as_array(func_decl * f) {
     vector<parameter> parameters;
     for (unsigned i = 0; i < f->get_arity(); i++) {
@@ -502,6 +523,8 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         return mk_set_complement(arity, domain);
     case OP_SET_SUBSET:
         return mk_set_subset(arity, domain);
+    case OP_SET_HAS_SIZE:
+        return mk_set_has_size(arity, domain);
     case OP_AS_ARRAY: {
         if (num_parameters != 1 ||
             !parameters[0].is_ast() || 
@@ -544,6 +567,7 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
         op_names.push_back(builtin_name("subset",OP_SET_SUBSET));
         op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
         op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT));
+        op_names.push_back(builtin_name("set-has-size", OP_SET_HAS_SIZE));
     }
 }
 
@@ -576,6 +600,26 @@ func_decl * array_recognizers::get_as_array_func_decl(func_decl * f) const {
     return to_func_decl(f->get_parameter(0).get_ast()); 
 }
 
+bool array_recognizers::is_const(expr* e, expr*& v) const {
+    return is_const(e) && (v = to_app(e)->get_arg(0), true);
+}
+
+bool array_recognizers::is_store_ext(expr* _e, expr_ref& a, expr_ref_vector& args, expr_ref& value) {
+    if (is_store(_e)) {
+        app* e = to_app(_e);
+        a = e->get_arg(0);
+        unsigned sz = e->get_num_args();
+        args.reset();
+        for (unsigned i = 1; i < sz-1; ++i) {
+            args.push_back(e->get_arg(i));
+        }
+        value = e->get_arg(sz-1);
+        return true;
+    }
+    return false;
+}
+
+
 array_util::array_util(ast_manager& m): 
     array_recognizers(m.mk_family_id("array")),
     m_manager(m) {

src/ast/array_decl_plugin.h

@@ -51,6 +51,7 @@ enum array_op_kind {
     OP_SET_DIFFERENCE,
     OP_SET_COMPLEMENT,
     OP_SET_SUBSET,
+    OP_SET_HAS_SIZE,
     OP_AS_ARRAY, // used for model construction
     LAST_ARRAY_OP
 };
@@ -68,6 +69,7 @@ class array_decl_plugin : public decl_plugin {
     symbol m_set_subset_sym;
     symbol m_array_ext_sym;
     symbol m_as_array_sym;
+    symbol m_set_has_size_sym;
 
     bool check_set_arguments(unsigned arity, sort * const * domain);
 
@@ -95,6 +97,8 @@ class array_decl_plugin : public decl_plugin {
 
     func_decl * mk_as_array(func_decl * f);
 
+    func_decl* mk_set_has_size(unsigned arity, sort * const* domain);
+
     bool is_array_sort(sort* s) const;
  public:
     array_decl_plugin();
@@ -144,14 +148,20 @@ public:
     bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
     bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
     bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
+    bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); }
     bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
     bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
     bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
     bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
     bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
+    bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); }
     bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
     func_decl * get_as_array_func_decl(expr * n) const;
     func_decl * get_as_array_func_decl(func_decl* f) const;
+
+    bool is_const(expr* e, expr*& v) const;
+
+    bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value);
 };
 
 class array_util : public array_recognizers {
@@ -185,6 +195,10 @@ public:
         return mk_const_array(s, m_manager.mk_true());
     }
 
+    app* mk_has_size(expr* set, expr* n) {
+        return m_manager.mk_app(m_fid, OP_SET_HAS_SIZE, set, n);
+    }
+
     func_decl * mk_array_ext(sort* domain, unsigned i);
 
     sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); }

src/ast/ast.cpp

@@ -1584,8 +1584,8 @@ void ast_manager::raise_exception(char const * msg) {
     throw ast_exception(msg);
 }
 
-void ast_manager::raise_exception(std::string const&  msg) {
-    throw ast_exception(msg.c_str());
+void ast_manager::raise_exception(std::string &&  msg) {
+    throw ast_exception(std::move(msg));
 }
 
 
@@ -1875,7 +1875,6 @@ void ast_manager::delete_node(ast * n) {
 
     while ((n = m_ast_table.pop_erase())) {
 
-        TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";);
         CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";);
         TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";);
         TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";);

src/ast/ast.h

@@ -1574,7 +1574,7 @@ public:
 
     // Equivalent to throw ast_exception(msg)
     Z3_NORETURN void raise_exception(char const * msg);
-    Z3_NORETURN void raise_exception(std::string const& s);
+    Z3_NORETURN void raise_exception(std::string && s);
 
     std::ostream& display(std::ostream& out, parameter const& p);
 
@@ -2122,6 +2122,7 @@ public:
     app * mk_or(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2); }
     app * mk_and(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2); }
     app * mk_or(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2, arg3); }
+    app * mk_or(expr* a, expr* b, expr* c, expr* d) { expr* args[4] = { a, b, c, d }; return mk_app(m_basic_family_id, OP_OR, 4, args); }
     app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2, arg3); }
     app * mk_implies(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_IMPLIES, arg1, arg2); }
     app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); }

src/ast/ast_smt_pp.cpp

@@ -951,7 +951,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
         strm << "(set-logic " << m_logic << ")\n";
     }
     if (!m_attributes.empty()) {
-        strm << "; " << m_attributes.c_str();
+        strm << "; " << m_attributes;
     }
 
 #if 0

src/ast/ast_util.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include "ast/ast_util.h"
+#include "ast/arith_decl_plugin.h"
 
 app * mk_list_assoc_app(ast_manager & m, func_decl * f, unsigned num_args, expr * const * args) {
     SASSERT(f->is_associative());
@@ -361,3 +362,13 @@ void flatten_or(expr* fml, expr_ref_vector& result) {
     result.push_back(fml);
     flatten_or(result);
 }
+
+static app_ref plus(ast_manager& m, expr* a, expr* b) {
+    arith_util arith(m);
+    return app_ref(arith.mk_add(a, b), m);
+}
+
+
+app_ref operator+(expr_ref& a, expr_ref& b) { 
+    return plus(a.m(), a.get(), b.get()); 
+}

src/ast/ast_util.h

@@ -111,6 +111,17 @@ app  * mk_and(ast_manager & m, unsigned num_args, app * const * args);
 inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 
+inline app_ref operator&(expr_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); }
+inline app_ref operator&(app_ref& a,  expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); }
+inline app_ref operator&(var_ref& a,  expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); }
+inline app_ref operator&(quantifier_ref& a,  expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); }
+
+inline app_ref operator|(expr_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
+inline app_ref operator|(app_ref& a,  expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
+inline app_ref operator|(var_ref& a,  expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
+inline app_ref operator|(quantifier_ref& a,  expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
+app_ref operator+(expr_ref& a, expr_ref& b);
+
 /**
    Return (or args[0] ... args[num_args-1]) if num_args >= 2
    Return args[0]                           if num_args == 1
@@ -129,6 +140,9 @@ expr * mk_not(ast_manager & m, expr * arg);
 
 expr_ref mk_not(const expr_ref& e);
 
+inline app_ref mk_not(const app_ref& e) { return app_ref(e.m().mk_not(e), e.m()); }
+
+
 /**
    Negate and push over conjunction or disjunction.
  */

src/ast/bv_decl_plugin.cpp

@@ -624,7 +624,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
             if (m.get_sort(args[i]) != r->get_domain(i)) {
                 std::ostringstream buffer;
                 buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m);
-                m.raise_exception(buffer.str().c_str());
+                m.raise_exception(buffer.str());
                 return nullptr;
             }
         }

src/ast/datatype_decl_plugin.cpp

@@ -290,6 +290,7 @@ namespace datatype {
                     obj_map<sort, sort_size> S;
                     for (unsigned i = 0; i + 1 < num_parameters; ++i) {
                         sort* r = to_sort(parameters[i + 1].get_ast());
+                        TRACE("datatype", tout << "inserting " << mk_ismt2_pp(r, *m_manager) << " " << r->get_num_elements() << "\n";);
                         S.insert(d->params()[i], r->get_num_elements()); 
                     }
                     sort_size ts = d->sort_size()->eval(S);
@@ -342,7 +343,7 @@ namespace datatype {
                 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());
+                m.raise_exception(buffer.str());
                 return nullptr;
             }
             range = domain[0];
@@ -454,6 +455,7 @@ namespace datatype {
         }
 
         void plugin::log_axiom_definitions(symbol const& s, sort * new_sort) {
+            std::ostream& out = m_manager->trace_stream();
             symbol const& family_name = m_manager->get_family_name(get_family_id());
             for (constructor const* c : *m_defs[s]) {
                 func_decl_ref f = c->instantiate(new_sort);
@@ -462,19 +464,19 @@ namespace datatype {
 
                 // log constructor with quantified variables as arguments
                 for (unsigned i = 0; i < num_args; ++i) {
-                    m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n";
+                    out << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n";
                     ++m_id_counter;
                 }
                 const unsigned constructor_id = m_id_counter;
-                m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name();
+                out << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name();
                 for (unsigned i = 0; i < num_args; ++i) {
-                    m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i;
+                    out << " " << family_name << "#" << constructor_id - num_args + i;
                 }
-                m_manager->trace_stream() << "\n";
+                out << "\n";
                 ++m_id_counter;
 
                 // axioms for all accessors are generated when a constructor is applied => use constructor as pattern
-                m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n";
+                out << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n";
                 ++m_id_counter;
                 m_axiom_bases.insert(f->get_name(), constructor_id + 4);
                 std::ostringstream var_sorts;
@@ -487,14 +489,14 @@ namespace datatype {
                 unsigned i = 0;
                 for (accessor const* a : *c) {
                     func_decl_ref acc = a->instantiate(new_sort);
-                    m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n";
+                    out << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n";
                     ++m_id_counter;
-                    m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i 
+                    out << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i 
                         << " " << family_name << "#" << m_id_counter - 1 << "\n";
                     ++m_id_counter;
-                    m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1
+                    out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1
                         << " " << family_name << "#" << m_id_counter - 1 << "\n";
-                    m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n";
+                    out << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n";
                     ++m_id_counter;
                     ++i;
                 }
@@ -698,7 +700,7 @@ namespace datatype {
     }
 
     param_size::size* util::get_sort_size(sort_ref_vector const& params, sort* s) {
-        if (params.empty()) {
+        if (params.empty() && !is_datatype(s)) {
             return param_size::size::mk_offset(s->get_num_elements());
         }
         if (is_datatype(s)) {
@@ -747,6 +749,7 @@ namespace datatype {
         map<symbol, status, symbol_hash_proc, symbol_eq_proc> already_found;
         map<symbol, param_size::size*, symbol_hash_proc, symbol_eq_proc> szs;
 
+        TRACE("datatype", for (auto const& s : names) tout << s << " "; tout << "\n";);
         svector<symbol> todo(names);
         status st;
         while (!todo.empty()) {
@@ -785,6 +788,7 @@ namespace datatype {
             todo.pop_back();
             already_found.insert(s, BLACK);
             if (is_infinite) {
+                TRACE("datatype", tout << "infinite " << s << "\n";);
                 d.set_sort_size(param_size::size::mk_offset(sort_size::mk_infinite()));
                 continue;
             }
@@ -797,6 +801,7 @@ namespace datatype {
                 }
                 s_add.push_back(param_size::size::mk_times(s_mul));
             }
+            TRACE("datatype", tout << "set sort size " << s << "\n";);
             d.set_sort_size(param_size::size::mk_plus(s_add));
         }
     }
@@ -1193,6 +1198,85 @@ namespace datatype {
             }
         }
     }
+
+    sort_ref util::mk_list_datatype(sort* elem, symbol const& name, 
+                                    func_decl_ref& cons, func_decl_ref& is_cons, 
+                                    func_decl_ref& hd, func_decl_ref& tl, 
+                                    func_decl_ref& nil, func_decl_ref& is_nil) {
+
+        accessor_decl* head_tail[2] = {
+            mk_accessor_decl(m, symbol("head"), type_ref(elem)),
+            mk_accessor_decl(m, symbol("tail"), type_ref(0))
+        };
+        constructor_decl* constrs[2] = {
+            mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, nullptr),
+            mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail)
+        };
+        decl::plugin& p = *get_plugin();
+
+        sort_ref_vector sorts(m);
+        datatype_decl * decl = mk_datatype_decl(*this, name, 0, nullptr, 2, constrs);
+        bool is_ok = p.mk_datatypes(1, &decl, 0, nullptr, sorts);
+        del_datatype_decl(decl);
+        
+        if (!is_ok) {
+            return sort_ref(m);
+        }
+        sort* s = sorts.get(0);
+        ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
+        SASSERT(cnstrs.size() == 2);
+        nil = cnstrs[0];
+        is_nil = get_constructor_is(cnstrs[0]);
+        cons = cnstrs[1];
+        is_cons = get_constructor_is(cnstrs[1]);
+        ptr_vector<func_decl> const& acc = *get_constructor_accessors(cnstrs[1]);
+        SASSERT(acc.size() == 2);
+        hd = acc[0];
+        tl = acc[1];
+        return sort_ref(s, m);
+    }
+
+    sort_ref util::mk_pair_datatype(sort* a, sort* b, func_decl_ref& fst, func_decl_ref& snd, func_decl_ref& pair) {
+        type_ref t1(a), t2(b);
+        accessor_decl* fstd = mk_accessor_decl(m, symbol("fst"), t1);
+        accessor_decl* sndd = mk_accessor_decl(m, symbol("snd"), t2);
+        accessor_decl* accd[2] = { fstd, sndd };
+        auto * p = mk_constructor_decl(symbol("pair"), symbol("is-pair"), 2, accd);
+        auto* dt = mk_datatype_decl(*this, symbol("pair"), 0, nullptr, 1, &p);
+        sort_ref_vector sorts(m);
+        VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts));
+        del_datatype_decl(dt);
+        sort* s = sorts.get(0);
+        ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
+        SASSERT(cnstrs.size() == 1);
+        ptr_vector<func_decl> const& acc = *get_constructor_accessors(cnstrs[0]);
+        SASSERT(acc.size() == 2);
+        fst = acc[0];
+        snd = acc[1];
+        pair = cnstrs[0];
+        return sort_ref(s, m);
+    }
+
+    sort_ref util::mk_tuple_datatype(svector<std::pair<symbol, sort*>> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs) {
+        ptr_vector<accessor_decl> accd;
+        for (auto const& e : elems) {
+            type_ref t(e.second);
+            accd.push_back(mk_accessor_decl(m, e.first, t));
+        }
+        auto* tuple = mk_constructor_decl(name, test, accd.size(), accd.c_ptr());
+        auto* dt = mk_datatype_decl(*this, name, 0, nullptr, 1, &tuple);
+        sort_ref_vector sorts(m);
+        VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts));
+        del_datatype_decl(dt);
+        sort* s = sorts.get(0);
+        ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
+        SASSERT(cnstrs.size() == 1);
+        ptr_vector<func_decl> const& acc = *get_constructor_accessors(cnstrs[0]);
+        for (auto* f : acc) accs.push_back(f);
+        tup = cnstrs[0];
+        return sort_ref(s, m);
+    }
+
 }
 
 datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs) {

src/ast/datatype_decl_plugin.h

@@ -364,6 +364,12 @@ namespace datatype {
         decl::plugin* get_plugin() { return m_plugin; }
         void get_defs(sort* s, ptr_vector<def>& defs);
         def const& get_def(sort* s) const;
+        sort_ref mk_list_datatype(sort* elem, symbol const& name,
+                                  func_decl_ref& cons, func_decl_ref& is_cons, 
+                                  func_decl_ref& hd, func_decl_ref& tl, 
+                                  func_decl_ref& nil, func_decl_ref& is_nil);
+        sort_ref mk_pair_datatype(sort* a, sort* b, func_decl_ref& fst, func_decl_ref& snd, func_decl_ref& pair);
+        sort_ref mk_tuple_datatype(svector<std::pair<symbol, sort*>> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs);
     };
 
 };

src/ast/display_dimacs.cpp

@@ -26,6 +26,7 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
     ptr_vector<expr> exprs;
     unsigned num_vars = 0;
     unsigned num_cls  = fmls.size();
+    bool is_from_dimacs = true;
     for (expr * f : fmls) {
         unsigned num_lits;
         expr * const * lits;
@@ -41,10 +42,51 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
             expr * l = lits[j];
             if (m.is_not(l))
                 l = to_app(l)->get_arg(0);
-            if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
-                num_vars++;
-                expr2var.setx(l->get_id(), num_vars, UINT_MAX);
-                exprs.setx(l->get_id(), l, nullptr);
+            if (!is_uninterp_const(l)) {
+                is_from_dimacs = false;
+                break;
+            }
+            symbol const& s = to_app(l)->get_decl()->get_name();
+            if (s.is_numerical() && s.get_num() > 0) {
+                if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
+                    ++num_vars;
+                    expr2var.setx(l->get_id(), s.get_num(), UINT_MAX);
+                    exprs.setx(l->get_id(), l, nullptr);
+                }
+                continue;
+            }
+            is_from_dimacs = false;
+            break;            
+        }
+        if (!is_from_dimacs) {
+            num_vars = 0;
+            expr2var.reset();
+            exprs.reset();
+            break;
+        }
+    }
+    
+    if (!is_from_dimacs) {
+        for (expr * f : fmls) {
+            unsigned num_lits;
+            expr * const * lits;
+            if (m.is_or(f)) {
+                num_lits = to_app(f)->get_num_args();
+                lits     = to_app(f)->get_args();
+            }
+            else {
+                num_lits = 1;
+                lits     = &f;
+            }
+            for (unsigned j = 0; j < num_lits; j++) {
+                expr * l = lits[j];
+                if (m.is_not(l))
+                    l = to_app(l)->get_arg(0);
+                if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
+                    num_vars++;
+                    expr2var.setx(l->get_id(), num_vars, UINT_MAX);
+                    exprs.setx(l->get_id(), l, nullptr);
+                }
             }
         }
     }
@@ -71,10 +113,12 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
         }
         out << "0\n";
     }
-    for (expr* e : exprs) {
-        if (e && is_app(e)) {
-            symbol const& n = to_app(e)->get_decl()->get_name();
-            out << "c " << expr2var[e->get_id()] << " " << n << "\n";            
+    if (!is_from_dimacs) {
+        for (expr* e : exprs) {
+            if (e && is_app(e)) {
+                symbol const& n = to_app(e)->get_decl()->get_name();
+                out << "c " << expr2var[e->get_id()] << " " << n << "\n";            
+            }
         }
     }
     return out;

src/ast/dl_decl_plugin.cpp

@@ -54,7 +54,7 @@ namespace datalog {
         }
         std::ostringstream buffer;
         buffer << msg << ", value is not within bound " << low << " <= " << val << " <= " << up;
-        m_manager->raise_exception(buffer.str().c_str());
+        m_manager->raise_exception(buffer.str());
         return false;
     }
 
@@ -676,7 +676,7 @@ namespace datalog {
         }
         std::stringstream strm;
         strm << "sort '" << mk_pp(s, m) << "' is not recognized as a sort that contains numeric values.\nUse Bool, BitVec, Int, Real, or a Finite domain sort";
-        m.raise_exception(strm.str().c_str());
+        m.raise_exception(strm.str());
         return nullptr;
     }
 

src/ast/expr_substitution.cpp

@@ -65,8 +65,8 @@ std::ostream& expr_substitution::display(std::ostream& out) {
 }
 
 void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
-    obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0); 
-    if (entry->get_data().m_value == 0) {
+    obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, nullptr); 
+    if (entry->get_data().m_value == nullptr) {
         // new entry
         m_manager.inc_ref(c);
         m_manager.inc_ref(def);
@@ -89,14 +89,14 @@ void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_depend
         entry->get_data().m_value = def;
         if (proofs_enabled()) {
             obj_map<expr, proof*>::obj_map_entry * entry_pr = m_subst_pr->find_core(c);
-            SASSERT(entry_pr != 0);
+            SASSERT(entry_pr != nullptr);
             m_manager.inc_ref(def_pr);
             m_manager.dec_ref(entry_pr->get_data().m_value);
             entry_pr->get_data().m_value = def_pr;
         }
         if (unsat_core_enabled()) {
             obj_map<expr, expr_dependency*>::obj_map_entry * entry_dep = m_subst_dep->find_core(c);
-            SASSERT(entry_dep != 0);
+            SASSERT(entry_dep != nullptr);
             m_manager.inc_ref(def_dep);
             m_manager.dec_ref(entry_dep->get_data().m_value);
             entry_dep->get_data().m_value = def_dep;

src/ast/fpa/fpa2bv_converter.cpp

@@ -1986,15 +1986,17 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref &
 
     SASSERT(is_well_sorted(m, v4));
 
-    // exponent >= sbits-1
+    // exponent >= sbits-1 -> x
     expr_ref exp_is_large(m);
-    exp_is_large = m_bv_util.mk_sle(m_bv_util.mk_numeral(sbits-1, ebits), a_exp);
+    exp_is_large = log2(sbits-1)+1 <= ebits-1 ?
+                        m_bv_util.mk_sle(m_bv_util.mk_numeral(sbits-1, ebits), a_exp) :
+                        m.mk_false();
     dbg_decouple("fpa2bv_r2i_exp_is_large", exp_is_large);
     c5 = exp_is_large;
     v5 = x;
 
     // Actual conversion with rounding.
-    // x.exponent >= 0 && x.exponent < x.sbits - 1
+    // exponent >= 0 && exponent < sbits - 1
 
     expr_ref res_sgn(m), res_sig(m), res_exp(m);
     res_sgn = a_sgn;
@@ -2070,7 +2072,6 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref &
     m_simp.mk_ite(c53, v53, res_sig, res_sig);
     m_simp.mk_ite(c52, v52, res_sig, res_sig);
     m_simp.mk_ite(c51, v51, res_sig, res_sig);
-    res_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(res_sig, m_bv_util.mk_numeral(0, 3))); // rounding bits are all 0.
 
     SASSERT(m_bv_util.get_bv_size(res_exp) == ebits);
     SASSERT(m_bv_util.get_bv_size(shift) == sbits);
@@ -2082,11 +2083,37 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref &
     res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), e_shift);
 
     SASSERT(m_bv_util.get_bv_size(res_sgn) == 1);
-    SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
+    SASSERT(m_bv_util.get_bv_size(res_sig) == sbits);
     SASSERT(m_bv_util.get_bv_size(res_exp) == ebits + 2);
 
-    // CMW: We use the rounder for normalization.
-    round(s, rm, res_sgn, res_sig, res_exp, v6);
+    // Renormalize
+    expr_ref zero_e2(m), min_exp(m), sig_lz(m), max_exp_delta(m), sig_lz_capped(m), renorm_delta(m);
+    zero_e2 = m_bv_util.mk_numeral(0, ebits+2);
+    mk_min_exp(ebits, min_exp);
+    min_exp = m_bv_util.mk_sign_extend(2, min_exp);
+    mk_leading_zeros(res_sig, ebits+2, sig_lz);
+    max_exp_delta = m_bv_util.mk_bv_sub(res_exp, min_exp);
+    sig_lz_capped = m.mk_ite(m_bv_util.mk_sle(sig_lz, max_exp_delta), sig_lz, max_exp_delta);
+    renorm_delta = m.mk_ite(m_bv_util.mk_sle(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2);
+    SASSERT(m_bv_util.get_bv_size(renorm_delta) == ebits + 2);
+    res_exp = m_bv_util.mk_bv_sub(res_exp, renorm_delta);
+    res_sig = m_bv_util.mk_bv_shl(res_sig, m_bv_util.mk_zero_extend(sbits-ebits-2, renorm_delta));
+    dbg_decouple("fpa2bv_r2i_renorm_delta", renorm_delta);
+
+    res_exp = m_bv_util.mk_extract(ebits-1, 0, res_exp);
+    mk_bias(res_exp, res_exp);
+    res_sig = m_bv_util.mk_extract(sbits-2, 0, res_sig);
+    v6 = m_util.mk_fp(res_sgn, res_exp, res_sig);
+
+    dbg_decouple("fpa2bv_r2i_res_sgn", res_sgn);
+    dbg_decouple("fpa2bv_r2i_res_sig", res_sig);
+    dbg_decouple("fpa2bv_r2i_res_exp", res_exp);
+
+    dbg_decouple("fpa2bv_r2i_c1", c1);
+    dbg_decouple("fpa2bv_r2i_c2", c2);
+    dbg_decouple("fpa2bv_r2i_c3", c3);
+    dbg_decouple("fpa2bv_r2i_c4", c4);
+    dbg_decouple("fpa2bv_r2i_c5", c5);
 
     // And finally, we tie them together.
     mk_ite(c5, v5, v6, result);

src/ast/normal_forms/defined_names.cpp

@@ -159,11 +159,11 @@ void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbo
         expr * patterns[1] = { m.mk_pattern(name) };
         quantifier_ref q(m);
         q = m.mk_forall(sorts.size(),
-                                sorts.c_ptr(),
-                                names.c_ptr(),
-                                def_conjunct,
-                                1, qid, symbol::null,
-                                1, patterns);
+                        sorts.c_ptr(),
+                        names.c_ptr(),
+                        def_conjunct,
+                        1, qid, symbol::null,
+                        1, patterns);
         TRACE("mk_definition_bug", tout << "before elim_unused_vars:\n" << mk_ismt2_pp(q, m) << "\n";);
         result = elim_unused_vars(m, q, params_ref());
         TRACE("mk_definition_bug", tout << "after elim_unused_vars:\n" << result << "\n";);

src/ast/pattern/expr_pattern_match.cpp

@@ -52,35 +52,57 @@ expr_pattern_match::match_quantifier(quantifier* qf, app_ref_vector& patterns, u
     }
     m_regs[0] = qf->get_expr();
     for (unsigned i = 0; i < m_precompiled.size(); ++i) {
-        quantifier* qf2 = m_precompiled[i].get();
-        if (qf2->get_kind() != qf->get_kind() || is_lambda(qf)) {
-            continue;
-        }
-        if (qf2->get_num_decls() != qf->get_num_decls()) {
-            continue;
-        }
-        subst s;
-        if (match(qf->get_expr(), m_first_instrs[i], s)) {
-            for (unsigned j = 0; j < qf2->get_num_patterns(); ++j) {
-                app* p = static_cast<app*>(qf2->get_pattern(j));
-                expr_ref p_result(m_manager);
-                instantiate(p, qf->get_num_decls(), s, p_result);
-                patterns.push_back(to_app(p_result.get()));
-            }
-            weight = qf2->get_weight();
-            return true;            
+        if (match_quantifier(i, qf, patterns, weight)) 
+            return true;
+    }    
+    return false;
+}
+
+bool
+expr_pattern_match::match_quantifier(unsigned i, quantifier* qf, app_ref_vector& patterns, unsigned& weight) {
+    quantifier* qf2 = m_precompiled[i].get();
+    if (qf2->get_kind() != qf->get_kind() || is_lambda(qf)) {
+        return false;
+    }
+    if (qf2->get_num_decls() != qf->get_num_decls()) {
+        return false;
+    }
+    subst s;
+    if (match(qf->get_expr(), m_first_instrs[i], s)) {
+        for (unsigned j = 0; j < qf2->get_num_patterns(); ++j) {
+            app* p = static_cast<app*>(qf2->get_pattern(j));
+            expr_ref p_result(m_manager);
+            instantiate(p, qf->get_num_decls(), s, p_result);
+            patterns.push_back(to_app(p_result.get()));
         }
+        weight = qf2->get_weight();
+        return true;            
     }
     return false;
 }
 
+bool expr_pattern_match::match_quantifier_index(quantifier* qf, app_ref_vector& patterns, unsigned& index) {
+    if (m_regs.empty()) return false;
+    m_regs[0] = qf->get_expr();
+
+    for (unsigned i = 0; i < m_precompiled.size(); ++i) {
+        unsigned weight = 0;
+        if (match_quantifier(i, qf, patterns, weight)) {
+            index = i;
+            return true;
+        }
+    }    
+    return false;
+}
+
+
 void
 expr_pattern_match::instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result) {
     bound b;
     for (unsigned i = 0; i < num_bound; ++i) {
         b.insert(m_bound_dom[i], m_bound_rng[i]);
     }
-    
+    TRACE("expr_pattern_match", tout << mk_pp(a, m_manager) << " " << num_bound << "\n";);
     inst_proc proc(m_manager, s, b, m_regs);
     for_each_ast(proc, a);
     expr* v = nullptr;
@@ -251,11 +273,7 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s)
             break;
         }
         case CHECK_BOUND:
-            TRACE("expr_pattern_match", 
-                  tout 
-                  << "check bound " 
-                  << pc.m_num_bound << " " << pc.m_reg;
-                  );
+            TRACE("expr_pattern_match", tout << "check bound " << pc.m_num_bound << " " << pc.m_reg << "\n";);
             ok = m_bound_rng[pc.m_num_bound] == m_regs[pc.m_reg];
             break;            
         case BIND:
@@ -396,11 +414,18 @@ expr_pattern_match::initialize(char const * spec_string) {
     for (expr * e : ctx.assertions()) {
         compile(e);
     }
-    TRACE("expr_pattern_match", display(tout); );
 }
 
-void 
-expr_pattern_match::display(std::ostream& out) const {
+unsigned expr_pattern_match::initialize(quantifier* q) {
+    if (m_instrs.empty()) {
+        m_instrs.push_back(instr(BACKTRACK));
+    }    
+    compile(q);
+    return m_precompiled.size() - 1;
+}
+
+
+void expr_pattern_match::display(std::ostream& out) const {
     for (unsigned i = 0; i < m_instrs.size(); ++i) {
         display(out, m_instrs[i]);
     }
@@ -414,7 +439,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
         break;
     case BIND:
         out << "bind       ";
-        out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
         out << mk_pp(pc.m_pat, m_manager) << "\n";
         out << "next:      " << pc.m_next << "\n";
         out << "offset:    " << pc.m_offset << "\n";
@@ -422,7 +446,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
         break;
     case BIND_AC:
         out << "bind_ac    ";
-        out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
         out << mk_pp(pc.m_pat, m_manager) << "\n";
         out << "next:      " << pc.m_next << "\n";
         out << "offset:    " << pc.m_offset << "\n";
@@ -430,7 +453,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
         break;
     case BIND_C:
         out << "bind_c     ";
-        out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
         out << mk_pp(pc.m_pat, m_manager) << "\n";
         out << "next:      " << pc.m_next << "\n";
         out << "offset:    " << pc.m_offset << "\n";

src/ast/pattern/expr_pattern_match.h

@@ -80,13 +80,7 @@ class expr_pattern_match {
         }
 
         void operator()(var* v) {
-            var* b = nullptr;
-            if (m_bound.find(v, b)) {
-                m_memoize.insert(v, b);
-            }
-            else {
-                UNREACHABLE();
-            }
+            m_memoize.insert(v, m_bound[v]);
         }
                 
         void operator()(app * n) {  
@@ -98,15 +92,9 @@ class expr_pattern_match {
             if (m_subst.find(decl, r)) {
                 decl = to_app(m_regs[r])->get_decl();
             }
-            for (unsigned i = 0; i < num_args; ++i) {
-                expr* arg = nullptr;
-                if (m_memoize.find(n->get_arg(i), arg)) {
-                    SASSERT(arg);
-                    args.push_back(arg);
-                }
-                else {
-                    UNREACHABLE();
-                }
+            for (expr* arg : *n) {
+                arg = m_memoize[arg];
+                args.push_back(arg);
             }
             if (m_manager.is_pattern(n)) {
                 result = m_manager.mk_pattern(num_args, reinterpret_cast<app**>(args.c_ptr()));
@@ -116,7 +104,6 @@ class expr_pattern_match {
             }
             m_pinned.push_back(result);
             m_memoize.insert(n, result);
-            return;
         }
     };
 
@@ -131,11 +118,14 @@ class expr_pattern_match {
  public:
     expr_pattern_match(ast_manager & manager);
     ~expr_pattern_match();
-    virtual bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight);
-    virtual void initialize(char const * database);
+    bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight);
+    bool match_quantifier_index(quantifier* qf, app_ref_vector & patterns, unsigned& index);
+    unsigned initialize(quantifier* qf);
+    void initialize(char const * database);
     void display(std::ostream& out) const;
 
  private:
+    bool match_quantifier(unsigned i, quantifier * qf, app_ref_vector & patterns, unsigned & weight);
     void instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result);
     void compile(expr* q);
     bool match(expr* a, unsigned init, subst& s);

src/ast/recfun_decl_plugin.cpp

@@ -50,7 +50,7 @@ namespace recfun {
     }
 
     def::def(ast_manager &m, family_id fid, symbol const & s,
-             unsigned arity, sort* const * domain, sort* range)
+             unsigned arity, sort* const * domain, sort* range, bool is_generated)
         :   m(m), m_name(s),
             m_domain(m, arity, domain), 
             m_range(range, m), m_vars(m), m_cases(),
@@ -59,7 +59,8 @@ namespace recfun {
             m_fid(fid)
     {
         SASSERT(arity == get_arity());        
-        func_decl_info info(fid, OP_FUN_DEFINED);
+        parameter p(is_generated);
+        func_decl_info info(fid, OP_FUN_DEFINED, 1, &p);
         m_decl = m.mk_func_decl(s, arity, domain, range, info);
     }
 
@@ -238,6 +239,7 @@ namespace recfun {
                 while (! stack.empty()) {
                     expr * e = stack.back();
                     stack.pop_back();
+                    TRACEFN("unfold: " << mk_pp(e, m));
 
                     if (m.is_ite(e)) {
                         // need to do a case split on `e`, forking the search space
@@ -257,6 +259,7 @@ namespace recfun {
             if (b.to_split != nullptr) {
                 // split one `ite`, which will lead to distinct (sets of) cases
                 app * ite = b.to_split->ite;
+                TRACEFN("split: " << mk_pp(ite, m));
                 expr* c = nullptr, *th = nullptr, *el = nullptr;
                 VERIFY(m.is_ite(ite, c, th, el));
 
@@ -287,6 +290,7 @@ namespace recfun {
                 
                 // substitute, to get rid of `ite` terms
                 expr_ref case_rhs = subst(rhs);
+                TRACEFN("case_rhs: " << case_rhs);
                 for (unsigned i = 0; i < conditions.size(); ++i) {
                     conditions[i] = subst(conditions.get(i));
                 }
@@ -312,10 +316,11 @@ namespace recfun {
     util::~util() {
     }
 
-    def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range) {
-        return alloc(def, m(), m_fid, name, n, domain, range);
+    def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range, bool is_generated) {
+        return alloc(def, m(), m_fid, name, n, domain, range, is_generated);
     }
 
+
     void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
         d.set_definition(subst, n_vars, vars, rhs);
     }
@@ -382,9 +387,19 @@ namespace recfun {
             return *(m_util.get());
         }
 
-        promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range) {
-            def* d = u().decl_fun(name, n, params, range);
-            SASSERT(! m_defs.contains(d->get_decl()));
+        promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) {
+            def* d = u().decl_fun(name, n, params, range, is_generated);
+            SASSERT(!m_defs.contains(d->get_decl()));
+            m_defs.insert(d->get_decl(), d);
+            return promise_def(&u(), d);
+        }
+
+        promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) {
+            def* d = u().decl_fun(name, n, params, range, is_generated);
+            def* d2 = nullptr;
+            if (m_defs.find(d->get_decl(), d2)) {
+                dealloc(d2);
+            }
             m_defs.insert(d->get_decl(), d);
             return promise_def(&u(), d);
         }

src/ast/recfun_decl_plugin.h

@@ -108,7 +108,7 @@ namespace recfun {
         expr_ref            m_rhs;  //!< definition
         family_id           m_fid;
 
-        def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range);
+        def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range, bool is_generated);
 
         // compute cases for a function, given its RHS (possibly containing `ite`).
         void compute_cases(replace& subst, is_immediate_pred &, 
@@ -147,6 +147,7 @@ namespace recfun {
         class plugin : public decl_plugin {
             typedef obj_map<func_decl, def*> def_map;
             typedef obj_map<func_decl, case_def*> case_def_map;
+            
 
             mutable scoped_ptr<util> m_util;
             def_map                  m_defs;       // function->def
@@ -171,7 +172,9 @@ namespace recfun {
             func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                      unsigned arity, sort * const * domain, sort * range) override;
             
-            promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range);
+            promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false);
+
+            promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false);
             
             void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
             
@@ -214,6 +217,7 @@ namespace recfun {
         bool is_case_pred(expr * e) const { return is_app_of(e, m_fid, OP_FUN_CASE_PRED); }
         bool is_defined(expr * e) const { return is_app_of(e, m_fid, OP_FUN_DEFINED); }
         bool is_defined(func_decl* f) const { return is_decl_of(f, m_fid, OP_FUN_DEFINED); }
+        bool is_generated(func_decl* f) const { return is_defined(f) && f->get_parameter(0).get_int() == 1; }
         bool is_depth_limit(expr * e) const { return is_app_of(e, m_fid, OP_DEPTH_LIMIT); }
         bool owns_app(app * e) const { return e->get_family_id() == m_fid; }
 
@@ -221,8 +225,7 @@ namespace recfun {
         bool has_defs() const { return m_plugin->has_defs(); }
 
         //<! add a function declaration
-        def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range);
-
+        def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range, bool is_generated);
 
         def& get_def(func_decl* f) {
             SASSERT(m_plugin->has_def(f));

src/ast/reg_decl_plugins.cpp

@@ -27,6 +27,7 @@ Revision History:
 #include "ast/seq_decl_plugin.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/fpa_decl_plugin.h"
+#include "ast/special_relations_decl_plugin.h"
 
 void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("arith")))) {
@@ -56,4 +57,7 @@ void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("pb")))) {
         m.register_plugin(symbol("pb"), alloc(pb_decl_plugin));
     }
+    if (!m.get_plugin(m.mk_family_id(symbol("special_relations")))) {
+        m.register_plugin(symbol("special_relations"), alloc(special_relations_decl_plugin));
+    }
 }

src/ast/rewriter/CMakeLists.txt

@@ -19,6 +19,7 @@ z3_add_component(rewriter
     factor_equivs.cpp
     factor_rewriter.cpp
     fpa_rewriter.cpp
+    func_decl_replace.cpp
     hoist_rewriter.cpp
     inj_axiom.cpp
     label_rewriter.cpp

src/ast/rewriter/array_rewriter.cpp

@@ -36,36 +36,48 @@ void array_rewriter::get_param_descrs(param_descrs & r) {
 
 br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(f->get_family_id() == get_fid());
-    TRACE("array_rewriter", tout << mk_pp(f, m()) << "\n";
-          for (unsigned i = 0; i < num_args; ++i) {
-              tout << mk_pp(args[i], m()) << "\n";
-          });
+    br_status st;
     switch (f->get_decl_kind()) {
     case OP_SELECT:
-        return mk_select_core(num_args, args, result);
+        st = mk_select_core(num_args, args, result);
+        break;
     case OP_STORE:
-        return mk_store_core(num_args, args, result);
+        st = mk_store_core(num_args, args, result);
+        break;
     case OP_ARRAY_MAP:
         SASSERT(f->get_num_parameters() == 1);
         SASSERT(f->get_parameter(0).is_ast());
         SASSERT(is_func_decl(f->get_parameter(0).get_ast()));
-        return mk_map_core(to_func_decl(f->get_parameter(0).get_ast()), num_args, args, result);
+        st = mk_map_core(to_func_decl(f->get_parameter(0).get_ast()), num_args, args, result);
+        break;
     case OP_SET_UNION:
-        return mk_set_union(num_args, args, result);
+        st = mk_set_union(num_args, args, result);
+        break;
     case OP_SET_INTERSECT:
-        return mk_set_intersect(num_args, args, result);
+        st = mk_set_intersect(num_args, args, result);
+        break;
     case OP_SET_SUBSET: 
         SASSERT(num_args == 2);
-        return mk_set_subset(args[0], args[1], result);
+        st = mk_set_subset(args[0], args[1], result);
+        break;
     case OP_SET_COMPLEMENT:
         SASSERT(num_args == 1);
-        return mk_set_complement(args[0], result);
+        st = mk_set_complement(args[0], result);
+        break;
     case OP_SET_DIFFERENCE:
         SASSERT(num_args == 2);
-        return mk_set_difference(args[0], args[1], result);
+        st = mk_set_difference(args[0], args[1], result);
+        break;
     default:
         return BR_FAILED;
     }
+    TRACE("array_rewriter", tout << mk_pp(f, m()) << "\n";
+          for (unsigned i = 0; i < num_args; ++i) {
+              tout << mk_pp(args[i], m()) << "\n";
+          }
+          tout << "\n --> " << result << "\n";
+          );
+    return st;
 }
 
 // l_true  -- all equal
@@ -230,105 +242,98 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
 }
 
 br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
-    SASSERT(num_args >= 0);
-    bool is_store0 = m_util.is_store(args[0]);
-    bool is_const0 = m_util.is_const(args[0]);
-    if (num_args == 1) {
-        //
-        // map_f (store a j v) = (store (map_f a) j (f v)) 
-        //
-        if (is_store0) {
-            app * store_expr = to_app(args[0]);
-            unsigned num_args = store_expr->get_num_args();
-            SASSERT(num_args >= 3);
-            expr * a = store_expr->get_arg(0);
-            expr * v = store_expr->get_arg(num_args-1);
-            
-            ptr_buffer<expr> new_args;
-            
-            new_args.push_back(m_util.mk_map(f, 1, &a)); // (map_f a)
-            new_args.append(num_args - 2, store_expr->get_args() + 1); // j
-            new_args.push_back(m().mk_app(f, v));   // (f v)
-            
-            result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr());
-            return BR_REWRITE2;
-        }
-        
-        //
-        // map_f (const v) = (const (f v))
-        //
-        if (is_const0) {
-            expr * fv = m().mk_app(f, to_app(args[0])->get_arg(0));
-            result = m_util.mk_const_array(m().get_sort(args[0]), fv);
-            return BR_REWRITE2;
-        }
-        return BR_FAILED;
-    }
 
-    SASSERT(num_args > 1);
-    
-    if (is_store0) {
-        unsigned num_indices = to_app(args[0])->get_num_args() - 2;
-        unsigned i;
-        for (i = 1; i < num_args; i++) {
-            if (!m_util.is_store(args[i]))
-                break;
-            unsigned j;
-            for (j = 1; j < num_indices+1; j++) {
-                if (to_app(args[0])->get_arg(j) != to_app(args[i])->get_arg(j))
-                    break;
-            }
-            if (j < num_indices+1)
-                break;
+    app* store_expr = nullptr;
+    unsigned num_indices = 0;
+    bool same_store = true;
+    for (unsigned i = 0; same_store && i < num_args; i++) {
+        expr* a = args[i];
+        if (m_util.is_const(a)) {
+            continue;
         }
-        //
-        // map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n))
-        //
-        if (i == num_args) {
-            ptr_buffer<expr> arrays;
-            ptr_buffer<expr> values;
-            for (unsigned i = 0; i < num_args; i++) {
-                arrays.push_back(to_app(args[i])->get_arg(0));
-                values.push_back(to_app(args[i])->get_arg(num_indices+1));
+        else if (!m_util.is_store(a)) {
+            same_store = false;
+        }
+        else if (!store_expr) {
+            num_indices = to_app(a)->get_num_args() - 2;
+            store_expr = to_app(a);
+        }
+        else {
+            for (unsigned j = 1; same_store && j < num_indices + 1; j++) {
+                same_store = (store_expr->get_arg(j) == to_app(a)->get_arg(j));
             }
+        }
+    }
+    
+    //
+    // map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n))
+    //
+    if (same_store) {
+        ptr_buffer<expr> arrays;
+        ptr_buffer<expr> values;
+        for (unsigned i = 0; i < num_args; i++) {
+            expr* a = args[i];
+            if (m_util.is_const(a)) {
+                arrays.push_back(a);
+                values.push_back(to_app(a)->get_arg(0));
+            }
+            else {
+                arrays.push_back(to_app(a)->get_arg(0));
+                values.push_back(to_app(a)->get_arg(num_indices+1));
+            }
+        }
+        if (store_expr) {
             ptr_buffer<expr> new_args;
             new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr()));
             new_args.append(num_indices, to_app(args[0])->get_args() + 1);
             new_args.push_back(m().mk_app(f, values.size(), values.c_ptr()));
             result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr());
-            return BR_REWRITE2;
         }
-        return BR_FAILED;
+        else {
+            expr_ref value(m().mk_app(f, values.size(), values.c_ptr()), m());
+            sort* s0 = m().get_sort(args[0]);
+            unsigned sz = get_array_arity(s0);
+            ptr_vector<sort> domain;
+            for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i));
+            sort_ref s(m_util.mk_array_sort(sz, domain.c_ptr(), m().get_sort(value)), m());
+            result = m_util.mk_const_array(s, value);
+        }
+        return BR_REWRITE2;
     }
 
-    if (is_const0) {
-        unsigned i;
-        for (i = 1; i < num_args; i++) {
-            if (!m_util.is_const(args[i]))
-                break;
+    //
+    // map_f (lambda x1 b1) ... (lambda x1 bn) -> lambda x1 (f b1 .. bn)
+    //
+    quantifier* lam = nullptr;
+    for (unsigned i = 0; i < num_args; ++i) {
+        if (is_lambda(args[i])) {
+            lam = to_quantifier(args[i]);
         }
-        if (i == num_args) {
-            //
-            // map_f (const v_1) ... (const v_n) = (const (f v_1 ... v_n))
-            //
-            ptr_buffer<expr> values;
-            for (unsigned i = 0; i < num_args; i++) {
-                values.push_back(to_app(args[i])->get_arg(0));
+    }
+    if (lam) {
+        expr_ref_vector args1(m());
+        for (unsigned i = 0; i < num_args; ++i) {
+            expr* a = args[i];
+            if (m_util.is_const(a)) {
+                args1.push_back(to_app(a)->get_arg(0));
+            }
+            else if (is_lambda(a)) {
+                lam = to_quantifier(a);
+                args1.push_back(lam->get_expr());
+            }
+            else {
+                expr_ref_vector sel(m());
+                sel.push_back(a);
+                unsigned n = lam->get_num_decls();
+                for (unsigned i = 0; i < n; ++i) {
+                    sel.push_back(m().mk_var(n - i - 1, lam->get_decl_sort(i)));
+                }
+                args1.push_back(m_util.mk_select(sel.size(), sel.c_ptr()));
             }
-            
-            expr * fv = m().mk_app(f, values.size(), values.c_ptr());
-            sort * in_s = get_sort(args[0]);
-            ptr_vector<sort> domain;
-            unsigned domain_sz = get_array_arity(in_s);
-            for (unsigned i = 0; i < domain_sz; i++) 
-                domain.push_back(get_array_domain(in_s, i));
-            sort_ref out_s(m());
-            out_s = m_util.mk_array_sort(domain_sz, domain.c_ptr(), f->get_range());
-            parameter p(out_s.get());
-            result = m().mk_app(get_fid(), OP_CONST_ARRAY, 1, &p, 1, &fv);
-            return BR_REWRITE2;
         }
-        return BR_FAILED;
+        result = m().mk_app(f, args1.size(), args1.c_ptr());
+        result = m().update_quantifier(lam, result);
+        return BR_REWRITE3;        
     }
 
     return BR_FAILED;
@@ -396,10 +401,107 @@ br_status array_rewriter::mk_set_subset(expr * arg1, expr * arg2, expr_ref & res
     return BR_REWRITE3;
 }
 
+void array_rewriter::mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls) {
+    expr_ref tmp1(m()), tmp2(m());
+    expr_ref a(m()), v(m());
+    expr_ref_vector args0(m()), args(m());
+    while (m_util.is_store_ext(e, a, args0, v)) {                                        
+        args.reset();
+        args.push_back(lhs);
+        args.append(args0);
+        mk_select(args.size(), args.c_ptr(), tmp1);                     
+        args[0] = rhs;                                                  
+        mk_select(args.size(), args.c_ptr(), tmp2);                     
+        fmls.push_back(m().mk_eq(tmp1, tmp2));    
+        e = a;
+    }                                                
+}
+
+bool array_rewriter::has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector>& indices) {
+    expr_ref_vector args(m());
+    expr_ref a(m()), v(m());
+    a = e;
+    while (m_util.is_store_ext(e, a, args, v)) {
+        indices.push_back(args);
+        e = a;
+    }
+    e0 = e;
+    if (is_lambda(e0)) {
+        quantifier* q = to_quantifier(e0);
+        e = q->get_expr();
+        unsigned num_idxs = q->get_num_decls();
+        expr* e1, *e2, *e3;
+        ptr_vector<expr> eqs;
+        while (!is_ground(e) && m().is_ite(e, e1, e2, e3) && is_ground(e2)) {
+            args.reset();
+            args.resize(num_idxs, nullptr);
+            eqs.reset();
+            eqs.push_back(e1);
+            for (unsigned i = 0; i < eqs.size(); ++i) {
+                expr* e = eqs[i];
+                if (m().is_and(e)) {
+                    eqs.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+                }
+                else if (m().is_eq(e, e1, e2)) {
+                    if (is_var(e2)) {
+                        std::swap(e1, e2);
+                    }
+                    if (is_var(e1) && is_ground(e2)) {
+                        unsigned idx = to_var(e1)->get_idx();
+                        args[num_idxs - idx - 1] = e2;
+                    }
+                    else {
+                        return false;
+                    }
+                }                
+            }
+            for (unsigned i = 0; i < num_idxs; ++i) {
+                if (!args.get(i)) return false;
+            }
+            indices.push_back(args);
+            e = e3;
+        }
+        e0 = e;
+        return is_ground(e);
+    }
+    return true;
+}
+
 br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
+    TRACE("array_rewriter", tout << mk_pp(lhs, m()) << " " << mk_pp(rhs, m()) << "\n";);
+    expr* v = nullptr;
+    if (m_util.is_const(rhs) && is_lambda(lhs)) {
+        std::swap(lhs, rhs);
+    }
+    if (m_util.is_const(lhs, v) && is_lambda(rhs)) {
+        quantifier* lam = to_quantifier(rhs);
+        expr_ref e(m().mk_eq(lam->get_expr(), v), m());
+        result = m().update_quantifier(lam, quantifier_kind::forall_k, e);
+        return BR_REWRITE2; 
+    }
     if (!m_expand_store_eq) {
         return BR_FAILED;
     }
+    expr_ref_vector fmls(m());
+
+#if 0
+    // lambda friendly version of array equality rewriting.
+    vector<expr_ref_vector> indices;
+    expr_ref lhs0(m()), rhs0(m());
+    expr_ref tmp1(m()), tmp2(m());
+    if (has_index_set(lhs, lhs0, indices) && has_index_set(rhs, rhs0, indices) && lhs0 == rhs0) {
+        expr_ref_vector args(m());
+        for (auto const& idxs : indices) {
+            args.reset();
+            args.push_back(lhs);
+            args.append(idxs);
+            mk_select(args.size(), args.c_ptr(), tmp1);
+            args[0] = rhs;
+            mk_select(args.size(), args.c_ptr(), tmp2);
+            fmls.push_back(m().mk_eq(tmp1, tmp2));
+        }
+    }
+#endif
     expr* lhs1 = lhs;
     while (m_util.is_store(lhs1)) {
         lhs1 = to_app(lhs1)->get_arg(0);
@@ -411,25 +513,9 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
     if (lhs1 != rhs1) {
         return BR_FAILED;
     }
-    ptr_buffer<expr> fmls, args;
-    expr* e;
-    expr_ref tmp1(m()), tmp2(m());
-#define MK_EQ()                                                         \
-    while (m_util.is_store(e)) {                                        \
-        args.push_back(lhs);                                            \
-        args.append(to_app(e)->get_num_args()-2,to_app(e)->get_args()+1); \
-        mk_select(args.size(), args.c_ptr(), tmp1);                     \
-        args[0] = rhs;                                                  \
-        mk_select(args.size(), args.c_ptr(), tmp2);                     \
-        fmls.push_back(m().mk_eq(tmp1, tmp2));                          \
-        e = to_app(e)->get_arg(0);                                      \
-        args.reset();                                                   \
-    }                                                \
-    
-    e = lhs;
-    MK_EQ();
-    e = rhs;
-    MK_EQ();
+
+    mk_eq(lhs, lhs, rhs, fmls);
+    mk_eq(rhs, lhs, rhs, fmls);
     result = m().mk_and(fmls.size(), fmls.c_ptr());
     return BR_REWRITE_FULL;
 }

src/ast/rewriter/array_rewriter.h

@@ -35,6 +35,8 @@ class array_rewriter {
     bool          m_expand_select_ite;
     template<bool CHECK_DISEQ>
     lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2);
+    bool has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector>& indices);
+    void mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls);
 public:    
     array_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         m_util(m) {
@@ -43,6 +45,7 @@ public:
     }
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
+    array_util& util() { return m_util; }
 
     void set_expand_select_store(bool f) { m_expand_select_store = f; }
     void set_expand_select_ite(bool f) { m_expand_select_ite = f; }
@@ -66,6 +69,20 @@ public:
     br_status mk_set_difference(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_set_subset(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+
+    expr_ref mk_set_difference(expr* a, expr* b) {
+        expr_ref result(m());
+        mk_set_difference(a, b, result);
+        return result;
+    }
+
+    expr_ref mk_set_intersect(expr* a, expr* b) {
+        expr_ref result(m());
+        expr* args[2] = { a, b };
+        mk_set_intersect(2, args, result);
+        return result;
+    }
+
 };
 
 #endif

src/ast/rewriter/bool_rewriter.cpp

@@ -24,6 +24,7 @@ void bool_rewriter::updt_params(params_ref const & _p) {
     bool_rewriter_params p(_p);
     m_flat                 = p.flat();
     m_elim_and             = p.elim_and();
+    m_elim_ite             = p.elim_ite();
     m_local_ctx            = p.local_ctx();
     m_local_ctx_limit      = p.local_ctx_limit();
     m_blast_distinct       = p.blast_distinct();
@@ -797,48 +798,52 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
                 result = c;
                 return BR_DONE;
             }
-            mk_or(c, e, result);
-            return BR_DONE;
+            if (m_elim_ite) {
+                mk_or(c, e, result);
+                return BR_DONE;
+            }
         }
         if (m().is_false(t)) {
             if (m().is_true(e)) {
                 mk_not(c, result);
                 return BR_DONE;
             }
-            expr_ref tmp(m());
-            mk_not(c, tmp);
-            mk_and(tmp, e, result);
-            return BR_DONE;
+            if (m_elim_ite) {
+                expr_ref tmp(m());
+                mk_not(c, tmp);
+                mk_and(tmp, e, result);
+                return BR_DONE;
+            }
         }
-        if (m().is_true(e)) {
+        if (m().is_true(e) && m_elim_ite) {            
             expr_ref tmp(m());
             mk_not(c, tmp);
             mk_or(tmp, t, result);
             return BR_DONE;
         }
-        if (m().is_false(e)) {
+        if (m().is_false(e) && m_elim_ite) {
             mk_and(c, t, result);
             return BR_DONE;
         }
-        if (c == e) {
+        if (c == e && m_elim_ite) {
             mk_and(c, t, result);
             return BR_DONE;
         }
-        if (c == t) {
+        if (c == t && m_elim_ite) {
             mk_or(c, e, result);
             return BR_DONE;
         }
-        if (m().is_complement_core(t, e)) { // t = not(e)
+        if (m().is_complement_core(t, e) && m_elim_ite) { // t = not(e)
             mk_eq(c, t, result);
             return BR_DONE;
         }
-        if (m().is_complement_core(e, t)) { // e = not(t)
+        if (m().is_complement_core(e, t) && m_elim_ite) { // e = not(t)
             mk_eq(c, t, result);
             return BR_DONE;
         }
     }
 
-    if (m().is_ite(t) && m_ite_extra_rules) {
+    if (m().is_ite(t) && m_ite_extra_rules && m_elim_ite) {
         // (ite c1 (ite c2 t1 t2) t1) ==> (ite (and c1 (not c2)) t2 t1)
         if (e == to_app(t)->get_arg(1)) {
             expr_ref not_c2(m());
@@ -891,7 +896,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
         }
     }
 
-    if (m().is_ite(e) && m_ite_extra_rules) {
+    if (m().is_ite(e) && m_ite_extra_rules && m_elim_ite) {
         // (ite c1 t1 (ite c2 t1 t2)) ==> (ite (or c1 c2)        t1 t2)
         if (t == to_app(e)->get_arg(1)) {
             expr_ref new_c(m());

src/ast/rewriter/bool_rewriter.h

@@ -59,6 +59,7 @@ class bool_rewriter {
     bool           m_ite_extra_rules;
     unsigned       m_local_ctx_limit;
     unsigned       m_local_ctx_cost;
+    bool           m_elim_ite;
 
     br_status mk_flat_and_core(unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_flat_or_core(unsigned num_args, expr * const * args, expr_ref & result);

src/ast/rewriter/bool_rewriter_params.pyg

@@ -4,6 +4,7 @@ def_module_params(module_name='rewriter',
                   params=(("ite_extra_rules", BOOL, False, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"),
                           ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"),
                           ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"),
+                          ('elim_ite', BOOL, True,  "eliminate ite in favor of and/or"),
                           ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"),
                           ("local_ctx_limit", UINT, UINT_MAX, "limit for applying local context simplifier"),
                           ("blast_distinct", BOOL, False, "expand a distinct predicate into a quadratic number of disequalities"), 

src/ast/rewriter/bv_rewriter.cpp

@@ -500,12 +500,14 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
     // (bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1))
     // (bvsle (+ x (* -1 (srem_i x c1))) c2)
     // pre: (and (> c1 0) (> c2 0) (= c2 % c1 0) (<= (+ c1 c2 -1) max_int))
-    if (is_signed && is_num2 && m_util.is_bv_add(a, a1, a2) &&
+    if (is_signed && is_num2 && 
+        m_util.is_bv_add(a, a1, a2) &&
         m_util.is_bv_mul(a2, a3, a4) && is_numeral(a3, r1, sz) &&
         m_util.norm(r1, sz, is_signed).is_minus_one() &&
         m_util.is_bv_sremi(a4, a5, a6) && is_numeral(a6, r1, sz) &&
         (r1 = m_util.norm(r1, sz, is_signed), r1.is_pos()) &&
         r2.is_pos() &&
+        (a1 == a5) && 
         (r2 % r1).is_zero() && r1 + r2 - rational::one() < rational::power_of_two(sz-1)) {
         result = m_util.mk_sle(a1, m_util.mk_numeral(r1 + r2 - rational::one(), sz));
         return BR_REWRITE2;

src/ast/rewriter/enum2bv_rewriter.cpp

@@ -86,7 +86,7 @@ struct enum2bv_rewriter::imp {
         void throw_non_fd(expr* e) {
             std::stringstream strm;
             strm << "unable to handle nested data-type expression " << mk_pp(e, m);
-            throw rewriter_exception(strm.str().c_str());
+            throw rewriter_exception(strm.str());
         }
 
         void check_for_fd(unsigned n, expr* const* args) {

src/ast/rewriter/func_decl_replace.cpp

@@ -0,0 +1,97 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    func_decl_replace.cpp
+
+Abstract:
+
+    Replace functions in expressions.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-03-28
+
+Revision History:
+
+
+--*/
+
+
+#include "ast/rewriter/func_decl_replace.h"
+
+expr_ref func_decl_replace::operator()(expr* e) {
+    m_todo.push_back(e);
+    
+    while (!m_todo.empty()) {
+        expr* a = m_todo.back(), *b;
+        if (m_cache.contains(a)) {
+            m_todo.pop_back();
+        }
+        else if (is_var(a)) {
+            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();
+            m_args.reset();            
+            bool arg_differs = false;
+            for (unsigned i = 0; i < n; ++i) {
+                expr* d = nullptr, *arg = c->get_arg(i);
+                if (m_cache.find(arg, d)) {
+                    m_args.push_back(d);
+                    arg_differs |= arg != d;
+                    SASSERT(m.get_sort(arg) == m.get_sort(d));
+                }
+                else {
+                    m_todo.push_back(arg);
+                }
+            }
+            if (m_args.size() == n) {
+                if (arg_differs) {
+                    b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
+                    m_refs.push_back(b);
+                    SASSERT(m.get_sort(a) == m.get_sort(b));
+                } else {
+                    b = a;
+                }
+                func_decl* f = nullptr;
+                if (m_subst.find(c->get_decl(), f)) {
+                    b = m.mk_app(f, m_args.size(), m_args.c_ptr());
+                    m_refs.push_back(b);
+                }
+                m_cache.insert(a, b);
+                m_todo.pop_back();
+            }
+        }
+        else {
+            quantifier* q = to_quantifier(a);
+            SASSERT(is_quantifier(a));
+            expr* body = q->get_expr(), *new_body;
+            if (m_cache.find(body, new_body)) {
+                if (new_body == body) {
+                    b = a;
+                }
+                else {
+                    b = m.update_quantifier(q, new_body);
+                    m_refs.push_back(b);
+                }
+                m_cache.insert(a, b);
+                m_todo.pop_back();
+            }
+            else {
+                m_todo.push_back(body);
+            }
+        }        
+    }
+    return expr_ref(m_cache.find(e), m);
+}
+
+void func_decl_replace::reset() {
+    m_cache.reset();
+    m_subst.reset();
+    m_refs.reset();
+    m_funs.reset();
+}

src/ast/rewriter/func_decl_replace.h

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    func_decl_replace.h
+
+Abstract:
+
+    Replace functions in expressions.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-03-28
+
+Revision History:
+
+
+--*/
+
+#ifndef FUNC_DECL_REPLACE_H_
+#define FUNC_DECL_REPLACE_H_
+
+#include "ast/ast.h"
+
+class func_decl_replace {
+    ast_manager& m;
+    obj_map<func_decl, func_decl*> m_subst;
+    obj_map<expr, expr*> m_cache;
+    ptr_vector<expr>     m_todo, m_args;
+    expr_ref_vector      m_refs;
+    func_decl_ref_vector m_funs;
+
+public:
+    func_decl_replace(ast_manager& m): m(m), m_refs(m), m_funs(m) {}
+
+    void insert(func_decl* src, func_decl* dst) { m_subst.insert(src, dst); m_funs.push_back(src), m_funs.push_back(dst); }
+
+    expr_ref operator()(expr* e);
+
+    void reset();
+
+    bool empty() const { return m_subst.empty(); }
+};
+
+#endif /* FUNC_DECL_REPLACE_H_ */

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -28,7 +28,7 @@ Notes:
 #include "util/uint_set.h"
 #include "util/gparams.h"
 
-const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17};
+static const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17};
 
 
 struct pb2bv_rewriter::imp {
@@ -161,7 +161,6 @@ struct pb2bv_rewriter::imp {
             }
 
             if (m_pb_solver == "segmented") {
-                expr_ref result(m);
                 switch (is_le) {
                 case l_true:  return mk_seg_le(k);
                 case l_false: return mk_seg_ge(k);
@@ -169,6 +168,11 @@ struct pb2bv_rewriter::imp {
                 }
             }
 
+            if (m_pb_solver == "binary_merge") {
+                expr_ref result = binary_merge(is_le, k);
+                if (result) return result;
+            }
+
             // fall back to divide and conquer encoding.
             SASSERT(k.is_pos());
             expr_ref zero(m), bound(m);
@@ -494,6 +498,37 @@ struct pb2bv_rewriter::imp {
             return true;
         }
 
+        /**
+           \brief binary merge encoding.
+        */
+        expr_ref binary_merge(lbool is_le, rational const& k) {
+            expr_ref result(m);
+            unsigned_vector coeffs;
+            for (rational const& c : m_coeffs) {
+                if (c.is_unsigned()) {
+                    coeffs.push_back(c.get_unsigned());
+                }
+                else {
+                    return result;
+                }
+            }
+            if (!k.is_unsigned()) {
+                return result;
+            }
+            switch (is_le) {
+            case l_true: 
+                result = m_sort.le(k.get_unsigned(), coeffs.size(), coeffs.c_ptr(), m_args.c_ptr());
+                break;
+            case l_false:
+                result = m_sort.ge(k.get_unsigned(), coeffs.size(), coeffs.c_ptr(), m_args.c_ptr());
+                break;
+            case l_undef:
+                result = m_sort.eq(k.get_unsigned(), coeffs.size(), coeffs.c_ptr(), m_args.c_ptr());
+                break;
+            }
+            return result;
+        }
+
         /**
            \brief Segment based encoding.
            The PB terms are partitoned into segments, such that each segment contains arguments with the same cofficient.

src/ast/rewriter/rewriter.h

@@ -300,7 +300,7 @@ protected:
     void process_var(var * v);
 
     template<bool ProofGen>
-    void process_const(app * t);
+    bool process_const(app * t);
 
     template<bool ProofGen>
     bool visit(expr * t, unsigned max_depth);

src/ast/rewriter/rewriter_def.h

@@ -80,27 +80,42 @@ void rewriter_tpl<Config>::process_var(var * v) {
 
 template<typename Config>
 template<bool ProofGen>
-void rewriter_tpl<Config>::process_const(app * t) {
+bool rewriter_tpl<Config>::process_const(app * t0) {
+    app_ref t(t0, m());
+    bool retried = false;
+ retry:
     SASSERT(t->get_num_args() == 0);
     br_status st = m_cfg.reduce_app(t->get_decl(), 0, nullptr, m_r, m_pr);
     SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
-    SASSERT(st == BR_FAILED || st == BR_DONE);
-    if (st == BR_DONE) {
+    switch (st) {
+    case BR_FAILED:
+        if (!retried) {
+            result_stack().push_back(t);
+            if (ProofGen)
+                result_pr_stack().push_back(nullptr); // implicit reflexivity
+            return true;
+        }
+        m_r = t;
+        // fall through
+    case BR_DONE:
         result_stack().push_back(m_r.get());
         if (ProofGen) {
             if (m_pr)
                 result_pr_stack().push_back(m_pr);
             else
-                result_pr_stack().push_back(m().mk_rewrite(t, m_r));
+                result_pr_stack().push_back(m().mk_rewrite(t0, m_r));
             m_pr = nullptr;
         }
         m_r = nullptr;
-        set_new_child_flag(t);
-    }
-    else {
-        result_stack().push_back(t);
-        if (ProofGen)
-            result_pr_stack().push_back(nullptr); // implicit reflexivity
+        set_new_child_flag(t0);
+        return true;
+    default: 
+        if (is_app(m_r) && to_app(m_r)->get_num_args() == 0) {
+            t = to_app(m_r);
+            retried = true;
+            goto retry;
+        }
+        return false;
     }
 }
 
@@ -115,6 +130,7 @@ void rewriter_tpl<Config>::process_const(app * t) {
 template<typename Config>
 template<bool ProofGen>
 bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
+ // retry:
     TRACE("rewriter_visit", tout << "visiting\n" << mk_ismt2_pp(t, m()) << "\n";);
     expr *  new_t = nullptr;
     proof * new_t_pr = nullptr;
@@ -164,15 +180,14 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
     switch (t->get_kind()) {
     case AST_APP:
         if (to_app(t)->get_num_args() == 0) {
-            process_const<ProofGen>(to_app(t));
-            return true;
-        }
-        else {
-            if (max_depth != RW_UNBOUNDED_DEPTH)
-                max_depth--;
-            push_frame(t, c, max_depth);
-            return false;
+            if (process_const<ProofGen>(to_app(t))) 
+                return true; 
+            t = m_r;
         }
+        if (max_depth != RW_UNBOUNDED_DEPTH)
+            max_depth--;
+        push_frame(t, c, max_depth);
+        return false;        
     case AST_VAR:
         process_var<ProofGen>(to_var(t));
         return true;
@@ -224,7 +239,7 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
-    SASSERT(t->get_num_args() > 0);
+    // SASSERT(t->get_num_args() > 0);
     SASSERT(!frame_stack().empty());
     switch (fr.m_state) {
     case PROCESS_CHILDREN: {

src/ast/rewriter/rewriter_types.h

@@ -46,7 +46,7 @@ inline br_status unsigned2br_status(unsigned u) {
 
 class rewriter_exception : public default_exception {
 public:                                                
-    rewriter_exception(char const * msg):default_exception(msg) {}
+    rewriter_exception(std::string && msg) : default_exception(std::move(msg)) {}
 };
 
 #endif

src/ast/rewriter/seq_rewriter.cpp

@@ -391,44 +391,57 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         
     case OP_SEQ_UNIT:
         SASSERT(num_args == 1);
-        return mk_seq_unit(args[0], result);
+        st = mk_seq_unit(args[0], result);
+        break;
     case OP_SEQ_EMPTY:
         return BR_FAILED;
     case OP_RE_PLUS:
         SASSERT(num_args == 1);
-        return mk_re_plus(args[0], result);
+        st = mk_re_plus(args[0], result);
+        break;
     case OP_RE_STAR:
         SASSERT(num_args == 1);
         st = mk_re_star(args[0], result);
         break;
     case OP_RE_OPTION:
         SASSERT(num_args == 1);
-        return mk_re_opt(args[0], result);
+        st = mk_re_opt(args[0], result);
+        break;
     case OP_RE_CONCAT:
         if (num_args == 1) {
             result = args[0]; 
-            return BR_DONE;
+            st = BR_DONE;
+        }
+        else {
+            SASSERT(num_args == 2);
+            st = mk_re_concat(args[0], args[1], result); 
         }
-        SASSERT(num_args == 2);
-        st = mk_re_concat(args[0], args[1], result); 
         break;
     case OP_RE_UNION:
         if (num_args == 1) {
-            result = args[0]; return BR_DONE;
+            result = args[0]; 
+            st = BR_DONE;
         }
-        SASSERT(num_args == 2);
-        return mk_re_union(args[0], args[1], result);
+        else {
+            SASSERT(num_args == 2);
+            st = mk_re_union(args[0], args[1], result);
+        }
+        break;
     case OP_RE_RANGE:
         SASSERT(num_args == 2);
-        return mk_re_range(args[0], args[1], result);
+        st = mk_re_range(args[0], args[1], result);
+        break;
     case OP_RE_INTERSECT:
         SASSERT(num_args == 2);
-        return mk_re_inter(args[0], args[1], result);
+        st = mk_re_inter(args[0], args[1], result);
+        break;
     case OP_RE_COMPLEMENT:
         SASSERT(num_args == 1);
-        return mk_re_complement(args[0], result);
+        st = mk_re_complement(args[0], result);
+        break;
     case OP_RE_LOOP:
-        return mk_re_loop(num_args, args, result);
+        st = mk_re_loop(num_args, args, result);
+        break;
     case OP_RE_EMPTY_SET:
         return BR_FAILED;    
     case OP_RE_FULL_SEQ_SET:
@@ -442,23 +455,29 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_SEQ_CONCAT: 
         if (num_args == 1) {
             result = args[0];
-            return BR_DONE;
+            st = BR_DONE;
         }
-        SASSERT(num_args == 2);
-        return mk_seq_concat(args[0], args[1], result);
+        else {
+            SASSERT(num_args == 2);
+            st = mk_seq_concat(args[0], args[1], result);
+        }
+        break;
     case OP_SEQ_LENGTH:
         SASSERT(num_args == 1);
-        return mk_seq_length(args[0], result);
+        st = mk_seq_length(args[0], result);
+        break;
     case OP_SEQ_EXTRACT:
         SASSERT(num_args == 3);
         st = mk_seq_extract(args[0], args[1], args[2], result);
         break;
     case OP_SEQ_CONTAINS: 
         SASSERT(num_args == 2);
-        return mk_seq_contains(args[0], args[1], result);
+        st = mk_seq_contains(args[0], args[1], result);
+        break;
     case OP_SEQ_AT:
         SASSERT(num_args == 2);
-        return mk_seq_at(args[0], args[1], result); 
+        st = mk_seq_at(args[0], args[1], result); 
+        break;
 #if 0
     case OP_SEQ_NTH:
         SASSERT(num_args == 2);
@@ -466,35 +485,49 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
 #endif
     case OP_SEQ_PREFIX: 
         SASSERT(num_args == 2);
-        return mk_seq_prefix(args[0], args[1], result);
+        st = mk_seq_prefix(args[0], args[1], result);
+        break;
     case OP_SEQ_SUFFIX: 
         SASSERT(num_args == 2);
-        return mk_seq_suffix(args[0], args[1], result);
+        st = mk_seq_suffix(args[0], args[1], result);
+        break;
     case OP_SEQ_INDEX:
         if (num_args == 2) {
             expr_ref arg3(m_autil.mk_int(0), m());
             result = m_util.str.mk_index(args[0], args[1], arg3);
-            return BR_REWRITE1;
+            st = BR_REWRITE1;
         }
-        SASSERT(num_args == 3);
-        return mk_seq_index(args[0], args[1], args[2], result);
+        else {
+            SASSERT(num_args == 3);
+            st = mk_seq_index(args[0], args[1], args[2], result);
+        }
+        break;
+    case OP_SEQ_LAST_INDEX:
+        SASSERT(num_args == 2);
+        st = mk_seq_last_index(args[0], args[1], result);
+        break;
     case OP_SEQ_REPLACE:
         SASSERT(num_args == 3);
-        return mk_seq_replace(args[0], args[1], args[2], result);
+        st = mk_seq_replace(args[0], args[1], args[2], result);
+        break;
     case OP_SEQ_TO_RE:
         SASSERT(num_args == 1);
-        return mk_str_to_regexp(args[0], result);
+        st = mk_str_to_regexp(args[0], result);
+        break;
     case OP_SEQ_IN_RE:
         SASSERT(num_args == 2);
-        return mk_str_in_regexp(args[0], args[1], result);
+        st = mk_str_in_regexp(args[0], args[1], result);
+        break;
     case OP_STRING_CONST:
         return BR_FAILED;
     case OP_STRING_ITOS: 
         SASSERT(num_args == 1);
-        return mk_str_itos(args[0], result);
+        st = mk_str_itos(args[0], result);
+        break;
     case OP_STRING_STOI: 
         SASSERT(num_args == 1);
-        return mk_str_stoi(args[0], result);
+        st = mk_str_stoi(args[0], result);
+        break;
     case _OP_STRING_CONCAT:
     case _OP_STRING_PREFIX:
     case _OP_STRING_SUFFIX:
@@ -908,6 +941,18 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 
+br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
+    zstring s1, s2;
+    bool isc1 = m_util.str.is_string(a, s1);
+    bool isc2 = m_util.str.is_string(b, s2);
+    if (isc1 && isc2) {
+        int idx = s1.last_indexof(s2);
+        result = m_autil.mk_numeral(rational(idx), true);
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
 br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) {
     zstring s1, s2;
     rational r;

src/ast/rewriter/seq_rewriter.h

@@ -116,6 +116,7 @@ class seq_rewriter {
     br_status mk_seq_at(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_nth(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result);
+    br_status mk_seq_last_index(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result);

src/ast/rewriter/th_rewriter.cpp

@@ -32,6 +32,7 @@ Notes:
 #include "ast/rewriter/var_subst.h"
 #include "ast/expr_substitution.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
 #include "ast/ast_util.h"
 #include "ast/well_sorted.h"
 
@@ -184,7 +185,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                     st = m_ar_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_seq_rw.get_fid())
                     st = m_seq_rw.mk_eq_core(args[0], args[1], result);
-
                 if (st != BR_FAILED)
                     return st;
             }
@@ -583,6 +583,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             m().trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << tmp->get_id() << "\n";
             m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n";
             m().trace_stream() << "[end-of-instance]\n";
+            m().trace_stream().flush();
         }
 
         if (st != BR_DONE && st != BR_FAILED) {
@@ -661,6 +662,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 p1 = m().mk_pull_quant(old_q, q1);
             }
         }
+        else if (
+                 old_q->get_kind() == lambda_k &&
+                 is_ground(new_body)) {
+            result = m_ar_rw.util().mk_const_array(old_q->get_sort(), new_body);
+            result_pr = nullptr;
+            return true;
+        }
         else {
             ptr_buffer<expr> new_patterns_buf;
             ptr_buffer<expr> new_no_patterns_buf;
@@ -677,10 +685,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             TRACE("reduce_quantifier", tout << mk_ismt2_pp(old_q, m()) << "\n----->\n" << mk_ismt2_pp(q1, m()) << "\n";);
             SASSERT(is_well_sorted(m(), q1));
         }
-
         SASSERT(m().get_sort(old_q) == m().get_sort(q1));
         result = elim_unused_vars(m(), q1, params_ref());
 
+
         TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << "\n";);
 
         result_pr = nullptr;
@@ -839,3 +847,13 @@ expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args)
 void th_rewriter::set_solver(expr_solver* solver) {
     m_imp->set_solver(solver);
 }
+
+
+bool th_rewriter::reduce_quantifier(quantifier * old_q, 
+                                    expr * new_body, 
+                                    expr * const * new_patterns, 
+                                    expr * const * new_no_patterns,
+                                    expr_ref & result,
+                                    proof_ref & result_pr) {
+    return m_imp->cfg().reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
+}

src/ast/rewriter/th_rewriter.h

@@ -41,7 +41,7 @@ public:
     static void get_param_descrs(param_descrs & r);
     unsigned get_cache_size() const;
     unsigned get_num_steps() const;
-
+   
     void operator()(expr_ref& term);
     void operator()(expr * t, expr_ref & result);
     void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
@@ -49,6 +49,13 @@ public:
 
     expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args);
 
+    bool reduce_quantifier(quantifier * old_q, 
+                           expr * new_body, 
+                           expr * const * new_patterns, 
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr);
+
     void cleanup();
     void reset();
 

src/ast/seq_decl_plugin.cpp

@@ -273,6 +273,21 @@ int zstring::indexof(zstring const& other, int offset) const {
     return -1;
 }
 
+int zstring::last_indexof(zstring const& other) const {
+    if (other.length() == 0) return length();
+    if (other.length() > length()) return -1;
+    for (unsigned last = length() - other.length(); last-- > 0; ) {
+        bool suffix = true;
+        for (unsigned j = 0; suffix && j < other.length(); ++j) {
+            suffix = m_buffer[last + j] == other[j];
+        }
+        if (suffix) {
+            return static_cast<int>(last);
+        }
+    }
+    return -1;
+}
+
 zstring zstring::extract(int offset, int len) const {
     zstring result(m_encoding);
     SASSERT(0 <= offset && 0 <= len);
@@ -400,7 +415,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do
         std::ostringstream strm;
         strm << "Unexpected number of arguments to '" << sig.m_name << "' ";
         strm << "at least one argument expected " << dsz << " given";
-        m.raise_exception(strm.str().c_str());
+        m.raise_exception(strm.str());
     }
     bool is_match = true;
     for (unsigned i = 0; is_match && i < dsz; ++i) {
@@ -420,7 +435,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do
         if (range) {
             strm << " and range: " << mk_pp(range, m);
         }
-        m.raise_exception(strm.str().c_str());
+        m.raise_exception(strm.str());
     }
     range_out = apply_binding(binding, sig.m_range);
     SASSERT(range_out);
@@ -434,7 +449,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
         std::ostringstream strm;
         strm << "Unexpected number of arguments to '" << sig.m_name << "' ";
         strm << sig.m_dom.size() << " arguments expected " << dsz << " given";
-        m.raise_exception(strm.str().c_str());
+        m.raise_exception(strm.str());
     }
     bool is_match = true;
     for (unsigned i = 0; is_match && i < dsz; ++i) {
@@ -459,13 +474,13 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
             strm << mk_pp(sig.m_dom[i].get(), m) << " ";
         }
 
-        m.raise_exception(strm.str().c_str());
+        m.raise_exception(strm.str());
     }
     if (!range && dsz == 0) {
         std::ostringstream strm;
         strm << "Sort of polymorphic function '" << sig.m_name << "' ";
         strm << "is ambiguous. Function takes no arguments and sort of range has not been constrained";
-        m.raise_exception(strm.str().c_str());
+        m.raise_exception(strm.str());
     }
     range_out = apply_binding(m_binding, sig.m_range);
     SASSERT(range_out);
@@ -530,6 +545,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_SEQ_EXTRACT]   = alloc(psig, m, "seq.extract",  1, 3, seqAint2T, seqA);
     m_sigs[OP_SEQ_REPLACE]   = alloc(psig, m, "seq.replace",  1, 3, seq3A, seqA);
     m_sigs[OP_SEQ_INDEX]     = alloc(psig, m, "seq.indexof",  1, 3, seq2AintT, intT);
+    m_sigs[OP_SEQ_LAST_INDEX] = alloc(psig, m, "seq.last_indexof",  1, 2, seqAseqA, intT);
     m_sigs[OP_SEQ_AT]        = alloc(psig, m, "seq.at",       1, 2, seqAintT, seqA);
     m_sigs[OP_SEQ_NTH]       = alloc(psig, m, "seq.nth",      1, 2, seqAintT, A);
     m_sigs[OP_SEQ_LENGTH]    = alloc(psig, m, "seq.len",      1, 1, &seqA, intT);
@@ -774,7 +790,13 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
             return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, OP_SEQ_INDEX));
         }
         return mk_str_fun(k, arity, domain, range, OP_SEQ_INDEX);
-
+    case OP_SEQ_LAST_INDEX:
+        if (arity != 2) {
+            m.raise_exception("two arguments expected tin last_indexof");
+        }
+        else {
+            return mk_seq_fun(k, arity, domain, range, OP_SEQ_LAST_INDEX);
+        }
     case OP_SEQ_PREFIX:
         return mk_seq_fun(k, arity, domain, range, _OP_STRING_PREFIX);
     case _OP_STRING_PREFIX:

src/ast/seq_decl_plugin.h

@@ -43,6 +43,7 @@ enum seq_op_kind {
     OP_SEQ_NTH,
     OP_SEQ_LENGTH,
     OP_SEQ_INDEX,
+    OP_SEQ_LAST_INDEX,
     OP_SEQ_TO_RE,
     OP_SEQ_IN_RE,
 
@@ -113,6 +114,7 @@ public:
     bool prefixof(zstring const& other) const;
     bool contains(zstring const& other) const;
     int  indexof(zstring const& other, int offset) const;
+    int  last_indexof(zstring const& other) const;
     zstring extract(int lo, int hi) const;
     zstring operator+(zstring const& other) const;
     bool operator==(const zstring& other) const;
@@ -260,6 +262,7 @@ public:
         app* mk_prefix(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); }
         app* mk_suffix(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); }
         app* mk_index(expr* a, expr* b, expr* i) const { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); }
+        app* mk_last_index(expr* a, expr* b) const { expr* es[2] = { a, b}; return m.mk_app(m_fid, OP_SEQ_LAST_INDEX, 2, es); }
         app* mk_unit(expr* u) const { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); }
         app* mk_char(zstring const& s, unsigned idx) const;
         app* mk_itos(expr* i) const { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); }
@@ -285,6 +288,7 @@ public:
         bool is_nth(expr const* n)       const { return is_app_of(n, m_fid, OP_SEQ_NTH); }
         bool is_nth(expr const* n, expr*& s, unsigned& idx) const;
         bool is_index(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_INDEX); }
+        bool is_last_index(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_LAST_INDEX); }
         bool is_replace(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_REPLACE); }
         bool is_prefix(expr const* n)   const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); }
         bool is_suffix(expr const* n)   const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); }
@@ -311,6 +315,7 @@ public:
         MATCH_BINARY(is_nth);
         MATCH_BINARY(is_index);
         MATCH_TERNARY(is_index);
+        MATCH_BINARY(is_last_index);
         MATCH_TERNARY(is_replace);
         MATCH_BINARY(is_prefix);
         MATCH_BINARY(is_suffix);

src/ast/special_relations_decl_plugin.cpp

@@ -0,0 +1,83 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    special_relations_decl_plugin.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-15-9.
+
+Revision History:
+
+--*/
+
+#include <sstream>
+#include "ast/ast.h"
+#include "ast/special_relations_decl_plugin.h"
+
+special_relations_decl_plugin::special_relations_decl_plugin():
+    m_lo("linear-order"),
+    m_po("partial-order"),
+    m_plo("piecewise-linear-order"),
+    m_to("tree-order"),
+    m_tc("transitive-closure")
+{}
+    
+func_decl * special_relations_decl_plugin::mk_func_decl(
+    decl_kind k, unsigned num_parameters, parameter const * parameters, 
+    unsigned arity, sort * const * domain, sort * range)    
+{
+    if (arity != 2) {
+        m_manager->raise_exception("special relations should have arity 2");
+        return nullptr;
+    }
+    if (domain[0] != domain[1]) {
+        m_manager->raise_exception("argument sort missmatch. The two arguments should have the same sort");
+        return nullptr;
+    }
+    if (!range) {
+        range = m_manager->mk_bool_sort();
+    }
+    if (!m_manager->is_bool(range)) {
+        m_manager->raise_exception("range type is expected to be Boolean for special relations");
+    }
+    func_decl_info info(m_family_id, k, num_parameters, parameters);
+    symbol name;
+    switch(k) {
+    case OP_SPECIAL_RELATION_PO: name = m_po; break;
+    case OP_SPECIAL_RELATION_LO: name = m_lo; break;
+    case OP_SPECIAL_RELATION_PLO: name = m_plo; break;
+    case OP_SPECIAL_RELATION_TO: name = m_to; break;
+    case OP_SPECIAL_RELATION_TC: name = m_tc; break;
+    }
+    return m_manager->mk_func_decl(name, arity, domain, range, info);
+}
+
+void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
+    if (logic == symbol::null) {
+        op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO));
+        op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO));
+        op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO));
+        op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO));
+        op_names.push_back(builtin_name(m_tc.bare_str(), OP_SPECIAL_RELATION_TC));
+    }
+}
+
+sr_property special_relations_util::get_property(func_decl* f) const {
+    switch (f->get_decl_kind()) {
+    case OP_SPECIAL_RELATION_PO: return sr_po;
+    case OP_SPECIAL_RELATION_LO: return sr_lo;
+    case OP_SPECIAL_RELATION_PLO: return sr_plo;
+    case OP_SPECIAL_RELATION_TO: return sr_to;
+    case OP_SPECIAL_RELATION_TC: return sr_tc;
+    default:
+        UNREACHABLE();
+        return sr_po;
+    }
+}

src/ast/special_relations_decl_plugin.h

@@ -0,0 +1,108 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    special_relations_decl_plugin.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-15-9.
+    Ashutosh Gupta 2016
+
+Revision History:
+
+--*/
+#ifndef SPECIAL_RELATIONS_DECL_PLUGIN_H_
+#define SPECIAL_RELATIONS_DECL_PLUGIN_H_
+
+#include "ast/ast.h"
+
+
+enum special_relations_op_kind {
+    OP_SPECIAL_RELATION_LO,
+    OP_SPECIAL_RELATION_PO,
+    OP_SPECIAL_RELATION_PLO,
+    OP_SPECIAL_RELATION_TO,
+    OP_SPECIAL_RELATION_TC,
+    LAST_SPECIAL_RELATIONS_OP
+};
+
+class special_relations_decl_plugin : public decl_plugin {
+    symbol m_lo;
+    symbol m_po;
+    symbol m_plo;
+    symbol m_to;
+    symbol m_tc;
+public:
+    special_relations_decl_plugin();
+
+    ~special_relations_decl_plugin() override {}
+
+    decl_plugin * mk_fresh() override {
+        return alloc(special_relations_decl_plugin);
+    }
+    
+    func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+                             unsigned arity, sort * const * domain, sort * range) override;
+
+    void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
+    
+    sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { return nullptr; }
+};
+
+enum sr_property {
+    sr_none          = 0x00,
+    sr_transitive    = 0x01,                              // Rxy & Ryz -> Rxz
+    sr_reflexive     = 0x02,                              // Rxx
+    sr_antisymmetric = 0x04,                              // Rxy & Ryx -> x = y
+    sr_lefttree      = 0x08,                              // Ryx & Rzx -> Ryz | Rzy
+    sr_righttree     = 0x10,                              // Rxy & Rxz -> Ryx | Rzy
+    sr_total         = 0x20,                              // Rxy | Ryx
+    sr_po            = 0x01 | 0x02 | 0x04,                // partial order
+    sr_to            = 0x01 | 0x02 | 0x04 | 0x10,         // right-tree
+    sr_plo           = 0x01 | 0x02 | 0x04 | 0x08 | 0x10,  // piecewise linear order
+    sr_lo            = 0x01 | 0x02 | 0x04 | 0x20,         // linear order
+    sr_tc            = 0x40,                              // transitive closure of relation
+};
+
+class special_relations_util {
+    ast_manager& m;
+    family_id    m_fid;
+    func_decl* mk_rel_decl(func_decl* f, decl_kind k) {
+        parameter p(f); SASSERT(f->get_arity() == 2); 
+        return m.mk_func_decl(m_fid, k, 1, &p, 2, f->get_domain(), f->get_range()); 
+    }    
+public:
+    special_relations_util(ast_manager& m) : m(m), m_fid(m.get_family_id("special_relations")) {}
+    
+    bool is_special_relation(func_decl* f) const { return f->get_family_id() == m_fid; }
+    bool is_special_relation(app* e) const { return is_special_relation(e->get_decl()); }
+    sr_property get_property(func_decl* f) const;
+    sr_property get_property(app* e) const { return get_property(e->get_decl()); }
+
+    func_decl* mk_to_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TO); }
+    func_decl* mk_po_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PO); }
+    func_decl* mk_plo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PLO); }
+    func_decl* mk_lo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_LO); }
+    func_decl* mk_tc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TC); }
+
+    bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); }
+    bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); }
+    bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); }
+    bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); }
+    bool is_tc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TC); }
+    
+    app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO,  arg1, arg2); }
+    app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO,  arg1, arg2); }
+    app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PLO, arg1, arg2); }
+    app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_TO,  arg1, arg2); }
+
+};
+
+
+#endif /* SPECIAL_RELATIONS_DECL_PLUGIN_H_ */

src/ast/static_features.cpp

@@ -30,6 +30,7 @@ static_features::static_features(ast_manager & m):
     m_afid(m.mk_family_id("arith")),
     m_lfid(m.mk_family_id("label")),
     m_arrfid(m.mk_family_id("array")),
+    m_srfid(m.mk_family_id("special_relations")),
     m_label_sym("label"),
     m_pattern_sym("pattern"),
     m_expr_list_sym("expr-list") {
@@ -78,6 +79,7 @@ void static_features::reset() {
     m_has_real                             = false; 
     m_has_bv                               = false;
     m_has_fpa                              = false;
+    m_has_sr                               = false;
     m_has_str                              = false;
     m_has_seq_non_str                      = false;
     m_has_arrays                           = false;
@@ -274,6 +276,8 @@ void static_features::update_core(expr * e) {
         m_has_bv = true;
     if (!m_has_fpa && (m_fpautil.is_float(e) || m_fpautil.is_rm(e)))
         m_has_fpa = true;
+    if (is_app(e) && to_app(e)->get_family_id() == m_srfid) 
+        m_has_sr = true;
     if (!m_has_arrays && m_arrayutil.is_array(e)) 
         m_has_arrays = true;
     if (!m_has_ext_arrays && m_arrayutil.is_array(e) && 
@@ -281,9 +285,8 @@ void static_features::update_core(expr * e) {
         m_has_ext_arrays = true;
     if (!m_has_str && m_sequtil.str.is_string_term(e))
         m_has_str = true;
-    if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) {
+    if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) 
         m_has_seq_non_str = true;
-    }
     if (is_app(e)) {
         family_id fid = to_app(e)->get_family_id();
         mark_theory(fid);

src/ast/static_features.h

@@ -25,6 +25,7 @@ Revision History:
 #include "ast/array_decl_plugin.h"
 #include "ast/fpa_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
+#include "ast/special_relations_decl_plugin.h"
 #include "util/map.h"
 
 struct static_features {
@@ -38,6 +39,7 @@ struct static_features {
     family_id                m_afid;
     family_id                m_lfid;    
     family_id                m_arrfid;
+    family_id                m_srfid;
     ast_mark                 m_already_visited;
     bool                     m_cnf;
     unsigned                 m_num_exprs;             // 
@@ -79,6 +81,7 @@ struct static_features {
     bool                     m_has_real;        //
     bool                     m_has_bv;          //
     bool                     m_has_fpa;         //
+    bool                     m_has_sr;          // has special relations
     bool                     m_has_str;         // has String-typed terms
     bool                     m_has_seq_non_str; // has non-String-typed Sequence terms
     bool                     m_has_arrays;      //