diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index ad78c5956..a0117ca6d 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/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); +} \ No newline at end of file diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h index 6b63a29f9..fad785cb4 100644 --- a/src/ast/rewriter/finite_set_axioms.h +++ b/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); diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index faea056bf..f485079de 100644 --- a/src/smt/theory_finite_set.cpp +++ b/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: - * 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. + * Axioms that can be added immediately. * */ 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. - * For every (set.in x S) where S is a union, assert (or propagate) (set.in x S1) or (set.in x S2) - * - It saturates with respect to extensionality: - * Sets corresponding to shared variables having the same interpretation should also be congruent + * - membership axioms + * - extensionality axioms */ 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()) - continue; // elem is then equal to set1 but not elem1. This is a different case. + 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. 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; - - // TODO: Extensionality axioms for sets - return FC_DONE; + return true; + return false; + } + + /** + * 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) { - TRACE(finite_set, tout << "instantiate_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); - + 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 { obj_pair_hashtable &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; diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 418384252..3ac6acff5 100644 --- a/src/smt/theory_finite_set.h +++ b/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);