mirror of
https://github.com/Z3Prover/z3
synced 2025-07-23 20:58:54 +00:00
remove cm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
342f4473b0
commit
deeb6c7784
2 changed files with 5 additions and 8 deletions
|
@ -29,8 +29,6 @@ TODO: when we check that 'x' is "unary":
|
||||||
|
|
||||||
namespace polysat {
|
namespace polysat {
|
||||||
|
|
||||||
constraint_manager& inference_engine::cm() { return s().m_constraints; }
|
|
||||||
|
|
||||||
bool inf_saturate::perform(pvar v, conflict_core& core) {
|
bool inf_saturate::perform(pvar v, conflict_core& core) {
|
||||||
for (auto c1 : core) {
|
for (auto c1 : core) {
|
||||||
if (!c1->is_ule())
|
if (!c1->is_ule())
|
||||||
|
@ -50,9 +48,9 @@ namespace polysat {
|
||||||
|
|
||||||
signed_constraint inf_saturate::ineq(bool is_strict, pdd const& lhs, pdd const& rhs) {
|
signed_constraint inf_saturate::ineq(bool is_strict, pdd const& lhs, pdd const& rhs) {
|
||||||
if (is_strict)
|
if (is_strict)
|
||||||
return cm().ult(lhs, rhs);
|
return s().ult(lhs, rhs);
|
||||||
else
|
else
|
||||||
return cm().ule(lhs, rhs);
|
return s().ule(lhs, rhs);
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -125,8 +123,8 @@ namespace polysat {
|
||||||
// conflict resolution should be able to pick up this as a valid justification.
|
// conflict resolution should be able to pick up this as a valid justification.
|
||||||
// or we resort to the same extension as in the original mul_overflow code
|
// or we resort to the same extension as in the original mul_overflow code
|
||||||
// where we add explicit equality propagations from the current assignment.
|
// where we add explicit equality propagations from the current assignment.
|
||||||
auto c1 = cm().ule(x, pddm.mk_val(x_lo));
|
auto c1 = s().ule(x, pddm.mk_val(x_lo));
|
||||||
auto c2 = cm().ule(y, pddm.mk_val(y_lo));
|
auto c2 = s().ule(y, pddm.mk_val(y_lo));
|
||||||
reason.push(~c1);
|
reason.push(~c1);
|
||||||
reason.push(~c2);
|
reason.push(~c2);
|
||||||
}
|
}
|
||||||
|
@ -262,7 +260,7 @@ namespace polysat {
|
||||||
|
|
||||||
clause_builder reason(s());
|
clause_builder reason(s());
|
||||||
if (!c.is_strict)
|
if (!c.is_strict)
|
||||||
reason.push(cm().eq(x));
|
reason.push(s().eq(x));
|
||||||
reason.push(~c.as_signed_constraint());
|
reason.push(~c.as_signed_constraint());
|
||||||
push_omega(reason, x, y);
|
push_omega(reason, x, y);
|
||||||
return propagate(core, c, c.is_strict, y, z, reason);
|
return propagate(core, c, c.is_strict, y, z, reason);
|
||||||
|
|
|
@ -25,7 +25,6 @@ namespace polysat {
|
||||||
void set_solver(solver& s) { m_solver = &s; }
|
void set_solver(solver& s) { m_solver = &s; }
|
||||||
protected:
|
protected:
|
||||||
solver& s() { return *m_solver; }
|
solver& s() { return *m_solver; }
|
||||||
constraint_manager& cm();
|
|
||||||
public:
|
public:
|
||||||
virtual ~inference_engine() {}
|
virtual ~inference_engine() {}
|
||||||
/** Try to apply an inference rule.
|
/** Try to apply an inference rule.
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue