mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-02 09:23:59 -07:00
parent edb26e7be7
commit e9a4a9a390
3 changed files with 18 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/sat/smt/user_solver.cpp
View file

@ -44,6 +44,7 @@ namespace user {
unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs,
expr* conseq) { expr* conseq) {
m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m))); m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m)));
DEBUG_CODE(validate_propagation(););
} }
sat::check_result solver::check() { sat::check_result solver::check() {
@ -95,7 +96,7 @@ namespace user {
ctx.push(value_trail<unsigned>(m_qhead)); ctx.push(value_trail<unsigned>(m_qhead));
unsigned np = m_stats.m_num_propagations; unsigned np = m_stats.m_num_propagations;
for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) { for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) {
auto const& prop = m_prop[m_qhead]; auto const& prop = m_prop[m_qhead];
sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true); sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true);
if (s().value(lit) != l_true) { if (s().value(lit) != l_true) {
s().assign(lit, mk_justification(m_qhead)); s().assign(lit, mk_justification(m_qhead));
@ -126,6 +127,19 @@ namespace user {
ctx.add_antecedent(var2enode(p.first), var2enode(p.second)); ctx.add_antecedent(var2enode(p.first), var2enode(p.second));
} }
/*
* All assumptions and equalities have to be true in the current scope.
* A caller could mistakingly supply some assumption that isn't set.
*/
void solver::validate_propagation() {
auto const& prop = m_prop.back();
for (unsigned id : prop.m_ids)
for (auto lit: m_id2justification[id])
VERIFY(s().value(lit) == l_true);
for (auto const& p : prop.m_eqs)
VERIFY(var2enode(p.first)->get_root() == var2enode(p.second)->get_root());
}
std::ostream& solver::display(std::ostream& out) const { std::ostream& solver::display(std::ostream& out) const {
for (unsigned i = 0; i < get_num_vars(); ++i) for (unsigned i = 0; i < get_num_vars(); ++i)
out << i << ": " << mk_pp(var2expr(i), m) << "\n"; out << i << ": " << mk_pp(var2expr(i), m) << "\n";

2
src/sat/smt/user_solver.h
View file

@ -79,6 +79,8 @@ namespace user {
sat::justification mk_justification(unsigned propagation_index); sat::justification mk_justification(unsigned propagation_index);
void validate_propagation();
public: public:
solver(euf::solver& ctx); solver(euf::solver& ctx);

1
src/smt/user_propagator.cpp
View file

@ -128,6 +128,7 @@ void user_propagator::propagate() {
DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id));); DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id)););
DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true);); DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true););
if (m.is_false(prop.m_conseq)) { if (m.is_false(prop.m_conseq)) {
js = ctx.mk_justification( js = ctx.mk_justification(
ext_theory_conflict_justification( ext_theory_conflict_justification(