mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

notes

Browse source
This commit is contained in:
Jakob Rath 2021-09-08 18:21:09 +02:00
parent 6766c1c349
commit 64ce6cb5c1
3 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/clause_builder.h
View file

@ -23,7 +23,6 @@ Notes:
namespace polysat { namespace polysat {
// TODO: this is now incorporated in conflict_core
class clause_builder { class clause_builder {
solver* m_solver; solver* m_solver;
sat::literal_vector m_literals; sat::literal_vector m_literals;

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

@ -23,6 +23,7 @@ namespace polysat {
// c1 is true, c2 is false // c1 is true, c2 is false
SASSERT(c1.is_currently_true(s())); SASSERT(c1.is_currently_true(s()));
SASSERT(c2.is_currently_false(s())); SASSERT(c2.is_currently_false(s()));
LOG_H3("Resolving upon v" << v);
LOG("c1: " << c1); LOG("c1: " << c1);
LOG("c2: " << c2); LOG("c2: " << c2);
pdd a = c1->to_eq().p(); pdd a = c1->to_eq().p();

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

@ -154,6 +154,7 @@ namespace polysat {
#if ENABLE_LINEAR_SOLVER #if ENABLE_LINEAR_SOLVER
m_linear_solver.new_constraint(*c.get()); m_linear_solver.new_constraint(*c.get());
#endif #endif
// TODO: there is an issue when the input contains both c and ~c. (see test_ineq_basic2)
if (activate && !is_conflict()) if (activate && !is_conflict())
propagate_bool(c.blit(), unit); propagate_bool(c.blit(), unit);
} }