diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 7f9542fe4..354a945e3 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1378,6 +1378,7 @@ void ast_manager::init() { ENSURE(model_value_family_id == mk_family_id("model-value")); ENSURE(user_sort_family_id == mk_family_id("user-sort")); ENSURE(arith_family_id == mk_family_id("arith")); + ENSURE(poly_family_id == mk_family_id("polymorphic")); basic_decl_plugin * plugin = alloc(basic_decl_plugin); register_plugin(basic_family_id, plugin); m_bool_sort = plugin->mk_bool_sort(); @@ -2019,6 +2020,11 @@ sort * ast_manager::mk_uninterpreted_sort(symbol const & name, unsigned num_para return plugin->mk_sort(kind, num_parameters, parameters); } +sort * ast_manager::mk_type_var(symbol const& name) { + sort_info si(poly_family_id, 0); + return mk_sort(name, &si); +} + func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, bool assoc, bool comm, bool inj) { func_decl_info info(null_family_id, null_decl_kind); diff --git a/src/ast/ast.h b/src/ast/ast.h index e0ae7b92f..bdb76b2dc 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -85,6 +85,7 @@ const family_id user_sort_family_id = 4; const family_id last_builtin_family_id = 4; const family_id arith_family_id = 5; +const family_id poly_family_id = 6; // ----------------------------------- // @@ -622,6 +623,7 @@ public: sort_size const & get_num_elements() const { return get_info()->get_num_elements(); } void set_num_elements(sort_size const& s) { get_info()->set_num_elements(s); } unsigned get_size() const { return get_obj_size(); } + bool is_type_var() const { return get_family_id() == poly_family_id; } }; // ----------------------------------- @@ -1709,6 +1711,8 @@ public: sort * mk_uninterpreted_sort(symbol const & name) { return mk_uninterpreted_sort(name, 0, nullptr); } + sort * mk_type_var(symbol const& name); + sort * mk_sort(symbol const & name, sort_info const & info) { if (info.get_family_id() == null_family_id) { return mk_uninterpreted_sort(name); diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 9806424a3..9354b53f6 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -665,12 +665,19 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) SASSERT(m().is_value(val)); if (m().are_distinct(val, e)) { - mk_eq(t, val, result); + if (get_depth(t) < 500) + mk_eq(t, val, result); + else + result = m().mk_eq(t, val); + result = m().mk_and(result, cond); return BR_REWRITE2; } if (m().are_distinct(val, t)) { - mk_eq(e, val, result); + if (get_depth(e) < 500) + mk_eq(e, val, result); + else + result = m().mk_eq(e, val); result = m().mk_and(result, m().mk_not(cond)); return BR_REWRITE2; } diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 776a91a28..a64d0ede9 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -348,6 +348,26 @@ std::ostream& psort_user_decl::display(std::ostream & out) const { return out << ")"; } +// ------------------- +// psort_type_var_decl + +psort_type_var_decl::psort_type_var_decl(unsigned id, pdecl_manager & m, symbol const & n): + psort_decl(id, 0, m, n) { + m_psort_kind = PSORT_TV; +} + +void psort_type_var_decl::finalize(pdecl_manager & m) { + psort_decl::finalize(m); +} + +sort * psort_type_var_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { + return m.m().mk_type_var(m_name); +} + +std::ostream& psort_type_var_decl::display(std::ostream & out) const { + return out << "(declare-type-var " << m_name << ")"; +} + // ------------------- // psort_dt_decl @@ -969,6 +989,10 @@ psort_decl * pdecl_manager::mk_psort_dt_decl(unsigned num_params, symbol const & return new (a().allocate(sizeof(psort_dt_decl))) psort_dt_decl(m_id_gen.mk(), num_params, *this, n); } +psort_decl * pdecl_manager::mk_psort_type_var_decl(symbol const & n) { + return new (a().allocate(sizeof(psort_type_var_decl))) psort_type_var_decl(m_id_gen.mk(), *this, n); +} + psort_decl * pdecl_manager::mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k) { return new (a().allocate(sizeof(psort_builtin_decl))) psort_builtin_decl(m_id_gen.mk(), *this, n, fid, k); diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 818c97eda..a3005f182 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -62,7 +62,7 @@ class psort_inst_cache; */ class psort : public pdecl { protected: - psort_inst_cache * m_inst_cache; + psort_inst_cache* m_inst_cache; friend class pdecl_manager; psort(unsigned id, unsigned num_params):pdecl(id, num_params), m_inst_cache(nullptr) {} bool is_psort() const override { return true; } @@ -86,7 +86,7 @@ typedef ptr_hashtable psort_table; #define PSORT_DECL_VAR_PARAMS UINT_MAX -typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN, PSORT_DT } psort_decl_kind; +typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN, PSORT_DT, PSORT_TV } psort_decl_kind; class psort_decl : public pdecl { protected: @@ -123,7 +123,19 @@ public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; std::ostream& display(std::ostream & out) const override; }; - + +class psort_type_var_decl : public psort_decl { +protected: + friend class pdecl_manager; + psort * m_def; + psort_type_var_decl(unsigned id, pdecl_manager & m, symbol const & n); + size_t obj_size() const override { return sizeof(psort_type_var_decl); } + void finalize(pdecl_manager & m) override; +public: + sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; + std::ostream& display(std::ostream & out) const override; +}; + class psort_builtin_decl : public psort_decl { protected: friend class pdecl_manager; @@ -304,6 +316,7 @@ public: psort_decl * mk_psort_dt_decl(unsigned num_params, symbol const & n); psort_decl * mk_psort_user_decl(unsigned num_params, symbol const & n, psort * def); psort_decl * mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k); + psort_decl * mk_psort_type_var_decl(symbol const& n); paccessor_decl * mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p); pconstructor_decl * mk_pconstructor_decl(unsigned num_params, symbol const & s, symbol const & r, unsigned num, paccessor_decl * const * as); pdatatype_decl * mk_pdatatype_decl(unsigned num_params, symbol const & s, unsigned num, pconstructor_decl * const * cs); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index b72b88f55..b6e9b63fe 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1858,7 +1858,8 @@ namespace lp { m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; set_upper_bound_witness(j, ci); insert_to_columns_with_changed_bounds(j); - } break; + break; + } case GT: y_of_bound = 1; case GE: { @@ -1873,8 +1874,8 @@ namespace lp { set_lower_bound_witness(j, ci); m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed); insert_to_columns_with_changed_bounds(j); - - } break; + break; + } case EQ: { auto v = numeric_pair(right_side, zero_of_type()); if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j] || v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { @@ -1911,8 +1912,8 @@ namespace lp { set_upper_bound_witness(j, ci); m_mpq_lar_core_solver.m_column_types[j] = (up == m_mpq_lar_core_solver.m_r_lower_bounds[j] ? column_type::fixed : column_type::boxed); insert_to_columns_with_changed_bounds(j); - - } break; + break; + } case GT: y_of_bound = 1; case GE: { @@ -1923,8 +1924,8 @@ namespace lp { m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; set_lower_bound_witness(j, ci); insert_to_columns_with_changed_bounds(j); - - } break; + break; + } case EQ: { auto v = numeric_pair(right_side, zero_of_type()); if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 00d079f77..e058100ab 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -309,8 +309,9 @@ public: case column_type::boxed: if (x < m_lower_bounds[j]) { delta = m_lower_bounds[j] - x; - ret = true;; - } else if (x > m_upper_bounds[j]) { + ret = true; + } + else if (x > m_upper_bounds[j]) { delta = m_upper_bounds[j] - x; ret = true; } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 081a8c838..5e22d9d29 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -102,6 +102,7 @@ namespace smt2 { symbol m_declare_const; symbol m_define_sort; symbol m_declare_sort; + symbol m_declare_type_var; symbol m_declare_datatypes; symbol m_declare_datatype; symbol m_par; @@ -856,6 +857,26 @@ namespace smt2 { if (ct_decls.empty()) throw parser_exception("invalid datatype declaration, datatype does not have any constructors"); } + + void parse_declare_type_var() { + SASSERT(curr_is_identifier()); + SASSERT(curr_id() == m_declare_type_var); + next(); + + check_nonreserved_identifier("invalid sort declaration, symbol expected"); + symbol id = curr_id(); + if (m_ctx.find_psort_decl(id) != nullptr) + throw parser_exception("invalid sort declaration, sort already declared/defined"); + next(); + check_rparen("invalid sort declaration, ')' expected"); + + psort_decl * decl = pm().mk_psort_type_var_decl(id); + m_ctx.insert(decl); + + m_ctx.print_success(); + next(); + + } void parse_declare_datatypes() { SASSERT(curr_is_identifier()); @@ -2975,6 +2996,10 @@ namespace smt2 { parse_declare_sort(); return; } + if (s == m_declare_type_var) { + parse_declare_type_var(); + return; + } if (s == m_declare_datatypes) { parse_declare_datatypes(); return; @@ -3048,6 +3073,7 @@ namespace smt2 { m_declare_const("declare-const"), m_define_sort("define-sort"), m_declare_sort("declare-sort"), + m_declare_type_var("declare-type-var"), m_declare_datatypes("declare-datatypes"), m_declare_datatype("declare-datatype"), m_par("par"),