mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-08 23:35:07 +00:00
Code Activity

add some comments on todos

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-21 08:43:48 -08:00
parent 899cd0aa2c
commit 302a27e89b
1 changed files with 18 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/solver/smtmus.cpp
View file

@ -13,6 +13,20 @@ Author:
Jaroslav Bendik, Nikolaj Bjorner (nbjorner) 2021-12-20 Jaroslav Bendik, Nikolaj Bjorner (nbjorner) 2021-12-20
Notes:
- hard constraints need to be handled.
- we need an occurs index into hard constraints so that rotations can be checked
to not violate hard constraints.
- extraction of soft clauses from hard constraints to be revised, made solid.
- soundness of core reduction to be checked.
- The call to check-sat uses negated soft constraints
- In other core reduction code I don't minimize cores if there is a dependency on
negated soft constraints.
- sign of ineq::get_value is probably wrong,
- negate it
- check if it works with strict inequalities.
--*/ --*/
#include "solver/solver.h" #include "solver/solver.h"
@ -305,6 +319,7 @@ struct smtmus::imp {
for (unsigned i = 0; i < m_soft_clauses.size(); ++i) { for (unsigned i = 0; i < m_soft_clauses.size(); ++i) {
if (!shrunk[i] || crits[i]) if (!shrunk[i] || crits[i])
continue; continue;
// TODO - is prev_size used?
unsigned prev_size = count_ones(shrunk); unsigned prev_size = count_ones(shrunk);
shrunk[i] = false; shrunk[i] = false;
switch (solve(shrunk, max_cores > 0, false)) { switch (solve(shrunk, max_cores > 0, false)) {
@ -540,6 +555,8 @@ struct smtmus::imp {
return true; return true;
if (!e) if (!e)
return true; return true;
if (!a.is_numeral(e->m_base))
return true;
if (!e->m_coeffs.contains(v)) if (!e->m_coeffs.contains(v))
continue; continue;
auto b = e->get_bound_type(v); auto b = e->get_bound_type(v);