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

env params

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-01 20:56:40 -08:00
parent 9bd4fd969a
commit 02e763bb6b
15 changed files with 133 additions and 80 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/smt/asserted_formulas.cpp
View file

@ -248,7 +248,6 @@ void asserted_formulas::reduce() {
if (m_macro_manager.has_macros())
expand_macros();
TRACE("before_reduce", display(tout););
IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";);
CASSERT("well_sorted", check_well_sorted());
#define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); } TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return; }
@ -280,7 +279,7 @@ void asserted_formulas::reduce() {
CASSERT("well_sorted",check_well_sorted());
IF_VERBOSE(10, verbose_stream() << "simplifier done.\n";);
IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done)\n";);
TRACE("after_reduce", display(tout););
TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
TRACE("macros", m_macro_manager.display(tout););
@ -288,7 +287,7 @@ void asserted_formulas::reduce() {
}
void asserted_formulas::eliminate_and() {
IF_IVERBOSE(10, verbose_stream() << "eliminating and...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-and)\n";);
set_eliminate_and(true);
reduce_asserted_formulas();
TRACE("after_elim_and", display(tout););
@ -393,19 +392,19 @@ void asserted_formulas::find_macros_core() {
}
void asserted_formulas::find_macros() {
IF_IVERBOSE(10, verbose_stream() << "trying to find macros...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.find-macros)\n";);
TRACE("before_find_macros", display(tout););
find_macros_core();
TRACE("after_find_macros", display(tout););
}
void asserted_formulas::expand_macros() {
IF_IVERBOSE(10, verbose_stream() << "expanding macros...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.expand-macros)\n";);
find_macros_core();
}
void asserted_formulas::apply_quasi_macros() {
IF_IVERBOSE(10, verbose_stream() << "finding quasi macros...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";);
TRACE("before_quasi_macros", display(tout););
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
@ -423,7 +422,7 @@ void asserted_formulas::apply_quasi_macros() {
}
void asserted_formulas::nnf_cnf() {
IF_IVERBOSE(10, verbose_stream() << "applying nnf...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.nnf)\n";);
nnf apply_nnf(m_manager, m_defined_names);
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
@ -471,7 +470,7 @@ void asserted_formulas::nnf_cnf() {
#define MK_SIMPLE_SIMPLIFIER(NAME, FUNCTOR_DEF, LABEL, MSG) \
void asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << MSG << "...\n";); \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(LABEL, tout << "before:\n"; display(tout);); \
FUNCTOR_DEF; \
expr_ref_vector new_exprs(m_manager); \
@ -503,16 +502,16 @@ void asserted_formulas::NAME() {
TRACE(LABEL, display(tout);); \
}
MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute forall");
MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute-forall");
void asserted_formulas::reduce_and_solve() {
IF_IVERBOSE(10, verbose_stream() << "reducing...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";);
flush_cache(); // collect garbage
reduce_asserted_formulas();
}
void asserted_formulas::infer_patterns() {
IF_IVERBOSE(10, verbose_stream() << "pattern inference...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";);
TRACE("before_pattern_inference", display(tout););
pattern_inference infer(m_manager, m_params);
expr_ref_vector new_exprs(m_manager);
@ -546,7 +545,7 @@ void asserted_formulas::commit() {
}
void asserted_formulas::eliminate_term_ite() {
IF_IVERBOSE(10, verbose_stream() << "eliminating ite term...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";);
TRACE("before_elim_term_ite", display(tout););
elim_term_ite elim(m_manager, m_defined_names);
expr_ref_vector new_exprs(m_manager);
@ -583,7 +582,7 @@ void asserted_formulas::eliminate_term_ite() {
}
void asserted_formulas::propagate_values() {
IF_IVERBOSE(10, verbose_stream() << "constant propagation...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.constant-propagation)\n";);
TRACE("propagate_values", tout << "before:\n"; display(tout););
flush_cache();
bool found = false;
@ -661,7 +660,7 @@ void asserted_formulas::propagate_booleans() {
flush_cache();
while (cont) {
TRACE("propagate_booleans", tout << "before:\n"; display(tout););
IF_IVERBOSE(10, verbose_stream() << "boolean propagation...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.propagate-booleans)\n";);
cont = false;
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
@ -704,7 +703,7 @@ void asserted_formulas::propagate_booleans() {
#define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \
bool asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << MSG << "...\n";); \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
FUNCTOR; \
bool changed = false; \
@ -741,9 +740,9 @@ bool asserted_formulas::NAME() { \
return changed; \
}
MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m_manager, m_simplifier), "pull_cheap_ite_trees", "pull cheap ite trees", false);
MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m_manager, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false);
MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m_manager), "pull_nested_quantifiers", "pull nested quantifiers", false);
MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m_manager), "pull_nested_quantifiers", "pull-nested-quantifiers", false);
proof * asserted_formulas::get_inconsistency_proof() const {
if (!inconsistent())
@ -761,7 +760,7 @@ proof * asserted_formulas::get_inconsistency_proof() const {
}
void asserted_formulas::refine_inj_axiom() {
IF_IVERBOSE(10, verbose_stream() << "refining injectivity...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.refine-injectivity)\n";);
TRACE("inj_axiom", display(tout););
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
@ -783,9 +782,9 @@ void asserted_formulas::refine_inj_axiom() {
TRACE("inj_axiom", display(tout););
}
MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate bit-vector over integers", true);
MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate-bit-vector-over-integers", true);
MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap fourier-motzkin", true);
MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap-fourier-motzkin", true);
// MK_SIMPLIFIER(quant_elim, qe::expr_quant_elim_star1 &functor = m_quant_elim,
// "quantifiers", "quantifier elimination procedures", true);
@ -795,11 +794,11 @@ bool asserted_formulas::quant_elim() {
return false;
}
MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate bit-vectors from quantifiers", true);
MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true);
#define LIFT_ITE(NAME, FUNCTOR, MSG) \
void asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << MSG;); \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE("lift_ite", display(tout);); \
FUNCTOR; \
unsigned i = m_asserted_qhead; \
@ -822,8 +821,8 @@ void asserted_formulas::NAME() {
reduce_and_solve(); \
}
LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite...\n");
LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite...\n");
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");
unsigned asserted_formulas::get_total_size() const {
expr_mark visited;
@ -835,7 +834,7 @@ unsigned asserted_formulas::get_total_size() const {
}
void asserted_formulas::max_bv_sharing() {
IF_IVERBOSE(10, verbose_stream() << "maximizing bv sharing...\n";);
IF_IVERBOSE(10, verbose_stream() << "(smt.maximizing-bv-sharing)\n";);
TRACE("bv_sharing", display(tout););
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();

45
src/smt/smt_context.cpp
View file

@ -2488,7 +2488,7 @@ namespace smt {
SASSERT(check_clauses(m_lemmas));
SASSERT(check_clauses(m_aux_clauses));
IF_VERBOSE(2, verbose_stream() << "simplifying clause set... "; verbose_stream().flush(););
IF_VERBOSE(2, verbose_stream() << "(smt.simplifying-clause-set"; verbose_stream().flush(););
// m_simp_counter is used to balance the cost of simplify_clause.
//
@ -2503,8 +2503,7 @@ namespace smt {
// the field m_simp_qhead is used to check whether there are
// new assigned literals at the base level.
m_simp_qhead = m_assigned_literals.size();
unsigned num_clauses = m_aux_clauses.size() + m_lemmas.size();
unsigned num_del_clauses = 0;
SASSERT(m_scope_lvl == m_base_lvl);
@ -2519,7 +2518,7 @@ namespace smt {
num_del_clauses += simplify_clauses(m_lemmas, bs.m_lemmas_lim);
}
TRACE("simp_counter", tout << "simp_counter: " << m_simp_counter << " scope_lvl: " << m_scope_lvl << "\n";);
IF_VERBOSE(2, verbose_stream() << "num. deleted clauses: " << num_del_clauses << " (out of " << num_clauses << ")" << std::endl;);
IF_VERBOSE(2, verbose_stream() << " :num-deleted-clauses " << num_del_clauses << ")" << std::endl;);
TRACE("simplify_clauses_detail", tout << "after:\n"; display_clauses(tout, m_lemmas););
SASSERT(check_clauses(m_lemmas) && check_clauses(m_aux_clauses));
}
@ -2551,7 +2550,7 @@ namespace smt {
SASSERT(start_at <= sz);
if (start_at + m_fparams.m_recent_lemmas_size >= sz)
return;
IF_VERBOSE(2, verbose_stream() << "deleting inactive lemmas... "; verbose_stream().flush(););
IF_VERBOSE(2, verbose_stream() << "(smt.delete-inactive-lemmas"; verbose_stream().flush(););
SASSERT (m_fparams.m_recent_lemmas_size < sz);
unsigned end_at = sz - m_fparams.m_recent_lemmas_size;
SASSERT(start_at < end_at);
@ -2595,7 +2594,7 @@ namespace smt {
cls->set_activity(cls->get_activity() / m_fparams.m_clause_decay);
}
}
IF_VERBOSE(2, verbose_stream() << "num. deleted clauses: " << num_del_cls << " (out of " << sz << ")" << std::endl;);
IF_VERBOSE(2, verbose_stream() << " :num-deleted-clauses " << num_del_cls << ")" << std::endl;);
}
/**
@ -2606,7 +2605,7 @@ namespace smt {
depends on which group the clauses is in.
*/
void context::del_inactive_lemmas2() {
IF_VERBOSE(2, verbose_stream() << "deleting inactive clauses... "; verbose_stream().flush(););
IF_VERBOSE(2, verbose_stream() << "(smt.delete-inactive-clauses "; verbose_stream().flush(););
unsigned sz = m_lemmas.size();
unsigned start_at = m_base_lvl == 0 ? 0 : m_base_scopes[m_base_lvl - 1].m_lemmas_lim;
SASSERT(start_at <= sz);
@ -2645,7 +2644,7 @@ namespace smt {
}
SASSERT(j <= sz);
m_lemmas.shrink(j);
IF_VERBOSE(2, verbose_stream() << "num. deleted clauses: " << num_del_cls << " (out of " << sz << ")" << std::endl;);
IF_VERBOSE(2, verbose_stream() << " :num-deleted-clauses " << num_del_cls << ")" << std::endl;);
}
/**
@ -2786,7 +2785,7 @@ namespace smt {
}
void context::assert_expr(expr * e, proof * pr) {
timeit tt(get_verbosity_level() >= 100, "simplifying");
timeit tt(get_verbosity_level() >= 100, "smt.simplifying");
assert_expr_core(e, pr);
}
@ -2800,7 +2799,7 @@ namespace smt {
void context::internalize_assertions() {
TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
timeit tt(get_verbosity_level() >= 100, "preprocessing");
timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
reduce_assertions();
if (!m_asserted_formulas.inconsistent()) {
unsigned sz = m_asserted_formulas.get_num_formulas();
@ -3158,7 +3157,7 @@ namespace smt {
exit(1);
}
#endif
timeit tt(get_verbosity_level() >= 100, "searching");
timeit tt(get_verbosity_level() >= 100, "smt.stats");
scoped_mk_model smk(*this);
SASSERT(at_search_level());
TRACE("search", display(tout); display_enodes_lbls(tout););
@ -3166,7 +3165,7 @@ namespace smt {
init_search();
flet<bool> l(m_searching, true);
TRACE("after_init_search", display(tout););
IF_VERBOSE(2, verbose_stream() << "searching...\n";);
IF_VERBOSE(2, verbose_stream() << "(smt.searching)\n";);
TRACE("search_lite", tout << "searching...\n";);
lbool status = l_undef;
unsigned curr_lvl = m_scope_lvl;
@ -3215,16 +3214,16 @@ namespace smt {
inc_limits();
if (force_restart || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
SASSERT(!inconsistent());
IF_VERBOSE(1, verbose_stream() << "restarting... propagations: " << m_stats.m_num_propagations
<< ", decisions: " << m_stats.m_num_decisions
<< ", conflicts: " << m_stats.m_num_conflicts << ", restart: " << m_restart_threshold;
IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
<< " :decisions " << m_stats.m_num_decisions
<< " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {
verbose_stream() << ", restart-outer: " << m_restart_outer_threshold;
verbose_stream() << " :restart-outer " << m_restart_outer_threshold;
}
if (m_fparams.m_restart_adaptive) {
verbose_stream() << ", agility: " << m_agility;
verbose_stream() << " :agility " << m_agility;
}
verbose_stream() << std::endl; verbose_stream().flush(););
verbose_stream() << ")" << std::endl; verbose_stream().flush(););
// execute the restart
m_stats.m_num_restarts++;
if (m_scope_lvl > curr_lvl) {
@ -3259,12 +3258,12 @@ namespace smt {
void context::tick(unsigned & counter) const {
counter++;
if (counter > m_fparams.m_tick) {
IF_VERBOSE(3, verbose_stream() << "working...";
verbose_stream() << " num. conflicts: " << m_num_conflicts;
IF_VERBOSE(3, verbose_stream() << "(smt.working";
verbose_stream() << " :conflicts " << m_num_conflicts;
// verbose_stream() << " lemma avg. activity: " << get_lemma_avg_activity();
if (m_fparams.m_restart_adaptive)
verbose_stream() << " agility: " << m_agility;
verbose_stream() << std::endl; verbose_stream().flush(););
verbose_stream() << " :agility " << m_agility;
verbose_stream() << ")" << std::endl; verbose_stream().flush(););
TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout); tout << "\n";);
counter = 0;
}
@ -3410,7 +3409,7 @@ namespace smt {
final_check_status ok;
if (m_final_check_idx < num_th) {
theory * th = m_theory_set[m_final_check_idx];
IF_VERBOSE(100, verbose_stream() << "final check '" << th->get_name() << "' ...\n";);
IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"" << th->get_name() << "\")\n";);
ok = th->final_check_eh();
TRACE("final_check_step", tout << "final check '" << th->get_name() << " ok: " << ok << " inconsistent " << inconsistent() << "\n";);
if (ok == FC_GIVEUP) {

2
src/smt/smt_quantifier.cpp
View file

@ -211,7 +211,7 @@ namespace smt {
final_check_status final_check_eh(bool full) {
if (full) {
IF_VERBOSE(100, verbose_stream() << "final check 'quantifiers'...\n";);
IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
final_check_status result = m_qi_queue.final_check_eh() ? FC_DONE : FC_CONTINUE;
final_check_status presult = m_plugin->final_check_eh(full);
if (presult != FC_DONE)

4
src/smt/smt_setup.cpp
View file

@ -118,7 +118,7 @@ namespace smt {
void setup::setup_auto_config() {
static_features st(m_manager);
IF_VERBOSE(100, verbose_stream() << "configuring...\n";);
IF_VERBOSE(100, verbose_stream() << "(smt.configuring)\n";);
TRACE("setup", tout << "setup, logic: " << m_logic << "\n";);
// HACK: do not collect features for QF_BV and QF_AUFBV... since they do not use them...
if (m_logic == "QF_BV") {
@ -128,7 +128,7 @@ namespace smt {
setup_QF_AUFBV();
}
else {
IF_VERBOSE(100, verbose_stream() << "collecting features...\n";);
IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
if (m_logic == "QF_UF")