fix bogus axioms

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

src/ast/rewriter/finite_set_axioms.cpp

@@ -230,14 +230,18 @@ void finite_set_axioms::in_range_axiom(expr* r) {
     if (!u.is_range(r, lo, hi))
         return;
     theory_axiom* ax = alloc(theory_axiom, m, "range-bounds");
+    arith_util a(m);
+    expr_ref lo_le_hi(a.mk_le(a.mk_sub(lo, hi), a.mk_int(0)), m);
+    m_rewriter(lo_le_hi);
+    ax->clause.push_back(m.mk_not(lo_le_hi));
     ax->clause.push_back(u.mk_in(lo, r));
     m_add_clause(ax);
 
     ax = alloc(theory_axiom, m, "range-bounds", r);
+    ax->clause.push_back(m.mk_not(lo_le_hi));
     ax->clause.push_back(u.mk_in(hi, r));
     m_add_clause(ax);
 
-    arith_util a(m);
     ax = alloc(theory_axiom, m, "range-bounds", r);
     ax->clause.push_back(m.mk_not(u.mk_in(a.mk_add(hi, a.mk_int(1)), r)));
     m_add_clause(ax);

src/smt/theory_finite_set.cpp

@@ -228,12 +228,16 @@ namespace smt {
             ctx.attach_th_var(e, this, mk_var(e));
 
         // Assert immediate axioms
-        // if (!ctx.relevancy())
-        add_immediate_axioms(term);
+        if (!ctx.relevancy())
+            add_immediate_axioms(term);
                 
         return true;
     }
 
+    void theory_finite_set::relevant_eh(app* t) {
+        add_immediate_axioms(t);
+    }
+
     void theory_finite_set::apply_sort_cnstr(enode* n, sort* s) {
         SASSERT(u.is_finite_set(s));
         if (!is_attached_to_var(n))
@@ -248,9 +252,6 @@ namespace smt {
     /**
     * Every dissequality has to be supported by at distinguishing element.
     * 
-    * TODO: we can avoid instantiating the extensionality axiom if we know statically that e1, e2
-    * can never be equal (say, they have different cardinalities or they are finite sets by construction
-    * with elements that can differentiate the sets)
     */
     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");
@@ -263,10 +264,23 @@ namespace smt {
                 std::swap(e1, e2);
             if (!is_new_axiom(e1, e2))
                 return;
+            if (are_forced_distinct(n1, n2))
+                return;
             m_axioms.extensionality_axiom(e1, e2);
         }
     }
 
+    //
+    // TODO: add implementation that detects sets that are known to be distinct.
+    // for example, 
+    // . x in a is assigned to true and y in b is assigned to false and x ~ y
+    // . or upper-bound(set.size(a)) < lower-bound(set.size(b))
+    //   where upper and lower bounds can be queried using arith_value
+    // 
+    bool theory_finite_set::are_forced_distinct(enode* a, enode* b) {
+        return false;
+    }
+
     /**
     * Final check for the finite set theory.
      * The Final Check method is called when the solver has assigned truth values to all Boolean variables.
@@ -297,12 +311,13 @@ namespace smt {
      * 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.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.empty)       -> (set.size (set.empty)) = 0
-     * - (set.range lo hi) -> lo-1,hi+1 not in range, lo, hi in range
+
      */
     void theory_finite_set::add_immediate_axioms(app* term) {
         expr *elem = nullptr, *set = nullptr;

src/smt/theory_finite_set.h

@@ -160,6 +160,7 @@ namespace smt {
         bool can_propagate() override;
         void propagate() override;
         void assign_eh(bool_var v, bool is_true) override;
+        void relevant_eh(app *n) override;
         
         theory * mk_fresh(context * new_ctx) override;
         char const * get_name() const override { return "finite_set"; }
@@ -199,6 +200,8 @@ namespace smt {
         bool is_root(theory_var v) const { return m_find.is_root(v); }
 
         std::ostream &display_var(std::ostream &out, theory_var v) const;
+
+        bool are_forced_distinct(enode *a, enode *b);
         
     public:
         theory_finite_set(context& ctx);