3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-19 15:19:07 +01:00
parent 0f03ef4ab0
commit e5767bf2b8
6 changed files with 43 additions and 7 deletions

View file

@ -2470,6 +2470,10 @@ namespace smt2 {
next();
}
/**
* (declare-fun f (sorts) sort)
* (declare-fun (alphas) (sorts) sort)
*/
void parse_declare_fun() {
SASSERT(curr_is_identifier());
SASSERT(curr_id() == m_declare_fun);

View file

@ -761,6 +761,10 @@ namespace euf {
return true;
}
bool solver::is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain) {
return false;
}
void solver::pre_simplify() {
for (auto* e : m_solvers)
e->pre_simplify();

View file

@ -371,6 +371,7 @@ namespace euf {
void rewrite(expr_ref& e) { m_rewriter(e); }
bool is_shared(euf::enode* n) const;
bool enable_ackerman_axioms(expr* n) const;
bool is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain);
// relevancy

View file

@ -36,6 +36,10 @@ namespace user_solver {
return n->get_th_var(get_id());
euf::theory_var v = mk_var(n);
ctx.attach_th_var(n, this, v);
expr_ref r(m);
sat::literal_vector explain;
if (ctx.is_fixed(n, r, explain))
m_prop.push_back(prop_info(explain, v, r));
return v;
}
@ -93,6 +97,18 @@ namespace user_solver {
m_pop_eh(m_user_context, num_scopes);
}
void solver::propagate_consequence(prop_info const& prop) {
sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true);
if (s().value(lit) != l_true) {
s().assign(lit, mk_justification(m_qhead));
++m_stats.m_num_propagations;
}
}
void solver::propagate_new_fixed(prop_info const& prop) {
new_fixed_eh(prop.m_var, prop.m_conseq, prop.m_lits.size(), prop.m_lits.data());
}
bool solver::unit_propagate() {
if (m_qhead == m_prop.size())
return false;
@ -100,12 +116,11 @@ namespace user_solver {
ctx.push(value_trail<unsigned>(m_qhead));
unsigned np = m_stats.m_num_propagations;
for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) {
auto const& prop = m_prop[m_qhead];
sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true);
if (s().value(lit) != l_true) {
s().assign(lit, mk_justification(m_qhead));
++m_stats.m_num_propagations;
}
auto const& prop = m_prop[m_qhead];
if (prop.m_var == euf::null_theory_var)
propagate_consequence(prop);
else
propagate_new_fixed(prop);
}
return np < m_stats.m_num_propagations;
}

View file

@ -32,6 +32,9 @@ namespace user_solver {
unsigned_vector m_ids;
expr_ref m_conseq;
svector<std::pair<unsigned, unsigned>> m_eqs;
sat::literal_vector m_lits;
euf::theory_var m_var = euf::null_theory_var;
prop_info(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr_ref const& c):
m_ids(num_fixed, fixed_ids),
m_conseq(c)
@ -39,6 +42,12 @@ namespace user_solver {
for (unsigned i = 0; i < num_eqs; ++i)
m_eqs.push_back(std::make_pair(eq_lhs[i], eq_rhs[i]));
}
prop_info(sat::literal_vector const& lits, euf::theory_var v, expr_ref const& val):
m_conseq(val),
m_lits(lits),
m_var(v) {}
};
struct stats {
@ -80,6 +89,9 @@ namespace user_solver {
sat::justification mk_justification(unsigned propagation_index);
void propagate_consequence(prop_info const& prop);
void propagate_new_fixed(prop_info const& prop);
void validate_propagation();
public:

View file

@ -48,7 +48,7 @@ unsigned theory_user_propagator::add_expr(expr* e) {
ctx.assert_expr(eq);
ctx.internalize_assertions();
e = r;
ctx.mark_as_relevant(eq);
ctx.mark_as_relevant(eq.get());
}
enode* n = ensure_enode(e);
if (is_attached_to_var(n))