mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

don't add viable premises on decisions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-25 20:19:58 +01:00
parent a4e29ecd7e
commit fc6e127cca
4 changed files with 13 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/conflict.cpp
View file

@ -298,12 +298,16 @@ namespace polysat {
return false; return false;
} }
auto const& j = s.m_justification[v];
s.inc_activity(v); s.inc_activity(v);
m_vars.remove(v); m_vars.remove(v);
if (!j.is_decision()) {
for (auto const& c : s.m_viable.get_constraints(v)) for (auto const& c : s.m_viable.get_constraints(v))
insert(c); insert(c);
}
for (auto* engine : ex_engines) for (auto* engine : ex_engines)
if (engine->try_explain(v, *this)) if (engine->try_explain(v, *this))
@ -318,7 +322,7 @@ namespace polysat {
break; break;
} }
set_bailout(); set_bailout();
if (s.is_assigned(v) && s.m_justification[v].is_decision()) if (s.is_assigned(v) && j.is_decision())
m_vars.insert(v); m_vars.insert(v);
return false; return false;
} }

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

@ -50,7 +50,6 @@ namespace polysat {
m_branch_bool = m_params.get_bool("branch_bool", false); m_branch_bool = m_params.get_bool("branch_bool", false);
m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX); m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX);
m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX); m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX);
std::cout << m_max_conflicts << "\n";
} }
bool solver::should_search() { bool solver::should_search() {

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

@ -278,7 +278,6 @@ namespace polysat {
} }
bool viable::resolve(pvar v, conflict& core) { bool viable::resolve(pvar v, conflict& core) {
std::cout << "resolve " << v << "\n";
if (has_viable(v)) if (has_viable(v))
return false; return false;
auto* e = m_viable[v]; auto* e = m_viable[v];

11
src/test/polysat.cpp
View file

@ -18,8 +18,7 @@ namespace polysat {
public: public:
scoped_solver(std::string name): solver(lim), m_name(name) { scoped_solver(std::string name): solver(lim), m_name(name) {
std::cout << "\n\n\n" << std::string(78, '#') << "\n"; LOG("\n\n\n" << std::string(78, '#') << "\n\nSTART: " << m_name << "\n");
std::cout << "\nSTART: " << m_name << "\n";
params_ref p; params_ref p;
p.set_uint("max_conflicts", 10); p.set_uint("max_conflicts", 10);
updt_params(p); updt_params(p);
@ -27,11 +26,10 @@ namespace polysat {
void check() { void check() {
m_last_result = check_sat(); m_last_result = check_sat();
std::cout << m_name << ": " << m_last_result << "\n"; LOG(m_name << ": " << m_last_result << "\n");
statistics st; statistics st;
collect_statistics(st); collect_statistics(st);
std::cout << st << "\n"; LOG(st << "\n" << *this << "\n");
std::cout << *this << "\n";
} }
void expect_unsat() { void expect_unsat() {
@ -1068,6 +1066,9 @@ namespace polysat {
void tst_polysat() { void tst_polysat() {
polysat::test_l5();
return;
polysat::test_ineq_basic6(); polysat::test_ineq_basic6();
// polysat::test_monot_bounds(8); // polysat::test_monot_bounds(8);