mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
ae5e39a8b8
20 changed files with 282 additions and 86 deletions
|
|
@ -6054,6 +6054,24 @@ class Solver(Z3PPObject):
|
|||
"""
|
||||
Z3_solver_pop(self.ctx.ref(), self.solver, num)
|
||||
|
||||
def num_scopes(self):
|
||||
"""Return the current number of backtracking points.
|
||||
|
||||
>>> s = Solver()
|
||||
>>> s.num_scopes()
|
||||
0L
|
||||
>>> s.push()
|
||||
>>> s.num_scopes()
|
||||
1L
|
||||
>>> s.push()
|
||||
>>> s.num_scopes()
|
||||
2L
|
||||
>>> s.pop()
|
||||
>>> s.num_scopes()
|
||||
1L
|
||||
"""
|
||||
return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
|
||||
|
||||
def reset(self):
|
||||
"""Remove all asserted constraints and backtracking points created using `push()`.
|
||||
|
||||
|
|
|
|||
|
|
@ -421,7 +421,7 @@ typedef enum
|
|||
It has the same semantics as Z3_OP_BUREM, but created in a context where the second operand can be assumed to be non-zero.
|
||||
|
||||
- Z3_OP_BSMOD_I: Binary signed modulus.
|
||||
It has the same semantics as Z3_OP_BSMOND, but created in a context where the second operand can be assumed to be non-zero.
|
||||
It has the same semantics as Z3_OP_BSMOD, but created in a context where the second operand can be assumed to be non-zero.
|
||||
|
||||
- Z3_OP_PR_UNDEF: Undef/Null proof object.
|
||||
|
||||
|
|
|
|||
|
|
@ -732,7 +732,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
|
|||
op_names.push_back(builtin_name("bvudiv_i", OP_BUDIV_I));
|
||||
op_names.push_back(builtin_name("bvsrem_i", OP_BSREM_I));
|
||||
op_names.push_back(builtin_name("bvurem_i", OP_BUREM_I));
|
||||
op_names.push_back(builtin_name("bvumod_i", OP_BSMOD_I));
|
||||
op_names.push_back(builtin_name("bvsmod_i", OP_BSMOD_I));
|
||||
|
||||
op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT));
|
||||
op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT));
|
||||
|
|
|
|||
|
|
@ -1632,8 +1632,6 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
res_exp = e_exp;
|
||||
|
||||
// Result could overflow into 4.xxx ...
|
||||
|
||||
family_id bvfid = m_bv_util.get_fid();
|
||||
expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
|
||||
expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m);
|
||||
|
|
@ -1646,11 +1644,34 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
|
||||
res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
|
||||
|
||||
// Result could have overflown into 4.xxx.
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs) == 2 * sbits + 2);
|
||||
expr_ref ovfl_into_4(m);
|
||||
ovfl_into_4 = m.mk_eq(m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits, sig_abs),
|
||||
m_bv_util.mk_numeral(1, 2));
|
||||
dbg_decouple("fpa2bv_fma_ovfl_into_4", ovfl_into_4);
|
||||
if (sbits > 5) {
|
||||
sticky_raw = m_bv_util.mk_extract(sbits - 5, 0, sig_abs);
|
||||
sticky = m_bv_util.mk_zero_extend(sbits + 3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()));
|
||||
expr * res_or_args[2] = { m_bv_util.mk_extract(2 * sbits - 1, sbits - 4, sig_abs), sticky };
|
||||
res_sig = m_bv_util.mk_bv_or(2, res_or_args);
|
||||
expr_ref sticky_raw(m), sig_upper(m), sticky_redd(m), res_sig_norm(m);
|
||||
sticky_raw = m_bv_util.mk_extract(sbits - 4, 0, sig_abs);
|
||||
sig_upper = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_upper) == sbits + 4);
|
||||
sticky_redd = m.mk_app(bvfid, OP_BREDOR, sticky_raw.get());
|
||||
sticky = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd);
|
||||
expr * res_or_args[2] = { sig_upper, sticky };
|
||||
res_sig_norm = m_bv_util.mk_bv_or(2, res_or_args);
|
||||
|
||||
expr_ref sticky_raw_ovfl(m), sig_upper_ovfl(m), sticky_redd_ovfl(m), sticky_ovfl(m), res_sig_ovfl(m);
|
||||
sticky_raw_ovfl = m_bv_util.mk_extract(sbits - 4, 0, sig_abs);
|
||||
sig_upper_ovfl = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_upper_ovfl) == sbits + 4);
|
||||
sticky_redd_ovfl = m.mk_app(bvfid, OP_BREDOR, sticky_raw_ovfl.get());
|
||||
sticky_ovfl = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd_ovfl);
|
||||
expr * res_or_args_ovfl[2] = { sig_upper_ovfl, sticky_ovfl };
|
||||
res_sig_ovfl = m_bv_util.mk_bv_or(2, res_or_args_ovfl);
|
||||
|
||||
res_sig = m.mk_ite(ovfl_into_4, res_sig_ovfl, res_sig_norm);
|
||||
res_exp = m.mk_ite(ovfl_into_4, m_bv_util.mk_bv_add(res_exp, m_bv_util.mk_numeral(1, ebits+2)),
|
||||
res_exp);
|
||||
}
|
||||
else {
|
||||
unsigned too_short = 6 - sbits;
|
||||
|
|
@ -1658,6 +1679,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
res_sig = m_bv_util.mk_extract(sbits + 3, 0, sig_abs);
|
||||
}
|
||||
dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky);
|
||||
dbg_decouple("fpa2bv_fma_sig_abs", sig_abs);
|
||||
dbg_decouple("fpa2bv_fma_res_sig", res_sig);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
|
||||
|
||||
expr_ref is_zero_sig(m), nil_sbits4(m);
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ namespace sat {
|
|||
void model_converter::reset() {
|
||||
m_entries.finalize();
|
||||
}
|
||||
|
||||
|
||||
void model_converter::operator()(model & m) const {
|
||||
vector<entry>::const_iterator begin = m_entries.begin();
|
||||
vector<entry>::const_iterator it = m_entries.end();
|
||||
|
|
@ -46,7 +46,7 @@ namespace sat {
|
|||
literal_vector::const_iterator it2 = it->m_clauses.begin();
|
||||
literal_vector::const_iterator end2 = it->m_clauses.end();
|
||||
for (; it2 != end2; ++it2) {
|
||||
literal l = *it2;
|
||||
literal l = *it2;
|
||||
if (l == null_literal) {
|
||||
// end of clause
|
||||
if (!sat) {
|
||||
|
|
@ -56,6 +56,7 @@ namespace sat {
|
|||
sat = false;
|
||||
continue;
|
||||
}
|
||||
|
||||
if (sat)
|
||||
continue;
|
||||
bool sign = l.sign();
|
||||
|
|
@ -125,7 +126,7 @@ namespace sat {
|
|||
}
|
||||
return ok;
|
||||
}
|
||||
|
||||
|
||||
model_converter::entry & model_converter::mk(kind k, bool_var v) {
|
||||
m_entries.push_back(entry(k, v));
|
||||
entry & e = m_entries.back();
|
||||
|
|
@ -218,7 +219,7 @@ namespace sat {
|
|||
out << *it2;
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
}
|
||||
out << ")\n";
|
||||
}
|
||||
|
||||
|
|
@ -237,4 +238,22 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
unsigned model_converter::max_var(unsigned min) const {
|
||||
unsigned result = min;
|
||||
vector<entry>::const_iterator it = m_entries.begin();
|
||||
vector<entry>::const_iterator end = m_entries.end();
|
||||
for (; it != end; ++it) {
|
||||
literal_vector::const_iterator lvit = it->m_clauses.begin();
|
||||
literal_vector::const_iterator lvend = it->m_clauses.end();
|
||||
for (; lvit != lvend; ++lvit) {
|
||||
literal l = *lvit;
|
||||
if (l != null_literal) {
|
||||
if (l.var() > result)
|
||||
result = l.var();
|
||||
}
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ namespace sat {
|
|||
\brief Stores eliminated variables and Blocked clauses.
|
||||
It uses these clauses to extend/patch the model produced for the
|
||||
simplified CNF formula.
|
||||
|
||||
|
||||
This information may also be used to support incremental solving.
|
||||
If new clauses are asserted into the SAT engine, then we can
|
||||
restore the state by re-asserting all clauses in the model
|
||||
|
|
@ -50,7 +50,7 @@ namespace sat {
|
|||
m_kind(src.m_kind),
|
||||
m_clauses(src.m_clauses) {
|
||||
}
|
||||
bool_var var() const { return m_var; }
|
||||
bool_var var() const { return m_var; }
|
||||
kind get_kind() const { return static_cast<kind>(m_kind); }
|
||||
};
|
||||
private:
|
||||
|
|
@ -74,8 +74,9 @@ namespace sat {
|
|||
|
||||
void copy(model_converter const & src);
|
||||
void collect_vars(bool_var_set & s) const;
|
||||
unsigned max_var(unsigned min) const;
|
||||
};
|
||||
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -2628,7 +2628,7 @@ namespace sat {
|
|||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < clauses.size(); ++i) {
|
||||
clause & c = *(clauses[i]);
|
||||
if (c.contains(lit)) {
|
||||
if (c.contains(lit) || c.contains(~lit)) {
|
||||
detach_clause(c);
|
||||
del_clause(c);
|
||||
}
|
||||
|
|
@ -2684,6 +2684,7 @@ namespace sat {
|
|||
w = max_var(m_clauses, w);
|
||||
w = max_var(true, w);
|
||||
w = max_var(false, w);
|
||||
v = m_mc.max_var(w);
|
||||
for (unsigned i = 0; i < m_trail.size(); ++i) {
|
||||
if (m_trail[i].var() > w) w = m_trail[i].var();
|
||||
}
|
||||
|
|
@ -3150,9 +3151,9 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// Algorithm 7: Corebased Algorithm with Chunking
|
||||
|
||||
|
||||
static void back_remove(sat::literal_vector& lits, sat::literal l) {
|
||||
for (unsigned i = lits.size(); i > 0; ) {
|
||||
--i;
|
||||
|
|
@ -3176,7 +3177,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
|
||||
sat::literal_vector lambda;
|
||||
for (unsigned i = 0; i < vars.size(); i++) {
|
||||
|
|
@ -3375,7 +3376,7 @@ namespace sat {
|
|||
if (check_inconsistent()) return l_false;
|
||||
|
||||
unsigned num_iterations = 0;
|
||||
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
|
||||
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
|
||||
update_unfixed_literals(unfixed_lits, unfixed_vars);
|
||||
while (!unfixed_lits.empty()) {
|
||||
if (scope_lvl() > 1) {
|
||||
|
|
@ -3390,7 +3391,7 @@ namespace sat {
|
|||
unsigned num_assigned = 0;
|
||||
lbool is_sat = l_true;
|
||||
for (; it != end; ++it) {
|
||||
literal lit = *it;
|
||||
literal lit = *it;
|
||||
if (value(lit) != l_undef) {
|
||||
++num_fixed;
|
||||
if (lvl(lit) <= 1 && value(lit) == l_true) {
|
||||
|
|
@ -3445,8 +3446,8 @@ namespace sat {
|
|||
<< " iterations: " << num_iterations
|
||||
<< " variables: " << unfixed_lits.size()
|
||||
<< " fixed: " << conseq.size()
|
||||
<< " status: " << is_sat
|
||||
<< " pre-assigned: " << num_fixed
|
||||
<< " status: " << is_sat
|
||||
<< " pre-assigned: " << num_fixed
|
||||
<< " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size()
|
||||
<< ")\n";);
|
||||
|
||||
|
|
|
|||
|
|
@ -131,7 +131,7 @@ public:
|
|||
}
|
||||
|
||||
bool is_literal(expr* e) const {
|
||||
return
|
||||
return
|
||||
is_uninterp_const(e) ||
|
||||
(m.is_not(e, e) && is_uninterp_const(e));
|
||||
}
|
||||
|
|
@ -153,7 +153,7 @@ public:
|
|||
asm2fml.insert(assumptions[i], assumptions[i]);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
TRACE("sat", tout << _assumptions << "\n";);
|
||||
dep2asm_t dep2asm;
|
||||
m_model = 0;
|
||||
|
|
@ -163,7 +163,7 @@ public:
|
|||
if (r != l_true) return r;
|
||||
|
||||
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
|
||||
|
||||
|
||||
switch (r) {
|
||||
case l_true:
|
||||
if (sz > 0) {
|
||||
|
|
@ -280,14 +280,14 @@ public:
|
|||
return r;
|
||||
}
|
||||
|
||||
// build map from bound variables to
|
||||
// build map from bound variables to
|
||||
// the consequences that cover them.
|
||||
u_map<unsigned> bool_var2conseq;
|
||||
for (unsigned i = 0; i < lconseq.size(); ++i) {
|
||||
TRACE("sat", tout << lconseq[i] << "\n";);
|
||||
bool_var2conseq.insert(lconseq[i][0].var(), i);
|
||||
}
|
||||
|
||||
|
||||
// extract original fixed variables
|
||||
u_map<expr*> asm2dep;
|
||||
extract_asm2dep(dep2asm, asm2dep);
|
||||
|
|
@ -441,7 +441,7 @@ private:
|
|||
|
||||
lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) {
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
internalize_var(vars[i], bvars);
|
||||
internalize_var(vars[i], bvars);
|
||||
}
|
||||
return l_true;
|
||||
}
|
||||
|
|
@ -453,7 +453,7 @@ private:
|
|||
bool internalized = false;
|
||||
if (is_uninterp_const(v) && m.is_bool(v)) {
|
||||
sat::bool_var b = m_map.to_bool_var(v);
|
||||
|
||||
|
||||
if (b != sat::null_bool_var) {
|
||||
bvars.push_back(b);
|
||||
internalized = true;
|
||||
|
|
@ -479,7 +479,7 @@ private:
|
|||
else if (is_uninterp_const(v) && bvutil.is_bv(v)) {
|
||||
// variable does not occur in assertions, so is unconstrained.
|
||||
}
|
||||
CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";);
|
||||
CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";);
|
||||
return internalized;
|
||||
}
|
||||
|
||||
|
|
@ -506,7 +506,7 @@ private:
|
|||
}
|
||||
expr_ref val(m);
|
||||
expr_ref_vector conj(m);
|
||||
internalize_value(value, v, val);
|
||||
internalize_value(value, v, val);
|
||||
while (!premises.empty()) {
|
||||
expr* e = 0;
|
||||
VERIFY(asm2dep.find(premises.pop().index(), e));
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cache
|
|||
return false;
|
||||
if (k1->m_num_bindings != k2->m_num_bindings)
|
||||
return false;
|
||||
for (unsigned i = 0; i < k1->m_num_bindings; i++)
|
||||
for (unsigned i = 0; i < k1->m_num_bindings; i++)
|
||||
if (k1->m_bindings[i] != k2->m_bindings[i])
|
||||
return false;
|
||||
return true;
|
||||
|
|
@ -49,9 +49,9 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e
|
|||
|
||||
new_key->m_qa = qa;
|
||||
new_key->m_num_bindings = num_bindings;
|
||||
for (unsigned i = 0; i < num_bindings; i++)
|
||||
for (unsigned i = 0; i < num_bindings; i++)
|
||||
new_key->m_bindings[i] = bindings[i]->get_owner();
|
||||
|
||||
|
||||
instances::entry * entry = m_instances.insert_if_not_there2(new_key, 0);
|
||||
if (entry->get_data().m_key != new_key) {
|
||||
SASSERT(entry->get_data().m_value != 0);
|
||||
|
|
@ -60,20 +60,27 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e
|
|||
result = entry->get_data().m_value;
|
||||
return;
|
||||
}
|
||||
|
||||
m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result);
|
||||
|
||||
SASSERT(entry->get_data().m_value == 0);
|
||||
try {
|
||||
m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result);
|
||||
}
|
||||
catch (...) {
|
||||
// CMW: The var_subst reducer was interrupted and m_instances is
|
||||
// in an inconsistent state; we need to remove (new_key, 0).
|
||||
m_instances.remove(new_key);
|
||||
throw; // Throw on to smt::qi_queue/smt::solver.
|
||||
}
|
||||
|
||||
// cache result
|
||||
entry->get_data().m_value = result;
|
||||
|
||||
// remove key from cache
|
||||
m_new_keys[num_bindings] = 0;
|
||||
|
||||
|
||||
// increment reference counters
|
||||
m_refs.push_back(qa);
|
||||
for (unsigned i = 0; i < new_key->m_num_bindings; i++)
|
||||
m_refs.push_back(new_key->m_bindings[i]);
|
||||
m_refs.push_back(result);
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -41,7 +41,7 @@ namespace smt {
|
|||
init_parser_vars();
|
||||
m_vals.resize(15, 0.0f);
|
||||
}
|
||||
|
||||
|
||||
qi_queue::~qi_queue() {
|
||||
}
|
||||
|
||||
|
|
@ -50,7 +50,7 @@ namespace smt {
|
|||
if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) {
|
||||
// it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided.
|
||||
// throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str());
|
||||
|
||||
|
||||
// using warning message instead
|
||||
warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str());
|
||||
// Trying again with default function
|
||||
|
|
@ -107,7 +107,7 @@ namespace smt {
|
|||
m_vals[SIZE] = static_cast<float>(stat->get_size());
|
||||
m_vals[DEPTH] = static_cast<float>(stat->get_depth());
|
||||
m_vals[GENERATION] = static_cast<float>(generation);
|
||||
m_vals[QUANT_GENERATION] = static_cast<float>(stat->get_generation());
|
||||
m_vals[QUANT_GENERATION] = static_cast<float>(stat->get_generation());
|
||||
m_vals[WEIGHT] = static_cast<float>(q->get_weight());
|
||||
m_vals[VARS] = static_cast<float>(q->get_num_decls());
|
||||
m_vals[PATTERN_WIDTH] = pat ? static_cast<float>(pat->get_num_args()) : 1.0f;
|
||||
|
|
@ -118,7 +118,7 @@ namespace smt {
|
|||
TRACE("qi_queue_detail", for (unsigned i = 0; i < m_vals.size(); i++) { tout << m_vals[i] << " "; } tout << "\n";);
|
||||
return stat;
|
||||
}
|
||||
|
||||
|
||||
float qi_queue::get_cost(quantifier * q, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) {
|
||||
quantifier_stat * stat = set_values(q, pat, generation, min_top_generation, max_top_generation, 0);
|
||||
float r = m_evaluator(m_cost_function, m_vals.size(), m_vals.c_ptr());
|
||||
|
|
@ -132,11 +132,11 @@ namespace smt {
|
|||
float r = m_evaluator(m_new_gen_function, m_vals.size(), m_vals.c_ptr());
|
||||
return static_cast<unsigned>(r);
|
||||
}
|
||||
|
||||
|
||||
void qi_queue::insert(fingerprint * f, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) {
|
||||
quantifier * q = static_cast<quantifier*>(f->get_data());
|
||||
float cost = get_cost(q, pat, generation, min_top_generation, max_top_generation);
|
||||
TRACE("qi_queue_detail",
|
||||
TRACE("qi_queue_detail",
|
||||
tout << "new instance of " << q->get_qid() << ", weight " << q->get_weight()
|
||||
<< ", generation: " << generation << ", scope_level: " << m_context.get_scope_level() << ", cost: " << cost << "\n";
|
||||
for (unsigned i = 0; i < f->get_num_args(); i++) {
|
||||
|
|
@ -157,7 +157,7 @@ namespace smt {
|
|||
quantifier * qa = static_cast<quantifier*>(f->get_data());
|
||||
|
||||
if (curr.m_cost <= m_eager_cost_threshold) {
|
||||
instantiate(curr);
|
||||
instantiate(curr);
|
||||
}
|
||||
else if (m_params.m_qi_promote_unsat && m_checker.is_unsat(qa->get_expr(), f->get_num_args(), f->get_args())) {
|
||||
// do not delay instances that produce a conflict.
|
||||
|
|
@ -193,7 +193,7 @@ namespace smt {
|
|||
// This nasty side-effect may change the behavior of Z3.
|
||||
m_manager.trace_stream() << " #" << bindings[i]->get_owner_id();
|
||||
}
|
||||
|
||||
|
||||
#endif
|
||||
if (m_manager.proofs_enabled())
|
||||
m_manager.trace_stream() << " #" << proof_id;
|
||||
|
|
@ -233,7 +233,7 @@ namespace smt {
|
|||
if (m_manager.is_true(s_instance)) {
|
||||
TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager););
|
||||
|
||||
if (m_manager.has_trace_stream())
|
||||
if (m_manager.has_trace_stream())
|
||||
m_manager.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
return;
|
||||
|
|
@ -278,7 +278,7 @@ namespace smt {
|
|||
pr1 = m_manager.mk_modus_ponens(qi_pr, rw);
|
||||
}
|
||||
else {
|
||||
app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance);
|
||||
app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance);
|
||||
proof * prs[1] = { pr.get() };
|
||||
proof * cg = m_manager.mk_congruence(bare_lemma, bare_s_lemma, 1, prs);
|
||||
proof * rw = m_manager.mk_rewrite(bare_s_lemma, lemma);
|
||||
|
|
@ -331,13 +331,13 @@ namespace smt {
|
|||
s.m_instances_lim = m_instances.size();
|
||||
s.m_instantiated_trail_lim = m_instantiated_trail.size();
|
||||
}
|
||||
|
||||
|
||||
void qi_queue::pop_scope(unsigned num_scopes) {
|
||||
unsigned new_lvl = m_scopes.size() - num_scopes;
|
||||
scope & s = m_scopes[new_lvl];
|
||||
unsigned old_sz = s.m_instantiated_trail_lim;
|
||||
unsigned sz = m_instantiated_trail.size();
|
||||
for (unsigned i = old_sz; i < sz; i++)
|
||||
for (unsigned i = old_sz; i < sz; i++)
|
||||
m_delayed_entries[m_instantiated_trail[i]].m_instantiated = false;
|
||||
m_instantiated_trail.shrink(old_sz);
|
||||
m_delayed_entries.shrink(s.m_delayed_entries_lim);
|
||||
|
|
@ -359,7 +359,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool qi_queue::final_check_eh() {
|
||||
TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold
|
||||
TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold
|
||||
<< ", scope_level: " << m_context.get_scope_level() << "\n";);
|
||||
if (m_params.m_qi_conservative_final_check) {
|
||||
bool init = false;
|
||||
|
|
@ -379,7 +379,7 @@ namespace smt {
|
|||
entry & e = m_delayed_entries[i];
|
||||
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
|
||||
if (!e.m_instantiated && e.m_cost <= min_cost) {
|
||||
TRACE("qi_queue",
|
||||
TRACE("qi_queue",
|
||||
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
|
||||
result = false;
|
||||
m_instantiated_trail.push_back(i);
|
||||
|
|
@ -389,13 +389,13 @@ namespace smt {
|
|||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
bool result = true;
|
||||
for (unsigned i = 0; i < m_delayed_entries.size(); i++) {
|
||||
entry & e = m_delayed_entries[i];
|
||||
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
|
||||
if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) {
|
||||
TRACE("qi_queue",
|
||||
TRACE("qi_queue",
|
||||
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
|
||||
result = false;
|
||||
m_instantiated_trail.push_back(i);
|
||||
|
|
@ -443,7 +443,7 @@ namespace smt {
|
|||
quantifier * qa = *it2;
|
||||
delayed_qa_info info;
|
||||
qa2info.find(qa, info);
|
||||
out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n";
|
||||
out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -482,6 +482,6 @@ namespace smt {
|
|||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -135,7 +135,7 @@ namespace smt {
|
|||
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
|
||||
m_num_instances++;
|
||||
}
|
||||
TRACE("quantifier",
|
||||
TRACE("quantifier",
|
||||
tout << mk_pp(q, m()) << " ";
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
tout << mk_pp(bindings[i]->get_owner(), m()) << " ";
|
||||
|
|
@ -372,7 +372,7 @@ namespace smt {
|
|||
quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh();
|
||||
m_imp->~imp();
|
||||
m_imp = new (m_imp) imp(*this, ctx, p, plugin);
|
||||
plugin->set_manager(*this);
|
||||
plugin->set_manager(*this);
|
||||
}
|
||||
|
||||
void quantifier_manager::display(std::ostream & out) const {
|
||||
|
|
|
|||
|
|
@ -75,7 +75,7 @@ namespace smt {
|
|||
};
|
||||
|
||||
bool model_based() const;
|
||||
bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
|
||||
bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
|
||||
void adjust_model(proto_model * m);
|
||||
check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value);
|
||||
|
||||
|
|
@ -167,7 +167,7 @@ namespace smt {
|
|||
virtual void push() = 0;
|
||||
virtual void pop(unsigned num_scopes) = 0;
|
||||
|
||||
|
||||
|
||||
|
||||
};
|
||||
};
|
||||
|
|
|
|||
|
|
@ -47,10 +47,10 @@ class collect_statistics_tactic : public tactic {
|
|||
|
||||
public:
|
||||
collect_statistics_tactic(ast_manager & m, params_ref const & p) :
|
||||
m(m),
|
||||
m(m),
|
||||
m_params(p) {
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
virtual ~collect_statistics_tactic() {}
|
||||
|
||||
virtual tactic * translate(ast_manager & m_) {
|
||||
|
|
@ -60,21 +60,21 @@ public:
|
|||
virtual void updt_params(params_ref const & p) {
|
||||
m_params = p;
|
||||
}
|
||||
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {}
|
||||
|
||||
virtual void operator()(goal_ref const & g, goal_ref_buffer & result,
|
||||
model_converter_ref & mc, proof_converter_ref & pc,
|
||||
model_converter_ref & mc, proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
mc = 0;
|
||||
tactic_report report("collect-statistics", *g);
|
||||
|
||||
tactic_report report("collect-statistics", *g);
|
||||
|
||||
collect_proc cp(m, m_stats);
|
||||
expr_mark visited;
|
||||
expr_mark visited;
|
||||
const unsigned sz = g->size();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
for_each_expr(cp, visited, g->form(i));
|
||||
|
||||
|
||||
std::cout << "(" << std::endl;
|
||||
stats_type::iterator it = m_stats.begin();
|
||||
stats_type::iterator end = m_stats.end();
|
||||
|
|
@ -84,7 +84,7 @@ public:
|
|||
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
}
|
||||
}
|
||||
|
||||
virtual void cleanup() {}
|
||||
|
||||
|
|
@ -98,11 +98,12 @@ protected:
|
|||
class collect_proc {
|
||||
public:
|
||||
ast_manager & m;
|
||||
stats_type & m_stats;
|
||||
stats_type & m_stats;
|
||||
obj_hashtable<sort> m_seen_sorts;
|
||||
obj_hashtable<func_decl> m_seen_func_decls;
|
||||
unsigned m_qdepth;
|
||||
|
||||
collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s) {}
|
||||
collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s), m_qdepth(0) {}
|
||||
|
||||
void operator()(var * v) {
|
||||
m_stats["bound-variables"]++;
|
||||
|
|
@ -113,7 +114,18 @@ protected:
|
|||
m_stats["quantifiers"]++;
|
||||
SASSERT(is_app(q->get_expr()));
|
||||
app * body = to_app(q->get_expr());
|
||||
if (q->is_forall())
|
||||
m_stats["forall-variables"] += q->get_num_decls();
|
||||
else
|
||||
m_stats["exists-variables"] += q->get_num_decls();
|
||||
m_stats["patterns"] += q->get_num_patterns();
|
||||
m_stats["no-patterns"] += q->get_num_no_patterns();
|
||||
m_qdepth++;
|
||||
if (m_stats.find("max-quantification-depth") == m_stats.end() ||
|
||||
m_stats["max-quantification-depth"] < m_qdepth)
|
||||
m_stats["max-quantification-depth"] = m_qdepth;
|
||||
this->operator()(body);
|
||||
m_qdepth--;
|
||||
}
|
||||
|
||||
void operator()(app * n) {
|
||||
|
|
@ -121,7 +133,7 @@ protected:
|
|||
this->operator()(n->get_decl());
|
||||
}
|
||||
|
||||
void operator()(sort * s) {
|
||||
void operator()(sort * s) {
|
||||
if (m.is_uninterp(s)) {
|
||||
if (!m_seen_sorts.contains(s)) {
|
||||
m_stats["uninterpreted-sorts"]++;
|
||||
|
|
@ -135,7 +147,7 @@ protected:
|
|||
std::stringstream ss;
|
||||
ss << "(declare-sort " << mk_ismt2_pp(s, m, prms) << ")";
|
||||
m_stats[ss.str()]++;
|
||||
|
||||
|
||||
if (s->get_info()->get_num_parameters() > 0) {
|
||||
std::stringstream ssname;
|
||||
ssname << "(declare-sort (_ " << s->get_name() << " *))";
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue