mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

conflict_core helpers

Browse source
This commit is contained in:
Jakob Rath 2021-09-08 13:58:20 +02:00
parent 05b846a472
commit c0f51eacf8
2 changed files with 37 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/math/polysat/conflict_core.cpp
View file

@ -16,6 +16,7 @@ Author:
#include "math/polysat/solver.h"
#include "math/polysat/log.h"
#include "math/polysat/log_helper.h"
#include "math/polysat/explain.h"
#include "math/polysat/saturation.h"
#include "math/polysat/variable_elimination.h"
#include <algorithm>
@ -79,6 +80,31 @@ namespace polysat {
m_saturation_premises.insert(c, std::move(premises)); // TODO: map doesn't have move-insertion, so this still copies the vector. Maybe we want a clause_ref (but this doesn't work either since c doesn't have a boolean variable yet).
}
void conflict_core::remove(signed_constraint c) {
m_constraints.erase(c);
}
void conflict_core::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises) {
remove(c_old);
insert(c_new, c_new_premises);
}
void conflict_core::remove_var(pvar v) {
unsigned j = 0;
for (unsigned i = 0; i < m_constraints.size(); ++i)
if (m_constraints[i]->contains_var(v))
m_constraints[j++] = m_constraints[i];
m_constraints.shrink(j);
}
void conflict_core::keep(signed_constraint c) {
SASSERT(!c->has_bvar());
cm().ensure_bvar(c.get());
LOG("new constraint: " << c);
// Insert the temporary constraint from saturation into \Gamma.
handle_saturation_premises(c);
}
void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
// Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
// clause: x \/ u \/ v
@ -166,13 +192,8 @@ namespace polysat {
// TODO: try a final core reduction step?
for (auto c : m_constraints) {
if (!c->has_bvar()) {
// temporary constraint -> keep it
cm().ensure_bvar(c.get());
LOG("new constraint: " << c);
// Insert the temporary constraint from saturation into \Gamma.
handle_saturation_premises(c);
}
if (!c->has_bvar())
keep(c);
lemma.push(c);
}

10
src/math/polysat/conflict_core.h
View file

@ -18,6 +18,7 @@ Author:
namespace polysat {
class solver;
class explainer;
class inference_engine;
class variable_elimination_engine;
@ -40,6 +41,7 @@ namespace polysat {
solver* m_solver = nullptr;
constraint_manager& cm();
scoped_ptr_vector<explainer> ex_engines;
scoped_ptr_vector<variable_elimination_engine> ve_engines;
scoped_ptr_vector<inference_engine> inf_engines;
@ -77,7 +79,13 @@ namespace polysat {
void insert(signed_constraint c);
void insert(signed_constraint c, vector<signed_constraint> premises);
void remove(signed_constraint c) { NOT_IMPLEMENTED_YET(); }
void remove(signed_constraint c);
void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises);
/** remove all constraints that contain the variable v */
void remove_var(pvar v);
void keep(signed_constraint c);
/** Perform boolean resolution with the clause upon variable 'var'.
* Precondition: core/clause contain complementary 'var'-literals.