mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-06-15 14:58:10 -07:00
commit 6fc08e9c9f
236 changed files with 14093 additions and 16593 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) {

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();
}

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;

326
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
@ -627,7 +627,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;
@ -672,7 +672,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();
@ -1002,7 +1002,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;
@ -1197,7 +1197,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()))) {
@ -1229,7 +1229,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())
@ -1239,7 +1239,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())
@ -1277,7 +1277,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())
@ -1288,7 +1288,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())
@ -1813,6 +1813,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);
@ -2152,7 +2163,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);
}
/**
@ -2907,6 +2918,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());
@ -3049,12 +3061,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";);
@ -3087,32 +3134,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;
}
@ -3120,11 +3151,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
@ -3134,18 +3223,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
@ -3155,8 +3247,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() {
@ -3165,7 +3258,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());
@ -3182,18 +3276,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) {
@ -3217,6 +3309,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;
}
@ -3240,8 +3336,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);
@ -3254,20 +3349,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;
}
@ -3281,7 +3364,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();
@ -3316,78 +3399,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;
@ -3450,6 +3500,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());
@ -3473,24 +3529,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
@ -3643,6 +3694,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) {
@ -3700,6 +3753,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);
@ -4228,7 +4282,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";);

21
src/smt/smt_context.h
View file

@ -168,6 +168,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
@ -892,7 +894,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;
@ -1104,15 +1105,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();
@ -1497,6 +1506,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);
@ -1524,6 +1535,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())

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: {

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.
*/

3
src/smt/smt_model_finder.cpp
View file

@ -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

@ -311,11 +311,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);
@ -324,6 +319,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));
}

4
src/smt/smt_setup.cpp
View file

@ -574,7 +574,6 @@ 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));
setup_arrays();
}
@ -644,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 :-)
@ -672,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;
@ -733,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));
}

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;
}
}

469
src/smt/theory_arith_core.h
View file

File diff suppressed because it is too large Load diff

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: