mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Typos

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2019-10-24 18:01:22 +01:00
parent efa3c0f68e
commit 1d4f8c0168
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/smt/smt_model_checker.cpp
View file

@ -213,7 +213,7 @@ namespace smt {
return false; // get_some_value failed... giving up return false; // get_some_value failed... giving up
} }
TRACE("model_checker", tout << "Got some value " << sk_value << "\n";); TRACE("model_checker", tout << "Got some value " << sk_value << "\n";);
if (use_inv) { if (use_inv) {
unsigned sk_term_gen; unsigned sk_term_gen;
expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen); expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen);
@ -337,18 +337,18 @@ namespace smt {
flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true); flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
lbool r = m_aux_context->check(); lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";); TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
if (r != l_true) { if (r != l_true) {
return r == l_false; // quantifier is satisfied by m_curr_model return r == l_false; // quantifier is satisfied by m_curr_model
} }
model_ref complete_cex; model_ref complete_cex;
m_aux_context->get_model(complete_cex); m_aux_context->get_model(complete_cex);
// try to find new instances using instantiation sets. // try to find new instances using instantiation sets.
m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks); m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks);
unsigned num_new_instances = 0; unsigned num_new_instances = 0;
while (true) { while (true) {
flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true); flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
lbool r = m_aux_context->check(); lbool r = m_aux_context->check();
@ -400,7 +400,7 @@ namespace smt {
add_instance(q, args, 0, nullptr); add_instance(q, args, 0, nullptr);
return false; return false;
} }
TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";); TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
} }
} }
return true; return true;
@ -501,7 +501,7 @@ namespace smt {
for (quantifier * q : *m_qm) { for (quantifier * q : *m_qm) {
if (m.is_rec_fun_def(q)) { if (m.is_rec_fun_def(q)) {
rec_funs.insert(m.get_rec_fun_decl(q)); rec_funs.insert(m.get_rec_fun_decl(q));
} }
} }
expr_fast_mark1 visited; expr_fast_mark1 visited;
has_rec_fun_proc proc(rec_funs); has_rec_fun_proc proc(rec_funs);
@ -509,21 +509,21 @@ namespace smt {
if (!m.is_rec_fun_def(q)) { if (!m.is_rec_fun_def(q)) {
quick_for_each_expr(proc, visited, q); quick_for_each_expr(proc, visited, q);
if (proc.has_rec_fun()) return true; if (proc.has_rec_fun()) return true;
} }
} }
return false; return false;
} }
// //
// (repeated from defined_names.cpp) // (repeated from defined_names.cpp)
// NB. The pattern for lambdas is incomplete. // NB. The pattern for lambdas is incomplete.
// consider store(a, i, v) == \lambda j . if i = j then v else a[j] // consider store(a, i, v) == \lambda j . if i = j then v else a[j]
// the instantiation rules for store(a, i, v) are: // the instantiation rules for store(a, i, v) are:
// sotre(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] } // sotre(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
// The first pattern is not included. // The first pattern is not included.
// TBD use a model-based scheme for exracting instantiations instead of // TBD use a model-based scheme for extracting instantiations instead of
// using multi-patterns. // using multi-patterns.
// //
void model_checker::check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures) { void model_checker::check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures) {
for (quantifier * q : *m_qm) { for (quantifier * q : *m_qm) {
@ -607,7 +607,7 @@ namespace smt {
if (inst.m_def) { if (inst.m_def) {
m_context->internalize_assertion(inst.m_def, nullptr, gen); m_context->internalize_assertion(inst.m_def, nullptr, gen);
} }
TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n"; TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";
tout << "inconsistent: " << m_context->inconsistent() << "\n"; tout << "inconsistent: " << m_context->inconsistent() << "\n";
tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.c_ptr() + offset) << "\n";); tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.c_ptr() + offset) << "\n";);