updated with immediate axioms

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

src/ast/rewriter/finite_set_axioms.cpp

@@ -140,6 +140,15 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) {
         return;
     
     expr_ref x_in_a(u.mk_in(x, a), m);
+
+    if (x == b) {
+        // If x and b are syntactically identical, then (x in a) is always true
+        expr_ref_vector clause(m);
+        clause.push_back(x_in_a);
+        m_add_clause(clause);
+        return;
+    }
+
     expr_ref x_eq_b(m.mk_eq(x, b), m);
     
     // (x in a) => (x == b)
@@ -271,3 +280,22 @@ void finite_set_axioms::size_singleton_axiom(expr *a) {
     clause.push_back(eq);
     m_add_clause(clause);
 }
+
+void finite_set_axioms::subset_axiom(expr* a) {
+    expr *b = nullptr, *c = nullptr;
+    if (!u.is_subset(a, b, c))
+        return;
+    
+    expr_ref intersect_bc(u.mk_intersect(b, c), m);
+    expr_ref eq(m.mk_eq(intersect_bc, b), m);
+    
+    expr_ref_vector clause1(m);
+    clause1.push_back(m.mk_not(a));
+    clause1.push_back(eq);
+    m_add_clause(clause1);
+    
+    expr_ref_vector clause2(m);
+    clause2.push_back(a);
+    clause2.push_back(m.mk_not(eq));
+    m_add_clause(clause2);
+}

src/ast/rewriter/finite_set_axioms.h

@@ -61,6 +61,10 @@ public:
     // (x in a) <=> (x in b) and p(x)
     void in_select_axiom(expr *x, expr *a);
 
+    // a := set.subset(b, c)
+    // (a) <=> (set.intersect(b, c) = b)
+    void subset_axiom(expr *a);
+
     // a := set.singleton(b)
     // set.size(a) = 1
     void size_singleton_axiom(expr *a);

src/smt/theory_finite_set.cpp

@@ -53,11 +53,7 @@ namespace smt {
     * The second effect is to set up tracking and assert axioms.
     * Tracking:
     *    For every occurrence (set.in x_i S_i) we track x_i. 
-    * Axioms:
+    * Axioms that can be added immediately.
-    *    We can immediately assert some axioms because they are unit literals:
-    *    - (set.in x set.empty) is false
-    *    - (set.subset S T) <=> (= (set.union S T) T)  (or (= (set.intersect S T) S))
-    *    Axioms can be deffered to when the atomic formulas become "relevant" for the theory solver.
     *    
     */
     bool theory_finite_set::internalize_atom(app * atom, bool gate_ctx) {
@@ -76,7 +72,8 @@ namespace smt {
         }
 
         // Assert immediate axioms
-        // add_immediate_axioms(atom);
+        // if (!ctx.relevancy())
+        add_immediate_axioms(atom);
         
         return true;
     }
@@ -135,51 +132,96 @@ namespace smt {
      * It is responsible for asserting any remaining axioms and checking for inconsistencies.
      * 
      * It ensures saturation with respect to the theory axioms:
-     * - Set membership is saturated with respect to set operations.
+     * - membership axioms
-     *    For every (set.in x S) where S is a union, assert (or propagate) (set.in x S1) or (set.in x S2)
+     * - extensionality axioms
-     * - It saturates with respect to extensionality:
-     *   Sets corresponding to shared variables having the same interpretation should also be congruent
     */
     final_check_status theory_finite_set::final_check_eh() {
         TRACE(finite_set, tout << "final_check_eh\n";);
 
+        if (add_membership_axioms())
+            return FC_CONTINUE;
+
+        if (add_extensionality_axioms())
+            return FC_CONTINUE;
+        
+        return FC_DONE;
+    }
+
+
+    /**
+     * Add immediate axioms that can be asserted when the atom is created.
+     * These are unit clauses that can be added immediately.
+     * - (set.in x set.empty) is false
+     * - (set.subset S T) <=> (= (set.union S T) T)  (or (= (set.intersect S T) S))
+     * 
+     * Other axioms:
+     * - (set.singleton x) -> (set.in x (set.singleton x))
+     * - (set.singleton x) -> (set.size (set.singleton x)) = 1
+     * - (set.empty)       -> (set.size (set.empty)) = 0
+     */
+    void theory_finite_set::add_immediate_axioms(app* term) {
+        expr *elem = nullptr, *set = nullptr;
+        unsigned sz = m_lemmas.size();
+        if (u.is_in(term, elem, set) && u.is_empty(set))
+            add_membership_axioms(elem, set);
+        else if (u.is_subset(term))
+            m_axioms.subset_axiom(term);
+        else if (u.is_singleton(term, elem))
+            m_axioms.in_singleton_axiom(elem, term);
+
+        // Assert all new lemmas as clauses
+        for (unsigned i = sz; i < m_lemmas.size(); ++i) 
+            assert_clause(m_lemmas[i]);
+    }
+
+    /**
+     *   Set membership is saturated with respect to set operations.
+     *    For every (set.in x S) where S is a union, assert (or propagate) (set.in x S1) or (set.in x S2)
+     */
+    bool theory_finite_set::add_membership_axioms() {
+        expr *elem1 = nullptr, *set1 = nullptr;
+
         // walk all parents of elem in congruence table.
         // if a parent is of the form elem' in S u T, or similar.
         // create clauses for elem in S u T.
 
-        // Saturate membership constraints
-        expr* elem1 = nullptr, *set1 = nullptr;
         for (auto elem : m_elements) {
             if (!ctx.is_relevant(elem))
                 continue;
             for (auto p : enode::parents(elem)) {
-                if (!u.is_in(p->get_expr(), elem1, set1)) 
+                if (!u.is_in(p->get_expr(), elem1, set1))
                     continue;
-                if (elem->get_root() != p->get_arg(0)->get_root())                    
+                if (elem->get_root() != p->get_arg(0)->get_root())
-                    continue; // elem is then equal to set1 but not elem1. This is a different case.
+                    continue;  // elem is then equal to set1 but not elem1. This is a different case.
                 if (!ctx.is_relevant(p))
                     continue;
                 for (auto sib : *p->get_arg(1))
-                    instantiate_axioms(elem->get_expr(), sib->get_expr());
+                    add_membership_axioms(elem->get_expr(), sib->get_expr());
             }
         }
         if (instantiate_false_lemma())
-            return FC_CONTINUE;
+            return true;
         if (instantiate_unit_propagation())
-            return FC_CONTINUE;
+            return true;
         if (instantiate_free_lemma())
-            return FC_CONTINUE;
+            return true;
-        
+        return false;
-        // TODO: Extensionality axioms for sets
+    }
-        return FC_DONE;
+
+    /**
+     *  Saturate with respect to extensionality:
+     *  - Sets corresponding to shared variables having the same interpretation should also be congruent
+    */
+    bool theory_finite_set::add_extensionality_axioms() {
+        return false;
     }
 
     /**
     * Instantiate axioms for a given element in a set.
     */
-    void theory_finite_set::instantiate_axioms(expr* elem, expr* set) {
+    void theory_finite_set::add_membership_axioms(expr *elem, expr *set) {
-        TRACE(finite_set, tout << "instantiate_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";);
+        TRACE(finite_set, tout << "add_membership_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";);
-        
+
         struct insert_obj_pair_table : public trail {
             obj_pair_hashtable<expr, expr> &table;
             expr *a, *b;
@@ -218,13 +260,7 @@ namespace smt {
         }
         else if (u.is_select(set)) {
             m_axioms.in_select_axiom(elem, set);
-        }
+        }        
-        
-        // Instantiate size axioms for singleton sets
-        // TODO, such axioms don't belong here
-        if (u.is_singleton(set)) {
-            m_axioms.size_singleton_axiom(set);
-        }
     }
 
     void theory_finite_set::add_clause(expr_ref_vector const& clause) {
@@ -281,7 +317,7 @@ namespace smt {
      * A theory axiom is also removed during backtracking.
     */
     bool theory_finite_set::instantiate_unit_propagation() {
-        bool propagaed = false;
+        bool propagated = false;
         for (auto const &clause : m_lemmas) {
             expr *undef = nullptr;
             bool is_unit_propagating = true;

src/smt/theory_finite_set.h

@@ -115,13 +115,16 @@ namespace smt {
         model_value_proc * mk_value(enode * n, model_generator & mg) override;
 
         // Helper methods for axiom instantiation
-        void instantiate_axioms(expr* elem, expr* set);
+        void add_membership_axioms(expr* elem, expr* set);
         void add_clause(expr_ref_vector const& clause);
         void assert_clause(expr_ref_vector const &clause);
         bool instantiate_false_lemma();
         bool instantiate_unit_propagation();
         bool instantiate_free_lemma();
         lbool truth_value(expr *e);
+        void add_immediate_axioms(app *atom);
+        bool add_membership_axioms();
+        bool add_extensionality_axioms();
         
     public:
         theory_finite_set(context& ctx);