mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

build warnings #2748

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-28 15:36:46 -08:00
parent 30d9ea5c2c
commit a257ec0cc1
7 changed files with 66 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/seq_decl_plugin.cpp
View file

@ -1090,6 +1090,7 @@ app* seq_util::str::mk_is_empty(expr* s) const {
sort* seq_util::re::to_seq(sort* re) {
(void)u;
SASSERT(u.is_re(re));
return to_sort(re->get_parameter(0).get_ast());
}

2
src/smt/params/smt_params_helper.pyg
View file

@ -67,7 +67,7 @@ def_module_params(module_name='smt',
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver), \'empty\' (a no-op solver that forces an answer unknown if strings were used), \'none\' (no solver)'),
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'),
('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),
('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'),

2
src/smt/smt_context.cpp
View file

@ -325,7 +325,7 @@ namespace smt {
TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
TRACE("relevancy",
tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";);
tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << " relevancy-lvl: " << relevancy_lvl() << "\n";);
if (d.is_atom() && (relevancy_lvl() == 0 || (relevancy_lvl() == 1 && !d.is_quantifier()) || is_relevant_core(l)))
m_atom_propagation_queue.push_back(l);

8
src/smt/smt_context_inv.cpp
View file

@ -430,6 +430,7 @@ namespace smt {
if (!get_fparams().m_core_validate) {
return;
}
warning_msg("Users should not set smt.core.validate. This option is for debugging only.");
context ctx(get_manager(), get_fparams(), get_params());
ptr_vector<expr> assertions;
get_assertions(assertions);
@ -443,10 +444,13 @@ namespace smt {
}
lbool res = ctx.check();
switch (res) {
case l_false:
case l_false:
break;
default:
case l_true:
throw default_exception("Core could not be validated");
case l_undef:
IF_VERBOSE(1, verbose_stream() << "core validation produced unknown\n");
break;
}
}

7
src/smt/smt_model_finder.cpp
View file

@ -92,8 +92,9 @@ namespace smt {
obj_map<expr, unsigned> const & get_elems() const { return m_elems; }
void insert(expr * n, unsigned generation) {
if (m_elems.contains(n) || contains_model_value(n))
if (m_elems.contains(n) || contains_model_value(n)) {
return;
}
TRACE("model_finder", tout << mk_pp(n, m) << "\n";);
m.inc_ref(n);
m_elems.insert(n, generation);
@ -255,8 +256,8 @@ namespace smt {
void merge(node * other) {
node * r1 = get_root();
node * r2 = other->get_root();
SASSERT(r1->m_set == 0);
SASSERT(r2->m_set == 0);
SASSERT(r1->m_set == nullptr);
SASSERT(r2->m_set == nullptr);
SASSERT(r1->get_sort() == r2->get_sort());
if (r1 == r2)
return;

4
src/smt/theory_str.cpp
View file

@ -7701,11 +7701,11 @@ namespace smt {
lbool theory_str::validate_unsat_core(expr_ref_vector & unsat_core) {
app * target_term = to_app(get_manager().mk_not(m_theoryStrOverlapAssumption_term));
get_context().internalize(target_term, false);
enode* e1 = get_context().get_enode(target_term);
enode* e1 = get_context().get_enode(target_term);
for (unsigned i = 0; i < unsat_core.size(); ++i) {
app * core_term = to_app(unsat_core.get(i));
// not sure if this is the correct way to compare terms in this context
if (!get_context().e_internalized(core_term)) continue;
if (!get_context().e_internalized(core_term)) continue;
enode *e2 = get_context().get_enode(core_term);
if (e1 == e2) {
TRACE("str", tout << "overlap detected in unsat core, changing UNSAT to UNKNOWN" << std::endl;);

69
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -321,6 +321,11 @@ namespace smtfd {
else if (is_uninterp_const(t) && m_butil.is_bv(t)) {
r = t;
}
else if (m.is_model_value(t)) {
int idx = a->get_parameter(0).get_int();
r = m_butil.mk_numeral(rational(idx), 24);
// std::cout << expr_ref(t, m) << " --> " << mk_pp(r, m) << "\n";
}
else {
r = fresh_var(t);
}
@ -797,8 +802,8 @@ namespace smtfd {
v2e.insert(v, t);
}
}
if (m.is_value(t)) {
// std::cout << mk_bounded_pp(t, m, 2) << " " << eval_abs(t) << " " << mk_pp(s, m) << "\n";
if (m.is_model_value(t)) {
//std::cout << "model value: " << mk_bounded_pp(t, m, 2) << " " << eval_abs(t) << " " << mk_pp(s, m) << "\n";
}
}
@ -1342,8 +1347,9 @@ namespace smtfd {
ref<::solver> m_solver;
obj_pair_map<expr, sort, expr*> m_val2term;
expr_ref_vector m_val2term_trail;
obj_map<sort, expr*> m_fresh;
expr_ref_vector m_fresh_trail;
obj_map<sort, obj_hashtable<expr>*> m_fresh;
scoped_ptr_vector<obj_hashtable<expr>> m_values;
expr* abs(expr* e) { return m_context.get_abs().abs(e); }
expr_ref eval_abs(expr* t) { return (*m_model)(abs(t)); }
@ -1358,20 +1364,30 @@ namespace smtfd {
m_solver->assert_expr(fml);
}
expr_ref fresh(sort* s) {
expr* e = nullptr;
if (!m_fresh.find(s, e)) {
e = m.mk_fresh_const(s->get_name(), s, false);
m_fresh.insert(s, e);
void register_value(expr* e) {
sort* s = m.get_sort(e);
obj_hashtable<expr>* values = nullptr;
if (!m_fresh.find(s, values)) {
values = alloc(obj_hashtable<expr>);
m_fresh.insert(s, values);
m_values.push_back(values);
}
if (!values->contains(e)) {
for (expr* b : *values) {
m_context.add(m.mk_not(m.mk_eq(e, b)), __FUNCTION__);
}
values->insert(e);
m_fresh_trail.push_back(e);
}
return expr_ref(e, m);
}
// sort -> [ value -> expr ]
// for fixed value return expr
// new fixed value is distinct from other expr
expr_ref replace_model_value(expr* e) {
if (m.is_model_value(e)) {
expr_ref r = fresh(m.get_sort(e));
std::cout << expr_ref(e, m) << " |-> " << r << "\n";
if (m.is_model_value(e)) {
register_value(e);
expr_ref r(e, m);
return r;
}
if (is_app(e) && to_app(e)->get_num_args() > 0) {
@ -1467,7 +1483,7 @@ namespace smtfd {
else {
body = m.mk_implies(body, q);
}
IF_VERBOSE(1, verbose_stream() << body << "\n");
IF_VERBOSE(10, verbose_stream() << body << "\n");
m_context.add(body, __FUNCTION__);
}
m_solver->pop(1);
@ -1543,7 +1559,7 @@ namespace smtfd {
});
for (expr* c : core) {
lbool r = l_false;
IF_VERBOSE(1, verbose_stream() << "core: " << mk_bounded_pp(c, m, 2) << "\n");
IF_VERBOSE(10, verbose_stream() << "core: " << mk_bounded_pp(c, m, 2) << "\n");
if (is_forall(c)) {
r = check_forall(to_quantifier(c));
}
@ -1742,12 +1758,13 @@ namespace smtfd {
}
}
m_context.populate_model(m_model, terms);
TRACE("smtfd",
tout << "axioms: " << m_axioms << "\n";
for (expr* a : subterms(terms)) {
expr_ref val0 = (*m_model)(a);
expr_ref val1 = (*m_model)(abs(a));
if (val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) {
if (is_ground(a) && val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) {
tout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
}
if (!is_forall(a) && !is_exists(a) && (!m_context.term_covered(a) || !m_context.sort_covered(m.get_sort(a)))) {
@ -1758,6 +1775,18 @@ namespace smtfd {
tout << "has quantifier: " << has_q << "\n" << core << "\n";
tout << *m_model.get() << "\n";
);
for (expr* a : subterms(core)) {
expr_ref val0 = (*m_model)(a);
expr_ref val1 = (*m_model)(abs(a));
if (is_ground(a) && val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) {
std::cout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
std::cout << "core: " << core << "\n";
std::cout << *m_model.get() << "\n";
exit(0);
}
}
if (!has_q) {
return is_decided;
}
@ -1797,6 +1826,9 @@ namespace smtfd {
}
else if (m_model->is_true(a)) {
//for (expr* t : subterms(expr_ref(a, m))) {
// std::cout << expr_ref(t, m) << " " << (*m_model.get())(t) << "\n";
//}
asms.push_back(a);
}
else {
@ -1811,8 +1843,8 @@ namespace smtfd {
}
}
expr* rep(expr* e) { return m_abs.rep(e); }
expr* abs(expr* e) { return m_abs.abs(e); }
expr* rep(expr* e) { return m_abs.rep(e); }
expr* abs(expr* e) { return m_abs.abs(e); }
expr* abs_assumption(expr* e) { return m_abs.abs_assumption(e); }
expr_ref_vector& rep(expr_ref_vector& v) { for (unsigned i = v.size(); i-- > 0; ) v[i] = rep(v.get(i)); return v; }
expr_ref_vector& abs(expr_ref_vector& v) { for (unsigned i = v.size(); i-- > 0; ) v[i] = abs(v.get(i)); return v; }
@ -1843,8 +1875,8 @@ namespace smtfd {
solver(unsigned indent, ast_manager& m, params_ref const& p):
solver_na2as(m),
m(m),
m_indent(indent),
m_abs(m),
m_indent(indent),
m_context(m_abs, m),
m_uf(m_context),
m_ar(m_context),
@ -1908,6 +1940,7 @@ namespace smtfd {
for (expr* f : m_abs.atom_defs()) {
m_fd_sat_solver->assert_expr(f);
m_fd_core_solver->assert_expr(f);
// TBD we want these too: m_axioms.push_back(f);
}
m_abs.reset_atom_defs();
}