mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Small modifs in ackermannization.

Browse source
This commit is contained in:
Mikolas Janota 2016-01-29 16:43:18 +00:00
parent 2ce7dc68ad
commit 470b5c20fe
3 changed files with 12 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/tactic/ackr/ackr_bound_probe.cpp
View file

@ -16,6 +16,7 @@
--*/ --*/
#include"ackr_helper.h" #include"ackr_helper.h"
#include"ackr_bound_probe.h" #include"ackr_bound_probe.h"
#include"ast_smt2_pp.h"
/** \brief /** \brief
* For each function f, calculate the number of its occurrences o_f and compute "o_f choose 2". * For each function f, calculate the number of its occurrences o_f and compute "o_f choose 2".
@ -66,7 +67,13 @@ public:
proc::fun2terms_map::iterator it = p.m_fun2terms.begin(); proc::fun2terms_map::iterator it = p.m_fun2terms.begin();
proc::fun2terms_map::iterator end = p.m_fun2terms.end(); proc::fun2terms_map::iterator end = p.m_fun2terms.end();
unsigned total = 0; unsigned total = 0;
for (; it != end; ++it) total += n_choose_2(it->m_value->size()); for (; it != end; ++it) {
const unsigned fsz = it->m_value->size();
const unsigned n2 = n_choose_2(fsz);
TRACE("ackr_bound_probe", tout << mk_ismt2_pp(it->m_key, g.m(), 0) << " #" << fsz << " n_choose_2=" << n2 << std::endl;);
total += n2;
}
TRACE("ackr_bound_probe", tout << "total=" << total << std::endl;);
return result(total); return result(total);
} }

12
src/tactic/ackr/lackr_model_constructor.cpp
View file

@ -190,17 +190,7 @@ struct lackr_model_constructor::imp {
return true; return true;
} }
inline bool is_val(expr * e) { inline bool is_val(expr * e) { return m_m.is_value(e); }
if (!is_app(e)) return false;
return is_val(to_app(e));
}
inline bool is_val(app * a) {
const family_id fid = a->get_decl()->get_family_id();
const bool rv = fid != null_family_id && a->get_num_args() == 0;
SASSERT(rv == (m_bv_rw.is_numeral(a) || m_m.is_true(a) || m_m.is_false(a)));
return rv;
}
inline bool eval_cached(app * a, expr *& val) { inline bool eval_cached(app * a, expr *& val) {
if (is_val(a)) { val = a; return true; } if (is_val(a)) { val = a; return true; }

4
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -33,6 +33,8 @@ Notes:
#define MEMLIMIT 300 #define MEMLIMIT 300
#define ACKRLIMIT 1000
tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
params_ref solve_eq_p; params_ref solve_eq_p;
@ -69,7 +71,7 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
// //
using_params(mk_simplify_tactic(m), hoist_p), using_params(mk_simplify_tactic(m), hoist_p),
mk_max_bv_sharing_tactic(m), mk_max_bv_sharing_tactic(m),
when(mk_lt(mk_ackr_bound_probe(), mk_const_probe(static_cast<double>(100))), mk_ackermannize_tactic(m,p)) when(mk_lt(mk_ackr_bound_probe(), mk_const_probe(static_cast<double>(ACKRLIMIT))), mk_ackermannize_tactic(m,p))
); );
} }