From d74978c2772fa5a474a6eb266ade720c613ecc64 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Jul 2018 20:29:26 +0100 Subject: [PATCH] fix #1762, #1764, #1768 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 8 -------- src/opt/opt_context.cpp | 8 +++----- src/smt/mam.cpp | 24 ++++++++++-------------- src/smt/params/theory_arith_params.h | 2 +- src/smt/theory_lra.cpp | 5 +++-- src/util/approx_nat.h | 2 +- src/util/bit_vector.cpp | 2 +- src/util/fixed_bit_vector.cpp | 2 +- src/util/hashtable.h | 4 ++-- src/util/lp/lar_solver.cpp | 8 ++++++-- src/util/memory_manager.cpp | 2 +- src/util/mpz.h | 1 - src/util/nat_set.h | 2 +- src/util/scoped_timer.cpp | 2 +- src/util/symbol.h | 2 +- 15 files changed, 32 insertions(+), 42 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 7711ec4cd..0eeeeaecc 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1675,7 +1675,6 @@ def Or(*args): class PatternRef(ExprRef): """Patterns are hints for quantifier instantiation. - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. """ def as_ast(self): return Z3_pattern_to_ast(self.ctx_ref(), self.ast) @@ -1686,8 +1685,6 @@ class PatternRef(ExprRef): def is_pattern(a): """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. - >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ]) @@ -1705,8 +1702,6 @@ def is_pattern(a): def MultiPattern(*args): """Create a Z3 multi-pattern using the given expressions `*args` - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. - >>> f = Function('f', IntSort(), IntSort()) >>> g = Function('g', IntSort(), IntSort()) >>> x = Int('x') @@ -1966,8 +1961,6 @@ def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. - >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') @@ -1985,7 +1978,6 @@ def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 566aaa1f6..e5c0bcddb 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1012,8 +1012,7 @@ namespace opt { } } // fix types of objectives: - for (unsigned i = 0; i < m_objectives.size(); ++i) { - objective & obj = m_objectives[i]; + for (objective & obj : m_objectives) { expr* t = obj.m_term; switch(obj.m_type) { case O_MINIMIZE: @@ -1189,13 +1188,12 @@ namespace opt { void context::update_bound(bool is_lower) { expr_ref val(m); if (!m_model.get()) return; - for (unsigned i = 0; i < m_objectives.size(); ++i) { - objective const& obj = m_objectives[i]; + for (objective const& obj : m_objectives) { rational r; switch(obj.m_type) { case O_MINIMIZE: { val = (*m_model)(obj.m_term); - TRACE("opt", tout << obj.m_term << " " << val << " " << is_numeral(val, r) << "\n";); + TRACE("opt", tout << obj.m_term << " " << val << "\n";); if (is_numeral(val, r)) { inf_eps val = inf_eps(obj.m_adjust_value(r)); TRACE("opt", tout << "adjusted value: " << val << "\n";); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 5267800db..00e079989 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -405,7 +405,7 @@ namespace smt { unsigned m_num_regs; unsigned m_num_choices; instruction * m_root; - obj_hashtable m_candidates; + enode_vector m_candidates; #ifdef Z3DEBUG context * m_context; ptr_vector m_patterns; @@ -539,7 +539,7 @@ namespace smt { } void add_candidate(enode * n) { - m_candidates.insert(n); + m_candidates.push_back(n); } bool has_candidates() const { @@ -550,7 +550,7 @@ namespace smt { m_candidates.reset(); } - obj_hashtable const & get_candidates() const { + enode_vector const & get_candidates() const { return m_candidates; } @@ -1978,10 +1978,10 @@ namespace smt { #define INIT_ARGS_SIZE 16 public: - interpreter(context & ctx, mam & m, bool use_filters): + interpreter(context & ctx, mam & ma, bool use_filters): m_context(ctx), m_ast_manager(ctx.get_manager()), - m_mam(m), + m_mam(ma), m_use_filters(use_filters) { m_args.resize(INIT_ARGS_SIZE); } @@ -2001,7 +2001,6 @@ namespace smt { TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout);); init(t); if (t->filter_candidates()) { - //t->display(std::cout << "ncf: " << t->get_candidates().size() << "\n"); for (enode* app : t->get_candidates()) { TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); if (!app->is_marked() && app->is_cgr()) { @@ -2016,9 +2015,6 @@ namespace smt { } } else { - //t->display(std::cout << "ncu: " << t->get_candidates().size() << "\n"); - //for (enode* app : t->get_candidates()) { std::cout << expr_ref(app->get_owner(), m_ast_manager) << "\n"; } - //std::cout.flush(); for (enode* app : t->get_candidates()) { TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); if (app->is_cgr()) { @@ -2842,7 +2838,7 @@ namespace smt { mk_tree_trail(ptr_vector & t, unsigned id):m_trees(t), m_lbl_id(id) {} void undo(mam_impl & m) override { dealloc(m_trees[m_lbl_id]); - m_trees[m_lbl_id] = 0; + m_trees[m_lbl_id] = nullptr; } }; @@ -2875,8 +2871,8 @@ namespace smt { app * p = to_app(mp->get_arg(first_idx)); func_decl * lbl = p->get_decl(); unsigned lbl_id = lbl->get_decl_id(); - m_trees.reserve(lbl_id+1, 0); - if (m_trees[lbl_id] == 0) { + m_trees.reserve(lbl_id+1, nullptr); + if (m_trees[lbl_id] == nullptr) { m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false); SASSERT(m_trees[lbl_id]->expected_num_args() == p->get_num_args()); DEBUG_CODE(m_trees[lbl_id]->set_context(m_context);); @@ -2961,7 +2957,7 @@ namespace smt { m_ground_arg(ground_arg), m_pattern_idx(pat_idx), m_child(child) { - SASSERT(ground_arg != 0 || ground_arg_idx == 0); + SASSERT(ground_arg != nullptr || ground_arg_idx == 0); } }; @@ -3228,7 +3224,7 @@ namespace smt { path_tree * mk_path_tree(path * p, quantifier * qa, app * mp) { SASSERT(m_ast_manager.is_pattern(mp)); - SASSERT(p != 0); + SASSERT(p != nullptr); unsigned pat_idx = p->m_pattern_idx; path_tree * head = nullptr; path_tree * curr = nullptr; diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 9d09b4c38..fe7cc6060 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -19,7 +19,7 @@ Revision History: #ifndef THEORY_ARITH_PARAMS_H_ #define THEORY_ARITH_PARAMS_H_ -#include +#include #include "util/params.h" enum arith_solver_id { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a057ace03..2f89b7168 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2648,6 +2648,7 @@ public: else { rational r = get_value(v); TRACE("arith", tout << "v" << v << " := " << r << "\n";); + SASSERT(!a.is_int(o) || r.is_int()); if (a.is_int(o) && !r.is_int()) r = floor(r); return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o))); } @@ -2797,6 +2798,7 @@ public: lp::var_index vi = m_theory_var2var_index[v]; st = m_solver->maximize_term(vi, term_max); } + TRACE("arith", display(tout << st << " v" << v << "\n");); switch (st) { case lp::lp_status::OPTIMAL: { inf_rational val(term_max.x, term_max.y); @@ -2804,13 +2806,12 @@ public: return inf_eps(rational::zero(), val); } case lp::lp_status::FEASIBLE: { - inf_rational val(term_max.x, term_max.y); + inf_rational val = get_value(v); blocker = mk_gt(v); return inf_eps(rational::zero(), val); } default: SASSERT(st == lp::lp_status::UNBOUNDED); - TRACE("arith", tout << "Unbounded v" << v << "\n";); has_shared = false; blocker = m.mk_false(); return inf_eps(rational::one(), inf_rational()); diff --git a/src/util/approx_nat.h b/src/util/approx_nat.h index b5e1edb8f..be5fc4fb6 100644 --- a/src/util/approx_nat.h +++ b/src/util/approx_nat.h @@ -21,7 +21,7 @@ Notes: #define APPROX_NAT_H_ #include -#include +#include class approx_nat { unsigned m_value; diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp index f9f0a0797..78b7f15aa 100644 --- a/src/util/bit_vector.cpp +++ b/src/util/bit_vector.cpp @@ -16,7 +16,7 @@ Author: Revision History: --*/ -#include +#include #include "util/bit_vector.h" #include "util/trace.h" diff --git a/src/util/fixed_bit_vector.cpp b/src/util/fixed_bit_vector.cpp index aafc58404..e227aa524 100644 --- a/src/util/fixed_bit_vector.cpp +++ b/src/util/fixed_bit_vector.cpp @@ -19,7 +19,7 @@ Revision History: --*/ -#include +#include #include "util/fixed_bit_vector.h" #include "util/trace.h" #include "util/hash.h" diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 420e48949..55866065e 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -19,9 +19,9 @@ Revision History: #ifndef HASHTABLE_H_ #define HASHTABLE_H_ #include "util/debug.h" -#include +#include #include "util/util.h" -#include +#include #include "util/memory_manager.h" #include "util/hash.h" #include "util/vector.h" diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 041b49389..13ef79a96 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -538,12 +538,16 @@ lp_status lar_solver::maximize_term(unsigned ext_j, if (column_value_is_integer(j)) continue; if (m_int_solver->is_base(j)) { - if (!remove_from_basis(j)) // consider a special version of remove_from_basis that would not remove inf_int columns + if (!remove_from_basis(j)) { // consider a special version of remove_from_basis that would not remove inf_int columns + m_mpq_lar_core_solver.m_r_x = backup; return lp_status::FEASIBLE; // it should not happen + } } m_int_solver->patch_nbasic_column(j, false); - if (!column_value_is_integer(j)) + if (!column_value_is_integer(j)) { + m_mpq_lar_core_solver.m_r_x = backup; return lp_status::FEASIBLE; + } change = true; } if (change) { diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 59a6cb009..0a1d360c8 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -6,7 +6,7 @@ Copyright (c) 2015 Microsoft Corporation #include #include -#include +#include #include "util/trace.h" #include "util/memory_manager.h" #include "util/error_codes.h" diff --git a/src/util/mpz.h b/src/util/mpz.h index 187532a87..65f89f078 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -19,7 +19,6 @@ Revision History: #ifndef MPZ_H_ #define MPZ_H_ -#include #include #include "util/util.h" #include "util/small_object_allocator.h" diff --git a/src/util/nat_set.h b/src/util/nat_set.h index 6e9ab1b6d..f2f2cb8e1 100644 --- a/src/util/nat_set.h +++ b/src/util/nat_set.h @@ -19,7 +19,7 @@ Revision History: #ifndef NAT_SET_H_ #define NAT_SET_H_ -#include +#include #include "util/vector.h" class nat_set { diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 56d40c47a..8078c46ee 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -50,7 +50,7 @@ Revision History: #undef max #endif #include "util/util.h" -#include +#include #include "util/z3_omp.h" struct scoped_timer::imp { diff --git a/src/util/symbol.h b/src/util/symbol.h index 88e825551..40844cf3b 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -19,7 +19,7 @@ Revision History: #ifndef SYMBOL_H_ #define SYMBOL_H_ #include -#include +#include #include "util/util.h" #include "util/tptr.h"