From 9f5bd2feda960dbdd10977026478f3fcae792eb9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Sep 2017 19:58:05 -0700
Subject: [PATCH] fix front-end for datatype

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/arith_rewriter.cpp |  2 +-
 src/cmd_context/pdecl.cpp           |  8 ++++----
 src/parsers/smt2/smt2parser.cpp     | 12 +++---------
 src/test/get_consequences.cpp       |  2 +-
 4 files changed, 9 insertions(+), 15 deletions(-)

diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 275290665..631e1d8f3 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -455,7 +455,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
             st = BR_DONE;
         }
     }
-    if (m_arith_lhs && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
+    if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
         a2.neg();
         new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));
         switch (kind) {
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 9d6c5065e..1887d677d 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -660,6 +660,7 @@ void pdatatype_decl::display(std::ostream & out) const {
 
 #ifdef DATATYPE_V2
 bool pdatatype_decl::commit(pdecl_manager& m) {
+    TRACE("datatype", tout << m_name << "\n";);
     sort_ref_vector ps(m.m());
     for (unsigned i = 0; i < m_num_params; ++i) {
         ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, 0));
@@ -669,10 +670,8 @@ bool pdatatype_decl::commit(pdecl_manager& m) {
     datatype_decl * d_ptr = dts.m_buffer[0];
     sort_ref_vector sorts(m.m());
     bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, ps.c_ptr(), sorts);
-    if (is_ok) {
-        if (m_num_params == 0) {
-            m.notify_new_dt(sorts.get(0), this);        
-        }
+    if (is_ok && m_num_params == 0) {
+        m.notify_new_dt(sorts.get(0), this);        
     }
     return is_ok;
 }
@@ -917,6 +916,7 @@ pconstructor_decl * pdecl_manager::mk_pconstructor_decl(unsigned num_params,
 }
 
 pdatatype_decl * pdecl_manager::mk_pdatatype_decl(unsigned num_params, symbol const & s, unsigned num, pconstructor_decl * const * cs) {
+    TRACE("datatype", tout << s << " has " << num_params << " parameters\n";);
     return new (a().allocate(sizeof(pdatatype_decl))) pdatatype_decl(m_id_gen.mk(), num_params, *this,
                                                                      s, num, cs);
 }
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 9526429cb..8144ebc08 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -619,14 +619,7 @@ namespace smt2 {
             psort_decl * d = m_ctx.find_psort_decl(id);
             int idx = 0;
             if (d == 0) {
-                if (m_dt_name2idx.find(id, idx)) {
-                    throw parser_exception("smtlib 2.6 parametric datatype sorts are not supported");
-                    // unsigned num_params = m_dt_name2arity.find(id);
-                    // d = pm().mk_psort_dt_decl(num_params, id);
-                }
-                else {
-                    unknown_sort(id);                
-                }
+                unknown_sort(id);                                
             }
             next();
             void * mem      = m_stack.allocate(sizeof(psort_frame));
@@ -924,10 +917,11 @@ namespace smt2 {
                 pdatatype_decl * d = new_dt_decls[i];
                 symbol duplicated;
                 check_duplicate(d, line, pos);
+                m_ctx.insert(d);
             }                
 #endif
             TRACE("declare_datatypes", tout << "i: " << i << " new_dt_decls.size(): " << sz << "\n";
-                  for (unsigned i = 0; i < sz; i++) tout << new_dt_decls[i]->get_name() << "\n";);
+                  for (unsigned j = 0; j < new_dt_decls.size(); ++j) tout << new_dt_decls[j]->get_name() << "\n";);
             m_ctx.print_success();
             next();
         }
diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp
index b9a54245e..6d600f594 100644
--- a/src/test/get_consequences.cpp
+++ b/src/test/get_consequences.cpp
@@ -66,7 +66,7 @@ void test2() {
     constructor_decl* B = mk_constructor_decl(symbol("B"), symbol("is-B"), 0, 0);
     constructor_decl* constrs[3] = { R, G, B };
     datatype_decl * enum_sort = mk_datatype_decl(dtutil, symbol("RGB"), 0, nullptr, 3, constrs);
-    VERIFY(dt.mk_datatypes(1, &enum_sort, 0, 0, new_sorts));    
+    VERIFY(dt.mk_datatypes(1, &enum_sort, 0, nullptr, new_sorts));    
     sort* rgb = new_sorts[0].get();
 
     expr_ref x = mk_const(m, "x", rgb), y = mk_const(m, "y", rgb), z = mk_const(m, "z", rgb);