Merge pull request #1226 from NikolajBjorner/master

removing dependencies on simplifier, support SMTLIB2 parametric algebraic datatypes.
This is a breaking change. It introduces two substantial changes:
1. The legacy simplifier is removed. It was obsoleted with the introduction of the rewriter facilities, but many dependencies made it a major change to remove the legacy simplifier. All uses of the legacy simplifier have now been replaced by corresponding calls to the rewriter. It means that some normalization may behave differently. At this point, Z3 passes regressions and passes performance tests without regressing.
2. Algebraic datatypes in the form of SMT-LIB2.6 are now supported. These generalize the datatypes supported so far as parametric datatype constructors may be applied to different arguments within a recursive definition.

examples/c++/example.cpp

@@ -470,7 +470,7 @@ void unsat_core_example2() {
     // The solver s already contains p1 => F
     // To disable F, we add (not p1) as an additional assumption
     qs.push_back(!p1);
-    std::cout << s.check(qs.size(), &qs[0]) << "\n";
+    std::cout << s.check((unsigned)qs.size(), &qs[0]) << "\n";
     expr_vector core2 = s.unsat_core();
     std::cout << core2 << "\n";
     std::cout << "size: " << core2.size() << "\n";

scripts/mk_project.py

@@ -23,10 +23,7 @@ def init_project_def():
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
     add_lib('rewriter', ['ast', 'polynomial', 'automata'], 'ast/rewriter')
-    # Simplifier module will be deleted in the future.
-    # It has been replaced with rewriter module.
-    add_lib('simplifier', ['rewriter'], 'ast/simplifier')
-    add_lib('macros', ['simplifier'], 'ast/macros')
+    add_lib('macros', ['rewriter'], 'ast/macros')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
     add_lib('model', ['rewriter'])
     add_lib('tactic', ['ast', 'model'])
@@ -47,11 +44,11 @@ def init_project_def():
     add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
     add_lib('proof_checker', ['rewriter'], 'ast/proof_checker')
-    add_lib('fpa', ['ast', 'util', 'simplifier', 'model'], 'ast/fpa')
-    add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern')
-    add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster')
-    add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params')
-    add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
+    add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
+    add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
+    add_lib('bit_blaster', ['rewriter', 'rewriter'], 'ast/rewriter/bit_blaster')
+    add_lib('smt_params', ['ast', 'rewriter', 'pattern', 'bit_blaster'], 'smt/params')
+    add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
                     'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa', 'lp'])
     add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')

src/CMakeLists.txt

@@ -68,9 +68,6 @@ add_subdirectory(cmd_context)
 add_subdirectory(cmd_context/extra_cmds)
 add_subdirectory(parsers/smt2)
 add_subdirectory(ast/proof_checker)
-## Simplifier module will be deleted in the future.
-## It has been replaced with rewriter component.
-add_subdirectory(ast/simplifier)
 add_subdirectory(ast/fpa)
 add_subdirectory(ast/macros)
 add_subdirectory(ast/pattern)

src/api/api_context.cpp

@@ -150,8 +150,9 @@ namespace api {
 
     void context::set_error_code(Z3_error_code err) {
         m_error_code = err; 
-        if (err != Z3_OK) 
+        if (err != Z3_OK) {
             invoke_error_handler(err); 
+        }
     }
 
     void context::check_searching() {

src/api/api_datatype.cpp

@@ -45,13 +45,13 @@ extern "C" {
 
         ptr_vector<accessor_decl> acc;
         for (unsigned i = 0; i < num_fields; ++i) {
-            acc.push_back(mk_accessor_decl(to_symbol(field_names[i]), type_ref(to_sort(field_sorts[i]))));
+            acc.push_back(mk_accessor_decl(m, to_symbol(field_names[i]), type_ref(to_sort(field_sorts[i]))));
         }
 
         constructor_decl* constrs[1] = { mk_constructor_decl(to_symbol(name), recognizer, acc.size(), acc.c_ptr()) };
 
         {
-            datatype_decl * dt = mk_datatype_decl(to_symbol(name), 1, constrs);
+            datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, 1, constrs);
             bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, tuples);
             del_datatype_decl(dt);
 
@@ -69,18 +69,13 @@ extern "C" {
         // create constructor
         SASSERT(dt_util.is_datatype(tuple));
         SASSERT(!dt_util.is_recursive(tuple));
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple);
-        func_decl* decl = (*decls)[0];
+        ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(tuple);
+        func_decl* decl = (decls)[0];
         mk_c(c)->save_multiple_ast_trail(decl);
         *mk_tuple_decl = of_func_decl(decl);
 
         // Create projections
-        ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors(decl);
-        if (!accs) {
-            SET_ERROR_CODE(Z3_INVALID_ARG);
-            RETURN_Z3(0);
-        }
-        ptr_vector<func_decl> const & _accs = *accs;
+        ptr_vector<func_decl> const & _accs = *dt_util.get_constructor_accessors(decl);
         SASSERT(_accs.size() == num_fields);
         for (unsigned i = 0; i < _accs.size(); i++) {
             mk_c(c)->save_multiple_ast_trail(_accs[i]);
@@ -118,7 +113,7 @@ extern "C" {
 
 
         {
-            datatype_decl * dt = mk_datatype_decl(to_symbol(name), n, constrs.c_ptr());
+            datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 0, 0, n, constrs.c_ptr());
             bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, sorts);
             del_datatype_decl(dt);
 
@@ -136,10 +131,10 @@ extern "C" {
         // create constructor
         SASSERT(dt_util.is_datatype(e));
         SASSERT(!dt_util.is_recursive(e));
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(e);
-        SASSERT(decls && decls->size() == n);
+        ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(e);
+        SASSERT(decls.size() == n);
         for (unsigned i = 0; i < n; ++i) {
-            func_decl* decl = (*decls)[i];
+            func_decl* decl = (decls)[i];
             mk_c(c)->save_multiple_ast_trail(decl);
             enum_consts[i] = of_func_decl(decl);
             decl = dt_util.get_constructor_recognizer(decl);
@@ -165,11 +160,12 @@ extern "C" {
         LOG_Z3_mk_list_sort(c, name, elem_sort, nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl);
         RESET_ERROR_CODE();
         ast_manager& m = mk_c(c)->m();
+        datatype_util& dt_util = mk_c(c)->dtutil();
         mk_c(c)->reset_last_result();
         datatype_util data_util(m);
         accessor_decl* head_tail[2] = {
-            mk_accessor_decl(symbol("head"), type_ref(to_sort(elem_sort))),
-            mk_accessor_decl(symbol("tail"), type_ref(0))
+            mk_accessor_decl(m, symbol("head"), type_ref(to_sort(elem_sort))),
+            mk_accessor_decl(m, symbol("tail"), type_ref(0))
         };
         constructor_decl* constrs[2] = {
             mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, 0),
@@ -179,7 +175,7 @@ extern "C" {
 
         sort_ref_vector sorts(m);
         {
-            datatype_decl * decl = mk_datatype_decl(to_symbol(name), 2, constrs);
+            datatype_decl * decl = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, 2, constrs);
             bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, 0, 0, sorts);
             del_datatype_decl(decl);
 
@@ -215,18 +211,16 @@ extern "C" {
             *is_cons_decl = of_func_decl(f);
         }
         if (head_decl) {
-            ptr_vector<func_decl> const* acc = data_util.get_constructor_accessors(cnstrs[1]);
-            SASSERT(acc);
-            SASSERT(acc->size() == 2);
-            f = (*acc)[0];
+            ptr_vector<func_decl> const& acc = *data_util.get_constructor_accessors(cnstrs[1]);
+            SASSERT(acc.size() == 2);
+            f = (acc)[0];
             mk_c(c)->save_multiple_ast_trail(f);
             *head_decl = of_func_decl(f);
         }
         if (tail_decl) {
-            ptr_vector<func_decl> const* acc = data_util.get_constructor_accessors(cnstrs[1]);
-            SASSERT(acc);
-            SASSERT(acc->size() == 2);
-            f = (*acc)[1];
+            ptr_vector<func_decl> const& acc = *data_util.get_constructor_accessors(cnstrs[1]);
+            SASSERT(acc.size() == 2);
+            f = (acc)[1];
             mk_c(c)->save_multiple_ast_trail(f);
             *tail_decl = of_func_decl(f);
         }
@@ -301,13 +295,9 @@ extern "C" {
             *tester = of_func_decl(f2);
         }
 
-        ptr_vector<func_decl> const* accs = data_util.get_constructor_accessors(f);
-        if (!accs && num_fields > 0) {
-            SET_ERROR_CODE(Z3_INVALID_ARG);
-            return;
-        }
+        ptr_vector<func_decl> const& accs = *data_util.get_constructor_accessors(f);
         for (unsigned i = 0; i < num_fields; ++i) {
-            func_decl* f2 = (*accs)[i];
+            func_decl* f2 = (accs)[i];
             mk_c(c)->save_multiple_ast_trail(f2);
             accessors[i] = of_func_decl(f2);
         }
@@ -327,21 +317,23 @@ extern "C" {
                                            Z3_symbol name,
                                            unsigned num_constructors,
                                            Z3_constructor constructors[]) {
+        datatype_util& dt_util = mk_c(c)->dtutil();
+        ast_manager& m = mk_c(c)->m();
         ptr_vector<constructor_decl> constrs;
         for (unsigned i = 0; i < num_constructors; ++i) {
             constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
             ptr_vector<accessor_decl> acc;
             for (unsigned j = 0; j < cn->m_sorts.size(); ++j) {
                 if (cn->m_sorts[j].get()) {
-                    acc.push_back(mk_accessor_decl(cn->m_field_names[j], type_ref(cn->m_sorts[j].get())));
+                    acc.push_back(mk_accessor_decl(m, cn->m_field_names[j], type_ref(cn->m_sorts[j].get())));
                 }
                 else {
-                    acc.push_back(mk_accessor_decl(cn->m_field_names[j], type_ref(cn->m_sort_refs[j])));
+                    acc.push_back(mk_accessor_decl(m, cn->m_field_names[j], type_ref(cn->m_sort_refs[j])));
                 }
             }
             constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.c_ptr()));
         }
-        return mk_datatype_decl(to_symbol(name), num_constructors, constrs.c_ptr());
+        return mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, num_constructors, constrs.c_ptr());
     }
 
     Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
@@ -368,11 +360,11 @@ extern "C" {
         sort * s = sorts.get(0);
 
         mk_c(c)->save_ast_trail(s);
-        ptr_vector<func_decl> const* cnstrs = data_util.get_datatype_constructors(s);
+        ptr_vector<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s);
 
         for (unsigned i = 0; i < num_constructors; ++i) {
             constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
-            cn->m_constructor = (*cnstrs)[i];
+            cn->m_constructor = cnstrs[i];
         }
         RETURN_Z3_mk_datatype(of_sort(s));
         Z3_CATCH_RETURN(0);
@@ -417,7 +409,7 @@ extern "C" {
         ptr_vector<datatype_decl> datas;
         for (unsigned i = 0; i < num_sorts; ++i) {
             constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]);
-            datas.push_back(mk_datatype_decl(c,sort_names[i], cl->size(), reinterpret_cast<Z3_constructor*>(cl->c_ptr())));
+            datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast<Z3_constructor*>(cl->c_ptr())));
         }
         sort_ref_vector _sorts(m);
         bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), 0, 0, _sorts);
@@ -434,10 +426,10 @@ extern "C" {
             mk_c(c)->save_multiple_ast_trail(s);
             sorts[i] = of_sort(s);
             constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]);
-            ptr_vector<func_decl> const* cnstrs = data_util.get_datatype_constructors(s);
+            ptr_vector<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s);
             for (unsigned j = 0; j < cl->size(); ++j) {
                 constructor* cn = (*cl)[j];
-                cn->m_constructor = (*cnstrs)[j];
+                cn->m_constructor = cnstrs[j];
             }
         }
         RETURN_Z3_mk_datatypes;
@@ -456,12 +448,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls) {
-            SET_ERROR_CODE(Z3_INVALID_ARG);
-            return 0;
-        }
-        return decls->size();
+        return dt_util.get_datatype_constructors(_t)->size();
         Z3_CATCH_RETURN(0);
     }
 
@@ -474,12 +461,12 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls || idx >= decls->size()) {
+        ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(_t);
+        if (idx >= decls.size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        func_decl* decl = (*decls)[idx];
+        func_decl* decl = (decls)[idx];
         mk_c(c)->save_ast_trail(decl);
         return of_func_decl(decl);
     }
@@ -504,12 +491,12 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls || idx >= decls->size()) {
+        ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(_t);
+        if (idx >= decls.size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        func_decl* decl = (*decls)[idx];
+        func_decl* decl = (decls)[idx];
         decl = dt_util.get_constructor_recognizer(decl);
         mk_c(c)->save_ast_trail(decl);
         RETURN_Z3(of_func_decl(decl));
@@ -527,23 +514,23 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls || idx_c >= decls->size()) {
+        ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(_t);
+        if (idx_c >= decls.size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        func_decl* decl = (*decls)[idx_c];
+        func_decl* decl = (decls)[idx_c];
         if (decl->get_arity() <= idx_a) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors(decl);
-        SASSERT(accs && accs->size() == decl->get_arity());
-        if (!accs || accs->size() <= idx_a) {
+        ptr_vector<func_decl> const & accs = *dt_util.get_constructor_accessors(decl);
+        SASSERT(accs.size() == decl->get_arity());
+        if (accs.size() <= idx_a) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        decl = (*accs)[idx_a];
+        decl = (accs)[idx_a];
         mk_c(c)->save_ast_trail(decl);
         RETURN_Z3(of_func_decl(decl));
         Z3_CATCH_RETURN(0);
@@ -574,16 +561,13 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple);
-        if (!decls || decls->size() != 1) {
+        ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(tuple);
+        if (decls.size() != 1) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors((*decls)[0]);
-        if (!accs) {
-            return 0;
-        }
-        return accs->size();
+        ptr_vector<func_decl> const & accs = *dt_util.get_constructor_accessors(decls[0]);
+        return accs.size();
         Z3_CATCH_RETURN(0);
     }
 
@@ -597,21 +581,17 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple);
-        if (!decls || decls->size() != 1) {
-            SET_ERROR_CODE(Z3_INVALID_ARG);
-            RETURN_Z3(0);
-        }
-        ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors((*decls)[0]);
-        if (!accs) {
+        ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(tuple);
+        if (decls.size() != 1) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        if (accs->size() <= i) {
+        ptr_vector<func_decl> const & accs = *dt_util.get_constructor_accessors((decls)[0]);
+        if (accs.size() <= i) {
             SET_ERROR_CODE(Z3_IOB);
             RETURN_Z3(0);
         }
-        func_decl* acc = (*accs)[i];
+        func_decl* acc = (accs)[i];
         mk_c(c)->save_ast_trail(acc);
         RETURN_Z3(of_func_decl(acc));
         Z3_CATCH_RETURN(0);

src/api/python/z3/z3.py

@@ -8185,9 +8185,9 @@ def sequence_interpolant(v,p=None,ctx=None):
     If parameters p are supplied, these are used in creating the
     solver that determines satisfiability.
 
-    >>> x = Int('x')
-    >>> y = Int('y')
-    >>> print(sequence_interpolant([x < 0, y == x , y > 2]))
+    x = Int('x')
+    y = Int('y')
+    print(sequence_interpolant([x < 0, y == x , y > 2]))
     [Not(x >= 0), Not(y >= 0)]
     """
     f = v[0]

src/ast/array_decl_plugin.cpp

@@ -546,7 +546,7 @@ expr * array_decl_plugin::get_some_value(sort * s) {
     return m_manager->mk_app(m_family_id, OP_CONST_ARRAY, 1, &p, 1, &v);
 }
 
-bool array_decl_plugin::is_fully_interp(sort const * s) const {
+bool array_decl_plugin::is_fully_interp(sort * s) const {
     SASSERT(s->is_sort_of(m_family_id, ARRAY_SORT));
     unsigned sz = get_array_arity(s);
     for (unsigned i = 0; i < sz; i++) {