add finite_set to quantifieed theories in smt_setup, fix type signature for map-inverse axioms

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

src/ast/finite_set_decl_plugin.cpp

@@ -71,7 +71,7 @@ void finite_set_decl_plugin::init() {
     sort* arrABsetA[2] = { arrAB, setA };
     sort* arrABoolsetA[2] = { arrABool, setA };
     sort* intintT[2] = { intT, intT };
-    sort *arrABsetBsetA[3] = {arrAB, setB, setA};
+    sort *arrABBsetA[3] = {arrAB, B, setA};
     
     m_sigs.resize(LAST_FINITE_SET_OP);
     m_sigs[OP_FINITE_SET_EMPTY]      = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_EMPTY],      1, 0, nullptr, setA);
@@ -86,7 +86,7 @@ void finite_set_decl_plugin::init() {
     m_sigs[OP_FINITE_SET_FILTER]     = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_FILTER], 1, 2, arrABoolsetA, setA);
     m_sigs[OP_FINITE_SET_RANGE]      = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_RANGE],      0, 2, intintT, setInt);
     m_sigs[OP_FINITE_SET_EXT]        = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_EXT], 1, 2, setAsetA, A);
-    m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A);
+    m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_MAP_INVERSE], 2, 3, arrABBsetA, A);
 }
 
 sort * finite_set_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {

src/ast/finite_set_decl_plugin.h

@@ -201,8 +201,8 @@ public:
         return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP, arr, set);
     }
 
-    app *mk_map_inverse(expr *arr, expr *a, expr *b) {
+    app *mk_map_inverse(expr *f, expr *x, expr *b) {
-        return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP_INVERSE, arr, b, a);
+        return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP_INVERSE, f, x, b);
     }
 
     app * mk_filter(expr* arr, expr* set) {

src/ast/rewriter/finite_set_axioms.cpp

@@ -206,11 +206,15 @@ void finite_set_axioms::in_range_axiom(expr* r) {
 // a := set.map(f, b)
 // (x in a) <=> set.map_inverse(f, x, b) in b
 void finite_set_axioms::in_map_axiom(expr *x, expr *a) {
-    expr* f = nullptr, *b = nullptr;
+    expr *f = nullptr, *b = nullptr;
+    sort *elem_sort = nullptr;
+    VERIFY(u.is_finite_set(a->get_sort(), elem_sort));
+    if (x->get_sort() != elem_sort)
+        return;
     if (!u.is_map(a, f, b))
         return;
     
-    expr_ref inv(u.mk_map_inverse(x, f, b), m);
+    expr_ref inv(u.mk_map_inverse(f, x, b), m);
     expr_ref f1(u.mk_in(x, a), m);
     expr_ref f2(u.mk_in(inv, b), m);
     add_binary("map-inverse", x, a, m.mk_not(f1), f2);
@@ -221,8 +225,12 @@ void finite_set_axioms::in_map_axiom(expr *x, expr *a) {
 // (x in b) => f(x) in a
 void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) {
     expr* f = nullptr, *b = nullptr;
+    sort *elem_sort = nullptr;
     if (!u.is_map(a, f, b))
         return;
+    VERIFY(u.is_finite_set(b->get_sort(), elem_sort));
+    if (x->get_sort() != elem_sort)
+        return;
     
     expr_ref x_in_b(u.mk_in(x, b), m);
     
@@ -286,56 +294,59 @@ void finite_set_axioms::add_ternary(char const *name, expr *p1, expr *p2, expr *
 // Auxiliary algebraic axioms to ease reasoning about set.size
 // The axioms are not required for completenss for the base fragment
 // as they are handled by creating semi-linear sets.
-void finite_set_axioms::size_ub_axiom(expr *e) {
+void finite_set_axioms::size_ub_axiom(expr *sz) {
-    expr *b = nullptr, *x = nullptr, *y = nullptr;
+    expr *b = nullptr, *e = nullptr, *x = nullptr, *y = nullptr;
+    if (!u.is_size(sz, e))
+        return;
     arith_util a(m);
     expr_ref ineq(m);
 
     if (u.is_singleton(e, b)) 
-        add_unit("size", e, m.mk_eq(u.mk_size(e), a.mk_int(1)));    
+        add_unit("size", e, m.mk_eq(sz, a.mk_int(1)));    
     else if (u.is_empty(e)) 
-        add_unit("size", e, m.mk_eq(u.mk_size(e), a.mk_int(0)));    
+        add_unit("size", e, m.mk_eq(sz, a.mk_int(0)));    
     else if (u.is_union(e, x, y)) {
-        ineq = a.mk_le(u.mk_size(e), a.mk_add(u.mk_size(x), u.mk_size(y)));
+        ineq = a.mk_le(sz, a.mk_add(u.mk_size(x), u.mk_size(y)));
         m_rewriter(ineq);
         add_unit("size", e, ineq);
     }
     else if (u.is_intersect(e, x, y)) {        
-        ineq = a.mk_le(u.mk_size(e), u.mk_size(x));
+        ineq = a.mk_le(sz, u.mk_size(x));
         m_rewriter(ineq);
         add_unit("size", e, ineq);
-        ineq = a.mk_le(u.mk_size(e), u.mk_size(y));
+        ineq = a.mk_le(sz, u.mk_size(y));
         m_rewriter(ineq);
         add_unit("size", e, ineq);
     }
     else if (u.is_difference(e, x, y)) {
-        ineq = a.mk_le(u.mk_size(e), u.mk_size(x));
+        ineq = a.mk_le(sz, u.mk_size(x));
         m_rewriter(ineq);
         add_unit("size", e, ineq);
     }
     else if (u.is_filter(e, x, y)) {
-        ineq = a.mk_le(u.mk_size(e), u.mk_size(y));
+        ineq = a.mk_le(sz, u.mk_size(y));
         m_rewriter(ineq);
         add_unit("size", e, ineq);
     }
     else if (u.is_map(e, x, y)) {
-        ineq = a.mk_le(u.mk_size(e), u.mk_size(y));
+        ineq = a.mk_le(sz, u.mk_size(y));
         m_rewriter(ineq);
         add_unit("size", e, ineq);
     }
     else if (u.is_range(e, x, y)) {
-        ineq = a.mk_eq(u.mk_size(e), m.mk_ite(a.mk_le(x, y), a.mk_add(a.mk_sub(y, x), a.mk_int(1)), a.mk_int(0)));
+        ineq = a.mk_eq(sz, m.mk_ite(a.mk_le(x, y), a.mk_add(a.mk_sub(y, x), a.mk_int(1)), a.mk_int(0)));
         m_rewriter(ineq);
         add_unit("size", e, ineq);
     }    
 }
 
 void finite_set_axioms::size_lb_axiom(expr* e) {
+    VERIFY(u.is_size(e));
     arith_util a(m);
     expr_ref ineq(m);
-    ineq = a.mk_le(a.mk_int(0), u.mk_size(e));
+    ineq = a.mk_le(a.mk_int(0), e);
     m_rewriter(ineq);
-    add_unit("size-lb", e, ineq);
+    add_unit("size", e, ineq);
 }
 
 void finite_set_axioms::subset_axiom(expr* a) {

src/smt/smt_setup.cpp

@@ -845,6 +845,7 @@ namespace smt {
             setup_bv();
             setup_dl();
             setup_seq_str(st);
+            setup_finite_set();
             setup_fpa();
             setup_recfuns();
             setup_special_relations();

src/smt/theory_finite_set.cpp

@@ -66,6 +66,7 @@ namespace smt {
     *         (set.in (f x) (set.map f S))
     */
     theory_var theory_finite_set::mk_var(enode *n) {
+        TRACE(finite_set, tout << "mk_var: " << enode_pp(n, ctx) << "\n");
         theory_var r = theory::mk_var(n);
         VERIFY(r == static_cast<theory_var>(m_find.mk_var()));
         SASSERT(r == static_cast<int>(m_var_data.size()));
@@ -88,7 +89,7 @@ namespace smt {
         }
         else if (u.is_union(e) || u.is_intersect(e) || 
             u.is_difference(e) || u.is_singleton(e) ||
-            u.is_empty(e) || u.is_range(e)) {            
+            u.is_empty(e) || u.is_range(e) || u.is_filter(e) || u.is_map(e)) {            
             m_var_data[r]->m_setops.push_back(n);
             ctx.push_trail(push_back_trail(m_var_data[r]->m_setops));
             for (auto arg : enode::args(n)) {
@@ -104,9 +105,6 @@ namespace smt {
                 ctx.push_trail(push_back_trail(m_var_data[v]->m_parent_setops));
             }
         }
-        else if (u.is_map(e) || u.is_filter(e)) {
-            NOT_IMPLEMENTED_YET();
-        }
         else if (u.is_range(e)) {
             
         }
@@ -362,9 +360,7 @@ namespace smt {
      * - (set.range lo hi) -> lo-1,hi+1 not in range, lo, hi in range if lo <= hi     * 
      *
      * Other axioms:
-     * - (set.singleton x) -> (set.size (set.singleton x)) = 1
+     * - (set.size s)       -> 0 <= (set.size s) <= upper-bound(s)
-     * - (set.empty)       -> (set.size (set.empty)) = 0
-
      */
     void theory_finite_set::add_immediate_axioms(app* term) {
         expr *elem = nullptr, *set = nullptr;
@@ -390,6 +386,10 @@ namespace smt {
             range_local.push_back(a.mk_add(lo, a.mk_int(-1)));
             range_local.push_back(a.mk_add(hi, a.mk_int(1)));
         }
+        else if (u.is_size(term)) {
+            m_axioms.size_lb_axiom(term);
+            m_axioms.size_ub_axiom(term);
+        }
        
         // Assert all new lemmas as clauses
         for (unsigned i = sz; i < m_clauses.axioms.size(); ++i) {
@@ -631,7 +631,6 @@ namespace smt {
     void theory_finite_set::add_membership_axioms(expr *elem, expr *set) {
         TRACE(finite_set, tout << "add_membership_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";);
 
-        try {
             // Instantiate appropriate axiom based on set structure
         if (!is_new_axiom(elem, set))
             ;
@@ -654,16 +653,13 @@ namespace smt {
             m_axioms.in_range_axiom(elem, set);
         }
         else if (u.is_map(set)) {
+            // TODO type of elem could be from the pre-image
             m_axioms.in_map_axiom(elem, set);
             m_axioms.in_map_image_axiom(elem, set);
         }
         else if (u.is_filter(set)) {            
             m_axioms.in_filter_axiom(elem, set);
         }
-        } catch (...) {
-            TRACE(finite_set, tout << "exception\n");
-            throw;
-        }
         TRACE(finite_set, tout << "after add_membership_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";);
     }