mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-26 20:08:42 +00:00
Code Activity

remove incorrect assertion, make sat case for range + size conservative

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-12-06 13:07:14 -08:00
parent e90512388c
commit 1d3f6a7c70
3 changed files with 48 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/ast/rewriter/finite_set_axioms.cpp
View file

@ -33,23 +33,55 @@ std::ostream& operator<<(std::ostream& out, theory_axiom const& ax) {
}
void finite_set_axioms::add_unit(char const *name, expr *p1, expr *unit) {
expr_ref _f1(unit, m);
if (is_true(unit))
return;
theory_axiom *ax = alloc(theory_axiom, m, name, p1);
ax->clause.push_back(unit);
m_add_clause(ax);
}
bool finite_set_axioms::is_true(expr *f) {
if (m.is_true(f))
return true;
if (m.is_not(f, f) && m.is_false(f))
return true;
return false;
}
bool finite_set_axioms::is_false(expr* f) {
if (m.is_false(f))
return true;
if (m.is_not(f, f) && m.is_true(f))
return true;
return false;
}
void finite_set_axioms::add_binary(char const *name, expr *p1, expr *p2, expr *f1, expr *f2) {
expr_ref _f1(f1, m), _f2(f2, m);
if (is_true(f1) || is_true(f2))
return;
theory_axiom *ax = alloc(theory_axiom, m, name, p1, p2);
ax->clause.push_back(f1);
ax->clause.push_back(f2);
if (!is_false(f1))
ax->clause.push_back(f1);
if (!is_false(f2))
ax->clause.push_back(f2);
m_add_clause(ax);
}
void finite_set_axioms::add_ternary(char const *name, expr *p1, expr *p2, expr *f1, expr *f2, expr *f3) {
expr_ref _f1(f1, m), _f2(f2, m), _f3(f3, m);
if (is_true(f1) || is_true(f2) || is_true(f3))
return;
theory_axiom *ax = alloc(theory_axiom, m, name, p1, p2);
ax->clause.push_back(f1);
ax->clause.push_back(f2);
ax->clause.push_back(f3);
if (!is_false(f1))
ax->clause.push_back(f1);
if (!is_false(f2))
ax->clause.push_back(f2);
if (!is_false(f3))
ax->clause.push_back(f3);
m_add_clause(ax);
}

4
src/ast/rewriter/finite_set_axioms.h
View file

@ -52,6 +52,10 @@ class finite_set_axioms {
void add_ternary(char const *name, expr *p1, expr *p2, expr *f1, expr *f2, expr *f3);
bool is_true(expr *f);
bool is_false(expr *f);
public:
finite_set_axioms(ast_manager &m) : m(m), u(m), m_rewriter(m) {}

11
src/smt/theory_finite_set.cpp
View file

@ -331,7 +331,7 @@ namespace smt {
* - there is not both set.size and set.filter
*/
bool theory_finite_set::is_fully_solved() {
bool has_map = false, has_filter = false, has_size = false;
bool has_map = false, has_filter = false, has_size = false, has_range = false;
for (unsigned v = 0; v < get_num_vars(); ++v) {
auto n = get_enode(v);
auto e = n->get_expr();
@ -341,12 +341,16 @@ namespace smt {
has_map = true;
if (u.is_size(e))
has_size = true;
if (u.is_range(e))
has_range = true;
}
TRACE(finite_set, tout << "has-map " << has_map << " has-filter-size " << has_filter << has_size << "\n");
if (has_map)
return false; // todo use more expensive model check here
if (has_filter && has_size)
return false; // tood use more expensive model check here
return false; // todo use more expensive model check here
if (has_range && has_size)
return false; // todo use more expensive model check here or even ensure range expressions are handled natively by size.
return true;
}
@ -799,8 +803,7 @@ namespace smt {
result.push_back(model_value_dependency(n));
}
app *mk_value(model_generator &mg, expr_ref_vector const &values) override {
SASSERT(values.empty() == !m_elements);
app *mk_value(model_generator &mg, expr_ref_vector const &values) override {
auto s = n->get_sort();
if (values.empty())
return th.u.mk_empty(s);