mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
a few more spacer related warning messages
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9a78bec8a8
commit
b12882d94a
|
@ -335,8 +335,8 @@ bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m,
|
|||
|
||||
// for each substitution entry
|
||||
bool is_first_key = true;
|
||||
unsigned lower_bound;
|
||||
unsigned upper_bound;
|
||||
unsigned lower_bound = 0;
|
||||
unsigned upper_bound = 0;
|
||||
for (const auto& pair : au.get_substitution(0)) {
|
||||
// construct vector
|
||||
expr* key = &pair.get_key();
|
||||
|
@ -355,8 +355,8 @@ bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m,
|
|||
}
|
||||
|
||||
// check whether vector represents interval
|
||||
unsigned current_lower_bound;
|
||||
unsigned current_upper_bound;
|
||||
unsigned current_lower_bound = 0;
|
||||
unsigned current_upper_bound = 0;
|
||||
|
||||
// if vector represents interval
|
||||
if (get_range(entries, current_lower_bound, current_upper_bound)) {
|
||||
|
|
|
@ -389,11 +389,11 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
|
|||
simplify_bounds(lemmas);
|
||||
}
|
||||
|
||||
void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas)
|
||||
void farkas_learner::get_asserted(proof* p0, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas)
|
||||
{
|
||||
ast_manager& m = lemmas.get_manager();
|
||||
ast_mark visited;
|
||||
proof* p0 = p;
|
||||
proof* p = p0;
|
||||
ptr_vector<proof> todo;
|
||||
todo.push_back(p);
|
||||
|
||||
|
|
|
@ -133,9 +133,7 @@ void unsat_core_generalizer::operator()(lemma_ref &lemma)
|
|||
|
||||
unsigned uses_level;
|
||||
expr_ref_vector core(m);
|
||||
bool r;
|
||||
r = pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core);
|
||||
SASSERT(r);
|
||||
VERIFY(pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core));
|
||||
|
||||
CTRACE("spacer", old_sz > core.size(),
|
||||
tout << "unsat core reduced lemma from: "
|
||||
|
@ -185,6 +183,7 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma)
|
|||
// -- find array constants
|
||||
ast_manager &m = lemma->get_ast_manager();
|
||||
manager &pm = m_ctx.get_manager();
|
||||
(void)pm;
|
||||
|
||||
expr_ref_vector core(m);
|
||||
expr_ref v(m);
|
||||
|
|
|
@ -79,6 +79,7 @@ bool pred_transformer::legacy_frames::propagate_to_next_level(unsigned src_level
|
|||
{
|
||||
|
||||
ast_manager &m = m_pt.get_ast_manager();
|
||||
(void) m;
|
||||
if (m_levels.size() <= src_level) { return true; }
|
||||
if (m_levels [src_level].empty()) { return true; }
|
||||
|
||||
|
|
|
@ -264,6 +264,7 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
|
|||
else { m_ctx->assert_expr(bg[i]); }
|
||||
|
||||
unsigned soft_sz = soft.size();
|
||||
(void) soft_sz;
|
||||
lbool res = internal_check_assumptions(hard, soft);
|
||||
if (!m_use_push_bg) { m_ctx->pop(1); }
|
||||
|
||||
|
|
|
@ -788,7 +788,7 @@ namespace qe {
|
|||
}
|
||||
|
||||
unsigned find_max(model& mdl, bool do_pos) {
|
||||
unsigned result;
|
||||
unsigned result = UINT_MAX;
|
||||
bool found = false;
|
||||
bool found_strict = false;
|
||||
rational found_val (0), r, r_plus_x, found_c;
|
||||
|
@ -2078,6 +2078,7 @@ namespace qe {
|
|||
sort* v_sort = m.get_sort (v);
|
||||
sort* val_sort = get_array_range (v_sort);
|
||||
sort* idx_sort = get_array_domain (v_sort, 0);
|
||||
(void) idx_sort;
|
||||
|
||||
unsigned start = m_idx_reprs.size (); // append at the end
|
||||
|
||||
|
|
|
@ -444,10 +444,10 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
|
|||
}
|
||||
|
||||
|
||||
void unsat_core_plugin_farkas_lemma_bounded::finalize()
|
||||
{
|
||||
if(m_linear_combinations.empty())
|
||||
{return;}
|
||||
void unsat_core_plugin_farkas_lemma_bounded::finalize() {
|
||||
if (m_linear_combinations.empty()) {
|
||||
return;
|
||||
}
|
||||
DEBUG_CODE(
|
||||
for (auto& linear_combination : m_linear_combinations) {
|
||||
SASSERT(linear_combination.size() > 0);
|
||||
|
@ -457,12 +457,9 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
|
|||
ptr_vector<app> ordered_basis;
|
||||
obj_map<app, unsigned> map;
|
||||
unsigned counter = 0;
|
||||
for (const auto& linear_combination : m_linear_combinations)
|
||||
{
|
||||
for (const auto& pair : linear_combination)
|
||||
{
|
||||
if (!map.contains(pair.first))
|
||||
{
|
||||
for (const auto& linear_combination : m_linear_combinations) {
|
||||
for (const auto& pair : linear_combination) {
|
||||
if (!map.contains(pair.first)) {
|
||||
ordered_basis.push_back(pair.first);
|
||||
map.insert(pair.first, counter++);
|
||||
}
|
||||
|
@ -472,14 +469,12 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
|
|||
// 2. populate matrix
|
||||
spacer_matrix matrix(m_linear_combinations.size(), ordered_basis.size());
|
||||
|
||||
for (unsigned i=0; i < m_linear_combinations.size(); ++i)
|
||||
{
|
||||
for (unsigned i=0; i < m_linear_combinations.size(); ++i) {
|
||||
auto linear_combination = m_linear_combinations[i];
|
||||
for (const auto& pair : linear_combination)
|
||||
{
|
||||
for (const auto& pair : linear_combination) {
|
||||
matrix.set(i, map[pair.first], pair.second);
|
||||
}
|
||||
}
|
||||
}
|
||||
matrix.print_matrix();
|
||||
|
||||
// 3. normalize matrix to integer values
|
||||
|
@ -489,8 +484,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
|
|||
arith_util util(m);
|
||||
|
||||
vector<expr_ref_vector> coeffs;
|
||||
for (unsigned i=0; i < matrix.num_rows(); ++i)
|
||||
{
|
||||
for (unsigned i=0; i < matrix.num_rows(); ++i) {
|
||||
coeffs.push_back(expr_ref_vector(m));
|
||||
}
|
||||
|
||||
|
@ -532,19 +526,17 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
|
|||
}
|
||||
|
||||
// assert bounds for all s_jn
|
||||
for (unsigned l=0; l < n; ++l)
|
||||
{
|
||||
for (unsigned j=0; j < matrix.num_cols(); ++j)
|
||||
{
|
||||
for (unsigned l=0; l < n; ++l) {
|
||||
for (unsigned j=0; j < matrix.num_cols(); ++j) {
|
||||
expr* s_jn = bounded_vectors[j][l].get();
|
||||
|
||||
|
||||
expr_ref lb(util.mk_le(util.mk_int(0), s_jn), m);
|
||||
expr_ref ub(util.mk_le(s_jn, util.mk_int(1)), m);
|
||||
s->assert_expr(lb);
|
||||
s->assert_expr(ub);
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
// assert: forall i,j: a_ij = sum_k w_ik * s_jk
|
||||
for (unsigned i=0; i < matrix.num_rows(); ++i)
|
||||
{
|
||||
|
@ -568,34 +560,30 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
|
|||
lbool res = s->check_sat(0,0);
|
||||
|
||||
// if sat extract model and add corresponding linear combinations to core
|
||||
if (res == lbool::l_true)
|
||||
{
|
||||
if (res == lbool::l_true) {
|
||||
model_ref model;
|
||||
s->get_model(model);
|
||||
|
||||
for (int k=0; k < n; ++k)
|
||||
{
|
||||
ptr_vector<app> literals;
|
||||
vector<rational> coefficients;
|
||||
for (unsigned j=0; j < matrix.num_cols(); ++j)
|
||||
{
|
||||
|
||||
for (unsigned k=0; k < n; ++k) {
|
||||
ptr_vector<app> literals;
|
||||
vector<rational> coefficients;
|
||||
for (unsigned j=0; j < matrix.num_cols(); ++j) {
|
||||
expr_ref evaluation(m);
|
||||
|
||||
|
||||
model.get()->eval(bounded_vectors[j][k].get(), evaluation, false);
|
||||
if (!util.is_zero(evaluation))
|
||||
{
|
||||
if (!util.is_zero(evaluation)) {
|
||||
literals.push_back(ordered_basis[j]);
|
||||
coefficients.push_back(rational(1));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
SASSERT(!literals.empty()); // since then previous outer loop would have found solution already
|
||||
expr_ref linear_combination(m);
|
||||
compute_linear_combination(coefficients, literals, linear_combination);
|
||||
|
||||
m_learner.add_lemma_to_core(linear_combination);
|
||||
}
|
||||
expr_ref linear_combination(m);
|
||||
compute_linear_combination(coefficients, literals, linear_combination);
|
||||
|
||||
m_learner.add_lemma_to_core(linear_combination);
|
||||
}
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue