mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-21 13:16:40 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master'

Browse source
This commit is contained in:
nilsbecker 2018-06-24 08:08:32 +02:00
commit 4f64f069ab
301 changed files with 15728 additions and 18169 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/asserted_formulas.cpp
View file

@ -501,7 +501,7 @@ unsigned asserted_formulas::propagate_values(unsigned i) {
void asserted_formulas::update_substitution(expr* n, proof* pr) {
expr* lhs, *rhs, *n1;
proof_ref pr1(m);
if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) {
if (is_ground(n) && m.is_eq(n, lhs, rhs)) {
compute_depth(lhs);
compute_depth(rhs);
if (is_gt(lhs, rhs)) {
@ -517,7 +517,7 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) {
}
TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
}
if (m.is_not(n, n1)) {
if (m.is_not(n, n1)) {
pr1 = m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr;
m_scoped_substitution.insert(n1, m.mk_false(), pr1);
}
@ -639,4 +639,3 @@ void pp(asserted_formulas & f) {
f.display(std::cout);
}
#endif

3
src/smt/cost_evaluator.cpp
View file

@ -47,8 +47,7 @@ float cost_evaluator::eval(expr * f) const {
return 1.0f;
return 0.0f;
case OP_ITE: return E(0) != 0.0f ? E(1) : E(2);
case OP_EQ:
case OP_IFF: return E(0) == E(1) ? 1.0f : 0.0f;
case OP_EQ: return E(0) == E(1) ? 1.0f : 0.0f;
case OP_XOR: return E(0) != E(1) ? 1.0f : 0.0f;
case OP_IMPLIES:
if (E(0) == 0.0f)

18
src/smt/expr_context_simplifier.cpp
View file

@ -110,13 +110,15 @@ void expr_context_simplifier::reduce_rec(app * a, expr_ref & result) {
case OP_OR:
reduce_or(a->get_num_args(), a->get_args(), result);
return;
case OP_IFF: {
expr_ref tmp1(m_manager), tmp2(m_manager);
reduce_rec(a->get_arg(0), tmp1);
reduce_rec(a->get_arg(1), tmp2);
m_simp.mk_iff(tmp1.get(), tmp2.get(), result);
return;
}
case OP_EQ:
if (m_manager.is_iff(a)) {
expr_ref tmp1(m_manager), tmp2(m_manager);
reduce_rec(a->get_arg(0), tmp1);
reduce_rec(a->get_arg(1), tmp2);
m_simp.mk_iff(tmp1.get(), tmp2.get(), result);
return;
}
break;
case OP_XOR: {
expr_ref tmp1(m_manager), tmp2(m_manager);
reduce_rec(a->get_arg(0), tmp1);
@ -580,7 +582,7 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r
}
assignment_map.insert(a, value);
}
else if (m.is_iff(a, n1, n2) || m.is_eq(a, n1, n2)) {
else if (m.is_eq(a, n1, n2)) {
lbool v1 = assignment_map.find(n1);
lbool v2 = assignment_map.find(n2);
if (v1 == l_undef || v2 == l_undef) {

70
src/smt/mam.cpp
View file

@ -569,10 +569,9 @@ namespace smt {
if (m_context) {
ast_manager & m = m_context->get_manager();
out << "patterns:\n";
ptr_vector<app>::const_iterator it = m_patterns.begin();
ptr_vector<app>::const_iterator end = m_patterns.end();
for (; it != end; ++it)
out << mk_pp(*it, m) << "\n";
for (expr* p : m_patterns) {
out << mk_pp(p, m) << "\n";
}
}
#endif
out << "function: " << m_root_lbl->get_name();
@ -831,10 +830,8 @@ namespace smt {
void init(code_tree * t, quantifier * qa, app * mp, unsigned first_idx) {
SASSERT(m_ast_manager.is_pattern(mp));
#ifdef Z3DEBUG
svector<check_mark>::iterator it = m_mark.begin();
svector<check_mark>::iterator end = m_mark.end();
for (; it != end; ++it) {
SASSERT(*it == NOT_CHECKED);
for (auto cm : m_mark) {
SASSERT(cm == NOT_CHECKED);
}
#endif
m_tree = t;
@ -865,9 +862,7 @@ namespace smt {
That is, during execution time, the variables will be already bound
*/
bool all_args_are_bound_vars(app * n) {
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i);
for (expr* arg : *n) {
if (!is_var(arg))
return false;
if (m_vars[to_var(arg)->get_idx()] == -1)
@ -884,9 +879,7 @@ namespace smt {
if (n->is_ground()) {
return;
}
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i);
for (expr* arg : *n) {
if (is_var(arg)) {
sz++;
unsigned var_id = to_var(arg)->get_idx();
@ -928,10 +921,7 @@ namespace smt {
unsigned first_app_sz;
unsigned first_app_num_unbound_vars;
// generate first the non-BIND operations
unsigned_vector::iterator it = m_todo.begin();
unsigned_vector::iterator end = m_todo.end();
for (; it != end; ++it) {
unsigned reg = *it;
for (unsigned reg : m_todo) {
expr * p = m_registers[reg];
SASSERT(!is_quantifier(p));
if (is_var(p)) {
@ -1249,10 +1239,7 @@ namespace smt {
SASSERT(head->m_next == 0);
m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
ptr_vector<instruction>::iterator it = m_seq.begin();
ptr_vector<instruction>::iterator end = m_seq.end();
for (; it != end; ++it) {
instruction * curr = *it;
for (instruction * curr : m_seq) {
head->m_next = curr;
head = curr;
}
@ -1495,10 +1482,8 @@ namespace smt {
}
if (num_instr > SIMPLE_SEQ_THRESHOLD || (curr != nullptr && curr->m_opcode == CHOOSE))
simple = false;
unsigned_vector::iterator it = m_to_reset.begin();
unsigned_vector::iterator end = m_to_reset.end();
for (; it != end; ++it)
m_registers[*it] = 0;
for (unsigned reg : m_to_reset)
m_registers[reg] = 0;
return weight;
}
@ -1716,23 +1701,19 @@ namespace smt {
m_num_choices++;
// set: head -> c1 -> c2 -> c3 -> new_child_head1
curr = head;
ptr_vector<instruction>::iterator it1 = m_compatible.begin();
ptr_vector<instruction>::iterator end1 = m_compatible.end();
for (; it1 != end1; ++it1) {
set_next(curr, *it1);
curr = *it1;
for (instruction* instr : m_compatible) {
set_next(curr, instr);
curr = instr;
}
set_next(curr, new_child_head1);
// set: new_child_head1:CHOOSE(new_child_head2) -> i1 -> i2 -> first_child_head
curr = new_child_head1;
ptr_vector<instruction>::iterator it2 = m_incompatible.begin();
ptr_vector<instruction>::iterator end2 = m_incompatible.end();
for (; it2 != end2; ++it2) {
for (instruction* inc : m_incompatible) {
if (curr == new_child_head1)
curr->m_next = *it2; // new_child_head1 is a new node, I don't need to save trail
curr->m_next = inc; // new_child_head1 is a new node, I don't need to save trail
else
set_next(curr, *it2);
curr = *it2;
set_next(curr, inc);
curr = inc;
}
set_next(curr, first_child_head);
// build new_child_head2:NOOP -> linearise()
@ -3370,10 +3351,7 @@ namespace smt {
void update_vars(unsigned short var_id, path * p, quantifier * qa, app * mp) {
paths & var_paths = m_var_paths[var_id];
bool found = false;
paths::iterator it = var_paths.begin();
paths::iterator end = var_paths.end();
for (; it != end; ++it) {
path * curr_path = *it;
for (path* curr_path : var_paths) {
if (is_equal(p, curr_path))
found = true;
func_decl * lbl1 = curr_path->m_label;
@ -3664,18 +3642,12 @@ namespace smt {
TRACE("incremental_matcher", tout << "pp: plbls1: " << plbls1 << ", plbls2: " << plbls2 << "\n";);
TRACE("mam_info", tout << "pp: " << plbls1.size() * plbls2.size() << "\n";);
if (!plbls1.empty() && !plbls2.empty()) {
approx_set::iterator it1 = plbls1.begin();
approx_set::iterator end1 = plbls1.end();
for (; it1 != end1; ++it1) {
for (unsigned plbl1 : plbls1) {
if (m_context.get_cancel_flag()) {
break;
}
unsigned plbl1 = *it1;
SASSERT(plbls1.may_contain(plbl1));
approx_set::iterator it2 = plbls2.begin();
approx_set::iterator end2 = plbls2.end();
for (; it2 != end2; ++it2) {
unsigned plbl2 = *it2;
for (unsigned plbl2 : plbls2) {
SASSERT(plbls2.may_contain(plbl2));
unsigned n_plbl1 = plbl1;
unsigned n_plbl2 = plbl2;

1
src/smt/params/preprocessor_params.cpp
View file

@ -46,7 +46,6 @@ void preprocessor_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_eliminate_term_ite);
DISPLAY_PARAM(m_macro_finder);
DISPLAY_PARAM(m_propagate_values);
DISPLAY_PARAM(m_propagate_booleans);
DISPLAY_PARAM(m_refine_inj_axiom);
DISPLAY_PARAM(m_eliminate_bounds);
DISPLAY_PARAM(m_simplify_bit2int);

2
src/smt/params/preprocessor_params.h
View file

@ -37,7 +37,6 @@ struct preprocessor_params : public pattern_inference_params,
bool m_eliminate_term_ite;
bool m_macro_finder;
bool m_propagate_values;
bool m_propagate_booleans;
bool m_refine_inj_axiom;
bool m_eliminate_bounds;
bool m_simplify_bit2int;
@ -59,7 +58,6 @@ public:
m_eliminate_term_ite(false),
m_macro_finder(false),
m_propagate_values(true),
m_propagate_booleans(false), // TODO << check peformance
m_refine_inj_axiom(true),
m_eliminate_bounds(false),
m_simplify_bit2int(false),

2
src/smt/params/qi_params.cpp
View file

@ -35,12 +35,12 @@ void qi_params::updt_params(params_ref const & _p) {
m_qi_lazy_threshold = p.qi_lazy_threshold();
m_qi_cost = p.qi_cost();
m_qi_max_eager_multipatterns = p.qi_max_multi_patterns();
m_qi_quick_checker = static_cast<quick_checker_mode>(p.qi_quick_checker());
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void qi_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_qi_ematching);
DISPLAY_PARAM(m_qi_cost);
DISPLAY_PARAM(m_qi_new_gen);
DISPLAY_PARAM(m_qi_eager_threshold);

1
src/smt/params/qi_params.h
View file

@ -29,7 +29,6 @@ enum quick_checker_mode {
};
struct qi_params {
bool m_qi_ematching;
std::string m_qi_cost;
std::string m_qi_new_gen;
double m_qi_eager_threshold;

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

@ -36,6 +36,7 @@ def_module_params(module_name='smt',
('qi.lazy_threshold', DOUBLE, 20.0, 'threshold for lazy quantifier instantiation'),
('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
('qi.quick_checker', UINT, 0, 'specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances'),
('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
@ -53,6 +54,8 @@ def_module_params(module_name='smt',
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'),
('arith.greatest_error_pivot', BOOL, False, 'Pivoting strategy'),
('arith.eager_eq_axioms', BOOL, True, 'eager equality axioms'),
('arith.auto_config_simplex', BOOL, False, 'force simplex solver in auto_config'),
('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'),

3
src/smt/params/theory_arith_params.cpp
View file

@ -37,6 +37,9 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
m_arith_dump_lemmas = p.arith_dump_lemmas();
m_arith_reflect = p.arith_reflect();
m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
m_arith_auto_config_simplex = p.arith_auto_config_simplex();
arith_rewriter_params ap(_p);
m_arith_eq2ineq = ap.eq2ineq();
}

16
src/smt/proto_model/proto_model.cpp
View file

@ -342,10 +342,16 @@ void proto_model::compress() {
\brief Complete the interpretation fi of f if it is partial.
If f does not have an interpretation in the given model, then this is a noop.
*/
void proto_model::complete_partial_func(func_decl * f) {
void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) {
expr * else_value = fi->get_max_occ_result();
expr * else_value;
if (use_fresh) {
else_value = get_fresh_value(f->get_range());
}
else {
else_value = fi->get_max_occ_result();
}
if (else_value == nullptr)
else_value = get_some_value(f->get_range());
fi->set_else(else_value);
@ -355,14 +361,14 @@ void proto_model::complete_partial_func(func_decl * f) {
/**
\brief Set the (else) field of function interpretations...
*/
void proto_model::complete_partial_funcs() {
void proto_model::complete_partial_funcs(bool use_fresh) {
if (m_model_partial)
return;
// m_func_decls may be "expanded" when we invoke get_some_value.
// So, we must not use iterators to traverse it.
for (unsigned i = 0; i < m_func_decls.size(); i++) {
complete_partial_func(m_func_decls[i]);
for (unsigned i = 0; i < m_func_decls.size(); ++i) {
complete_partial_func(m_func_decls.get(i), use_fresh);
}
}

4
src/smt/proto_model/proto_model.h
View file

@ -100,8 +100,8 @@ public:
//
// Complete partial function interps
//
void complete_partial_func(func_decl * f);
void complete_partial_funcs();
void complete_partial_func(func_decl * f, bool use_fresh);
void complete_partial_funcs(bool use_fresh);
//
// Create final model object.

28
src/smt/smt_checker.cpp
View file

@ -61,8 +61,20 @@ namespace smt {
return is_true ? any_arg(a, true) : all_args(a, false);
case OP_AND:
return is_true ? all_args(a, true) : any_arg(a, false);
case OP_IFF:
if (is_true) {
case OP_EQ:
if (!m_manager.is_iff(a)) {
enode * lhs = get_enode_eq_to(a->get_arg(0));
enode * rhs = get_enode_eq_to(a->get_arg(1));
if (lhs && rhs && m_context.is_relevant(lhs) && m_context.is_relevant(rhs)) {
if (is_true && lhs->get_root() == rhs->get_root())
return true;
// if (!is_true && m_context.is_ext_diseq(lhs, rhs, 2))
if (!is_true && m_context.is_diseq(lhs, rhs))
return true;
}
return false;
}
else if (is_true) {
return
(check(a->get_arg(0), true) &&
check(a->get_arg(1), true)) ||
@ -86,18 +98,6 @@ namespace smt {
}
return check(a->get_arg(1), is_true) && check(a->get_arg(2), is_true);
}
case OP_EQ: {
enode * lhs = get_enode_eq_to(a->get_arg(0));
enode * rhs = get_enode_eq_to(a->get_arg(1));
if (lhs && rhs && m_context.is_relevant(lhs) && m_context.is_relevant(rhs)) {
if (is_true && lhs->get_root() == rhs->get_root())
return true;
// if (!is_true && m_context.is_ext_diseq(lhs, rhs, 2))
if (!is_true && m_context.is_diseq(lhs, rhs))
return true;
}
return false;
}
default:
break;
}

5
src/smt/smt_clause.cpp
View file

@ -25,7 +25,7 @@ namespace smt {
\brief Create a new clause.
bool_var2expr_map is a mapping from bool_var -> expr, it is only used if save_atoms == true.
*/
clause * clause::mk(ast_manager & m, unsigned num_lits, literal * lits, clause_kind k, justification * js,
clause * clause::mk(ast_manager & m, unsigned num_lits, literal * lits, clause_kind k, justification * js,
clause_del_eh * del_eh, bool save_atoms, expr * const * bool_var2expr_map) {
SASSERT(k == CLS_AUX || js == 0 || !js->in_region());
SASSERT(num_lits >= 2);
@ -67,7 +67,7 @@ namespace smt {
}});
return cls;
}
void clause::deallocate(ast_manager & m) {
clause_del_eh * del_eh = get_del_eh();
if (del_eh)
@ -115,4 +115,3 @@ namespace smt {
}
};

8
src/smt/smt_clause.h
View file

@ -192,13 +192,13 @@ namespace smt {
return m_lits[idx];
}
literal * begin_literals() { return m_lits; }
literal * begin() { return m_lits; }
literal * end_literals() { return m_lits + m_num_literals; }
literal * end() { return m_lits + m_num_literals; }
literal const * begin_literals() const { return m_lits; }
literal const * begin() const { return m_lits; }
literal const * end_literals() const { return m_lits + m_num_literals; }
literal const * end() const { return m_lits + m_num_literals; }
unsigned get_activity() const {
SASSERT(is_lemma());

5
src/smt/smt_conflict_resolution.cpp
View file

@ -771,7 +771,7 @@ namespace smt {
app * fact = to_app(m_manager.get_fact(pr));
app * n1_owner = n1->get_owner();
app * n2_owner = n2->get_owner();
bool is_eq = m_manager.is_eq(fact) || m_manager.is_iff(fact);
bool is_eq = m_manager.is_eq(fact);
if (!is_eq || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) {
CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2),
tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n";
@ -794,7 +794,7 @@ namespace smt {
TRACE("norm_eq_proof",
tout << "#" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";
tout << mk_ll_pp(pr, m_manager, true, false););
SASSERT(m_manager.is_eq(fact) || m_manager.is_iff(fact));
SASSERT(m_manager.is_eq(fact));
SASSERT((fact->get_arg(0) == n1->get_owner() && fact->get_arg(1) == n2->get_owner()) ||
(fact->get_arg(1) == n1->get_owner() && fact->get_arg(0) == n2->get_owner()));
if (fact->get_arg(0) == n1_owner && fact->get_arg(1) == n2_owner)
@ -1033,6 +1033,7 @@ namespace smt {
return pr;
}
SASSERT(js != 0);
TRACE("proof_gen_bug", tout << js << "\n";);
m_todo_pr.push_back(tp_elem(js));
return nullptr;
}

2
src/smt/smt_conflict_resolution.h
View file

@ -96,7 +96,7 @@ namespace smt {
};
tp_elem(literal l):m_kind(LITERAL), m_lidx(l.index()) {}
tp_elem(enode * lhs, enode * rhs):m_kind(EQUALITY), m_lhs(lhs), m_rhs(rhs) {}
tp_elem(justification * js):m_kind(JUSTIFICATION), m_js(js) {}
tp_elem(justification * js):m_kind(JUSTIFICATION), m_js(js) { SASSERT(js);}
};
svector<tp_elem> m_todo_pr;

7
src/smt/smt_consequences.cpp
View file

@ -637,15 +637,14 @@ namespace smt {
model_ref mdl;
for (unsigned i = 0; i < unfixed.size(); ++i) {
push();
for (unsigned j = 0; j < assumptions.size(); ++j) {
assert_expr(assumptions[j]);
}
for (expr* a : assumptions)
assert_expr(a);
TRACE("context", tout << "checking unfixed: " << mk_pp(unfixed[i], m) << "\n";);
lbool is_sat = check();
SASSERT(is_sat != l_false);
if (is_sat == l_true) {
get_model(mdl);
mdl->eval(unfixed[i], tmp);
tmp = (*mdl)(unfixed[i]);
if (m.is_value(tmp)) {
tmp = m.mk_not(m.mk_eq(unfixed[i], tmp));
assert_expr(tmp);

331
src/smt/smt_context.cpp
View file

@ -203,8 +203,8 @@ namespace smt {
literal l1 = to_literal(l_idx);
literal neg_l1 = ~l1;
watch_list const & wl = *it;
literal const * it2 = wl.begin_literals();
literal const * end2 = wl.end_literals();
literal const * it2 = wl.begin();
literal const * end2 = wl.end();
for (; it2 != end2; ++it2) {
literal l2 = *it2;
if (l1.index() < l2.index()) {
@ -385,8 +385,8 @@ namespace smt {
it2++;
}
else {
literal * it3 = cls->begin_literals() + 2;
literal * end3 = cls->end_literals();
literal * it3 = cls->begin() + 2;
literal * end3 = cls->end();
for(; it3 != end3; ++it3) {
if (get_assignment(*it3) != l_false) {
// swap literal *it3 with literal at position 0
@ -628,7 +628,7 @@ namespace smt {
*/
void context::remove_parents_from_cg_table(enode * r1) {
// Remove parents from the congruence table
for (enode * parent : r1->get_parents()) {
for (enode * parent : enode::parents(r1)) {
#if 0
{
static unsigned num_eqs = 0;
@ -673,7 +673,7 @@ namespace smt {
*/
void context::reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js) {
enode_vector & r2_parents = r2->m_parents;
for (enode * parent : r1->get_parents()) {
for (enode * parent : enode::parents(r1)) {
if (!parent->is_marked())
continue;
parent->unset_mark();
@ -1005,7 +1005,7 @@ namespace smt {
r2->m_parents.shrink(r2_num_parents);
// try to reinsert parents of r1 that are not cgr
for (enode * parent : r1->get_parents()) {
for (enode * parent : enode::parents(r1)) {
TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";);
if (parent->is_cgc_enabled()) {
enode * cg = parent->m_cg;
@ -1201,7 +1201,7 @@ namespace smt {
bool context::is_diseq_slow(enode * n1, enode * n2) const {
if (n1->get_num_parents() > n2->get_num_parents())
std::swap(n1, n2);
for (enode * parent : n1->get_parents()) {
for (enode * parent : enode::parents(n1)) {
if (parent->is_eq() && is_relevant(parent->get_owner()) && get_assignment(enode2bool_var(parent)) == l_false &&
((parent->get_arg(0)->get_root() == n1->get_root() && parent->get_arg(1)->get_root() == n2->get_root()) ||
(parent->get_arg(1)->get_root() == n1->get_root() && parent->get_arg(0)->get_root() == n2->get_root()))) {
@ -1233,7 +1233,7 @@ namespace smt {
return false;
if (r1->get_num_parents() < SMALL_NUM_PARENTS) {
TRACE("is_ext_diseq", tout << mk_bounded_pp(n1->get_owner(), m_manager) << " " << mk_bounded_pp(n2->get_owner(), m_manager) << " " << depth << "\n";);
for (enode* p1 : r1->get_parents()) {
for (enode * p1 : enode::parents(r1)) {
if (!is_relevant(p1))
continue;
if (p1->is_eq())
@ -1243,7 +1243,7 @@ namespace smt {
func_decl * f = p1->get_decl();
TRACE("is_ext_diseq", tout << "p1: " << mk_bounded_pp(p1->get_owner(), m_manager) << "\n";);
unsigned num_args = p1->get_num_args();
for (enode * p2 : r2->get_parents()) {
for (enode * p2 : enode::parents(r2)) {
if (!is_relevant(p2))
continue;
if (p2->is_eq())
@ -1281,7 +1281,7 @@ namespace smt {
}
almost_cg_table & table = *(m_almost_cg_tables[depth]);
table.reset(r1, r2);
for (enode* p1 : r1->get_parents()) {
for (enode * p1 : enode::parents(r1)) {
if (!is_relevant(p1))
continue;
if (p1->is_eq())
@ -1292,7 +1292,7 @@ namespace smt {
}
if (table.empty())
return false;
for (enode * p2 : r2->get_parents()) {
for (enode * p2 : enode::parents(r2)) {
if (!is_relevant(p2))
continue;
if (p2->is_eq())
@ -1817,6 +1817,17 @@ namespace smt {
more case splits to be performed.
*/
bool context::decide() {
if (at_search_level() && !m_tmp_clauses.empty()) {
switch (decide_clause()) {
case l_true: // already satisfied
break;
case l_undef: // made a decision
return true;
case l_false: // inconsistent
return false;
}
}
bool_var var;
lbool phase;
m_case_split_queue->next_case_split(var, phase);
@ -2156,7 +2167,7 @@ namespace smt {
\brief See cache_generation(unsigned new_scope_lvl)
*/
void context::cache_generation(clause const * cls, unsigned new_scope_lvl) {
cache_generation(cls->get_num_literals(), cls->begin_literals(), new_scope_lvl);
cache_generation(cls->get_num_literals(), cls->begin(), new_scope_lvl);
}
/**
@ -2640,10 +2651,11 @@ namespace smt {
}
TRACE("simplify_clauses_detail", tout << "before:\n"; display_clauses(tout, m_lemmas););
IF_VERBOSE(2, verbose_stream() << "(smt.simplifying-clause-set"; verbose_stream().flush(););
SASSERT(check_clauses(m_lemmas));
SASSERT(check_clauses(m_aux_clauses));
IF_VERBOSE(2, verbose_stream() << "(smt.simplifying-clause-set"; verbose_stream().flush(););
// m_simp_counter is used to balance the cost of simplify_clause.
//
@ -2911,6 +2923,7 @@ namespace smt {
del_clauses(m_aux_clauses, 0);
del_clauses(m_lemmas, 0);
del_justifications(m_justifications, 0);
reset_tmp_clauses();
if (m_is_diseq_tmp) {
m_is_diseq_tmp->del_eh(m_manager, false);
m_manager.dec_ref(m_is_diseq_tmp->get_owner());
@ -3053,12 +3066,47 @@ namespace smt {
bool context::reduce_assertions() {
if (!m_asserted_formulas.inconsistent()) {
SASSERT(at_base_level());
// SASSERT(at_base_level());
m_asserted_formulas.reduce();
}
return m_asserted_formulas.inconsistent();
}
static bool is_valid_assumption(ast_manager & m, expr * assumption) {
expr* arg;
if (!m.is_bool(assumption))
return false;
if (is_uninterp_const(assumption))
return true;
if (m.is_not(assumption, arg) && is_uninterp_const(arg))
return true;
if (!is_app(assumption))
return false;
if (to_app(assumption)->get_num_args() == 0)
return true;
if (m.is_not(assumption, arg) && is_app(arg) && to_app(arg)->get_num_args() == 0)
return true;
return false;
}
void context::internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy) {
for (expr* e : asms) {
if (is_valid_assumption(m_manager, e)) {
asm2proxy.push_back(std::make_pair(e, expr_ref(e, m_manager)));
}
else {
expr_ref proxy(m_manager), fml(m_manager);
proxy = m_manager.mk_fresh_const("proxy", m_manager.mk_bool_sort());
fml = m_manager.mk_implies(proxy, e);
m_asserted_formulas.assert_expr(fml);
asm2proxy.push_back(std::make_pair(e, proxy));
}
}
// The new assertions are of the form 'proxy => assumption'
// so clause simplification is sound even as these are removed after pop_scope.
internalize_assertions();
}
void context::internalize_assertions() {
if (get_cancel_flag()) return;
TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
@ -3091,32 +3139,16 @@ namespace smt {
}
TRACE("internalize_assertions", tout << "after internalize_assertions()...\n";
tout << "inconsistent: " << inconsistent() << "\n";);
}
bool is_valid_assumption(ast_manager & m, expr * assumption) {
expr* arg;
if (!m.is_bool(assumption))
return false;
if (is_uninterp_const(assumption))
return true;
if (m.is_not(assumption, arg) && is_uninterp_const(arg))
return true;
if (!is_app(assumption))
return false;
if (to_app(assumption)->get_num_args() == 0)
return true;
if (m.is_not(assumption, arg) && is_app(arg) && to_app(arg)->get_num_args() == 0)
return true;
return false;
TRACE("after_internalize_assertions", display(tout););
}
/**
\brief Assumptions must be uninterpreted boolean constants (aka propositional variables).
*/
bool context::validate_assumptions(unsigned num_assumptions, expr * const * assumptions) {
for (unsigned i = 0; i < num_assumptions; i++) {
SASSERT(assumptions[i]);
if (!is_valid_assumption(m_manager, assumptions[i])) {
bool context::validate_assumptions(expr_ref_vector const& asms) {
for (expr* a : asms) {
SASSERT(a);
if (!is_valid_assumption(m_manager, a)) {
warning_msg("an assumption must be a propositional variable or the negation of one");
return false;
}
@ -3124,11 +3156,69 @@ namespace smt {
return true;
}
void context::init_assumptions(unsigned num_assumptions, expr * const * assumptions) {
void context::init_clause(expr_ref_vector const& _clause) {
literal_vector lits;
for (expr* lit : _clause) {
internalize_formula(lit, true);
mark_as_relevant(lit);
lits.push_back(get_literal(lit));
}
clause* clausep = nullptr;
if (lits.size() >= 2) {
justification* js = nullptr;
if (m_manager.proofs_enabled()) {
proof * pr = mk_clause_def_axiom(lits.size(), lits.c_ptr(), nullptr);
js = mk_justification(justification_proof_wrapper(*this, pr));
}
clausep = clause::mk(m_manager, lits.size(), lits.c_ptr(), CLS_AUX, js);
}
m_tmp_clauses.push_back(std::make_pair(clausep, lits));
}
void context::reset_tmp_clauses() {
for (auto& p : m_tmp_clauses) {
if (p.first) del_clause(p.first);
}
m_tmp_clauses.reset();
}
lbool context::decide_clause() {
if (m_tmp_clauses.empty()) return l_true;
for (auto & tmp_clause : m_tmp_clauses) {
literal_vector& lits = tmp_clause.second;
for (literal l : lits) {
switch (get_assignment(l)) {
case l_false:
break;
case l_true:
goto next_clause;
default:
shuffle(lits.size(), lits.c_ptr(), m_random);
push_scope();
assign(l, b_justification::mk_axiom(), true);
return l_undef;
}
}
if (lits.size() == 1) {
set_conflict(b_justification(), ~lits[0]);
}
else {
set_conflict(b_justification(tmp_clause.first), null_literal);
}
VERIFY(!resolve_conflict());
return l_false;
next_clause:
;
}
return l_true;
}
void context::init_assumptions(expr_ref_vector const& asms) {
reset_assumptions();
m_literal2assumption.reset();
m_unsat_core.reset();
if (num_assumptions > 0) {
if (!asms.empty()) {
// We must give a chance to the theories to propagate before we create a new scope...
propagate();
// Internal backtracking scopes (created with push_scope()) must only be created when we are
@ -3138,18 +3228,21 @@ namespace smt {
if (get_cancel_flag())
return;
push_scope();
for (unsigned i = 0; i < num_assumptions; i++) {
expr * curr_assumption = assumptions[i];
vector<std::pair<expr*,expr_ref>> asm2proxy;
internalize_proxies(asms, asm2proxy);
for (auto const& p: asm2proxy) {
expr_ref curr_assumption = p.second;
expr* orig_assumption = p.first;
if (m_manager.is_true(curr_assumption)) continue;
SASSERT(is_valid_assumption(m_manager, curr_assumption));
proof * pr = m_manager.mk_asserted(curr_assumption);
internalize_assertion(curr_assumption, pr, 0);
literal l = get_literal(curr_assumption);
m_literal2assumption.insert(l.index(), curr_assumption);
m_literal2assumption.insert(l.index(), orig_assumption);
// mark_as_relevant(l); <<< not needed
// internalize_assertion marked l as relevant.
SASSERT(is_relevant(l));
TRACE("assumptions", tout << l << ":" << mk_pp(curr_assumption, m_manager) << "\n";);
TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m_manager) << "\n";);
if (m_manager.proofs_enabled())
assign(l, mk_justification(justification_proof_wrapper(*this, pr)));
else
@ -3159,8 +3252,9 @@ namespace smt {
}
}
m_search_lvl = m_scope_lvl;
SASSERT(!(num_assumptions > 0) || m_search_lvl > m_base_lvl);
SASSERT(!(num_assumptions == 0) || m_search_lvl == m_base_lvl);
SASSERT(asms.empty() || m_search_lvl > m_base_lvl);
SASSERT(!asms.empty() || m_search_lvl == m_base_lvl);
TRACE("after_internalization", display(tout););
}
void context::reset_assumptions() {
@ -3169,7 +3263,8 @@ namespace smt {
m_assumptions.reset();
}
lbool context::mk_unsat_core() {
lbool context::mk_unsat_core(lbool r) {
if (r != l_false) return r;
SASSERT(inconsistent());
if (!tracking_assumptions()) {
SASSERT(m_assumptions.empty());
@ -3186,18 +3281,16 @@ namespace smt {
SASSERT(m_literal2assumption.contains(l.index()));
if (!already_found_assumptions.contains(l.index())) {
already_found_assumptions.insert(l.index());
m_unsat_core.push_back(m_literal2assumption[l.index()]);
expr* orig_assumption = m_literal2assumption[l.index()];
m_unsat_core.push_back(orig_assumption);
TRACE("assumptions", tout << l << ": " << mk_pp(orig_assumption, m_manager) << "\n";);
}
}
reset_assumptions();
pop_to_base_lvl(); // undo the push_scope() performed by init_assumptions
m_search_lvl = m_base_lvl;
std::sort(m_unsat_core.c_ptr(), m_unsat_core.c_ptr() + m_unsat_core.size(), ast_lt_proc());
TRACE("unsat_core_bug", tout << "unsat core:\n";
unsigned sz = m_unsat_core.size();
for (unsigned i = 0; i < sz; i++) {
tout << mk_pp(m_unsat_core.get(i), m_manager) << "\n";
});
TRACE("unsat_core_bug", tout << "unsat core:\n" << m_unsat_core << "\n";);
validate_unsat_core();
// theory validation of unsat core
for (theory* th : m_theory_set) {
@ -3221,6 +3314,10 @@ namespace smt {
m_last_search_failure = MEMOUT;
return false;
}
reset_tmp_clauses();
m_unsat_core.reset();
m_stats.m_num_checks++;
pop_to_base_lvl();
return true;
}
@ -3244,8 +3341,7 @@ namespace smt {
and before internalizing any formulas.
*/
lbool context::setup_and_check(bool reset_cancel) {
if (!check_preamble(reset_cancel))
return l_undef;
if (!check_preamble(reset_cancel)) return l_undef;
SASSERT(m_scope_lvl == 0);
SASSERT(!m_setup.already_configured());
setup_context(m_fparams.m_auto_config);
@ -3258,20 +3354,8 @@ namespace smt {
}
internalize_assertions();
lbool r = l_undef;
TRACE("before_search", display(tout););
if (m_asserted_formulas.inconsistent()) {
r = l_false;
}
else {
if (inconsistent()) {
VERIFY(!resolve_conflict()); // build the proof
r = l_false;
}
else {
r = search();
}
}
lbool r = search();
r = check_finalize(r);
return r;
}
@ -3285,7 +3369,7 @@ namespace smt {
}
void context::setup_context(bool use_static_features) {
if (m_setup.already_configured())
if (m_setup.already_configured() || inconsistent())
return;
m_setup(get_config_mode(use_static_features));
setup_components();
@ -3320,78 +3404,45 @@ namespace smt {
}
}
lbool context::check(unsigned ext_num_assumptions, expr * const * ext_assumptions, bool reset_cancel, bool already_did_theory_assumptions) {
m_stats.m_num_checks++;
TRACE("check_bug", tout << "STARTING check(num_assumptions, assumptions)\n";
tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";
m_asserted_formulas.display(tout);
tout << "-----------------------\n";
display(tout););
if (!m_unsat_core.empty())
m_unsat_core.reset();
if (!check_preamble(reset_cancel))
return l_undef;
TRACE("check_bug", tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";);
pop_to_base_lvl();
TRACE("before_search", display(tout););
lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel, bool already_did_theory_assumptions) {
if (!check_preamble(reset_cancel)) return l_undef;
SASSERT(at_base_level());
lbool r = l_undef;
if (inconsistent()) {
r = l_false;
}
else {
setup_context(false);
expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
if (!already_did_theory_assumptions) {
add_theory_assumptions(all_assumptions);
}
unsigned num_assumptions = all_assumptions.size();
expr * const * assumptions = all_assumptions.c_ptr();
if (!validate_assumptions(num_assumptions, assumptions))
return l_undef;
TRACE("unsat_core_bug", tout << all_assumptions << "\n";);
internalize_assertions();
TRACE("after_internalize_assertions", display(tout););
if (m_asserted_formulas.inconsistent()) {
r = l_false;
}
else {
init_assumptions(num_assumptions, assumptions);
TRACE("after_internalization", display(tout););
if (inconsistent()) {
VERIFY(!resolve_conflict()); // build the proof
lbool result = mk_unsat_core();
if (result == l_undef) {
r = l_undef;
} else {
r = l_false;
}
}
else {
r = search();
if (r == l_false) {
lbool result = mk_unsat_core();
if (result == l_undef) {
r = l_undef;
}
}
}
}
}
setup_context(false);
expr_ref_vector asms(m_manager, num_assumptions, assumptions);
if (!already_did_theory_assumptions) add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
TRACE("unsat_core_bug", tout << asms << "\n";);
internalize_assertions();
init_assumptions(asms);
TRACE("before_search", display(tout););
lbool r = search();
r = mk_unsat_core(r);
r = check_finalize(r);
return r;
}
lbool context::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
if (!check_preamble(true)) return l_undef;
TRACE("before_search", display(tout););
setup_context(false);
expr_ref_vector asms(cube);
add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
internalize_assertions();
init_assumptions(asms);
for (auto const& clause : clauses) init_clause(clause);
lbool r = search();
r = mk_unsat_core(r);
r = check_finalize(r);
return r;
}
void context::init_search() {
for (theory* th : m_theory_set) {
th->init_search_eh();
}
m_qmanager->init_search_eh();
m_assumption_core.reset();
m_incomplete_theories.reset();
m_num_conflicts = 0;
m_num_conflicts_since_restart = 0;
@ -3454,6 +3505,12 @@ namespace smt {
exit(1);
}
#endif
if (m_asserted_formulas.inconsistent())
return l_false;
if (inconsistent()) {
VERIFY(!resolve_conflict());
return l_false;
}
timeit tt(get_verbosity_level() >= 100, "smt.stats");
scoped_mk_model smk(*this);
SASSERT(at_search_level());
@ -3477,24 +3534,19 @@ namespace smt {
if (!restart(status, curr_lvl)) {
break;
}
}
}
TRACE("search_lite", tout << "status: " << status << "\n";);
TRACE("guessed_literals",
expr_ref_vector guessed_lits(m_manager);
get_guessed_literals(guessed_lits);
unsigned sz = guessed_lits.size();
for (unsigned i = 0; i < sz; i++) {
tout << mk_pp(guessed_lits.get(i), m_manager) << "\n";
});
tout << guessed_lits << "\n";);
end_search();
return status;
}
bool context::restart(lbool& status, unsigned curr_lvl) {
if (m_last_search_failure != OK) {
if (status != l_false) {
// build candidate model before returning
@ -3647,6 +3699,8 @@ namespace smt {
simplify_clauses();
if (!decide()) {
if (inconsistent())
return l_false;
final_check_status fcs = final_check();
TRACE("final_check_result", tout << "fcs: " << fcs << " last_search_failure: " << m_last_search_failure << "\n";);
switch (fcs) {
@ -3704,6 +3758,7 @@ namespace smt {
TRACE("final_check", tout << "final_check inconsistent: " << inconsistent() << "\n"; display(tout); display_normalized_enodes(tout););
CASSERT("relevancy", check_relevancy());
if (m_fparams.m_model_on_final_check) {
mk_proto_model(l_undef);
model_pp(std::cout, *m_proto_model);
@ -4232,7 +4287,7 @@ namespace smt {
theory_var_list * l = n->get_th_var_list();
theory_id th_id = l->get_th_id();
for (enode* parent : n->get_parents()) {
for (enode * parent : enode::parents(n)) {
family_id fid = parent->get_owner()->get_family_id();
if (fid != th_id && fid != m_manager.get_basic_family_id()) {
TRACE("is_shared", tout << mk_pp(n->get_owner(), m_manager) << "\nis shared because of:\n" << mk_pp(parent->get_owner(), m_manager) << "\n";);
@ -4313,7 +4368,7 @@ namespace smt {
m_proto_model = m_model_generator->mk_model();
m_qmanager->adjust_model(m_proto_model.get());
TRACE("mbqi_bug", tout << "before complete_partial_funcs:\n"; model_pp(tout, *m_proto_model););
m_proto_model->complete_partial_funcs();
m_proto_model->complete_partial_funcs(false);
TRACE("mbqi_bug", tout << "before cleanup:\n"; model_pp(tout, *m_proto_model););
m_proto_model->cleanup();
if (m_fparams.m_model_compact)

21
src/smt/smt_context.h
View file

@ -169,6 +169,8 @@ namespace smt {
expr_ref_vector m_units_to_reassert;
svector<char> m_units_to_reassert_sign;
literal_vector m_assigned_literals;
typedef std::pair<clause*, literal_vector> tmp_clause;
vector<tmp_clause> m_tmp_clauses;
unsigned m_qhead;
unsigned m_simp_qhead;
int m_simp_counter; //!< can become negative
@ -893,7 +895,6 @@ namespace smt {
failure m_last_search_failure;
ptr_vector<theory> m_incomplete_theories; //!< theories that failed to produce a model
bool m_searching;
ptr_vector<expr> m_assumption_core;
unsigned m_num_conflicts;
unsigned m_num_conflicts_since_restart;
unsigned m_num_conflicts_since_lemma_gc;
@ -1105,15 +1106,23 @@ namespace smt {
void assert_assumption(expr * a);
bool validate_assumptions(unsigned num_assumptions, expr * const * assumptions);
bool validate_assumptions(expr_ref_vector const& asms);
void init_assumptions(unsigned num_assumptions, expr * const * assumptions);
void init_assumptions(expr_ref_vector const& asms);
void init_clause(expr_ref_vector const& clause);
lbool decide_clause();
void reset_tmp_clauses();
void reset_assumptions();
void reset_clause();
void add_theory_assumptions(expr_ref_vector & theory_assumptions);
lbool mk_unsat_core();
lbool mk_unsat_core(lbool result);
void validate_unsat_core();
@ -1498,6 +1507,8 @@ namespace smt {
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true, bool already_did_theory_assumptions = false);
lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses);
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
@ -1525,6 +1536,8 @@ namespace smt {
void internalize_assertion(expr * n, proof * pr, unsigned generation);
void internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy);
void internalize_instance(expr * body, proof * pr, unsigned generation) {
internalize_assertion(body, pr, generation);
if (relevancy())

83
src/smt/smt_context_inv.cpp
View file

@ -43,13 +43,9 @@ namespace smt {
}
bool context::check_clauses(clause_vector const & v) const {
clause_vector::const_iterator it = v.begin();
clause_vector::const_iterator end = v.end();
for (; it != end; ++it) {
clause * cls = *it;
for (clause* cls : v)
if (!cls->deleted())
check_clause(cls);
}
return true;
}
@ -92,10 +88,7 @@ namespace smt {
bool context::check_lit_occs(literal l) const {
clause_set const & v = m_lit_occs[l.index()];
clause_set::iterator it = v.begin();
clause_set::iterator end = v.end();
for (; it != end; ++it) {
clause * cls = *it;
for (clause * cls : v) {
unsigned num = cls->get_num_literals();
unsigned i = 0;
for (; i < num; i++)
@ -138,10 +131,8 @@ namespace smt {
}
bool context::check_enodes() const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
check_enode(*it);
for (enode* n : m_enodes) {
check_enode(n);
}
return true;
}
@ -157,11 +148,9 @@ namespace smt {
}
bool context::check_missing_clause_propagation(clause_vector const & v) const {
clause_vector::const_iterator it = v.begin();
clause_vector::const_iterator end = v.end();
for (; it != end; ++it) {
CTRACE("missing_propagation", is_unit_clause(*it), display_clause_detail(tout, *it); tout << "\n";);
SASSERT(!is_unit_clause(*it));
for (clause * cls : v) {
CTRACE("missing_propagation", is_unit_clause(cls), display_clause_detail(tout, cls); tout << "\n";);
SASSERT(!is_unit_clause(cls));
}
return true;
}
@ -188,10 +177,7 @@ namespace smt {
}
bool context::check_missing_eq_propagation() const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode* n : m_enodes) {
SASSERT(!n->is_true_eq() || get_assignment(n) == l_true);
if (n->is_eq() && get_assignment(n) == l_true) {
SASSERT(n->is_true_eq());
@ -201,13 +187,8 @@ namespace smt {
}
bool context::check_missing_congruence() const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * n = *it;
ptr_vector<enode>::const_iterator it2 = m_enodes.begin();
for (; it2 != end; ++it2) {
enode * n2 = *it2;
for (enode* n : m_enodes) {
for (enode* n2 : m_enodes) {
if (n->get_root() != n2->get_root()) {
if (n->is_true_eq() && n2->is_true_eq())
continue;
@ -222,10 +203,7 @@ namespace smt {
}
bool context::check_missing_bool_enode_propagation() const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode* n : m_enodes) {
if (m_manager.is_bool(n->get_owner()) && get_assignment(n) == l_undef) {
enode * first = n;
do {
@ -286,10 +264,7 @@ namespace smt {
For all a, b. root(a) == root(b) ==> get_assignment(a) == get_assignment(b)
*/
bool context::check_eqc_bool_assignment() const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * e = *it;
for (enode* e : m_enodes) {
if (m_manager.is_bool(e->get_owner())) {
enode * r = e->get_root();
CTRACE("eqc_bool", get_assignment(e) != get_assignment(r),
@ -343,24 +318,24 @@ namespace smt {
TRACE("check_th_diseq_propagation", tout << "checking theory: " << m_manager.get_family_name(th_id) << "\n";);
// if the theory doesn't use diseqs, then the diseqs are not propagated.
if (th->use_diseqs() && rhs->get_th_var(th_id) != null_theory_var) {
bool found = false;
// lhs and rhs are attached to theory th_id
svector<new_th_eq>::const_iterator it = m_propagated_th_diseqs.begin();
svector<new_th_eq>::const_iterator end = m_propagated_th_diseqs.end();
for (; it != end; ++it) {
if (it->m_th_id == th_id) {
enode * lhs_prime = th->get_enode(it->m_lhs)->get_root();
enode * rhs_prime = th->get_enode(it->m_rhs)->get_root();
for (new_th_eq const& eq : m_propagated_th_diseqs) {
if (eq.m_th_id == th_id) {
enode * lhs_prime = th->get_enode(eq.m_lhs)->get_root();
enode * rhs_prime = th->get_enode(eq.m_rhs)->get_root();
TRACE("check_th_diseq_propagation",
tout << m_manager.get_family_name(it->m_th_id) << "\n";);
tout << m_manager.get_family_name(eq.m_th_id) << "\n";);
if ((lhs == lhs_prime && rhs == rhs_prime) ||
(rhs == lhs_prime && lhs == rhs_prime)) {
TRACE("check_th_diseq_propagation", tout << "ok v" << v << " " << get_assignment(v) << "\n";);
found = true;
break;
}
}
}
if (it == end) {
if (!found) {
// missed theory diseq propagation
display(std::cout);
std::cout << "checking theory: " << m_manager.get_family_name(th_id) << "\n";
@ -369,8 +344,7 @@ namespace smt {
std::cout << "lhs: #" << lhs->get_owner_id() << ", rhs: #" << rhs->get_owner_id() << "\n";
std::cout << mk_bounded_pp(lhs->get_owner(), m_manager) << " " << mk_bounded_pp(rhs->get_owner(), m_manager) << "\n";
}
SASSERT(it != end);
VERIFY(found);
}
l = l->get_next();
}
@ -381,11 +355,9 @@ namespace smt {
}
bool context::check_missing_diseq_conflict() const {
svector<enode_pair>::const_iterator it = m_diseq_vector.begin();
svector<enode_pair>::const_iterator end = m_diseq_vector.end();
for (; it != end; ++it) {
enode * n1 = it->first;
enode * n2 = it->second;
for (enode_pair const& p : m_diseq_vector) {
enode * n1 = p.first;
enode * n2 = p.second;
if (n1->get_root() == n2->get_root()) {
TRACE("diseq_bug",
tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() <<
@ -420,10 +392,7 @@ namespace smt {
return true;
}
ast_manager& m = m_manager;
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
literal lit = *it;
for (literal lit : m_assigned_literals) {
if (!is_relevant(lit)) {
continue;
}
@ -435,7 +404,7 @@ namespace smt {
if (is_quantifier(n) && m.is_rec_fun_def(to_quantifier(n))) {
continue;
}
switch (get_assignment(*it)) {
switch (get_assignment(lit)) {
case l_undef:
break;
case l_true:

2
src/smt/smt_context_pp.cpp
View file

@ -583,7 +583,7 @@ namespace smt {
case b_justification::CLAUSE: {
clause * cls = j.get_clause();
out << "clause ";
if (cls) out << literal_vector(cls->get_num_literals(), cls->begin_literals());
if (cls) out << literal_vector(cls->get_num_literals(), cls->begin());
break;
}
case b_justification::JUSTIFICATION: {

2
src/smt/smt_implied_equalities.cpp
View file

@ -199,7 +199,7 @@ namespace smt {
for (unsigned i = 0; i < terms.size(); ++i) {
expr* t = terms[i].term;
model->eval(t, vl);
vl = (*model)(t);
TRACE("get_implied_equalities", tout << mk_pp(t, m) << " |-> " << mk_pp(vl, m) << "\n";);
reduce_value(model, vl);
if (!m.is_value(vl)) {

16
src/smt/smt_internalizer.cpp
View file

@ -34,9 +34,10 @@ namespace smt {
switch (to_app(n)->get_decl_kind()) {
case OP_AND:
case OP_OR:
case OP_IFF:
case OP_ITE:
return true;
case OP_EQ:
return m.is_bool(to_app(n)->get_arg(0));
default:
return false;
}
@ -229,7 +230,7 @@ namespace smt {
add_or_rel_watches(to_app(n));
break;
}
case OP_IFF: {
case OP_EQ: {
expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1);
internalize(lhs, true);
@ -381,7 +382,7 @@ namespace smt {
return;
}
if (m_manager.is_eq(n))
if (m_manager.is_eq(n) && !m_manager.is_iff(n))
internalize_eq(to_app(n), gate_ctx);
else if (m_manager.is_distinct(n))
internalize_distinct(to_app(n), gate_ctx);
@ -538,9 +539,7 @@ namespace smt {
bool _is_gate = is_gate(m_manager, n) || m_manager.is_not(n);
// process args
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = n->get_arg(i);
for (expr * arg : *n) {
internalize(arg, _is_gate);
}
@ -596,8 +595,9 @@ namespace smt {
mk_or_cnstr(to_app(n));
add_or_rel_watches(to_app(n));
break;
case OP_IFF:
mk_iff_cnstr(to_app(n));
case OP_EQ:
if (m_manager.is_iff(n))
mk_iff_cnstr(to_app(n));
break;
case OP_ITE:
mk_ite_cnstr(to_app(n));

9
src/smt/smt_kernel.cpp
View file

@ -115,6 +115,10 @@ namespace smt {
return m_kernel.check(num_assumptions, assumptions);
}
lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clause) {
return m_kernel.check(cube, clause);
}
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
return m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
}
@ -287,6 +291,11 @@ namespace smt {
return r;
}
lbool kernel::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
return m_imp->check(cube, clauses);
}
lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
return m_imp->get_consequences(assumptions, vars, conseq, unfixed);
}

2
src/smt/smt_kernel.h
View file

@ -132,6 +132,8 @@ namespace smt {
lbool check(app_ref_vector const& asms) { return check(asms.size(), (expr* const*)asms.c_ptr()); }
lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses);
/**
\brief extract consequences among variables.
*/

2
src/smt/smt_model_checker.cpp
View file

@ -439,7 +439,7 @@ namespace smt {
}
else if (!check(q)) {
if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
IF_VERBOSE(0, verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n");
}
TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";);
num_failures++;

5
src/smt/smt_model_finder.cpp
View file

@ -1028,7 +1028,7 @@ namespace smt {
void complete_partial_funcs(func_decl_set const & partial_funcs) {
for (func_decl * f : partial_funcs) {
// Complete the current interpretation
m_model->complete_partial_func(f);
m_model->complete_partial_func(f, true);
unsigned arity = f->get_arity();
func_interp * fi = m_model->get_func_interp(f);
@ -2315,9 +2315,6 @@ namespace smt {
case OP_ITE:
process_ite(to_app(curr), pol);
break;
case OP_IFF:
process_iff(to_app(curr));
break;
case OP_EQ:
if (m_manager.is_bool(to_app(curr)->get_arg(0))) {
process_iff(to_app(curr));

12
src/smt/smt_quantifier_stat.cpp
View file

@ -82,11 +82,13 @@ namespace smt {
if (depth > 0)
m_case_split_factor *= (num_args + 1);
break;
case OP_IFF:
if (depth == 0)
m_case_split_factor *= 4;
else
m_case_split_factor *= 9;
case OP_EQ:
if (m_manager.is_iff(n)) {
if (depth == 0)
m_case_split_factor *= 4;
else
m_case_split_factor *= 9;
}
break;
case OP_ITE:
if (depth == 0)

12
src/smt/smt_quick_checker.cpp
View file

@ -312,11 +312,6 @@ namespace smt {
return is_true ? any_arg(a, true) : all_args(a, false);
case OP_AND:
return is_true ? all_args(a, true) : any_arg(a, false);
case OP_IFF:
if (is_true)
return (check(a->get_arg(0), true) && check(a->get_arg(1), true)) || (check(a->get_arg(0), false) && check(a->get_arg(1), false));
else
return (check(a->get_arg(0), true) && check(a->get_arg(1), false)) || (check(a->get_arg(0), false) && check(a->get_arg(1), true));
case OP_ITE:
if (check(a->get_arg(0), true))
return check(a->get_arg(1), is_true);
@ -325,6 +320,13 @@ namespace smt {
else
return check(a->get_arg(1), is_true) && check(a->get_arg(2), is_true);
case OP_EQ:
if (m_manager.is_iff(a)) {
if (is_true)
return (check(a->get_arg(0), true) && check(a->get_arg(1), true)) || (check(a->get_arg(0), false) && check(a->get_arg(1), false));
else
return (check(a->get_arg(0), true) && check(a->get_arg(1), false)) || (check(a->get_arg(0), false) && check(a->get_arg(1), true));
}
if (is_true) {
return canonize(a->get_arg(0)) == canonize(a->get_arg(1));
}

25
src/smt/smt_setup.cpp
View file

@ -574,19 +574,19 @@ namespace smt {
m_params.m_bv_cc = false;
m_params.m_bb_ext_gates = true;
m_params.m_nnf_cnf = false;
m_params.m_propagate_booleans = true;
m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params));
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_QF_AX() {
TRACE("setup", tout << "QF_AX\n";);
m_params.m_array_mode = AR_SIMPLE;
m_params.m_nnf_cnf = false;
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_QF_AX(static_features const & st) {
m_params.m_array_mode = AR_SIMPLE;
m_params.m_array_mode = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
m_params.m_nnf_cnf = false;
if (st.m_num_clauses == st.m_num_units) {
m_params.m_relevancy_lvl = 0;
@ -595,7 +595,7 @@ namespace smt {
else {
m_params.m_relevancy_lvl = 2;
}
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_QF_AUFLIA() {
@ -607,11 +607,11 @@ namespace smt {
m_params.m_restart_factor = 1.5;
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
setup_i_arith();
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_QF_AUFLIA(static_features const & st) {
m_params.m_array_mode = AR_SIMPLE;
m_params.m_array_mode = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
if (st.m_has_real)
throw default_exception("Benchmark has real variables but it is marked as QF_AUFLIA (arrays, uninterpreted functions and linear integer arithmetic).");
m_params.m_nnf_cnf = false;
@ -631,7 +631,7 @@ namespace smt {
// m_context.register_plugin(new smt::theory_si_arith(m_manager, m_params));
// else
setup_i_arith();
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_AUFLIA(bool simple_array) {
@ -643,7 +643,6 @@ namespace smt {
m_params.m_restart_factor = 1.5;
m_params.m_eliminate_bounds = true;
m_params.m_qi_quick_checker = MC_UNSAT;
m_params.m_propagate_booleans = true;
m_params.m_qi_lazy_threshold = 20;
// m_params.m_qi_max_eager_multipatterns = 10; /// <<< HACK
m_params.m_mbqi = true; // enabling MBQI and MACRO_FINDER by default :-)
@ -671,7 +670,6 @@ namespace smt {
m_params.m_phase_selection = PS_ALWAYS_FALSE;
m_params.m_eliminate_bounds = true;
m_params.m_qi_quick_checker = MC_UNSAT;
m_params.m_propagate_booleans = true;
m_params.m_qi_eager_threshold = 5;
// Added for MBQI release
m_params.m_qi_lazy_threshold = 20;
@ -732,6 +730,7 @@ namespace smt {
}
void setup::setup_i_arith() {
// m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
}
@ -992,17 +991,17 @@ namespace smt {
}
if (st.num_theories() == 1 && st.m_has_arrays) {
setup_QF_AX();
setup_QF_AX(st);
return;
}
if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_bv) {
if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && !st.m_has_ext_arrays && st.m_has_bv) {
setup_QF_AUFBV();
return;
}
if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_int) {
setup_QF_AUFLIA();
setup_QF_AUFLIA(st);
return;
}

41
src/smt/smt_solver.cpp
View file

@ -110,14 +110,28 @@ namespace smt {
void updt_params(params_ref const & p) override {
solver::updt_params(p);
m_smt_params.updt_params(p);
m_context.updt_params(p);
smt_params_helper smth(p);
m_smt_params.updt_params(solver::get_params());
m_context.updt_params(solver::get_params());
smt_params_helper smth(solver::get_params());
m_core_extend_patterns = smth.core_extend_patterns();
m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
m_core_extend_nonlocal_patterns = smth.core_extend_nonlocal_patterns();
}
params_ref m_params_save;
smt_params m_smt_params_save;
void push_params() override {
m_params_save = params_ref();
m_params_save.copy(solver::get_params());
m_smt_params_save = m_smt_params;
}
void pop_params() override {
m_smt_params = m_smt_params_save;
solver::reset_params(m_params_save);
}
void collect_param_descrs(param_descrs & r) override {
m_context.collect_param_descrs(r);
}
@ -176,6 +190,11 @@ namespace smt {
return m_context.check(num_assumptions, assumptions);
}
lbool check_sat_cc_core(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) override {
return m_context.check(cube, clauses);
}
struct scoped_minimize_core {
smt_solver& s;
expr_ref_vector m_assumptions;
@ -190,17 +209,17 @@ namespace smt {
}
};
void get_unsat_core(ptr_vector<expr> & r) override {
void get_unsat_core(expr_ref_vector & r) override {
unsigned sz = m_context.get_unsat_core_size();
for (unsigned i = 0; i < sz; i++) {
r.push_back(m_context.get_unsat_core_expr(i));
}
if (m_minimizing_core && smt_params_helper(get_params()).core_minimize()) {
if (!m_minimizing_core && smt_params_helper(get_params()).core_minimize()) {
scoped_minimize_core scm(*this);
mus mus(*this);
mus.add_soft(r.size(), r.c_ptr());
ptr_vector<expr> r2;
expr_ref_vector r2(m);
if (l_true == mus.get_mus(r2)) {
r.reset();
r.append(r2);
@ -314,7 +333,7 @@ namespace smt {
for_each_expr(p, visited, e);
}
void compute_assrtn_fds(ptr_vector<expr> & core, vector<func_decl_set> & assrtn_fds) {
void compute_assrtn_fds(expr_ref_vector & core, vector<func_decl_set> & assrtn_fds) {
assrtn_fds.resize(m_name2assertion.size());
unsigned i = 0;
for (auto & kv : m_name2assertion) {
@ -335,7 +354,7 @@ namespace smt {
return false;
}
void add_pattern_literals_to_core(ptr_vector<expr> & core) {
void add_pattern_literals_to_core(expr_ref_vector & core) {
ast_manager & m = get_manager();
expr_ref_vector new_core_literals(m);
@ -394,7 +413,7 @@ namespace smt {
for_each_expr(p, visited, e);
}
void add_nonlocal_pattern_literals_to_core(ptr_vector<expr> & core) {
void add_nonlocal_pattern_literals_to_core(expr_ref_vector & core) {
ast_manager & m = get_manager();
for (auto const& kv : m_name2assertion) {
expr_ref name(kv.m_key, m);
@ -406,8 +425,8 @@ namespace smt {
collect_body_func_decls(assrtn, body_fds);
for (func_decl *fd : pattern_fds) {
if (!body_fds.contains(fd)) {
core.insert(name);
if (!body_fds.contains(fd) && !core.contains(name)) {
core.push_back(name);
break;
}
}

502
src/smt/theory_arith_core.h
View file

File diff suppressed because it is too large Load diff

2
src/smt/theory_fpa.h
View file

@ -62,7 +62,7 @@ namespace smt {
return true;
}
expr * get_fresh_value(sort * s) override { NOT_IMPLEMENTED_YET(); }
expr * get_fresh_value(sort * s) override { return get_some_value(s); }
void register_value(expr * n) override { /* Ignore */ }
app * mk_value(mpf const & x) {

2
src/smt/theory_pb.cpp
View file

@ -2251,7 +2251,7 @@ namespace smt {
for (unsigned i = 2; i < num_lits; ++i) {
process_antecedent(cls.get_literal(i), offset);
}
TRACE("pb", tout << literal_vector(cls.get_num_literals(), cls.begin_literals()) << "\n";);
TRACE("pb", tout << literal_vector(cls.get_num_literals(), cls.begin()) << "\n";);
break;
}
case b_justification::BIN_CLAUSE:

63
src/smt/theory_seq.cpp
View file

@ -712,12 +712,30 @@ unsigned theory_seq::find_branch_start(unsigned k) {
return 0;
}
bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs) {
expr_ref_vector theory_seq::expand_strings(expr_ref_vector const& es) {
expr_ref_vector ls(m);
for (expr* e : es) {
zstring s;
if (m_util.str.is_string(e, s)) {
for (unsigned i = 0; i < s.length(); ++i) {
ls.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, i)));
}
}
else {
ls.push_back(e);
}
}
return ls;
}
bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& _ls, expr_ref_vector const& _rs) {
expr_ref_vector ls = expand_strings(_ls);
expr_ref_vector rs = expand_strings(_rs);
if (ls.empty()) {
return false;
}
expr* l = ls[0];
expr* l = ls.get(0);
if (!is_var(l)) {
return false;
@ -735,9 +753,9 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
}
for (; start < rs.size(); ++start) {
unsigned j = start;
SASSERT(!m_util.str.is_concat(rs[j]));
SASSERT(!m_util.str.is_string(rs[j]));
if (l == rs[j]) {
SASSERT(!m_util.str.is_concat(rs.get(j)));
SASSERT(!m_util.str.is_string(rs.get(j)));
if (l == rs.get(j)) {
return false;
}
if (!can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - j - 1, rs.c_ptr() + j + 1)) {
@ -752,8 +770,11 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
}
bool all_units = true;
for (unsigned j = 0; all_units && j < rs.size(); ++j) {
all_units &= m_util.str.is_unit(rs[j]);
for (expr* r : rs) {
if (!m_util.str.is_unit(r)) {
all_units = false;
break;
}
}
if (all_units) {
context& ctx = get_context();
@ -765,20 +786,20 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
lits.push_back(~mk_eq(l, v0, false));
}
}
for (unsigned i = 0; i < lits.size(); ++i) {
switch (ctx.get_assignment(lits[i])) {
for (literal lit : lits) {
switch (ctx.get_assignment(lit)) {
case l_true: break;
case l_false: start = 0; return true;
case l_undef: ctx.force_phase(~lits[i]); start = 0; return true;
case l_undef: ctx.force_phase(~lit); start = 0; return true;
}
}
set_conflict(dep, lits);
TRACE("seq",
tout << "start: " << start << "\n";
for (unsigned i = 0; i < lits.size(); ++i) {
ctx.display_literal_verbose(tout << lits[i] << ": ", lits[i]);
for (literal lit : lits) {
ctx.display_literal_verbose(tout << lit << ": ", lit);
tout << "\n";
ctx.display(tout, ctx.get_justification(lits[i].var()));
ctx.display(tout, ctx.get_justification(lit.var()));
tout << "\n";
});
return true;
@ -2251,7 +2272,6 @@ bool theory_seq::internalize_term(app* term) {
e = ctx.mk_enode(term, false, m.is_bool(term), true);
}
mk_var(e);
return true;
}
@ -2905,6 +2925,9 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){
}
result = ed.first;
}
else if (false && m_util.str.is_string(e)) {
result = add_elim_string_axiom(e);
}
else {
m_expand_todo.push_back(e);
}
@ -2927,7 +2950,7 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
}
else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
result = e;
}
}
else if (m_util.str.is_prefix(e, e1, e2)) {
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);
@ -3086,6 +3109,7 @@ void theory_seq::propagate() {
void theory_seq::enque_axiom(expr* e) {
if (!m_axiom_set.contains(e)) {
TRACE("seq", tout << "add axiom " << mk_pp(e, m) << "\n";);
m_axioms.push_back(e);
m_axiom_set.insert(e);
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_axioms));
@ -3283,20 +3307,21 @@ void theory_seq::add_replace_axiom(expr* r) {
tightest_prefix(s, x);
}
void theory_seq::add_elim_string_axiom(expr* n) {
expr_ref theory_seq::add_elim_string_axiom(expr* n) {
zstring s;
TRACE("seq", tout << mk_pp(n, m) << "\n";);
VERIFY(m_util.str.is_string(n, s));
if (s.length() == 0) {
return;
return expr_ref(n, m);
}
expr_ref result(m_util.str.mk_unit(m_util.str.mk_char(s, s.length()-1)), m);
for (unsigned i = s.length()-1; i > 0; ) {
--i;
for (unsigned i = s.length()-1; i-- > 0; ) {
result = mk_concat(m_util.str.mk_unit(m_util.str.mk_char(s, i)), result);
}
add_axiom(mk_eq(n, result, false));
m_rep.update(n, result, nullptr);
m_new_solution = true;
return result;
}

3
src/smt/theory_seq.h
View file

@ -447,6 +447,7 @@ namespace smt {
void insert_branch_start(unsigned k, unsigned s);
unsigned find_branch_start(unsigned k);
bool find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs);
expr_ref_vector expand_strings(expr_ref_vector const& es);
bool can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const;
lbool assume_equality(expr* l, expr* r);
@ -504,7 +505,7 @@ namespace smt {
void add_int_string(expr* e);
bool check_int_string();
void add_elim_string_axiom(expr* n);
expr_ref add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n);
void add_in_re_axiom(expr* n);
void add_itos_axiom(expr* n);

7
src/smt/theory_str.cpp
View file

@ -8388,13 +8388,12 @@ 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);
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
enode * e1;
enode * e2;
e1 = get_context().get_enode(target_term);
e2 = get_context().get_enode(core_term);
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;);
return l_undef;