mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

get rid of timeb dependencies, pull request #1040

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-23 12:16:43 -07:00
parent edb164587f
commit 23ff580a67
6 changed files with 88 additions and 110 deletions
Download patch file Download diff file Expand all files Collapse all files

158
src/smt/asserted_formulas.cpp
View file

@ -677,25 +677,25 @@ void asserted_formulas::propagate_booleans() {
cont = false;
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
#define PROCESS() { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
m_simplifier(n, new_n, new_pr); \
m_asserted_formulas.set(i, new_n); \
if (m.proofs_enabled()) { \
new_pr = m.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
if (n != new_n) { \
cont = true; \
modified = true; \
} \
if (m.is_not(new_n)) \
m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \
else \
m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \
#define PROCESS() { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
m_simplifier(n, new_n, new_pr); \
m_asserted_formulas.set(i, new_n); \
if (m.proofs_enabled()) { \
new_pr = m.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
if (n != new_n) { \
cont = true; \
modified = true; \
} \
if (m.is_not(new_n)) \
m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \
else \
m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \
}
for (; i < sz; i++) {
PROCESS();
@ -715,43 +715,43 @@ void asserted_formulas::propagate_booleans() {
}
#define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \
bool asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
FUNCTOR; \
bool changed = false; \
expr_ref_vector new_exprs(m); \
proof_ref_vector new_prs(m); \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
functor(n, new_n, new_pr); \
if (n == new_n.get()) { \
push_assertion(n, pr, new_exprs, new_prs); \
} \
else if (m.proofs_enabled()) { \
changed = true; \
if (!new_pr) new_pr = m.mk_rewrite(n, new_n); \
new_pr = m.mk_modus_ponens(pr, new_pr); \
push_assertion(new_n, new_pr, new_exprs, new_prs); \
} \
else { \
changed = true; \
push_assertion(new_n, 0, new_exprs, new_prs); \
} \
} \
swap_asserted_formulas(new_exprs, new_prs); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
if (changed && REDUCE) { \
reduce_and_solve(); \
bool asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
} \
return changed; \
}
FUNCTOR; \
bool changed = false; \
expr_ref_vector new_exprs(m); \
proof_ref_vector new_prs(m); \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
functor(n, new_n, new_pr); \
if (n == new_n.get()) { \
push_assertion(n, pr, new_exprs, new_prs); \
} \
else if (m.proofs_enabled()) { \
changed = true; \
if (!new_pr) new_pr = m.mk_rewrite(n, new_n); \
new_pr = m.mk_modus_ponens(pr, new_pr); \
push_assertion(new_n, new_pr, new_exprs, new_prs); \
} \
else { \
changed = true; \
push_assertion(new_n, 0, new_exprs, new_prs); \
} \
} \
swap_asserted_formulas(new_exprs, new_prs); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
if (changed && REDUCE) { \
reduce_and_solve(); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
} \
return changed; \
}
MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false);
@ -803,30 +803,30 @@ MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m), "elim_bo
MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true);
#define LIFT_ITE(NAME, FUNCTOR, MSG) \
void asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE("lift_ite", display(tout);); \
FUNCTOR; \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
functor(n, new_n, new_pr); \
TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \
IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \
m_asserted_formulas.set(i, new_n); \
if (m.proofs_enabled()) { \
new_pr = m.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
} \
TRACE("lift_ite", display(tout);); \
reduce_and_solve(); \
}
#define LIFT_ITE(NAME, FUNCTOR, MSG) \
void asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE("lift_ite", display(tout);); \
FUNCTOR; \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
functor(n, new_n, new_pr); \
TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \
IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \
m_asserted_formulas.set(i, new_n); \
if (m.proofs_enabled()) { \
new_pr = m.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
} \
TRACE("lift_ite", display(tout);); \
reduce_and_solve(); \
}
LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite");
LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite");

4
src/util/lp/lp_primal_simplex.h
View file

@ -55,10 +55,6 @@ public:
void set_core_solver_bounds();
void update_time_limit_from_starting_time(int start_time) {
this->m_settings.time_limit -= (get_millisecond_span(start_time) / 1000.);
}
void find_maximal_solution();
void fill_A_x_and_basis_for_stage_one_total_inf();

2
src/util/lp/lp_primal_simplex.hpp
View file

@ -152,7 +152,6 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::set_core_solver_
template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_solution() {
int preprocessing_start_time = get_millisecond_count();
if (this->problem_is_empty()) {
this->m_status = lp_status::EMPTY;
return;
@ -169,7 +168,6 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_sol
fill_acceptable_values_for_x();
this->count_slacks_and_artificials();
set_core_solver_bounds();
update_time_limit_from_starting_time(preprocessing_start_time);
solve_with_total_inf();
}

15
src/util/lp/lp_settings.h
View file

@ -8,9 +8,9 @@
#include <string>
#include <algorithm>
#include <limits>
#include <sys/timeb.h>
#include <iomanip>
#include "util/lp/lp_utils.h"
#include "util/stopwatch.h"
namespace lean {
typedef unsigned var_index;
@ -69,10 +69,6 @@ enum non_basic_column_value_position { at_low_bound, at_upper_bound, at_fixed, f
template <typename X> bool is_epsilon_small(const X & v, const double& eps); // forward definition
int get_millisecond_count();
int get_millisecond_span(int start_time);
class lp_resource_limit {
public:
virtual bool get_cancel_flag() = 0;
@ -92,12 +88,13 @@ struct lp_settings {
private:
class default_lp_resource_limit : public lp_resource_limit {
lp_settings& m_settings;
int m_start_time;
stopwatch m_sw;
public:
default_lp_resource_limit(lp_settings& s): m_settings(s), m_start_time(get_millisecond_count()) {}
default_lp_resource_limit(lp_settings& s): m_settings(s) {
m_sw.start();
}
virtual bool get_cancel_flag() {
int span_in_mills = get_millisecond_span(m_start_time);
return (span_in_mills / 1000.0 > m_settings.time_limit);
return (m_sw.get_current_seconds() > m_settings.time_limit);
}
};

13
src/util/lp/lp_settings.hpp
View file

@ -52,19 +52,6 @@ lp_status lp_status_from_string(std::string status) {
lean_unreachable();
return lp_status::UNKNOWN; // it is unreachable
}
int get_millisecond_count() {
timeb tb;
ftime(&tb);
return tb.millitm + (tb.time & 0xfffff) * 1000;
}
int get_millisecond_span(int start_time) {
int span = get_millisecond_count() - start_time;
if (span < 0)
span += 0x100000 * 1000;
return span;
}
template <typename T>

6
src/util/lp/sparse_matrix.hpp
View file

@ -1050,8 +1050,8 @@ bool sparse_matrix<T, X>::get_pivot_for_column(unsigned &i, unsigned &j, int c_p
if (i_inv < k) continue;
unsigned j_inv = adjust_column_inverse(j);
if (j_inv < k) continue;
int small = elem_is_too_small(i, j, c_partial_pivoting);
if (!small) {
int _small = elem_is_too_small(i, j, c_partial_pivoting);
if (!_small) {
#ifdef LEAN_DEBUG
// if (!really_best_pivot(i, j, c_partial_pivoting, k)) {
// print_active_matrix(k);
@ -1063,7 +1063,7 @@ bool sparse_matrix<T, X>::get_pivot_for_column(unsigned &i, unsigned &j, int c_p
j = j_inv;
return true;
}
if (small != 2) { // 2 means that the pair is not in the matrix
if (_small != 2) { // 2 means that the pair is not in the matrix
pivots_candidates_that_are_too_small.push_back(std::make_pair(i, j));
}
}