patch definitions, add pretty print support

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

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<format> 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)) {

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

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

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, &param);
+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, &param));
@@ -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;
 }

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 {

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 {

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