mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-13 18:54:43 +00:00
Code Activity

wip - adding context equation solver

Browse source 
the solve_eqs_tactic is to be replaced by a re-implementation that uses solve_eqs in the simplifiers directory.
The re-implementation should address efficiency issues with the previous code.
At this point it punts on low level proofs. The plan is to use coarser
dependency tracking instead of low level proofs for pre-processing. Dependencies can be converted into a proof hint representation that can be checked using a stronger checker.
This commit is contained in:
Nikolaj Bjorner 2022-11-05 10:34:57 -07:00
parent ae2672f132
commit 4d8860c0bc
15 changed files with 416 additions and 117 deletions
Download patch file Download diff file Expand all files Collapse all files

203
src/ast/simplifiers/solve_context_eqs.cpp Normal file
View file

@ -0,0 +1,203 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
solve_context_eqs.cpp
Abstract:
simplifier for solving equations within a context
Author:
Nikolaj Bjorner (nbjorner) 2022-11-2.
Notes:
The variable v is solved based on expression e.
Check that every occurrence of v uses e in conjunctive context.
Walk formulas containing v in as and-or.
Equalities that occur within at least one alternation of or are
considered as candidates.
To constrain how formulas are traversed, first
label sub-expressions that contain v. An equality eq is safe for v
if every occurrence of v occurs in the same conjunctive context as eq.
--*/
#include "ast/ast.h"
#include "ast/ast_pp.h"
#include "ast/occurs.h"
#include "ast/simplifiers/solve_context_eqs.h"
#include "ast/simplifiers/solve_eqs.h"
namespace euf {
solve_context_eqs::solve_context_eqs(solve_eqs& s): m(s.m), m_fmls(s.m_fmls), m_solve_eqs(s) {}
bool solve_context_eqs::is_safe_eq(expr* e) {
m_and_pos.reset(); m_and_neg.reset(); m_or_pos.reset(); m_or_neg.reset();
for (unsigned i = 0; i < m_fmls.size(); ++i)
if (!is_safe_eq(m_fmls[i].fml(), e))
return false;
return true;
}
/**
* Check if some conjunction of f contains equality 'e'.
* If this is not the case, then check that every conjunct that contains v
* recursively contains a disjunction that contains 'e'.
*/
bool solve_context_eqs::is_safe_eq(unsigned recursion_depth, expr* f, bool sign, expr* e) {
if (!contains_v(f))
return true;
signed_expressions conjuncts;
if (contains_conjunctively(f, sign, e, conjuncts))
return true;
if (recursion_depth > 3)
return false;
return all_of(conjuncts, [&](std::pair<bool,expr*> const& p) { return is_disjunctively_safe(recursion_depth, p.second, p.first, e); });
}
/*
* Every disjunction in f that contains v also contains the equation e.
*/
bool solve_context_eqs::is_disjunctively_safe(unsigned recursion_depth, expr* f, bool sign, expr* e) {
signed_expressions todo;
todo.push_back({sign, f});
while (!todo.empty()) {
auto [s, f] = todo.back();
todo.pop_back();
if (s && m_or_neg.is_marked(f))
continue;
if (!s && m_or_pos.is_marked(f))
continue;
if (s)
m_or_neg.mark(f, true);
else
m_or_pos.mark(f, true);
if (!s && f == e)
continue;
else if (!contains_v(f))
continue;
else if (s && m.is_and(f))
for (auto* arg : *to_app(f))
todo.push_back({s, arg});
else if (!s && m.is_or(f))
for (auto* arg : *to_app(f))
todo.push_back({s, arg});
else if (m.is_not(f, f))
todo.push_back({!s, f});
else if (!is_safe_eq(recursion_depth + 1, f, s, e))
return false;
}
return true;
}
/**
* Determine whether some conjunction in f contains e.
* If no conjunction contains e, then return the set of conjunctions that contain v.
*/
bool solve_context_eqs::contains_conjunctively(expr* f, bool sign, expr* e, signed_expressions& conjuncts) {
signed_expressions todo;
todo.push_back({sign, f});
while (!todo.empty()) {
auto [s, f] = todo.back();
todo.pop_back();
if (!s && f == e)
return true;
if (!s && m_and_pos.is_marked(f))
continue;
if (s && m_and_neg.is_marked(f))
continue;
if (s)
m_and_neg.mark(f, true);
else
m_and_pos.mark(f, true);
if (!contains_v(f))
continue;
if (!s && m.is_and(f))
for (auto* arg : *to_app(f))
todo.push_back({false, arg});
else if (s && m.is_or(f))
for (auto* arg : *to_app(f))
todo.push_back({true, arg});
else if (m.is_not(f, f))
todo.push_back({!s, f});
else
conjuncts.push_back({s, f});
}
return false;
}
void solve_context_eqs::init_contains(expr* v) {
m_contains_v.reset();
for (unsigned i = 0; i < m_fmls.size(); ++i)
m_todo.push_back(m_fmls[i].fml());
mark_occurs(m_todo, v, m_contains_v);
SASSERT(m_todo.empty());
}
void solve_context_eqs::collect_nested_equalities(dep_eq_vector& eqs) {
expr_mark visited;
for (unsigned i = m_solve_eqs.m_qhead; i < m_fmls.size(); ++i)
collect_nested_equalities(m_fmls[i], visited, eqs);
unsigned j = 0;
for (auto const& eq : eqs) {
init_contains(eq.var);
if (is_safe_eq(eq.orig))
eqs[j++] = eq;
}
eqs.shrink(j);
}
void solve_context_eqs::collect_nested_equalities(dependent_expr const& df, expr_mark& visited, dep_eq_vector& eqs) {
svector<std::tuple<bool,unsigned,expr*>> todo;
todo.push_back({ false, 0, df.fml()});
// even depth is conjunctive context, odd is disjunctive
// when alternating between conjunctive and disjunctive context, increment depth.
auto inc_or = [](unsigned depth) {
return (0 == depth % 2) ? depth + 1 : depth;
};
auto inc_and = [](unsigned depth) {
return (0 == depth % 2) ? depth : depth + 1;
};
while (!todo.empty()) {
auto [s, depth, f] = todo.back();
todo.pop_back();
if (visited.is_marked(f))
continue;
visited.mark(f, true);
if (s && m.is_and(f)) {
for (auto* arg : *to_app(f))
todo.push_back({ s, inc_or(depth), arg });
}
else if (!s && m.is_or(f)) {
for (auto* arg : *to_app(f))
todo.push_back({ s, inc_or(depth), arg });
}
if (!s && m.is_and(f)) {
for (auto* arg : *to_app(f))
todo.push_back({ s, inc_and(depth), arg });
}
else if (s && m.is_or(f)) {
for (auto* arg : *to_app(f))
todo.push_back({ s, inc_and(depth), arg });
}
else if (m.is_not(f, f))
todo.push_back({ !s, depth, f });
else if (!s && 1 == depth % 2) {
for (extract_eq* ex : m_solve_eqs.m_extract_plugins)
ex->get_eqs(dependent_expr(m, f, df.dep()), eqs);
}
}
}
}