fix #6792, add scaffolding for type variables

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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);

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);

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)) {
+        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)) {
+        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;
     }

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);

src/cmd_context/pdecl.h

@@ -86,7 +86,7 @@ typedef ptr_hashtable<psort, psort_hash_proc, psort_eq_proc> 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:
@@ -124,6 +124,18 @@ public:
     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);

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<mpq>(right_side, zero_of_type<mpq>());
                 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<mpq>(right_side, zero_of_type<mpq>());
                 if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {

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;;
+                ret = true;
-            } else if (x > m_upper_bounds[j]) {
+            }
+            else if (x > m_upper_bounds[j]) {
                 delta = m_upper_bounds[j] - x;
                 ret = true;
             }

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;
@@ -857,6 +858,26 @@ namespace smt2 {
                 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());
             SASSERT(curr_id() == m_declare_datatypes);
@@ -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"),