add assume-eqs and extensionality

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

src/ast/finite_set_decl_plugin.cpp

@@ -70,6 +70,8 @@ void finite_set_decl_plugin::init() {
     m_sigs[OP_FINITE_SET_MAP]        = alloc(polymorphism::psig, m, "set.map",        2, 2, arrABsetA, setB);
     m_sigs[OP_FINITE_SET_SELECT]     = alloc(polymorphism::psig, m, "set.select",     1, 2, arrABoolsetA, setA);
     m_sigs[OP_FINITE_SET_RANGE]      = alloc(polymorphism::psig, m, "set.range",      0, 2, intintT, setInt);
+    m_sigs[OP_FINITE_SET_DIFF]       = alloc(polymorphism::psig, m, "set.diff", 1, 2, setAsetA, A);
+//    m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A);
 }
 
 sort * finite_set_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
@@ -152,6 +154,7 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param
     case OP_FINITE_SET_MAP:
     case OP_FINITE_SET_SELECT:
     case OP_FINITE_SET_RANGE:
+    case OP_FINITE_SET_DIFF:
         return mk_finite_set_op(k, arity, domain, range);
     default:
         return nullptr;

src/ast/finite_set_decl_plugin.h

@@ -23,6 +23,7 @@ Operators:
     set.map : (S -> T) (FiniteSet S) -> (FiniteSet T)
     set.select : (S -> Bool) (FiniteSet S) -> (FiniteSet S)
     set.range : Int Int -> (FiniteSet Int)
+    set.diff : (FiniteSet S) (FiniteSet S) -> S
    
 --*/
 #pragma once
@@ -46,6 +47,8 @@ enum finite_set_op_kind {
     OP_FINITE_SET_MAP,
     OP_FINITE_SET_SELECT,
     OP_FINITE_SET_RANGE,
+    OP_FINITE_SET_DIFF,
+    OP_FINITE_SET_MAP_INVERSE,
     LAST_FINITE_SET_OP
 };
 

src/ast/rewriter/finite_set_axioms.cpp

@@ -298,4 +298,19 @@ void finite_set_axioms::subset_axiom(expr* a) {
     clause2.push_back(a);
     clause2.push_back(m.mk_not(eq));
     m_add_clause(clause2);
+}
+
+void finite_set_axioms::extensionality_axiom(expr *a, expr* b) {
+    // a != b => set.in (set.diff(a, b) a) != set.in (set.diff(a, b) b)
+    expr_ref diff_ab(u.mk_difference(a, b), m);
+
+    expr_ref a_eq_b(m.mk_eq(a, b), m);
+    expr_ref diff_in_a(u.mk_in(diff_ab, a), m);
+    expr_ref diff_in_b(u.mk_in(diff_ab, b), m);
+    
+    // (a != b) => (x in diff_ab != x in diff_ba)
+    expr_ref_vector clause(m);
+    clause.push_back(a_eq_b);
+    clause.push_back(m.mk_not(m.mk_iff(diff_in_a, diff_in_b)));
+    m_add_clause(clause);   
 }

src/ast/rewriter/finite_set_axioms.h

@@ -69,4 +69,7 @@ public:
     // set.size(a) = 1
     void size_singleton_axiom(expr *a);
 
+    // a != b => set.in (set.diff(a, b) a) != set.in (set.diff(a, b) b)
+    void extensionality_axiom(expr *a, expr *b);
+
 };

src/smt/theory_finite_set.cpp

@@ -131,9 +131,18 @@ namespace smt {
     }
 
     void theory_finite_set::new_diseq_eh(theory_var v1, theory_var v2) {
-        TRACE(finite_set, tout << "new_diseq_eh: v" << v1 << " != v" << v2 << "\n";);
+        TRACE(finite_set, tout << "new_diseq_eh: v" << v1 << " != v" << v2 << "\n");
-        // Disequalities could trigger extensionality axioms
+        auto n1 = get_enode(v1);
-        // For now, we rely on the final_check to handle this
+        auto n2 = get_enode(v2);
+        auto e1 = n1->get_expr();
+        auto e2 = n2->get_expr();
+        if (u.is_finite_set(e1) && u.is_finite_set(e2)) {
+            if (e1->get_id() > e2->get_id())
+                std::swap(e1, e2);
+            if (!is_new_axiom(e1, e2))
+                return;
+            m_axioms.extensionality_axiom(e1, e2);
+        }
     }
 
     /**
@@ -143,7 +152,7 @@ namespace smt {
      * 
      * It ensures saturation with respect to the theory axioms:
      * - membership axioms
-     * - extensionality axioms
+     * - assume eqs axioms
     */
     final_check_status theory_finite_set::final_check_eh() {
         TRACE(finite_set, tout << "final_check_eh\n";);
@@ -151,7 +160,7 @@ namespace smt {
         if (add_membership_axioms())
             return FC_CONTINUE;
 
-        if (add_extensionality_axioms())
+        if (assume_eqs())
             return FC_CONTINUE;
         
         return FC_DONE;
@@ -219,32 +228,76 @@ namespace smt {
     }
 
     /**
-     *  Saturate with respect to extensionality:
+     *  Saturate with respect to equality sharing:
      *  - Sets corresponding to shared variables having the same interpretation should also be congruent
     */
-    bool theory_finite_set::add_extensionality_axioms() {
+    bool theory_finite_set::assume_eqs() {
+        collect_members();
+        expr_ref_vector trail(m); // make sure reference counts to union expressions are valid in this scope
+        obj_map<expr, enode*> set_reprs;
+
+        auto start = ctx.get_random_value();
+        auto sz = get_num_vars();
+        for (unsigned w = 0; w < sz; ++w) {
+            auto v = (w + start) % sz;
+            enode* n = get_enode(v);
+            if (!u.is_finite_set(n->get_expr()))
+                continue;
+            if (!is_relevant_and_shared(n))
+                continue;
+            auto r = n->get_root();
+            // Create a union expression that is canonical (sorted)
+            auto& set = *m_set_members[r];
+            ptr_vector<expr> elems;
+            for (auto e : set)
+                elems.push_back(e->get_expr());
+            std::sort(elems.begin(), elems.end(), [](expr *a, expr *b) { return a->get_id() < b->get_id(); });
+            expr* s = nullptr;
+            for (auto v : elems)
+                s = s ? u.mk_union(s, v) : v;
+            trail.push_back(s);
+            enode *n2 = nullptr;
+            if (!set_reprs.find(s, n2)) {
+                set_reprs.insert(s, n2);
+                continue;
+            }
+            if (n2->get_root() == r)
+                continue;
+            if (is_new_axiom(n->get_expr(), n2->get_expr()) && assume_eq(n, n2)) {
+                TRACE(finite_set,
+                      tout << "assume " << mk_pp(n->get_expr(), m) << " = " << mk_pp(n2->get_expr(), m) << "\n";);
+                return true;
+            }
+        }
         return false;
     }
 
+
+    bool theory_finite_set::is_new_axiom(expr* a, expr* b) {
+        struct insert_obj_pair_table : public trail {
+            obj_pair_hashtable<expr, expr> &table;
+            expr *a, *b;
+            insert_obj_pair_table(obj_pair_hashtable<expr, expr> &t, expr *a, expr *b) : table(t), a(a), b(b) {}
+            void undo() override {
+                table.erase({a, b});
+            }
+        };
+        if (m_lemma_exprs.contains({a, b}))
+            return false;
+        m_lemma_exprs.insert({a, b});
+        ctx.push_trail(insert_obj_pair_table(m_lemma_exprs, a, b));
+        return true;
+    }
+
     /**
     * Instantiate axioms for a given element in a set.
     */
     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";);
 
-        struct insert_obj_pair_table : public trail {
+        if (!is_new_axiom(elem, set))
-            obj_pair_hashtable<expr, expr> &table;
-            expr *a, *b;
-            insert_obj_pair_table(obj_pair_hashtable<expr, expr> &t, expr *a, expr *b) : 
-                table(t), a(a), b(b) {}
-            void undo() override {
-                table.erase({a, b});
-            }
-        };
-        if (m_lemma_exprs.contains({elem, set}))
             return;
-        m_lemma_exprs.insert({elem, set});
+
-        ctx.push_trail(insert_obj_pair_table(m_lemma_exprs, elem, set));
         // Instantiate appropriate axiom based on set structure
         if (u.is_empty(set)) {
             m_axioms.in_empty_axiom(elem);
@@ -296,8 +349,6 @@ namespace smt {
         collect_members();
     }
 
-
-
     void theory_finite_set::collect_members() {
         // This method can be used to collect all elements that are members of sets
         // and ensure that the model factory has values for them.

src/smt/theory_finite_set.h

@@ -128,7 +128,8 @@ namespace smt {
         lbool truth_value(expr *e);
         void add_immediate_axioms(app *atom);
         bool add_membership_axioms();
-        bool add_extensionality_axioms();
+        bool assume_eqs();
+        bool is_new_axiom(expr *a, expr *b);
 
         // model construction
         void collect_members();