mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

forbidden intervals only used by viable

Browse source
This commit is contained in:
Jakob Rath 2022-03-10 16:12:13 +01:00
parent afc711d6ec
commit c648b57493
5 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/solver.cpp
View file

@ -35,7 +35,6 @@ namespace polysat {
m_conflict(*this),
m_simplify(*this),
m_restart(*this),
m_forbidden_intervals(*this),
m_bvars(),
m_free_pvars(m_activity),
m_constraints(m_bvars),

2
src/math/polysat/solver.h
View file

@ -31,7 +31,6 @@ Author:
#include "math/polysat/justification.h"
#include "math/polysat/linear_solver.h"
#include "math/polysat/search_state.h"
#include "math/polysat/forbidden_intervals.h"
#include "math/polysat/trail.h"
#include "math/polysat/viable.h"
#include "math/polysat/log.h"
@ -89,7 +88,6 @@ namespace polysat {
conflict m_conflict;
simplify m_simplify;
restart m_restart;
forbidden_intervals m_forbidden_intervals;
bool_var_manager m_bvars; // Map boolean variables to constraints
var_queue m_free_pvars; // free poly vars
stats m_stats;

2
src/math/polysat/ule_constraint.cpp
View file

@ -133,7 +133,7 @@ namespace polysat {
LOG("Substituted RHS: " << rhs() << " := " << q);
if (is_always_false(is_positive, p, q)) {
s.set_conflict({this, is_positive});
s.set_conflict(sc);
return;
}
if (p.is_val() && q.is_val()) {

12
src/math/polysat/viable.cpp
View file

@ -27,7 +27,10 @@ just check if the cached phase is viable without detecting that it is a propagat
namespace polysat {
viable::viable(solver& s) : s(s) {}
viable::viable(solver& s):
s(s),
m_forbidden_intervals(s) {
}
viable::~viable() {
for (entry* e : m_alloc)
@ -93,9 +96,9 @@ namespace polysat {
return prop;
try_viable:
if (s.m_viable.intersect(v, sc)) {
if (intersect(v, sc)) {
rational val;
switch (s.m_viable.find_viable(v, val)) {
switch (find_viable(v, val)) {
case dd::find_t::singleton:
s.propagate(v, val, sc); // TBD why is sc used as justification? It should be all of viable
prop = true;
@ -116,9 +119,8 @@ namespace polysat {
}
bool viable::intersect(pvar v, signed_constraint const& c) {
auto& fi = s.m_forbidden_intervals;
entry* ne = alloc_entry();
if (!fi.get_interval(c, v, *ne)) {
if (!m_forbidden_intervals.get_interval(c, v, *ne)) {
m_alloc.push_back(ne);
return false;
}

2
src/math/polysat/viable.h
View file

@ -23,6 +23,7 @@ Author:
#include "math/polysat/types.h"
#include "math/polysat/conflict.h"
#include "math/polysat/constraint.h"
#include "math/polysat/forbidden_intervals.h"
#include "math/polysat/univariate/univariate_solver.h"
namespace polysat {
@ -33,6 +34,7 @@ namespace polysat {
friend class test_fi;
solver& s;
forbidden_intervals m_forbidden_intervals;
struct entry : public dll_base<entry>, public fi_record {
entry() : fi_record({ eval_interval::full(), {}, {}, rational::one()}) {}