diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 72382e366..6896b8ff8 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -437,6 +437,11 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast()))); return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"RegEx"); } + if ((get_fsutil().is_finite_set(s))) { + ptr_buffer fs; + fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast()))); + return mk_seq1(m, fs.begin(), fs.end(), f2f(), "FiniteSet"); + } std::string name = ensure_quote(s->get_name()); if (get_dtutil().is_datatype(s)) { diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h index 64ea2aec9..85e8e4a9a 100644 --- a/src/ast/ast_smt2_pp.h +++ b/src/ast/ast_smt2_pp.h @@ -30,6 +30,7 @@ Revision History: #include "ast/dl_decl_plugin.h" #include "ast/seq_decl_plugin.h" #include "ast/datatype_decl_plugin.h" +#include "ast/finite_set_decl_plugin.h" #include "ast/ast_smt_pp.h" #include "util/smt2_util.h" @@ -53,6 +54,7 @@ public: virtual array_util & get_arutil() = 0; virtual fpa_util & get_futil() = 0; virtual seq_util & get_sutil() = 0; + virtual finite_set_util &get_fsutil() = 0; virtual datalog::dl_decl_util& get_dlutil() = 0; virtual datatype_util& get_dtutil() = 0; virtual bool uses(symbol const & s) const = 0; @@ -80,9 +82,12 @@ class smt2_pp_environment_dbg : public smt2_pp_environment { fpa_util m_futil; seq_util m_sutil; datatype_util m_dtutil; + finite_set_util m_fsutil; datalog::dl_decl_util m_dlutil; public: - smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dtutil(m), m_dlutil(m) {} + smt2_pp_environment_dbg(ast_manager &m) + : m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dtutil(m), m_fsutil(m), + m_dlutil(m) {} ast_manager & get_manager() const override { return m_manager; } arith_util & get_autil() override { return m_autil; } bv_util & get_bvutil() override { return m_bvutil; } @@ -91,6 +96,7 @@ public: fpa_util & get_futil() override { return m_futil; } datalog::dl_decl_util& get_dlutil() override { return m_dlutil; } datatype_util& get_dtutil() override { return m_dtutil; } + finite_set_util &get_fsutil() override { return m_fsutil; } bool uses(symbol const & s) const override { return false; } }; diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 68936ac49..ce0923e0f 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -304,6 +304,7 @@ class smt_printer { void visit_sort(sort* s, bool bool2int = false) { symbol sym; + verbose_stream() << "visit sort " << s->get_name() << "\n"; if (s->is_sort_of(m_bv_fid, BV_SORT)) { sym = symbol("BitVec"); } diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index e03c05480..3a3a96bce 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -21,6 +21,7 @@ Revision History: #include "ast/arith_decl_plugin.h" #include "ast/array_decl_plugin.h" #include "ast/polymorphism_util.h" +#include "ast/ast_pp.h" #include "util/warning.h" finite_set_decl_plugin::finite_set_decl_plugin(): @@ -108,9 +109,10 @@ sort * finite_set_decl_plugin::get_element_sort(sort* finite_set_sort) const { return to_sort(params[0].get_ast()); } -func_decl * finite_set_decl_plugin::mk_empty(sort* element_sort) { - parameter param(element_sort); - sort * finite_set_sort = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, ¶m); +func_decl * finite_set_decl_plugin::mk_empty(sort* finite_set_sort) { + parameter param(finite_set_sort); + if (!is_finite_set(finite_set_sort)) + m_manager->raise_exception("set.empty range must be a finite set sort"); sort * const * no_domain = nullptr; return m_manager->mk_func_decl(m_sigs[OP_FINITE_SET_EMPTY]->m_name, 0u, no_domain, finite_set_sort, func_decl_info(m_family_id, OP_FINITE_SET_EMPTY, 1, ¶m)); @@ -132,11 +134,14 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param switch (k) { case OP_FINITE_SET_EMPTY: - if (num_parameters != 1 || !parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) { - m_manager->raise_exception("set.empty requires one sort parameter"); - return nullptr; - } - return mk_empty(to_sort(parameters[0].get_ast())); + if (!range) { + if ((num_parameters != 1 || !parameters[0].is_ast() || !is_sort(parameters[0].get_ast()))) { + m_manager->raise_exception("set.empty requires one sort parameter"); + return nullptr; + } + range = to_sort(parameters[0].get_ast()); + } + return mk_empty(range); case OP_FINITE_SET_SINGLETON: case OP_FINITE_SET_UNION: case OP_FINITE_SET_INTERSECT: @@ -182,11 +187,24 @@ bool finite_set_decl_plugin::is_fully_interp(sort * s) const { } bool finite_set_decl_plugin::is_value(app * e) const { - // Empty set is a value - return is_app_of(e, m_family_id, OP_FINITE_SET_EMPTY); + return is_unique_value(e); } bool finite_set_decl_plugin::is_unique_value(app* e) const { - // Empty set is a unique value for its sort - return is_value(e); + // Empty set is a value + return is_app_of(e, m_family_id, OP_FINITE_SET_EMPTY) || + (is_app_of(e, m_family_id, OP_FINITE_SET_SINGLETON) && is_unique_value(to_app(e->get_arg(0)))); +} + +bool finite_set_decl_plugin::are_distinct(app* e1, app* e2) const { + if (is_unique_value(e1) && is_unique_value(e2)) + return e1 != e2; + finite_set_recognizers r(get_family_id()); + if (r.is_empty(e1) && r.is_singleton(e2)) + return true; + if (r.is_singleton(e1) && r.is_empty(e2)) + return true; + // TODO: could be extended to cases where we can prove the sets are different by containing one element + // that the other doesn't contain. Such as (union (singleton a) (singleton b)) and (singleton c) where c is different from a, b. + return false; } diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index 851239558..78be3c4c1 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -99,6 +99,9 @@ public: bool is_value(app * e) const override; bool is_unique_value(app* e) const override; + + bool are_distinct(app *e1, app *e2) const override; + }; class finite_set_recognizers { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f5117bcbd..3f578212d 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -533,6 +533,7 @@ protected: fpa_util m_futil; seq_util m_sutil; datatype_util m_dtutil; + finite_set_util m_fsutil; datalog::dl_decl_util m_dlutil; @@ -554,7 +555,8 @@ protected: } public: - pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dtutil(o.m()), m_dlutil(o.m()) {} + pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), + m_sutil(o.m()), m_dtutil(o.m()), m_fsutil(o.m()), m_dlutil(o.m()) {} ast_manager & get_manager() const override { return m_owner.m(); } arith_util & get_autil() override { return m_autil; } bv_util & get_bvutil() override { return m_bvutil; } @@ -562,6 +564,7 @@ public: fpa_util & get_futil() override { return m_futil; } seq_util & get_sutil() override { return m_sutil; } datatype_util & get_dtutil() override { return m_dtutil; } + finite_set_util &get_fsutil() override { return m_fsutil; } datalog::dl_decl_util& get_dlutil() override { return m_dlutil; } bool uses(symbol const & s) const override { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 3ce1ece4a..46919620b 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1797,8 +1797,12 @@ namespace smt2 { void check_qualifier(expr * t, bool has_as) { if (has_as) { sort * s = sort_stack().back(); - if (s != t->get_sort()) - throw parser_exception("invalid qualified identifier, sort mismatch"); + if (s != t->get_sort()) { + std::ostringstream str; + str << "sort mismatch in qualified identifier, expected: " << mk_pp(s, m()) + << ", got: " << mk_pp(t->get_sort(), m()); + throw parser_exception(str.str()); + } sort_stack().pop_back(); } }