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' into develop

Browse source
This commit is contained in:
Murphy Berzish 2018-08-07 12:57:02 -04:00
commit 7a84486df2
206 changed files with 3045 additions and 1887 deletions
Download patch file Download diff file Expand all files Collapse all files

58
src/smt/mam.cpp
View file

@ -401,7 +401,7 @@ namespace smt {
label_hasher & m_lbl_hasher;
func_decl * m_root_lbl;
unsigned m_num_args; //!< we need this information to avoid the nary *,+ crash bug
unsigned char m_filter_candidates;
bool m_filter_candidates;
unsigned m_num_regs;
unsigned m_num_choices;
instruction * m_root;
@ -531,7 +531,7 @@ namespace smt {
}
bool filter_candidates() const {
return m_filter_candidates != 0;
return m_filter_candidates;
}
const instruction * get_root() const {
@ -1847,7 +1847,10 @@ namespace smt {
enode * m_n2;
enode * m_app;
const bind * m_b;
ptr_vector<enode> m_used_enodes;
// equalities used for pattern match. The first element of the tuple gives the argument (or null) of some term that was matched against some higher level
// structure of the trigger, the second element gives the term that argument is replaced with in order to match the trigger. Used for logging purposes only.
vector<std::tuple<enode *, enode *>> m_used_enodes;
unsigned m_curr_used_enodes_size;
ptr_vector<enode> m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation
unsigned_vector m_min_top_generation, m_max_top_generation;
@ -1864,11 +1867,11 @@ namespace smt {
m_pool.recycle(v);
}
void update_max_generation(enode * n) {
void update_max_generation(enode * n, enode * prev) {
m_max_generation = std::max(m_max_generation, n->get_generation());
if (m_ast_manager.has_trace_stream())
m_used_enodes.push_back(n);
m_used_enodes.push_back(std::make_tuple(prev, n));
}
// We have to provide the number of expected arguments because we have flat-assoc applications such as +.
@ -1877,7 +1880,7 @@ namespace smt {
enode * first = curr;
do {
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
update_max_generation(curr);
update_max_generation(curr, first);
return curr;
}
curr = curr->get_next();
@ -1890,7 +1893,7 @@ namespace smt {
curr = curr->get_next();
while (curr != first) {
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
update_max_generation(curr);
update_max_generation(curr, first);
return curr;
}
curr = curr->get_next();
@ -1914,7 +1917,7 @@ namespace smt {
do {
if (n->get_decl() == f &&
n->get_arg(0)->get_root() == m_args[0]) {
update_max_generation(n);
update_max_generation(n, first);
return true;
}
n = n->get_next();
@ -1929,7 +1932,7 @@ namespace smt {
if (n->get_decl() == f &&
n->get_arg(0)->get_root() == m_args[0] &&
n->get_arg(1)->get_root() == m_args[1]) {
update_max_generation(n);
update_max_generation(n, first);
return true;
}
n = n->get_next();
@ -1949,7 +1952,7 @@ namespace smt {
break;
}
if (i == num_args) {
update_max_generation(n);
update_max_generation(n, first);
return true;
}
}
@ -1975,10 +1978,10 @@ namespace smt {
#define INIT_ARGS_SIZE 16
public:
interpreter(context & ctx, mam & m, bool use_filters):
interpreter(context & ctx, mam & ma, bool use_filters):
m_context(ctx),
m_ast_manager(ctx.get_manager()),
m_mam(m),
m_mam(ma),
m_use_filters(use_filters) {
m_args.resize(INIT_ARGS_SIZE);
}
@ -1999,6 +2002,7 @@ namespace smt {
init(t);
if (t->filter_candidates()) {
for (enode* app : t->get_candidates()) {
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
if (!app->is_marked() && app->is_cgr()) {
if (m_context.resource_limits_exceeded() || !execute_core(t, app))
return;
@ -2196,7 +2200,7 @@ namespace smt {
if (bp.m_it == bp.m_end)
return nullptr;
m_top++;
update_max_generation(*(bp.m_it));
update_max_generation(*(bp.m_it), nullptr);
return *(bp.m_it);
}
@ -2277,7 +2281,7 @@ namespace smt {
if (m_ast_manager.has_trace_stream()) {
m_used_enodes.reset();
m_used_enodes.push_back(n);
m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level
}
m_pc = t->get_root();
@ -2382,6 +2386,10 @@ namespace smt {
SASSERT(m_n2 != 0);
if (m_n1->get_root() != m_n2->get_root())
goto backtrack;
// we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log
m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
m_pc = m_pc->m_next;
goto main_loop;
@ -2776,7 +2784,7 @@ namespace smt {
m_pattern_instances.pop_back();
m_pattern_instances.push_back(m_app);
// continue succeeded
update_max_generation(m_app);
update_max_generation(m_app, nullptr); // null indicates a top-level match
TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager););
m_num_args = c->m_num_args;
m_oreg = c->m_oreg;
@ -2830,7 +2838,7 @@ namespace smt {
mk_tree_trail(ptr_vector<code_tree> & t, unsigned id):m_trees(t), m_lbl_id(id) {}
void undo(mam_impl & m) override {
dealloc(m_trees[m_lbl_id]);
m_trees[m_lbl_id] = 0;
m_trees[m_lbl_id] = nullptr;
}
};
@ -2863,8 +2871,8 @@ namespace smt {
app * p = to_app(mp->get_arg(first_idx));
func_decl * lbl = p->get_decl();
unsigned lbl_id = lbl->get_decl_id();
m_trees.reserve(lbl_id+1, 0);
if (m_trees[lbl_id] == 0) {
m_trees.reserve(lbl_id+1, nullptr);
if (m_trees[lbl_id] == nullptr) {
m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false);
SASSERT(m_trees[lbl_id]->expected_num_args() == p->get_num_args());
DEBUG_CODE(m_trees[lbl_id]->set_context(m_context););
@ -2949,7 +2957,7 @@ namespace smt {
m_ground_arg(ground_arg),
m_pattern_idx(pat_idx),
m_child(child) {
SASSERT(ground_arg != 0 || ground_arg_idx == 0);
SASSERT(ground_arg != nullptr || ground_arg_idx == 0);
}
};
@ -3216,7 +3224,7 @@ namespace smt {
path_tree * mk_path_tree(path * p, quantifier * qa, app * mp) {
SASSERT(m_ast_manager.is_pattern(mp));
SASSERT(p != 0);
SASSERT(p != nullptr);
unsigned pat_idx = p->m_pattern_idx;
path_tree * head = nullptr;
path_tree * curr = nullptr;
@ -3509,9 +3517,7 @@ namespace smt {
std::cout << "Avg. " << static_cast<double>(total_sz)/static_cast<double>(counter) << ", Max. " << max_sz << "\n";
#endif
enode_vector::iterator it1 = v->begin();
enode_vector::iterator end1 = v->end();
for (; it1 != end1; ++it1) {
for (enode* n : *v) {
// Two different kinds of mark are used:
// - enode mark field: it is used to mark the already processed parents.
// - enode mark2 field: it is used to mark the roots already added to be processed in the next level.
@ -3520,7 +3526,7 @@ namespace smt {
// and Z3 may fail to find potential new matches.
//
// The file regression\acu.sx exposed this problem.
enode * curr_child = (*it1)->get_root();
enode * curr_child = n->get_root();
if (m_use_filters && curr_child->get_plbls().empty_intersection(filter))
continue;
@ -3584,7 +3590,7 @@ namespace smt {
is_eq(curr_tree->m_ground_arg, curr_parent->get_arg(curr_tree->m_ground_arg_idx))
)) {
if (curr_tree->m_code) {
TRACE("mam_path_tree", tout << "found candidate\n";);
TRACE("mam_path_tree", tout << "found candidate " << expr_ref(curr_parent->get_owner(), m_ast_manager) << "\n";);
add_candidate(curr_tree->m_code, curr_parent);
}
if (curr_tree->m_first_child) {
@ -3878,7 +3884,7 @@ namespace smt {
}
#endif
void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) override {
void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) override {
TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";);
#ifdef Z3DEBUG
if (m_check_missing_instances) {

3
src/smt/mam.h
View file

@ -21,6 +21,7 @@ Revision History:
#include "ast/ast.h"
#include "smt/smt_types.h"
#include <tuple>
namespace smt {
/**
@ -57,7 +58,7 @@ namespace smt {
virtual void display(std::ostream& out) = 0;
virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) = 0;
virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) = 0;
virtual bool is_shared(enode * n) const = 0;

15
src/smt/old_interval.cpp
View file

@ -561,15 +561,24 @@ interval & interval::operator/=(interval const & other) {
TRACE("interval", other.display_with_dependencies(tout););
if (other.m_lower.is_pos() || (other.m_lower.is_zero() && other.m_lower_open)) {
// other.lower > 0
// x in ([0, 0] / [other.lo, other.up]), for other.lo > 0
// <=>
// x >= 0: because y*x >= 0 & y > 0
// x <= 0: because y*x <= 0 & y > 0
m_lower_dep = join(m_lower_dep, other.m_lower_dep);
m_upper_dep = join(m_upper_dep, other.m_lower_dep);
}
else {
// assertion must hold since !other.contains_zero()
SASSERT(other.m_upper.is_neg() || (other.m_upper.is_zero() && other.m_upper_open));
SASSERT(other.m_upper.is_neg() || (other.m_upper.is_zero() && other.m_upper_open));
// other.upper < 0
m_lower_dep = join(m_lower_dep, other.m_upper_dep);
m_upper_dep = join(m_upper_dep, other.m_upper_dep);
// x in ([0, 0] / [other.lo, other.up]), for up < 0
// <=>
// x >= 0: because y*x <= 0 & y < 0
// x <= 0: because y*x >= 0 & y < 0
v_dependency* lower_dep = m_lower_dep;
m_lower_dep = join(m_upper_dep, other.m_upper_dep);
m_upper_dep = join(lower_dep, other.m_upper_dep);
}
return *this;
}

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

@ -19,7 +19,7 @@ Revision History:
#ifndef THEORY_ARITH_PARAMS_H_
#define THEORY_ARITH_PARAMS_H_
#include<limits.h>
#include<climits>
#include "util/params.h"
enum arith_solver_id {

63
src/smt/smt_context.cpp
View file

@ -51,6 +51,7 @@ namespace smt {
m_relevancy_propagator(mk_relevancy_propagator(*this)),
m_random(p.m_random_seed),
m_flushing(false),
m_lemma_id(0),
m_progress_callback(nullptr),
m_next_progress_sample(0),
m_fingerprints(m, m_region),
@ -227,7 +228,6 @@ namespace smt {
}
void context::copy_plugins(context& src, context& dst) {
// copy theory plugins
for (theory* old_th : src.m_theory_set) {
theory * new_th = old_th->mk_fresh(&dst);
@ -235,8 +235,8 @@ namespace smt {
}
}
context * context::mk_fresh(symbol const * l, smt_params * p) {
context * new_ctx = alloc(context, m_manager, p == nullptr ? m_fparams : *p);
context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) {
context * new_ctx = alloc(context, m_manager, p ? *p : m_fparams, pa);
new_ctx->set_logic(l == nullptr ? m_setup.get_logic() : *l);
copy_plugins(*this, *new_ctx);
return new_ctx;
@ -562,6 +562,7 @@ namespace smt {
invert_trans(n1);
n1->m_trans.m_target = n2;
n1->m_trans.m_justification = js;
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
SASSERT(r1->trans_reaches(n1));
// ---------------
// r1 -> .. -> n1 -> n2 -> ... -> r2
@ -741,12 +742,14 @@ namespace smt {
eq_justification js = n->m_trans.m_justification;
prev->m_trans.m_target = nullptr;
prev->m_trans.m_justification = null_eq_justification;
prev->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
while (curr != nullptr) {
SASSERT(prev->trans_reaches(n));
enode * new_curr = curr->m_trans.m_target;
eq_justification new_js = curr->m_trans.m_justification;
curr->m_trans.m_target = prev;
curr->m_trans.m_justification = js;
curr->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
prev = curr;
js = new_js;
curr = new_curr;
@ -1040,6 +1043,7 @@ namespace smt {
SASSERT(r1->trans_reaches(n1));
n1->m_trans.m_target = nullptr;
n1->m_trans.m_justification = null_eq_justification;
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
invert_trans(r1);
// ---------------
// n1 -> ... -> r1
@ -1346,18 +1350,9 @@ namespace smt {
\remark The method assign_eq adds a new entry on this queue.
*/
bool context::propagate_eqs() {
for (unsigned i = 0; i < m_eq_propagation_queue.size(); i++) {
TRACE("add_eq", tout << m_eq_propagation_queue.size() << "\n";);
for (unsigned i = 0; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) {
new_eq & entry = m_eq_propagation_queue[i];
#if 0
static unsigned counter1 = 0;
static unsigned counter2 = 0;
if (entry.m_lhs->is_eq() || entry.m_rhs->is_eq())
counter1++;
else
counter2++;
if ((counter1 + counter2) % 10000 == 0)
std::cout << counter1 << " " << counter2 << "\n";
#endif
add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification);
if (inconsistent())
return false;
@ -1371,7 +1366,7 @@ namespace smt {
*/
bool context::propagate_atoms() {
SASSERT(!inconsistent());
for (unsigned i = 0; i < m_atom_propagation_queue.size(); i++) {
for (unsigned i = 0; i < m_atom_propagation_queue.size() && !get_cancel_flag(); i++) {
SASSERT(!inconsistent());
literal l = m_atom_propagation_queue[i];
bool_var v = l.var();
@ -1553,16 +1548,17 @@ namespace smt {
lbool context::get_assignment(expr * n) const {
if (m_manager.is_false(n))
return l_false;
if (m_manager.is_not(n))
return ~get_assignment_core(to_app(n)->get_arg(0));
expr* arg = nullptr;
if (m_manager.is_not(n, arg))
return ~get_assignment_core(arg);
return get_assignment_core(n);
}
lbool context::find_assignment(expr * n) const {
if (m_manager.is_false(n))
return l_false;
if (m_manager.is_not(n)) {
expr * arg = to_app(n)->get_arg(0);
expr* arg = nullptr;
if (m_manager.is_not(n, arg)) {
if (b_internalized(arg))
return ~get_assignment_core(arg);
return l_undef;
@ -1747,6 +1743,10 @@ namespace smt {
return false;
if (!propagate_eqs())
return false;
if (get_cancel_flag()) {
m_qhead = qhead;
return true;
}
propagate_th_eqs();
propagate_th_diseqs();
if (inconsistent())
@ -1786,7 +1786,7 @@ namespace smt {
}
bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes) {
unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode *>> & used_enodes) {
return m_qmanager->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes);
}
@ -2877,6 +2877,7 @@ namespace smt {
void context::push() {
TRACE("trigger_bug", tout << "context::push()\n";);
scoped_suspend_rlimit _suspend_cancel(m_manager.limit());
pop_to_base_lvl();
setup_context(false);
bool was_consistent = !inconsistent();
@ -3182,6 +3183,7 @@ namespace smt {
if (m_tmp_clauses.empty()) return l_true;
for (auto & tmp_clause : m_tmp_clauses) {
literal_vector& lits = tmp_clause.second;
literal unassigned = null_literal;
for (literal l : lits) {
switch (get_assignment(l)) {
case l_false:
@ -3189,13 +3191,17 @@ namespace smt {
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;
unassigned = l;
}
}
if (unassigned != null_literal) {
shuffle(lits.size(), lits.c_ptr(), m_random);
push_scope();
assign(unassigned, b_justification::mk_axiom(), true);
return l_undef;
}
if (lits.size() == 1) {
set_conflict(b_justification(), ~lits[0]);
}
@ -3254,6 +3260,7 @@ namespace smt {
}
void context::reset_assumptions() {
TRACE("unsat_core_bug", tout << "reset " << m_assumptions << "\n";);
for (literal lit : m_assumptions)
get_bdata(lit.var()).m_assumption = false;
m_assumptions.reset();
@ -4096,9 +4103,7 @@ namespace smt {
}
SASSERT(!inconsistent());
unsigned sz = m_b_internalized_stack.size();
for (unsigned i = 0; i < sz; i++) {
expr * curr = m_b_internalized_stack.get(i);
for (expr * curr : m_b_internalized_stack) {
if (is_relevant(curr) && get_assignment(curr) == l_true) {
// if curr is a label literal, then its tags will be copied to result.
m_manager.is_label_lit(curr, result);
@ -4114,9 +4119,7 @@ namespace smt {
void context::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
SASSERT(!inconsistent());
buffer<symbol> lbls;
unsigned sz = m_b_internalized_stack.size();
for (unsigned i = 0; i < sz; i++) {
expr * curr = m_b_internalized_stack.get(i);
for (expr * curr : m_b_internalized_stack) {
if (is_relevant(curr) && get_assignment(curr) == l_true) {
lbls.reset();
if (m_manager.is_label_lit(curr, lbls)) {

13
src/smt/smt_context.h
View file

@ -49,6 +49,7 @@ Revision History:
#include "util/timer.h"
#include "util/statistics.h"
#include "solver/progress_callback.h"
#include <tuple>
// there is a significant space overhead with allocating 1000+ contexts in
// the case that each context only references a few expressions.
@ -87,6 +88,7 @@ namespace smt {
scoped_ptr<relevancy_propagator> m_relevancy_propagator;
random_gen m_random;
bool m_flushing; // (debug support) true when flushing
mutable unsigned m_lemma_id;
progress_callback * m_progress_callback;
unsigned m_next_progress_sample;
@ -489,7 +491,7 @@ namespace smt {
}
bool tracking_assumptions() const {
return m_search_lvl > m_base_lvl;
return !m_assumptions.empty() && m_search_lvl > m_base_lvl;
}
expr * bool_var2expr(bool_var v) const {
@ -970,7 +972,7 @@ namespace smt {
bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes);
unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
void set_global_generation(unsigned generation) { m_generation = generation; }
@ -1009,6 +1011,7 @@ namespace smt {
void push_eq(enode * lhs, enode * rhs, eq_justification const & js) {
SASSERT(lhs != rhs);
SASSERT(lhs->get_root() != rhs->get_root());
m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js));
}
@ -1317,12 +1320,12 @@ namespace smt {
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
literal consequent = false_literal, symbol const& logic = symbol::null) const;
void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
literal consequent = false_literal, symbol const& logic = symbol::null) const;
@ -1490,7 +1493,7 @@ namespace smt {
If l == 0, then the logic of this context is used in the new context.
If p == 0, then this->m_params is used
*/
context * mk_fresh(symbol const * l = nullptr, smt_params * p = nullptr);
context * mk_fresh(symbol const * l = nullptr, smt_params * smtp = nullptr, params_ref const & p = params_ref());
static void copy(context& src, context& dst);

38
src/smt/smt_context_pp.cpp
View file

@ -419,23 +419,16 @@ namespace smt {
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
out << "(check-sat)\n";
}
static unsigned g_lemma_id = 0;
#define BUFFER_SZ 128
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
char buffer[BUFFER_SZ];
#ifdef _WINDOWS
sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt2", g_lemma_id);
#else
sprintf(buffer, "lemma_%d.smt2", g_lemma_id);
#endif
std::ofstream out(buffer);
unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
std::stringstream strm;
strm << "lemma_" << (++m_lemma_id) << ".smt2";
std::ofstream out(strm.str());
display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic);
out.close();
g_lemma_id++;
return m_lemma_id;
}
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
@ -464,21 +457,18 @@ namespace smt {
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
out << "(check-sat)\n";
}
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, symbol const& logic) const {
char buffer[BUFFER_SZ];
#ifdef _WINDOWS
sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt2", g_lemma_id);
#else
sprintf(buffer, "lemma_%d.smt2", g_lemma_id);
#endif
std::ofstream out(buffer);
std::stringstream strm;
strm << "lemma_" << (++m_lemma_id) << ".smt2";
std::ofstream out(strm.str());
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close();
g_lemma_id++;
return m_lemma_id;
}
/**
@ -577,7 +567,7 @@ namespace smt {
case b_justification::BIN_CLAUSE: {
literal l2 = j.get_literal();
out << "bin-clause ";
display_literal_verbose(out, l2);
display_literal(out, l2);
break;
}
case b_justification::CLAUSE: {
@ -590,7 +580,7 @@ namespace smt {
out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals_verbose(out, lits);
display_literals(out, lits);
break;
}
default:

1
src/smt/smt_enode.cpp
View file

@ -47,6 +47,7 @@ namespace smt {
n->m_cgc_enabled = cgc_enabled;
n->m_iscope_lvl = iscope_lvl;
n->m_lbl_hash = -1;
n->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
enode * arg = app2enode[owner->get_arg(i)->get_id()];

15
src/smt/smt_enode.h
View file

@ -38,6 +38,15 @@ namespace smt {
}
};
/**
\brief Indicates whether the proof for membership in an equivalence class is already logged.
*/
enum logged_status {
NOT_LOGGED, //!< Proof is not logged or logged information is not up-to-date.
BEING_LOGGED, //!< We are currently in the process of logging all relevant information. This is used to prevent looping when logging congruence steps.
LOGGED //!< Proof is logged and logged information is still up-to-date.
};
/** \ brief Use sparse maps in SMT solver.
Define this to use hash maps rather than vectors over ast
@ -105,6 +114,7 @@ namespace smt {
enode_vector m_parents; //!< Parent enodes of the equivalence class.
theory_var_list m_th_var_list; //!< List of theories that 'care' about this enode.
trans_justification m_trans; //!< A justification for the enode being equal to its root.
logged_status m_proof_logged_status; //!< Indicates that the proof for the enode being equal to its root is in the log.
signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern
approx_set m_lbls;
approx_set m_plbls;
@ -113,6 +123,7 @@ namespace smt {
friend class context;
friend class euf_manager;
friend class conflict_resolution;
friend class quantifier_manager;
theory_var_list * get_th_var_list() {
@ -361,6 +372,10 @@ namespace smt {
theory_var get_th_var(theory_id th_id) const;
trans_justification get_trans_justification() {
return m_trans;
}
unsigned get_generation() const {
return m_generation;
}

14
src/smt/smt_internalizer.cpp
View file

@ -678,8 +678,18 @@ namespace smt {
push_trail(set_merge_tf_trail(n));
n->m_merge_tf = true;
lbool val = get_assignment(v);
if (val != l_undef)
push_eq(n, val == l_true ? m_true_enode : m_false_enode, eq_justification(literal(v, val == l_false)));
switch (val) {
case l_undef:
break;
case l_true:
if (n->get_root() != m_true_enode->get_root())
push_eq(n, m_true_enode, eq_justification(literal(v, false)));
break;
case l_false:
if (n->get_root() != m_false_enode->get_root())
push_eq(n, m_false_enode, eq_justification(literal(v, true)));
break;
}
}
}

2
src/smt/smt_literal.h
View file

@ -103,7 +103,7 @@ namespace smt {
void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map);
void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = " ");
void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n");
template<typename T>
void neg_literals(unsigned num_lits, literal const * lits, T & result) {

8
src/smt/smt_model_checker.cpp
View file

@ -33,6 +33,7 @@ Revision History:
#include "smt/smt_context.h"
#include "smt/smt_model_finder.h"
#include "model/model_pp.h"
#include <tuple>
namespace smt {
@ -383,10 +384,13 @@ namespace smt {
m_fparams = alloc(smt_params, m_context->get_fparams());
m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3.
m_fparams->m_arith_dump_lemmas = false;
}
if (!m_aux_context) {
symbol logic;
m_aux_context = m_context->mk_fresh(&logic, m_fparams.get());
params_ref p;
p.set_bool("arith.dump_lemmas", false);
m_aux_context = m_context->mk_fresh(&logic, m_fparams.get(), p);
}
}
@ -518,7 +522,7 @@ namespace smt {
void model_checker::assert_new_instances() {
TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";);
ptr_buffer<enode> bindings;
ptr_vector<enode> dummy;
vector<std::tuple<enode *, enode *>> dummy;
for (instance const& inst : m_new_instances) {
quantifier * q = inst.m_q;
if (m_context->b_internalized(q)) {

74
src/smt/smt_model_generator.cpp
View file

@ -28,6 +28,15 @@ Revision History:
namespace smt {
void fresh_value_proc::get_dependencies(buffer<model_value_dependency>& result) {
result.push_back(model_value_dependency(m_value));
}
std::ostream& operator<<(std::ostream& out, model_value_dependency const& src) {
if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx();
else return out << "#" << src.get_enode()->get_owner_id();
}
model_generator::model_generator(ast_manager & m):
m_manager(m),
m_context(nullptr),
@ -161,20 +170,20 @@ namespace smt {
source2color & colors,
obj_hashtable<sort> & already_traversed,
svector<source> & todo) {
if (src.is_fresh_value()) {
// there is an implicit dependency between a fresh value stub of sort S and the root enodes of sort S that are not associated with fresh values.
// there is an implicit dependency between a fresh value stub of
// sort S and the root enodes of sort S that are not associated with fresh values.
//
sort * s = src.get_value()->get_sort();
if (already_traversed.contains(s))
return true;
bool visited = true;
unsigned sz = roots.size();
for (unsigned i = 0; i < sz; i++) {
enode * r = roots[i];
for (enode * r : roots) {
if (m_manager.get_sort(r->get_owner()) != s)
continue;
SASSERT(r == r->get_root());
model_value_proc * proc = nullptr;
root2proc.find(r, proc);
model_value_proc * proc = root2proc[r];
SASSERT(proc);
if (proc->is_fresh())
continue; // r is associated with a fresh value...
@ -192,17 +201,12 @@ namespace smt {
enode * n = src.get_enode();
SASSERT(n == n->get_root());
bool visited = true;
model_value_proc * proc = nullptr;
root2proc.find(n, proc);
SASSERT(proc);
model_value_proc * proc = root2proc[n];
buffer<model_value_dependency> dependencies;
proc->get_dependencies(dependencies);
for (model_value_dependency const& dep : dependencies) {
visit_child(dep, colors, todo, visited);
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> ";
if (dep.is_fresh_value()) tout << "fresh!" << dep.get_value()->get_idx();
else tout << "#" << dep.get_enode()->get_owner_id();
tout << "\n";);
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> " << dep << " already visited: " << visited << "\n";);
}
return visited;
}
@ -215,9 +219,7 @@ namespace smt {
svector<source> & todo,
svector<source> & sorted_sources) {
TRACE("mg_top_sort", tout << "process source, is_fresh: " << src.is_fresh_value() << " ";
if (src.is_fresh_value()) tout << "fresh!" << src.get_value()->get_idx();
else tout << "#" << src.get_enode()->get_owner_id();
tout << ", todo.size(): " << todo.size() << "\n";);
tout << src << ", todo.size(): " << todo.size() << "\n";);
int color = get_color(colors, src);
SASSERT(color != Grey);
if (color == Black)
@ -227,17 +229,16 @@ namespace smt {
while (!todo.empty()) {
source curr = todo.back();
TRACE("mg_top_sort", tout << "current source, is_fresh: " << curr.is_fresh_value() << " ";
if (curr.is_fresh_value()) tout << "fresh!" << curr.get_value()->get_idx();
else tout << "#" << curr.get_enode()->get_owner_id();
tout << ", todo.size(): " << todo.size() << "\n";);
tout << curr << ", todo.size(): " << todo.size() << "\n";);
switch (get_color(colors, curr)) {
case White:
set_color(colors, curr, Grey);
visit_children(curr, roots, root2proc, colors, already_traversed, todo);
break;
case Grey:
SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo));
// SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo));
set_color(colors, curr, Black);
TRACE("mg_top_sort", tout << "append " << curr << "\n";);
sorted_sources.push_back(curr);
break;
case Black:
@ -266,18 +267,15 @@ namespace smt {
// topological sort
// traverse all extra fresh values...
unsigned sz = m_extra_fresh_values.size();
for (unsigned i = 0; i < sz; i++) {
extra_fresh_value * f = m_extra_fresh_values[i];
for (extra_fresh_value * f : m_extra_fresh_values) {
process_source(source(f), roots, root2proc, colors, already_traversed, todo, sorted_sources);
}
// traverse all enodes that are associated with fresh values...
sz = roots.size();
unsigned sz = roots.size();
for (unsigned i = 0; i < sz; i++) {
enode * r = roots[i];
model_value_proc * proc = nullptr;
root2proc.find(r, proc);
model_value_proc * proc = root2proc[r];
SASSERT(proc);
if (!proc->is_fresh())
continue;
@ -303,43 +301,38 @@ namespace smt {
TRACE("sorted_sources",
for (source const& curr : sources) {
if (curr.is_fresh_value()) {
tout << "fresh!" << curr.get_value()->get_idx() << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n";
tout << curr << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n";
}
else {
enode * n = curr.get_enode();
SASSERT(n->get_root() == n);
sort * s = m_manager.get_sort(n->get_owner());
tout << "#" << n->get_owner_id() << " " << mk_pp(s, m_manager);
model_value_proc * proc = 0;
root2proc.find(n, proc);
SASSERT(proc);
tout << " is_fresh: " << proc->is_fresh() << "\n";
tout << curr << " " << mk_pp(s, m_manager);
tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
}
});
for (source const& curr : sources) {
if (curr.is_fresh_value()) {
sort * s = curr.get_value()->get_sort();
TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " : " << mk_pp(s, m_manager) << "\n";);
TRACE("model_fresh_bug", tout << curr << " : " << mk_pp(s, m_manager) << "\n";);
expr * val = m_model->get_fresh_value(s);
TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " := #" << (val == 0 ? UINT_MAX : val->get_id()) << "\n";);
TRACE("model_fresh_bug", tout << curr << " := #" << (val == nullptr ? UINT_MAX : val->get_id()) << "\n";);
m_asts.push_back(val);
curr.get_value()->set_value(val);
}
else {
enode * n = curr.get_enode();
SASSERT(n->get_root() == n);
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << "\n";);
TRACE("mg_top_sort", tout << curr << "\n";);
dependencies.reset();
dependency_values.reset();
model_value_proc * proc = nullptr;
VERIFY(root2proc.find(n, proc));
model_value_proc * proc = root2proc[n];
SASSERT(proc);
proc->get_dependencies(dependencies);
for (model_value_dependency const& d : dependencies) {
if (d.is_fresh_value()) {
CTRACE("mg_top_sort", !d.get_value()->get_value(),
tout << "#" << n->get_owner_id() << " -> ";
tout << "fresh!" << d.get_value()->get_idx() << "\n";);
tout << "#" << n->get_owner_id() << " -> " << d << "\n";);
SASSERT(d.get_value()->get_value());
dependency_values.push_back(d.get_value()->get_value());
}
@ -445,8 +438,7 @@ namespace smt {
}
}
extra_fresh_value * model_generator::mk_extra_fresh_value(sort * s) {
SASSERT(s->is_infinite());
extra_fresh_value * model_generator::mk_extra_fresh_value(sort * s) {
extra_fresh_value * r = alloc(extra_fresh_value, s, m_fresh_idx);
m_fresh_idx++;
m_extra_fresh_values.push_back(r);

10
src/smt/smt_model_generator.h
View file

@ -100,14 +100,16 @@ namespace smt {
extra_fresh_value * m_value; //!< When m_fresh == true, contains the sort of the fresh value
};
public:
model_value_dependency():m_fresh(true), m_value(nullptr) {}
model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {}
model_value_dependency(extra_fresh_value * v):m_fresh(true), m_value(v) {}
model_value_dependency():m_fresh(true), m_value(nullptr) { }
explicit model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {}
explicit model_value_dependency(extra_fresh_value * v) :m_fresh(true), m_value(v) { SASSERT(v); }
bool is_fresh_value() const { return m_fresh; }
enode * get_enode() const { SASSERT(!is_fresh_value()); return m_enode; }
extra_fresh_value * get_value() const { SASSERT(is_fresh_value()); return m_value; }
};
std::ostream& operator<<(std::ostream& out, model_value_dependency const& d);
typedef model_value_dependency source;
struct source_hash_proc {
@ -166,7 +168,7 @@ namespace smt {
extra_fresh_value * m_value;
public:
fresh_value_proc(extra_fresh_value * v):m_value(v) {}
void get_dependencies(buffer<model_value_dependency> & result) override { result.push_back(m_value); }
void get_dependencies(buffer<model_value_dependency> & result) override;
app * mk_value(model_generator & m, ptr_vector<expr> & values) override { return to_app(values[0]); }
bool is_fresh() const override { return true; }
};

120
src/smt/smt_quantifier.cpp
View file

@ -104,6 +104,90 @@ namespace smt {
return m_plugin->is_shared(n);
}
/**
\brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its
equivalence class are in the log and up-to-date.
*/
void log_justification_to_root(std::ostream & log, enode *en) {
enode *root = en->get_root();
for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
if (it->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
log_single_justification(log, it);
it->m_proof_logged_status = smt::logged_status::LOGGED;
} else if (it->m_proof_logged_status != smt::logged_status::BEING_LOGGED && it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
// When the justification of an argument changes m_proof_logged_status is not reset => We need to check if the proofs of all arguments are logged.
it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
const unsigned num_args = it->get_num_args();
enode *target = it->get_trans_justification().m_target;
for (unsigned i = 0; i < num_args; ++i) {
log_justification_to_root(log, it->get_arg(i));
log_justification_to_root(log, target->get_arg(i));
}
it->m_proof_logged_status = smt::logged_status::LOGGED;
}
}
if (root->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
log << "[eq-expl] #" << root->get_owner_id() << " root\n";
root->m_proof_logged_status = smt::logged_status::LOGGED;
}
}
/**
\brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log
equalities needed by the step (e.g. argument equalities for congruence steps).
*/
void log_single_justification(std::ostream & out, enode *en) {
smt::literal lit;
unsigned num_args;
enode *target = en->get_trans_justification().m_target;
theory_id th_id;
switch (en->get_trans_justification().m_justification.get_kind()) {
case smt::eq_justification::kind::EQUATION:
lit = en->get_trans_justification().m_justification.get_literal();
out << "[eq-expl] #" << en->get_owner_id() << " lit #" << m_context.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n";
break;
case smt::eq_justification::kind::AXIOM:
out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n";
break;
case smt::eq_justification::kind::CONGRUENCE:
if (!en->get_trans_justification().m_justification.used_commutativity()) {
num_args = en->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
log_justification_to_root(out, en->get_arg(i));
log_justification_to_root(out, target->get_arg(i));
}
out << "[eq-expl] #" << en->get_owner_id() << " cg";
for (unsigned i = 0; i < num_args; ++i) {
out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
}
out << " ; #" << target->get_owner_id() << "\n";
break;
} else {
out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
break;
}
case smt::eq_justification::kind::JUSTIFICATION:
th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory();
if (th_id != null_theory_id) {
symbol const theory = m().get_family_name(th_id);
out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n";
} else {
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
}
break;
default:
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
break;
}
}
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
@ -111,7 +195,7 @@ namespace smt {
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
ptr_vector<enode> & used_enodes) {
vector<std::tuple<enode *, enode *>> & used_enodes) {
max_generation = std::max(max_generation, get_generation(q));
if (m_num_instances > m_params.m_qi_max_instances) {
return false;
@ -121,15 +205,39 @@ namespace smt {
if (f) {
if (has_trace_stream()) {
std::ostream & out = trace_stream();
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id();
// In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
// is used. We need to make sure that all of these equalities appear in the log.
for (unsigned i = 0; i < num_bindings; ++i) {
log_justification_to_root(out, bindings[i]);
}
for (auto n : used_enodes) {
enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n);
if (orig != nullptr) {
log_justification_to_root(out, orig);
log_justification_to_root(out, substituted);
}
}
// At this point all relevant equalities for the match are logged.
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id() << " #" << pat->get_id();
for (unsigned i = 0; i < num_bindings; i++) {
// I don't want to use mk_pp because it creates expressions for pretty printing.
// This nasty side-effect may change the behavior of Z3.
out << " #" << bindings[i]->get_owner_id();
}
out << " ;";
for (enode* n : used_enodes)
out << " #" << n->get_owner_id();
for (auto n : used_enodes) {
enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n);
if (orig == nullptr)
out << " #" << substituted->get_owner_id();
else {
out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
}
}
out << "\n";
}
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
@ -296,12 +404,12 @@ namespace smt {
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
ptr_vector<enode> & used_enodes) {
vector<std::tuple<enode *, enode *>> & used_enodes) {
return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_generation, used_enodes);
}
bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation) {
ptr_vector<enode> tmp;
vector<std::tuple<enode *, enode *>> tmp;
return add_instance(q, nullptr, num_bindings, bindings, def, generation, generation, generation, tmp);
}

3
src/smt/smt_quantifier.h
View file

@ -23,6 +23,7 @@ Revision History:
#include "util/statistics.h"
#include "util/params.h"
#include "smt/smt_types.h"
#include <tuple>
class proto_model;
struct smt_params;
@ -58,7 +59,7 @@ namespace smt {
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
ptr_vector<enode> & used_enodes);
vector<std::tuple<enode *, enode *>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation = 0);
void init_search_eh();

3
src/smt/smt_quick_checker.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include "smt/smt_context.h"
#include "smt/smt_quick_checker.h"
#include "ast/ast_pp.h"
#include <tuple>
namespace smt {
@ -197,7 +198,7 @@ namespace smt {
}
bool quick_checker::process_candidates(quantifier * q, bool unsat) {
ptr_vector<enode> empty_used_enodes;
vector<std::tuple<enode *, enode *>> empty_used_enodes;
buffer<unsigned> szs;
buffer<unsigned> it;
for (unsigned i = 0; i < m_num_bindings; i++) {

20
src/smt/smt_setup.cpp
View file

@ -492,7 +492,7 @@ namespace smt {
m_params.m_arith_eq2ineq = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_nnf_cnf = false;
m_params.m_nnf_cnf = false;
setup_lra_arith();
}
@ -627,9 +627,6 @@ namespace smt {
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
m_params.m_random_initial_activity = IA_ZERO;
}
// if (st.m_num_arith_ineqs == st.m_num_diff_ineqs && st.m_num_arith_eqs == st.m_num_diff_eqs && st.arith_k_sum_is_small())
// m_context.register_plugin(new smt::theory_si_arith(m_manager, m_params));
// else
setup_i_arith();
setup_arrays();
}
@ -654,7 +651,7 @@ namespace smt {
//
m_params.m_ng_lift_ite = LI_FULL;
TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
setup_i_arith();
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
setup_arrays();
}
@ -777,7 +774,11 @@ namespace smt {
IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum;
bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only;
switch(m_params.m_arith_mode) {
auto mode = m_params.m_arith_mode;
if (m_logic == "QF_LIA") {
mode = AS_NEW_ARITH;
}
switch(mode) {
case AS_NO_ARITH:
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
break;
@ -828,7 +829,10 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
break;
case AS_NEW_ARITH:
setup_lra_arith();
if (st.m_num_non_linear != 0)
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
else
setup_lra_arith();
break;
default:
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
@ -990,7 +994,7 @@ namespace smt {
}
if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) {
if (!st.m_has_real)
if (!st.m_has_real && st.m_num_non_linear == 0)
setup_QF_UFLIA(st);
else if (!st.m_has_int && st.m_num_non_linear == 0)
setup_QF_UFLRA();

2
src/smt/smt_theory.cpp
View file

@ -123,7 +123,7 @@ namespace smt {
context & ctx = get_context();
app * eq = ctx.mk_eq_atom(a, b);
TRACE("mk_var_bug", tout << "mk_eq: " << eq->get_id() << " " << a->get_id() << " " << b->get_id() << "\n";
tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager()););
tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager()););
ctx.internalize(eq, gate_ctx);
return ctx.get_literal(eq);
}

40
src/smt/theory_arith_aux.h
View file

@ -731,35 +731,34 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
TRACE("arith", tout << m_lits << " " << m_eqs.size() << "\n";);
if (proofs_enabled) {
for (unsigned i = 0; i < m_lits.size(); ++i) {
a.push_lit(m_lits[i], coeff, proofs_enabled);
}
for (unsigned i = 0; i < m_eqs.size(); ++i) {
a.push_eq(m_eqs[i], coeff, proofs_enabled);
}
for (literal l : m_lits)
a.push_lit(l, coeff, proofs_enabled);
for (auto const& e : m_eqs)
a.push_eq(e, coeff, proofs_enabled);
}
else {
a.append(m_lits.size(), m_lits.c_ptr());
a.append(m_eqs.size(), m_eqs.c_ptr());
a.append(m_eqs.size(), m_eqs.c_ptr());
}
}
template<typename Ext>
void theory_arith<Ext>::derived_bound::display(theory_arith<Ext> const& th, std::ostream& out) const {
out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value();
ast_manager& m = th.get_manager();
for (unsigned i = 0; i < m_eqs.size(); ++i) {
enode* a = m_eqs[i].first;
enode* b = m_eqs[i].second;
out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value() << "\n";
out << "expr: " << mk_pp(th.var2expr(bound::get_var()), m) << "\n";
for (auto const& e : m_eqs) {
enode* a = e.first;
enode* b = e.second;
out << " ";
out << "#" << a->get_owner_id() << " " << mk_pp(a->get_owner(), m) << " = "
<< "#" << b->get_owner_id() << " " << mk_pp(b->get_owner(), m);
<< "#" << b->get_owner_id() << " " << mk_pp(b->get_owner(), m) << "\n";
}
for (unsigned i = 0; i < m_lits.size(); ++i) {
literal l = m_lits[i];
out << " " << l << ":"; th.get_context().display_detailed_literal(out, l);
for (literal l : m_lits) {
out << l << ":"; th.get_context().display_detailed_literal(out, l) << "\n";
}
}
@ -882,13 +881,10 @@ namespace smt {
}
TRACE("derived_bound",
tout << "explanation:\n";
literal_vector::const_iterator it1 = new_bound->m_lits.begin();
literal_vector::const_iterator end1 = new_bound->m_lits.end();
for (; it1 != end1; ++it1) tout << *it1 << " ";
for (literal l : new_bound->m_lits) tout << l << " ";
tout << " ";
eq_vector::const_iterator it2 = new_bound->m_eqs.begin();
eq_vector::const_iterator end2 = new_bound->m_eqs.end();
for (; it2 != end2; ++it2) tout << "#" << it2->first->get_owner_id() << "=#" << it2->second->get_owner_id() << " ";
for (auto const& e : new_bound->m_eqs)
tout << "#" << e.first->get_owner_id() << "=#" << e.second->get_owner_id() << " ";
tout << "\n";);
DEBUG_CODE(CTRACE("derived_bound", k != val, tout << "k: " << k << ", k_norm: " << k_norm << ", val: " << val << "\n";););
SASSERT(k == val);

45
src/smt/theory_arith_core.h
View file

@ -1708,7 +1708,7 @@ namespace smt {
template<typename Ext>
theory* theory_arith<Ext>::mk_fresh(context* new_ctx) {
return alloc(theory_arith<Ext>, new_ctx->get_manager(), m_params);
return alloc(theory_arith<Ext>, new_ctx->get_manager(), new_ctx->get_fparams());
}
template<typename Ext>
@ -1853,10 +1853,7 @@ namespace smt {
void theory_arith<Ext>::restore_assignment() {
CASSERT("arith", valid_row_assignment());
TRACE("restore_assignment_bug", tout << "START restore_assignment...\n";);
typename svector<unsigned>::iterator it = m_update_trail_stack.begin();
typename svector<unsigned>::iterator end = m_update_trail_stack.end();
for(; it != end; ++it) {
theory_var v = *it;
for (theory_var v : m_update_trail_stack) {
TRACE("restore_assignment_bug", tout << "restoring v" << v << " <- " << m_old_value[v] << "\n";);
SASSERT(!is_quasi_base(v));
SASSERT(m_in_update_trail_stack.contains(v));
@ -2237,11 +2234,7 @@ namespace smt {
theory_var best = null_theory_var;
inf_numeral best_error;
inf_numeral curr_error;
typename var_heap::iterator it = m_to_patch.begin();
typename var_heap::iterator end = m_to_patch.end();
//unsigned n = 0;
for (; it != end; ++it) {
theory_var v = *it;
for (theory_var v : m_to_patch) {
if (below_lower(v))
curr_error = lower(v)->get_value() - get_value(v);
else if (above_upper(v))
@ -2391,10 +2384,11 @@ namespace smt {
TRACE("sign_row_conflict", tout << "v" << x_i << " is_below: " << is_below << " delta: " << delta << "\n"; display_var(tout, x_i);
tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";
display_row(tout, r, true);
display_row(tout, r, false);
ante.display(tout););
set_conflict(ante, ante, "farkas");
// display_bounds_in_smtlib();
}
// -----------------------------------
@ -2535,10 +2529,9 @@ namespace smt {
antecedents ante(*this);
b1->push_justification(ante, numeral(1), coeffs_enabled());
b2->push_justification(ante, numeral(1), coeffs_enabled());
set_conflict(ante, ante, "farkas");
TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n";
tout << "bounds: " << b1 << " " << b2 << "\n";);
set_conflict(ante, ante, "farkas");
}
// -----------------------------------
@ -2771,8 +2764,10 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::explain_bound(row const & r, int idx, bool is_lower, inf_numeral & delta, antecedents& ante) {
SASSERT(delta >= inf_numeral::zero());
if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty()))
TRACE("arith_conflict", tout << "relax: " << relax_bounds() << " lits: " << ante.lits().size() << " eqs: " << ante.eqs().size() << " idx: " << idx << "\n";);
if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty())) {
return;
}
context & ctx = get_context();
row_entry const & entry = r[idx];
numeral coeff = entry.m_coeff;
@ -2790,9 +2785,11 @@ namespace smt {
if (!it->is_dead() && idx != idx2) {
bound * b = get_bound(it->m_var, is_lower ? it->m_coeff.is_pos() : it->m_coeff.is_neg());
SASSERT(b);
if (!b->has_justification())
if (!b->has_justification()) {
continue;
}
if (!relax_bounds() || delta.is_zero()) {
TRACE("propagate_bounds", tout << "push justification: v" << it->m_var << "\n";);
b->push_justification(ante, it->m_coeff, coeffs_enabled());
continue;
}
@ -2821,10 +2818,7 @@ namespace smt {
inf_numeral k_2 = k_1;
atom * new_atom = nullptr;
atoms const & as = m_var_occs[it->m_var];
typename atoms::const_iterator it = as.begin();
typename atoms::const_iterator end = as.end();
for (; it != end; ++it) {
atom * a = *it;
for (atom * a : as) {
if (a == b)
continue;
bool_var bv = a->get_bool_var();
@ -2880,10 +2874,7 @@ namespace smt {
atoms const & as = m_var_occs[v];
inf_numeral const & epsilon = get_epsilon(v);
inf_numeral delta;
typename atoms::const_iterator it = as.begin();
typename atoms::const_iterator end = as.end();
for (; it != end; ++it) {
atom * a = *it;
for (atom* a : as) {
bool_var bv = a->get_bool_var();
literal l(bv);
if (get_context().get_assignment(bv) == l_undef) {
@ -2954,6 +2945,7 @@ namespace smt {
TRACE("arith", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";);
ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), l);
}
}
@ -2972,12 +2964,13 @@ namespace smt {
context & ctx = get_context();
antecedents ante(*this);
explain_bound(r, idx, is_lower, delta, ante);
dump_lemmas(l, ante);
TRACE("propagate_bounds",
ante.display(tout) << " --> ";
ctx.display_detailed_literal(tout, l);
tout << "\n";);
dump_lemmas(l, ante);
if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) {
literal_vector & lits = m_tmp_literal_vector2;
lits.reset();
@ -3060,14 +3053,14 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::set_conflict(antecedents const& ante, antecedents& bounds, char const* proof_rule) {
dump_lemmas(false_literal, ante);
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
dump_lemmas(false_literal, ante);
}
template<typename Ext>
void theory_arith<Ext>::set_conflict(derived_bound const& ante, antecedents& bounds, char const* proof_rule) {
dump_lemmas(false_literal, ante);
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
dump_lemmas(false_literal, ante);
}
template<typename Ext>

119
src/smt/theory_arith_nl.h
View file

@ -58,7 +58,6 @@ namespace smt {
void theory_arith<Ext>::mark_var(theory_var v, svector<theory_var> & vars, var_set & already_found) {
if (already_found.contains(v))
return;
TRACE("non_linear", tout << "marking: v" << v << "\n";);
already_found.insert(v);
vars.push_back(v);
}
@ -71,8 +70,7 @@ namespace smt {
if (is_pure_monomial(v)) {
expr * n = var2expr(v);
SASSERT(m_util.is_mul(n));
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
expr * curr = to_app(n)->get_arg(i);
for (expr * curr : *to_app(n)) {
theory_var v = expr2var(curr);
SASSERT(v != null_theory_var);
mark_var(v, vars, already_found);
@ -118,22 +116,19 @@ namespace smt {
var_set already_found;
row_set already_visited_rows;
context & ctx = get_context();
svector<theory_var>::const_iterator it = m_nl_monomials.begin();
svector<theory_var>::const_iterator end = m_nl_monomials.end();
for (; it != end; ++it) {
theory_var v = *it;
for (theory_var v : m_nl_monomials) {
expr * n = var2expr(v);
if (ctx.is_relevant(n))
mark_var(v, vars, already_found);
}
for (unsigned idx = 0; idx < vars.size(); idx++) {
TRACE("non_linear", tout << "marking dependents of: v" << vars[idx] << "\n";);
mark_dependents(vars[idx], vars, already_found, already_visited_rows);
// NB: vars changes inside of loop
for (unsigned idx = 0; idx < vars.size(); ++idx) {
theory_var v = vars[idx];
TRACE("non_linear", tout << "marking dependents of: v" << v << "\n";);
mark_dependents(v, vars, already_found, already_visited_rows);
}
TRACE("non_linear", tout << "variables in non linear cluster:\n";
svector<theory_var>::const_iterator it = vars.begin();
svector<theory_var>::const_iterator end = vars.end();
for (; it != end; ++it) tout << "v" << *it << " ";
for (theory_var v : vars) tout << "v" << v << " ";
tout << "\n";);
}
@ -227,9 +222,8 @@ namespace smt {
SASSERT(!m_util.is_numeral(m));
if (m_util.is_mul(m)) {
unsigned num_vars = 0;
expr * var = nullptr;
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * curr = to_app(m)->get_arg(i);
expr * var = nullptr;
for (expr * curr : *to_app(m)) {
if (var != curr) {
num_vars++;
var = curr;
@ -254,9 +248,7 @@ namespace smt {
unsigned curr_idx = 0;
expr * var = nullptr;
unsigned power = 0;
unsigned j;
for (j = 0; j < to_app(m)->get_num_args(); j++) {
expr * arg = to_app(m)->get_arg(j);
for (expr * arg : *to_app(m)) {
if (var == nullptr) {
var = arg;
power = 1;
@ -360,6 +352,7 @@ namespace smt {
template<typename Ext>
interval theory_arith<Ext>::evaluate_as_interval(expr * n) {
expr* arg;
rational val;
TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";);
if (has_var(n)) {
TRACE("nl_evaluate", tout << "n has a variable associated with it\n";);
@ -370,8 +363,8 @@ namespace smt {
else if (m_util.is_add(n)) {
TRACE("nl_evaluate", tout << "is add\n";);
interval r(m_dep_manager, rational(0));
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
r += evaluate_as_interval(to_app(n)->get_arg(i));
for (expr* arg : *to_app(n)) {
r += evaluate_as_interval(arg);
}
TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
return r;
@ -388,31 +381,28 @@ namespace smt {
it.expt(power);
r *= it;
}
TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
TRACE("nl_evaluate", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
return r;
}
else if (m_util.is_to_real(n, arg)) {
return evaluate_as_interval(arg);
}
else if (m_util.is_numeral(n, val)) {
TRACE("nl_evaluate", tout << "is numeral\n";);
return interval(m_dep_manager, val);
}
else {
rational val;
if (m_util.is_numeral(n, val)) {
TRACE("nl_evaluate", tout << "is numeral\n";);
return interval(m_dep_manager, val);
}
else {
TRACE("nl_evaluate", tout << "is unknown\n";);
return interval(m_dep_manager);
}
TRACE("nl_evaluate", tout << "is unknown\n";);
return interval(m_dep_manager);
}
}
template<typename Ext>
void theory_arith<Ext>::display_monomial(std::ostream & out, expr * m) const {
void theory_arith<Ext>::display_monomial(std::ostream & out, expr * n) const {
bool first = true;
unsigned num_vars = get_num_vars_in_monomial(m);
unsigned num_vars = get_num_vars_in_monomial(n);
for (unsigned i = 0; i < num_vars; i++) {
var_power_pair p = get_var_and_degree(m, i);
var_power_pair p = get_var_and_degree(n, i);
SASSERT(p.first != 0);
if (first) first = false; else out << " * ";
out << mk_bounded_pp(p.first, get_manager()) << "^" << p.second;
@ -425,10 +415,8 @@ namespace smt {
m_dep_manager.linearize(dep, bounds);
m_tmp_lit_set.reset();
m_tmp_eq_set.reset();
ptr_vector<void>::const_iterator it = bounds.begin();
ptr_vector<void>::const_iterator end = bounds.end();
for (; it != end; ++it) {
bound * b = static_cast<bound*>(*it);
for (void* _b : bounds) {
bound * b = static_cast<bound*>(_b);
accumulate_justification(*b, new_bound, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
}
}
@ -544,21 +532,19 @@ namespace smt {
the method returns without doing anything.
*/
template<typename Ext>
bool theory_arith<Ext>::propagate_nl_downward(expr * m, unsigned i) {
SASSERT(is_pure_monomial(m));
SASSERT(i < get_num_vars_in_monomial(m));
var_power_pair p = get_var_and_degree(m, i);
bool theory_arith<Ext>::propagate_nl_downward(expr * n, unsigned i) {
SASSERT(is_pure_monomial(n));
SASSERT(i < get_num_vars_in_monomial(n));
var_power_pair p = get_var_and_degree(n, i);
expr * v = p.first;
unsigned power = p.second;
TRACE("propagate_nl_downward", tout << "m: " << mk_ismt2_pp(m, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) <<
"\npower: " << power << "\n";);
if (power != 1)
return false; // TODO: remove, when the n-th root is implemented in interval.
unsigned num_vars = get_num_vars_in_monomial(m);
unsigned num_vars = get_num_vars_in_monomial(n);
interval other_bounds(m_dep_manager, rational(1));
// TODO: the following code can be improved it is quadratic on the degree of the monomial.
for (unsigned i = 0; i < num_vars; i++) {
var_power_pair p = get_var_and_degree(m, i);
var_power_pair p = get_var_and_degree(n, i);
if (p.first == v)
continue;
expr * var = p.first;
@ -567,7 +553,13 @@ namespace smt {
}
if (other_bounds.contains_zero())
return false; // interval division requires that divisor doesn't contain 0.
interval r = mk_interval_for(m);
interval r = mk_interval_for(n);
TRACE("nl_arith_bug", tout << "m: " << mk_ismt2_pp(n, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) <<
"\npower: " << power << "\n";
tout << "num_vars: " << num_vars << "\n";
display_interval(tout << "monomial bounds\n", r);
display_interval(tout << "other bounds\n", other_bounds);
);
r /= other_bounds;
return update_bounds_using_interval(v, r);
}
@ -907,7 +899,6 @@ namespace smt {
}
TRACE("non_linear_bug", tout << "enode: " << get_context().get_enode(rhs) << " enode_id: " << get_context().get_enode(rhs)->get_owner_id() << "\n";);
theory_var new_v = expr2var(rhs);
TRACE("non_linear_bug", ctx.display(tout););
SASSERT(new_v != null_theory_var);
new_lower = alloc(derived_bound, new_v, inf_numeral(0), B_LOWER);
new_upper = alloc(derived_bound, new_v, inf_numeral(0), B_UPPER);
@ -953,19 +944,17 @@ namespace smt {
}
accumulate_justification(*l, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
TRACE("non_linear",
for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
tout << " ";
TRACE("non_linear",
for (literal l : new_lower->m_lits) {
ctx.display_detailed_literal(tout, l) << " ";
}
tout << "\n";);
accumulate_justification(*u, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
TRACE("non_linear",
for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
tout << " ";
for (literal l : new_lower->m_lits) {
ctx.display_detailed_literal(tout, l) << " ";
}
tout << "\n";);
@ -977,9 +966,8 @@ namespace smt {
TRACE("non_linear",
new_lower->display(*this, tout << "lower: "); tout << "\n";
new_upper->display(*this, tout << "upper: "); tout << "\n";
for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_upper->m_lits[j]);
tout << " ";
for (literal lit : new_upper->m_lits) {
ctx.display_detailed_literal(tout, lit) << " ";
}
tout << "\n";);
@ -1123,14 +1111,14 @@ namespace smt {
continue;
if (is_pure_monomial(v)) {
expr * m = var2expr(v);
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
theory_var curr = expr2var(to_app(m)->get_arg(i));
for (expr* arg : *to_app(m)) {
theory_var curr = expr2var(arg);
if (m_tmp_var_set.contains(curr))
return true;
}
SASSERT(m == var2expr(v));
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
theory_var curr = expr2var(to_app(m)->get_arg(i));
for (expr* arg : *to_app(m)) {
theory_var curr = expr2var(arg);
if (!is_fixed(curr))
m_tmp_var_set.insert(curr);
}
@ -1936,10 +1924,7 @@ namespace smt {
derived_bound b(null_theory_var, inf_numeral(0), B_LOWER);
dependency2new_bound(d, b);
set_conflict(b, ante, "arith_nl");
TRACE("non_linear",
for (unsigned i = 0; i < b.m_lits.size(); ++i) {
tout << b.m_lits[i] << " ";
});
TRACE("non_linear", for (literal lit : b.m_lits) tout << lit << " "; tout << "\n";);
}
/**
@ -2387,7 +2372,7 @@ namespace smt {
elim_quasi_base_rows();
move_non_base_vars_to_bounds();
TRACE("non_linear", tout << "processing non linear constraints...\n"; get_context().display(tout););
TRACE("non_linear_verbose", tout << "processing non linear constraints...\n"; get_context().display(tout););
if (!make_feasible()) {
TRACE("non_linear", tout << "failed to move variables to bounds.\n";);
failed();

49
src/smt/theory_arith_pp.h
View file

@ -391,19 +391,19 @@ namespace smt {
void theory_arith<Ext>::display_vars(std::ostream & out) const {
out << "vars:\n";
int n = get_num_vars();
int inf_vars = 0;
int int_inf_vars = 0;
for (theory_var v = 0; v < n; v++) {
if ((lower(v) && lower(v)->get_value() > get_value(v))
|| (upper(v) && upper(v)->get_value() < get_value(v)))
inf_vars++;
if (is_int(v) && !get_value(v).is_int())
int_inf_vars++;
}
out << "infeasibles = " << inf_vars << " int_inf = " << int_inf_vars << std::endl;
for (theory_var v = 0; v < n; v++) {
display_var(out, v);
}
int inf_vars = 0;
int int_inf_vars = 0;
for (theory_var v = 0; v < n; v++) {
if ((lower(v) && lower(v)->get_value() > get_value(v))
|| (upper(v) && upper(v)->get_value() < get_value(v)))
inf_vars++;
if (is_int(v) && !get_value(v).is_int())
int_inf_vars++;
}
out << "infeasibles = " << inf_vars << " int_inf = " << int_inf_vars << std::endl;
for (theory_var v = 0; v < n; v++) {
display_var(out, v);
}
}
template<typename Ext>
@ -418,9 +418,9 @@ namespace smt {
th.get_context().display_literals_verbose(out, lits().size(), lits().c_ptr());
if (!lits().empty()) out << "\n";
ast_manager& m = th.get_manager();
for (unsigned i = 0; i < m_eqs.size(); ++i) {
out << mk_pp(m_eqs[i].first->get_owner(), m) << " ";
out << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
for (auto const& e : m_eqs) {
out << mk_pp(e.first->get_owner(), m) << " ";
out << mk_pp(e.second->get_owner(), m) << "\n";
}
return out;
}
@ -431,27 +431,24 @@ namespace smt {
m_dep_manager.linearize(dep, bounds);
m_tmp_lit_set.reset();
m_tmp_eq_set.reset();
ptr_vector<void>::const_iterator it = bounds.begin();
ptr_vector<void>::const_iterator end = bounds.end();
for (; it != end; ++it) {
bound * b = static_cast<bound*>(*it);
out << " ";
b->display(*this, out);
for (void *_b : bounds) {
bound * b = static_cast<bound*>(_b);
b->display(*this, out << "\n");
}
}
template<typename Ext>
void theory_arith<Ext>::display_interval(std::ostream & out, interval const& i) {
i.display(out);
display_deps(out << " lo:", i.get_lower_dependencies());
display_deps(out << " hi:", i.get_upper_dependencies());
display_deps(out << "\nlo:", i.get_lower_dependencies());
display_deps(out << "\nhi:", i.get_upper_dependencies());
}
template<typename Ext>
void theory_arith<Ext>::display_atoms(std::ostream & out) const {
out << "atoms:\n";
for (unsigned i = 0; i < m_atoms.size(); i++)
display_atom(out, m_atoms[i], false);
for (atom * a : m_atoms)
display_atom(out, a, false);
}
template<typename Ext>

106
src/smt/theory_bv.cpp
View file

@ -138,9 +138,9 @@ namespace smt {
void theory_bv::process_args(app * n) {
context & ctx = get_context();
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(n->get_arg(i), false);
for (expr* arg : *n) {
ctx.internalize(arg, false);
}
}
enode * theory_bv::mk_enode(app * n) {
@ -185,11 +185,9 @@ namespace smt {
void theory_bv::get_bits(theory_var v, expr_ref_vector & r) {
context & ctx = get_context();
literal_vector & bits = m_bits[v];
literal_vector::const_iterator it = bits.begin();
literal_vector::const_iterator end = bits.end();
for (; it != end; ++it) {
for (literal lit : bits) {
expr_ref l(get_manager());
ctx.literal2expr(*it, l);
ctx.literal2expr(lit, l);
r.push_back(l);
}
}
@ -358,18 +356,16 @@ namespace smt {
void mark_bits(conflict_resolution & cr, literal_vector const & bits) {
context & ctx = cr.get_context();
literal_vector::const_iterator it = bits.begin();
literal_vector::const_iterator end = bits.end();
for (; it != end; ++it) {
if (it->var() != true_bool_var) {
if (ctx.get_assignment(*it) == l_true)
cr.mark_literal(*it);
for (literal lit : bits) {
if (lit.var() != true_bool_var) {
if (ctx.get_assignment(lit) == l_true)
cr.mark_literal(lit);
else
cr.mark_literal(~(*it));
cr.mark_literal(~lit);
}
}
}
void get_proof(conflict_resolution & cr, literal l, ptr_buffer<proof> & prs, bool & visited) {
if (l.var() == true_bool_var)
return;
@ -489,7 +485,7 @@ namespace smt {
}
}
bool theory_bv::get_fixed_value(theory_var v, numeral & result) const {
bool theory_bv::get_fixed_value(theory_var v, numeral & result) const {
context & ctx = get_context();
result.reset();
literal_vector const & bits = m_bits[v];
@ -830,10 +826,9 @@ namespace smt {
while (i > 0) {
i--;
theory_var arg = get_arg_var(e, i);
literal_vector::const_iterator it = m_bits[arg].begin();
literal_vector::const_iterator end = m_bits[arg].end();
for (; it != end; ++it)
add_bit(v, *it);
for (literal lit : m_bits[arg]) {
add_bit(v, lit);
}
}
find_wpos(v);
}
@ -855,6 +850,8 @@ namespace smt {
}
bool theory_bv::internalize_term(app * term) {
scoped_suspend_rlimit _suspend_cancel(get_manager().limit());
try {
SASSERT(term->get_family_id() == get_family_id());
TRACE("bv", tout << "internalizing term: " << mk_bounded_pp(term, get_manager()) << "\n";);
if (approximate_term(term)) {
@ -912,6 +909,11 @@ namespace smt {
UNREACHABLE();
return false;
}
}
catch (z3_exception& ex) {
IF_VERBOSE(1, verbose_stream() << "internalize_term: " << ex.msg() << "\n";);
throw;
}
}
#define MK_NO_OVFL(NAME, OP) \
@ -1097,8 +1099,7 @@ namespace smt {
void theory_bv::apply_sort_cnstr(enode * n, sort * s) {
if (!is_attached_to_var(n) && !approximate_term(n->get_owner())) {
theory_var v = mk_var(n);
mk_bits(v);
mk_bits(mk_var(n));
}
}
@ -1308,10 +1309,9 @@ namespace smt {
theory_var v = e->get_th_var(get_id());
if (v != null_theory_var) {
literal_vector & bits = m_bits[v];
literal_vector::iterator it = bits.begin();
literal_vector::iterator end = bits.end();
for (; it != end; ++it)
ctx.mark_as_relevant(*it);
for (literal lit : bits) {
ctx.mark_as_relevant(lit);
}
}
}
}
@ -1463,35 +1463,27 @@ namespace smt {
SASSERT(bv_size == get_bv_size(r2));
m_merge_aux[0].reserve(bv_size+1, null_theory_var);
m_merge_aux[1].reserve(bv_size+1, null_theory_var);
#define RESET_MERGET_AUX() { \
zero_one_bits::iterator it = bits1.begin(); \
zero_one_bits::iterator end = bits1.end(); \
for (; it != end; ++it) \
m_merge_aux[it->m_is_true][it->m_idx] = null_theory_var; \
}
#define RESET_MERGET_AUX() for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = null_theory_var;
DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { SASSERT(m_merge_aux[0][i] == null_theory_var || m_merge_aux[1][i] == null_theory_var); });
// save info about bits1
zero_one_bits::iterator it = bits1.begin();
zero_one_bits::iterator end = bits1.end();
for (; it != end; ++it)
m_merge_aux[it->m_is_true][it->m_idx] = it->m_owner;
for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = zo.m_owner;
// check if bits2 is consistent with bits1, and copy new bits to bits1
it = bits2.begin();
end = bits2.end();
for (; it != end; ++it) {
theory_var v2 = it->m_owner;
theory_var v1 = m_merge_aux[!it->m_is_true][it->m_idx];
for (auto & zo : bits2) {
theory_var v2 = zo.m_owner;
theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx];
if (v1 != null_theory_var) {
// conflict was detected ... v1 and v2 have complementary bits
SASSERT(m_bits[v1][it->m_idx] == ~(m_bits[v2][it->m_idx]));
SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx]));
SASSERT(m_bits[v1].size() == m_bits[v2].size());
mk_new_diseq_axiom(v1, v2, it->m_idx);
mk_new_diseq_axiom(v1, v2, zo.m_idx);
RESET_MERGET_AUX();
return false;
}
if (m_merge_aux[it->m_is_true][it->m_idx] == null_theory_var) {
if (m_merge_aux[zo.m_is_true][zo.m_idx] == null_theory_var) {
// copy missing variable to bits1
bits1.push_back(*it);
bits1.push_back(zo);
}
}
// reset m_merge_aux vector
@ -1614,11 +1606,9 @@ namespace smt {
out << std::right << ", bits:";
context & ctx = get_context();
literal_vector const & bits = m_bits[v];
literal_vector::const_iterator it = bits.begin();
literal_vector::const_iterator end = bits.end();
for (; it != end; ++it) {
for (literal lit : bits) {
out << " ";
ctx.display_literal(out, *it);
ctx.display_literal(out, lit);
}
numeral val;
if (get_fixed_value(v, val))
@ -1668,7 +1658,7 @@ namespace smt {
}
#ifdef Z3DEBUG
bool theory_bv::check_assignment(theory_var v) const {
bool theory_bv::check_assignment(theory_var v) {
context & ctx = get_context();
if (!is_root(v))
return true;
@ -1709,7 +1699,7 @@ namespace smt {
\remark The method does nothing if v is not the root of the equivalence class.
*/
bool theory_bv::check_zero_one_bits(theory_var v) const {
bool theory_bv::check_zero_one_bits(theory_var v) {
if (get_context().inconsistent())
return true; // property is only valid if the context is not in a conflict.
if (is_root(v) && is_bv(v)) {
@ -1740,19 +1730,17 @@ namespace smt {
SASSERT(_bits.size() == num_bits);
svector<bool> already_found;
already_found.resize(bv_sz, false);
zero_one_bits::const_iterator it = _bits.begin();
zero_one_bits::const_iterator end = _bits.end();
for (; it != end; ++it) {
SASSERT(find(it->m_owner) == v);
SASSERT(bits[it->m_is_true][it->m_idx]);
SASSERT(!already_found[it->m_idx]);
already_found[it->m_idx] = true;
for (auto & zo : _bits) {
SASSERT(find(zo.m_owner) == v);
SASSERT(bits[zo.m_is_true][zo.m_idx]);
SASSERT(!already_found[zo.m_idx]);
already_found[zo.m_idx] = true;
}
}
return true;
}
bool theory_bv::check_invariant() const {
bool theory_bv::check_invariant() {
unsigned num = get_num_vars();
for (unsigned v = 0; v < num; v++) {
check_assignment(v);

6
src/smt/theory_bv.h
View file

@ -266,9 +266,9 @@ namespace smt {
#ifdef Z3DEBUG
bool check_assignment(theory_var v) const;
bool check_invariant() const;
bool check_zero_one_bits(theory_var v) const;
bool check_assignment(theory_var v);
bool check_invariant();
bool check_zero_one_bits(theory_var v);
#endif
};
};

212
src/smt/theory_lra.cpp
View file

@ -298,13 +298,15 @@ class theory_lra::imp {
void init_solver() {
if (m_solver) return;
lp_params lp(ctx().get_params());
m_solver = alloc(lp::lar_solver);
reset_variable_values();
m_theory_var2var_index.reset();
m_solver = alloc(lp::lar_solver);
lp_params lp(ctx().get_params());
m_solver->settings().set_resource_limit(m_resource_limit);
m_solver->settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lp.simplex_strategy());
reset_variable_values();
m_solver->settings().bound_propagation() = BP_NONE != propagation_mode();
m_solver->settings().m_enable_hnf = lp.enable_hnf();
m_solver->set_track_pivoted_rows(lp.bprop_on_pivoted_rows());
// todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
@ -514,7 +516,7 @@ class theory_lra::imp {
rational r1;
v = mk_var(t);
svector<lp::var_index> vars;
ptr_vector<expr> todo;
ptr_buffer<expr> todo;
todo.push_back(t);
while (!todo.empty()) {
expr* n = todo.back();
@ -534,7 +536,7 @@ class theory_lra::imp {
vars.push_back(get_var_index(mk_var(n)));
}
}
TRACE("arith", tout << mk_pp(t, m) << " " << _has_var << "\n";);
TRACE("arith", tout << "v" << v << "(" << get_var_index(v) << ") := " << mk_pp(t, m) << " " << _has_var << "\n";);
if (!_has_var) {
ensure_nra();
m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
@ -1118,7 +1120,7 @@ public:
(v != null_theory_var) &&
(v < static_cast<theory_var>(m_theory_var2var_index.size())) &&
(UINT_MAX != m_theory_var2var_index[v]) &&
!m_variable_values.empty();
(!m_variable_values.empty() || m_solver->is_term(m_theory_var2var_index[v]));
}
bool can_get_bound(theory_var v) const {
@ -1163,12 +1165,22 @@ public:
}
rational get_value(theory_var v) const {
if (!can_get_value(v)) return rational::zero();
if (v == null_theory_var ||
v >= static_cast<theory_var>(m_theory_var2var_index.size())) {
TRACE("arith", tout << "Variable v" << v << " not internalized\n";);
return rational::zero();
}
lp::var_index vi = m_theory_var2var_index[v];
if (m_variable_values.count(vi) > 0)
return m_variable_values[vi];
SASSERT (m_solver->is_term(vi));
if (!m_solver->is_term(vi)) {
TRACE("arith", tout << "not a term v" << v << "\n";);
return rational::zero();
}
m_todo_terms.push_back(std::make_pair(vi, rational::one()));
rational result(0);
while (!m_todo_terms.empty()) {
@ -1178,12 +1190,12 @@ public:
if (m_solver->is_term(wi)) {
const lp::lar_term& term = m_solver->get_term(wi);
result += term.m_v * coeff;
for (const auto & i : term.m_coeffs) {
if (m_variable_values.count(i.first) > 0) {
result += m_variable_values[i.first] * coeff * i.second;
for (const auto & i : term) {
if (m_variable_values.count(i.var()) > 0) {
result += m_variable_values[i.var()] * coeff * i.coeff();
}
else {
m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second));
m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
}
}
}
@ -1199,6 +1211,7 @@ public:
if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
reset_variable_values();
m_solver->get_model(m_variable_values);
TRACE("arith", display(tout););
}
}
@ -1360,20 +1373,42 @@ public:
// create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false
app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) {
app_ref t = mk_term(term, k.is_int());
bool is_int = k.is_int();
rational offset = -k;
u_map<rational> coeffs;
term2coeffs(term, coeffs, rational::one(), offset);
offset.neg();
if (is_int) {
// 3x + 6y >= 5 -> x + 3y >= 5/3, then x + 3y >= 2
// 3x + 6y <= 5 -> x + 3y <= 1
rational g = gcd_reduce(coeffs);
if (!g.is_one()) {
if (lower_bound) {
offset = div(offset + g - rational::one(), g);
}
else {
offset = div(offset, g);
}
}
}
if (!coeffs.empty() && coeffs.begin()->m_value.is_neg()) {
offset.neg();
lower_bound = !lower_bound;
for (auto& kv : coeffs) kv.m_value.neg();
}
app_ref atom(m);
app_ref t = coeffs2app(coeffs, rational::zero(), is_int);
if (lower_bound) {
atom = a.mk_ge(t, a.mk_numeral(k, k.is_int()));
atom = a.mk_ge(t, a.mk_numeral(offset, is_int));
}
else {
atom = a.mk_le(t, a.mk_numeral(k, k.is_int()));
atom = a.mk_le(t, a.mk_numeral(offset, is_int));
}
expr_ref atom1(m);
proof_ref atomp(m);
ctx().get_rewriter()(atom, atom1, atomp);
atom = to_app(atom1);
TRACE("arith", tout << atom << "\n";
m_solver->print_term(term, tout << "bound atom: "); tout << " <= " << k << "\n";);
TRACE("arith", tout << t << ": " << atom << "\n";
m_solver->print_term(term, tout << "bound atom: "); tout << (lower_bound?" >= ":" <= ") << k << "\n";);
ctx().internalize(atom, true);
ctx().mark_as_relevant(atom.get());
return atom;
@ -1392,6 +1427,7 @@ public:
case lp::lia_move::sat:
return l_true;
case lp::lia_move::branch: {
TRACE("arith", tout << "branch\n";);
app_ref b = mk_bound(term, k, !upper);
// branch on term >= k + 1
// branch on term <= k
@ -1401,6 +1437,7 @@ public:
return l_false;
}
case lp::lia_move::cut: {
TRACE("arith", tout << "cut\n";);
++m_stats.m_gomory_cuts;
// m_explanation implies term <= k
app_ref b = mk_bound(term, k, !upper);
@ -1444,7 +1481,7 @@ public:
}
if (!m_nra) return l_true;
if (!m_nra->need_check()) return l_true;
m_a1 = 0; m_a2 = 0;
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nra->check(m_explanation);
m_a1 = alloc(scoped_anum, m_nra->am());
m_a2 = alloc(scoped_anum, m_nra->am());
@ -1499,10 +1536,7 @@ public:
}
}
else {
enode_vector::const_iterator it = r->begin_parents();
enode_vector::const_iterator end = r->end_parents();
for (; it != end; ++it) {
enode * parent = *it;
for (enode * parent : r->get_const_parents()) {
if (is_underspecified(parent->get_owner())) {
return true;
}
@ -1703,6 +1737,7 @@ public:
void assign(literal lit) {
// SASSERT(validate_assign(lit));
dump_assign(lit);
if (m_core.size() < small_lemma_size() && m_eqs.empty()) {
m_core2.reset();
for (auto const& c : m_core) {
@ -1773,12 +1808,11 @@ public:
lp_api::bound* lo_inf = end, *lo_sup = end;
lp_api::bound* hi_inf = end, *hi_sup = end;
for (unsigned i = 0; i < bounds.size(); ++i) {
lp_api::bound& other = *bounds[i];
if (&other == &b) continue;
if (b.get_bv() == other.get_bv()) continue;
lp_api::bound_kind kind2 = other.get_bound_kind();
rational const& k2 = other.get_value();
for (lp_api::bound* other : bounds) {
if (other == &b) continue;
if (b.get_bv() == other->get_bv()) continue;
lp_api::bound_kind kind2 = other->get_bound_kind();
rational const& k2 = other->get_value();
if (k1 == k2 && kind1 == kind2) {
// the bounds are equivalent.
continue;
@ -1788,20 +1822,20 @@ public:
if (kind2 == lp_api::lower_t) {
if (k2 < k1) {
if (lo_inf == end || k2 > lo_inf->get_value()) {
lo_inf = &other;
lo_inf = other;
}
}
else if (lo_sup == end || k2 < lo_sup->get_value()) {
lo_sup = &other;
lo_sup = other;
}
}
else if (k2 < k1) {
if (hi_inf == end || k2 > hi_inf->get_value()) {
hi_inf = &other;
hi_inf = other;
}
}
else if (hi_sup == end || k2 < hi_sup->get_value()) {
hi_sup = &other;
hi_sup = other;
}
}
if (lo_inf != end) mk_bound_axiom(b, *lo_inf);
@ -2119,8 +2153,8 @@ public:
vi = m_todo_vars.back();
m_todo_vars.pop_back();
lp::lar_term const& term = m_solver->get_term(vi);
for (auto const& coeff : term.m_coeffs) {
lp::var_index wi = coeff.first;
for (auto const& coeff : term) {
lp::var_index wi = coeff.var();
if (m_solver->is_term(wi)) {
m_todo_vars.push_back(wi);
}
@ -2527,6 +2561,7 @@ public:
}
}
// SASSERT(validate_conflict());
dump_conflict();
ctx().set_conflict(
ctx().mk_justification(
ext_theory_conflict_justification(
@ -2570,19 +2605,23 @@ public:
m_todo_terms.push_back(std::make_pair(vi, rational::one()));
TRACE("arith", tout << "v" << v << " := w" << vi << "\n";
m_solver->print_term(m_solver->get_term(vi), tout); tout << "\n";);
m_nra->am().set(r, 0);
while (!m_todo_terms.empty()) {
rational wcoeff = m_todo_terms.back().second;
// lp::var_index wi = m_todo_terms.back().first; // todo : got a warning "wi is not used"
vi = m_todo_terms.back().first;
m_todo_terms.pop_back();
lp::lar_term const& term = m_solver->get_term(vi);
TRACE("arith", m_solver->print_term(term, tout); tout << "\n";);
scoped_anum r1(m_nra->am());
rational c1 = term.m_v * wcoeff;
m_nra->am().set(r1, c1.to_mpq());
m_nra->am().add(r, r1, r);
for (auto const coeff : term.m_coeffs) {
lp::var_index wi = coeff.first;
c1 = coeff.second * wcoeff;
for (auto const & arg : term) {
lp::var_index wi = m_solver->local2external(arg.var());
c1 = arg.coeff() * wcoeff;
if (m_solver->is_term(wi)) {
m_todo_terms.push_back(std::make_pair(wi, c1));
}
@ -2612,6 +2651,8 @@ public:
}
else {
rational r = get_value(v);
TRACE("arith", tout << "v" << v << " := " << r << "\n";);
SASSERT(!a.is_int(o) || r.is_int());
if (a.is_int(o) && !r.is_int()) r = floor(r);
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
}
@ -2684,10 +2725,14 @@ public:
}
};
bool validate_conflict() {
void dump_conflict() {
if (dump_lemmas()) {
ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
(void)id;
}
}
bool validate_conflict() {
if (m_arith_params.m_arith_mode != AS_NEW_ARITH) return true;
scoped_arith_mode _sa(ctx().get_fparams());
context nctx(m, ctx().get_fparams(), ctx().get_params());
@ -2699,10 +2744,14 @@ public:
return result;
}
bool validate_assign(literal lit) {
void dump_assign(literal lit) {
if (dump_lemmas()) {
ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
(void)id;
}
}
bool validate_assign(literal lit) {
if (m_arith_params.m_arith_mode != AS_NEW_ARITH) return true;
scoped_arith_mode _sa(ctx().get_fparams());
context nctx(m, ctx().get_fparams(), ctx().get_params());
@ -2728,13 +2777,13 @@ public:
}
void add_background(context& nctx) {
for (unsigned i = 0; i < m_core.size(); ++i) {
for (literal c : m_core) {
expr_ref tmp(m);
ctx().literal2expr(m_core[i], tmp);
ctx().literal2expr(c, tmp);
nctx.assert_expr(tmp);
}
for (unsigned i = 0; i < m_eqs.size(); ++i) {
nctx.assert_expr(m.mk_eq(m_eqs[i].first->get_owner(), m_eqs[i].second->get_owner()));
for (auto const& eq : m_eqs) {
nctx.assert_expr(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()));
}
}
@ -2753,20 +2802,22 @@ public:
lp::var_index vi = m_theory_var2var_index[v];
st = m_solver->maximize_term(vi, term_max);
}
TRACE("arith", display(tout << st << " v" << v << "\n"););
switch (st) {
case lp::lp_status::OPTIMAL: {
inf_rational val(term_max.x, term_max.y);
init_variable_values();
inf_rational val = get_value(v);
// inf_rational val(term_max.x, term_max.y);
blocker = mk_gt(v);
return inf_eps(rational::zero(), val);
}
case lp::lp_status::FEASIBLE: {
inf_rational val(term_max.x, term_max.y);
// todo , TODO , not sure what happens here
inf_rational val = get_value(v);
blocker = mk_gt(v);
return inf_eps(rational::zero(), val);
}
default:
SASSERT(st == lp::lp_status::UNBOUNDED);
TRACE("arith", tout << "Unbounded v" << v << "\n";);
has_shared = false;
blocker = m.mk_false();
return inf_eps(rational::one(), inf_rational());
@ -2802,29 +2853,48 @@ public:
}
theory_var add_objective(app* term) {
TRACE("opt", tout << expr_ref(term, m) << "\n";);
return internalize_def(term);
}
app_ref mk_term(lp::lar_term const& term, bool is_int) {
expr_ref_vector args(m);
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff, rational& offset) {
for (const auto & ti : term) {
theory_var w;
if (m_solver->is_term(ti.var())) {
w = m_term_index2theory_var[m_solver->adjust_term_index(ti.var())];
//w = m_term_index2theory_var.get(m_solver->adjust_term_index(ti.var()), null_theory_var);
//if (w == null_theory_var) // if extracing expressions directly from nested term
lp::lar_term const& term1 = m_solver->get_term(ti.var());
rational coeff2 = coeff * ti.coeff();
term2coeffs(term1, coeffs, coeff2, offset);
continue;
}
else {
w = m_var_index2theory_var[ti.var()];
}
rational c0(0);
coeffs.find(w, c0);
coeffs.insert(w, c0 + ti.coeff() * coeff);
}
offset += coeff * term.m_v;
}
app_ref coeffs2app(u_map<rational> const& coeffs, rational const& offset, bool is_int) {
expr_ref_vector args(m);
for (auto const& kv : coeffs) {
theory_var w = kv.m_key;
expr* o = get_enode(w)->get_owner();
if (ti.coeff().is_one()) {
if (kv.m_value.is_zero()) {
// continue
}
else if (kv.m_value.is_one()) {
args.push_back(o);
}
else {
args.push_back(a.mk_mul(a.mk_numeral(ti.coeff(), is_int), o));
args.push_back(a.mk_mul(a.mk_numeral(kv.m_value, is_int), o));
}
}
if (!term.m_v.is_zero()) {
args.push_back(a.mk_numeral(term.m_v, is_int));
if (!offset.is_zero()) {
args.push_back(a.mk_numeral(offset, is_int));
}
switch (args.size()) {
case 0:
@ -2836,6 +2906,26 @@ public:
}
}
app_ref mk_term(lp::lar_term const& term, bool is_int) {
u_map<rational> coeffs;
rational offset;
term2coeffs(term, coeffs, rational::one(), offset);
return coeffs2app(coeffs, offset, is_int);
}
rational gcd_reduce(u_map<rational>& coeffs) {
rational g(0);
for (auto const& kv : coeffs) {
g = gcd(g, kv.m_value);
}
if (!g.is_one() && !g.is_zero()) {
for (auto& kv : coeffs) {
kv.m_value /= g;
}
}
return g;
}
app_ref mk_obj(theory_var v) {
lp::var_index vi = m_theory_var2var_index[v];
bool is_int = a.is_int(get_enode(v)->get_owner());

34
src/smt/theory_pb.cpp
View file

@ -1429,23 +1429,27 @@ namespace smt {
return literal(ctx.mk_bool_var(y));
}
literal mk_max(literal a, literal b) {
if (a == b) return a;
expr_ref t1(m), t2(m), t3(m);
ctx.literal2expr(a, t1);
ctx.literal2expr(b, t2);
t3 = m.mk_or(t1, t2);
bool_var v = ctx.b_internalized(t3)?ctx.get_bool_var(t3):ctx.mk_bool_var(t3);
literal mk_max(unsigned n, literal const* lits) {
expr_ref_vector es(m);
expr_ref tmp(m);
for (unsigned i = 0; i < n; ++i) {
ctx.literal2expr(lits[i], tmp);
es.push_back(tmp);
}
tmp = m.mk_or(es.size(), es.c_ptr());
bool_var v = ctx.b_internalized(tmp)?ctx.get_bool_var(tmp):ctx.mk_bool_var(tmp);
return literal(v);
}
literal mk_min(literal a, literal b) {
if (a == b) return a;
expr_ref t1(m), t2(m), t3(m);
ctx.literal2expr(a, t1);
ctx.literal2expr(b, t2);
t3 = m.mk_and(t1, t2);
bool_var v = ctx.b_internalized(t3)?ctx.get_bool_var(t3):ctx.mk_bool_var(t3);
literal mk_min(unsigned n, literal const* lits) {
expr_ref_vector es(m);
expr_ref tmp(m);
for (unsigned i = 0; i < n; ++i) {
ctx.literal2expr(lits[i], tmp);
es.push_back(tmp);
}
tmp = m.mk_and(es.size(), es.c_ptr());
bool_var v = ctx.b_internalized(tmp)?ctx.get_bool_var(tmp):ctx.mk_bool_var(tmp);
return literal(v);
}

159
src/smt/theory_seq.cpp
View file

@ -367,7 +367,7 @@ bool theory_seq::branch_binary_variable(eq const& e) {
return false;
}
ptr_vector<expr> xs, ys;
expr* x, *y;
expr_ref x(m), y(m);
bool is_binary = is_binary_eq(e.ls(), e.rs(), x, xs, ys, y);
if (!is_binary) {
is_binary = is_binary_eq(e.rs(), e.ls(), x, xs, ys, y);
@ -630,7 +630,7 @@ bool theory_seq::branch_ternary_variable_base(
// Equation is of the form x ++ xs = y1 ++ ys ++ y2 where xs, ys are units.
bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
expr_ref_vector xs(m), ys(m);
expr* x = nullptr, *y1 = nullptr, *y2 = nullptr;
expr_ref x(m), y1(m), y2(m);
bool is_ternary = is_ternary_eq(e.ls(), e.rs(), x, xs, y1, ys, y2, flag1);
if (!is_ternary) {
is_ternary = is_ternary_eq(e.rs(), e.ls(), x, xs, y1, ys, y2, flag1);
@ -746,7 +746,7 @@ bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector
// Equation is of the form xs ++ x = y1 ++ ys ++ y2 where xs, ys are units.
bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
expr_ref_vector xs(m), ys(m);
expr* x = nullptr, *y1 = nullptr, *y2 = nullptr;
expr_ref x(m), y1(m), y2(m);
bool is_ternary = is_ternary_eq2(e.ls(), e.rs(), xs, x, y1, ys, y2, flag1);
if (!is_ternary) {
is_ternary = is_ternary_eq2(e.rs(), e.ls(), xs, x, y1, ys, y2, flag1);
@ -823,7 +823,7 @@ bool theory_seq::branch_quat_variable() {
// Equation is of the form x1 ++ xs ++ x2 = y1 ++ ys ++ y2 where xs, ys are units.
bool theory_seq::branch_quat_variable(eq const& e) {
expr_ref_vector xs(m), ys(m);
expr* x1_l = nullptr, *x2 = nullptr, *y1_l = nullptr, *y2 = nullptr;
expr_ref x1_l(m), x2(m), y1_l(m), y2(m);
bool is_quat = is_quat_eq(e.ls(), e.rs(), x1_l, xs, x2, y1_l, ys, y2);
if (!is_quat) {
return false;
@ -889,38 +889,35 @@ bool theory_seq::branch_quat_variable(eq const& e) {
return true;
}
void theory_seq::len_offset(expr* const& e, rational val) {
void theory_seq::len_offset(expr* e, rational val) {
context & ctx = get_context();
expr *l1 = nullptr, *l2 = nullptr, *l21 = nullptr, *l22 = nullptr;
rational fact;
if (m_autil.is_add(e, l1, l2) && m_autil.is_mul(l2, l21, l22) &&
m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
if (ctx.e_internalized(l1) && ctx.e_internalized(l22)) {
enode* r1 = ctx.get_enode(l1)->get_root(), *n1 = r1;
enode* r2 = ctx.get_enode(l22)->get_root(), *n2 = r2;
expr *e1 = nullptr, *e2 = nullptr;
do {
if (!m_util.str.is_length(n1->get_owner(), e1))
n1 = n1->get_next();
else
if (m_util.str.is_length(n1->get_owner(), e1))
break;
n1 = n1->get_next();
}
while (n1 != r1);
do {
if (!m_util.str.is_length(n2->get_owner(), e2))
n2 = n2->get_next();
else
if (m_util.str.is_length(n2->get_owner(), e2))
break;
n2 = n2->get_next();
}
while (n2 != r2);
obj_map<enode, int> tmp;
if (m_util.str.is_length(n1->get_owner(), e1)
&& m_util.str.is_length(n2->get_owner(), e2)) {
obj_map<enode, int> tmp;
m_len_offset.find(r1, tmp);
&& m_util.str.is_length(n2->get_owner(), e2) &&
m_len_offset.find(r1, tmp)) {
tmp.insert(r2, val.get_int32());
m_len_offset.insert(r1, tmp);
TRACE("seq", tout << "a length pair: " << mk_pp(e1, m)
<< ", " << mk_pp(e2, m) << "\n";);
TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";);
return;
}
}
@ -1083,8 +1080,8 @@ void theory_seq::find_max_eq_len(expr_ref_vector const& ls, expr_ref_vector cons
}
// TODO: propagate length offsets for last vars
bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned const& idx,
dependency*& deps, expr_ref_vector & res) {
bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned idx,
dependency*& deps, expr_ref_vector & res) {
context& ctx = get_context();
if (ls.empty() || rs.empty())
@ -1307,32 +1304,34 @@ bool theory_seq::len_based_split(eq const& e) {
y12 = mk_concat(Z, y12);
}
}
else
lenY11 = m_util.str.mk_length(y11);
else {
lenY11 = m_util.str.mk_length(y11);
}
dependency* dep = e.dep();
literal_vector lits;
literal lit1 = mk_eq(lenX11, lenY11, false);
if (ctx.get_assignment(lit1) != l_true) {
return false;
}
lits.push_back(lit1);
if (ls.size()>=2 && rs.size()>=2 && (ls.size()>2 || rs.size()>2)) {
if (ls.size() >= 2 && rs.size() >= 2 && (ls.size() > 2 || rs.size() > 2)) {
expr_ref len1(m_autil.mk_int(0),m), len2(m_autil.mk_int(0),m);
for (unsigned i = 2; i < ls.size(); ++i)
len1 = mk_add(len1, m_util.str.mk_length(ls[i]));
for (unsigned i = 2; i < rs.size(); ++i)
len2 = mk_add(len2, m_util.str.mk_length(rs[i]));
bool flag = false;
literal lit2;
if (!m_autil.is_numeral(len1) && !m_autil.is_numeral(len2)) {
literal lit2 = mk_eq(len1, len2, false);
flag = ctx.get_assignment(lit2) == l_true;
lit2 = mk_eq(len1, len2, false);
}
else {
expr_ref eq_len(m.mk_eq(len1, len2), m);
flag = ctx.find_assignment(eq_len) == l_true;
lit2 = mk_literal(eq_len);
}
if (flag) {
literal lit2 = mk_eq(len1, len2, false);
if (ctx.get_assignment(lit2) == l_true) {
lits.push_back(lit2);
TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";);
expr_ref lhs(m), rhs(m);
@ -2263,6 +2262,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
SASSERT(lhs.size() == rhs.size());
m_seq_rewrite.add_seqs(ls, rs, lhs, rhs);
if (lhs.empty()) {
TRACE("seq", tout << "solved\n";);
return true;
}
TRACE("seq",
@ -2412,6 +2412,7 @@ bool theory_seq::solve_eqs(unsigned i) {
m_eqs.pop_back();
change = true;
}
TRACE("seq", display_equations(tout););
}
return change || m_new_propagation || ctx.inconsistent();
}
@ -2430,6 +2431,7 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
display_deps(tout, deps);
);
if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
TRACE("seq", tout << "simplified\n";);
return true;
}
TRACE("seq", tout << ls << " = " << rs << "\n";);
@ -2465,6 +2467,7 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
if (!updated) {
m_eqs.push_back(eq(m_eq_id++, ls, rs, deps));
}
TRACE("seq", tout << "simplified\n";);
return true;
}
return false;
@ -2484,7 +2487,7 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
return false;
}
bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr*& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr*& y) {
bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
if (ls.size() > 1 && is_var(ls[0]) &&
rs.size() > 1 && is_var(rs.back())) {
xs.reset();
@ -2505,7 +2508,7 @@ bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const&
}
bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
expr*& x1, expr_ref_vector& xs, expr*& x2, expr*& y1, expr_ref_vector& ys, expr*& y2) {
expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
unsigned l_start = 1;
@ -2548,7 +2551,7 @@ expr*& x1, expr_ref_vector& xs, expr*& x2, expr*& y1, expr_ref_vector& ys, expr*
}
bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
expr*& x, expr_ref_vector& xs, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1) {
expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
if (ls.size() > 1 && (is_var(ls[0]) || flag1) &&
rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
unsigned l_start = ls.size()-1;
@ -2586,7 +2589,7 @@ expr*& x, expr_ref_vector& xs, expr*& y1, expr_ref_vector& ys, expr*& y2, bool f
}
bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs,
expr_ref_vector& xs, expr*& x, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1) {
expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
if (ls.size() > 1 && (is_var(ls.back()) || flag1) &&
rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
unsigned l_start = 0;
@ -2748,7 +2751,7 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
context& ctx = get_context();
ptr_vector<expr> xs, ys;
expr* x, *y;
expr_ref x(m), y(m);
bool is_binary = is_binary_eq(ls, rs, x, xs, ys, y);
if (!is_binary) {
is_binary = is_binary_eq(rs, ls, x, xs, ys, y);
@ -2771,49 +2774,36 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
UNREACHABLE();
return false;
}
unsigned sz = xs.size();
literal_vector conflict;
for (unsigned offset = 0; offset < sz; ++offset) {
bool has_conflict = false;
for (unsigned j = 0; !has_conflict && j < sz; ++j) {
unsigned j1 = (offset + j) % sz;
if (xs[j] == ys[j1]) continue;
literal eq = mk_eq(xs[j], ys[j1], false);
switch (ctx.get_assignment(eq)) {
case l_false:
conflict.push_back(~eq);
has_conflict = true;
break;
case l_undef: {
enode* n1 = ensure_enode(xs[j]);
enode* n2 = ensure_enode(ys[j1]);
if (n1->get_root() == n2->get_root()) {
break;
}
ctx.mark_as_relevant(eq);
if (sz == 1) {
propagate_lit(dep, 0, nullptr, eq);
return true;
}
m_new_propagation = true;
break;
}
case l_true:
break;
}
}
if (!has_conflict) {
TRACE("seq", tout << "offset: " << offset << " equality ";
for (unsigned j = 0; j < sz; ++j) {
tout << mk_pp(xs[j], m) << " = " << mk_pp(ys[(offset+j) % sz], m) << "; ";
}
tout << "\n";);
// current equalities can work when solving x ++ xs = ys ++ y
// Equation is of the form x ++ xs = ys ++ x
// where |xs| = |ys| are units of same length
// then xs is a wrap-around of ys
// x ++ ab = ba ++ x
//
if (xs.size() == 1) {
enode* n1 = ensure_enode(xs[0]);
enode* n2 = ensure_enode(ys[0]);
if (n1->get_root() == n2->get_root()) {
return false;
}
literal eq = mk_eq(xs[0], ys[0], false);
switch (ctx.get_assignment(eq)) {
case l_false: {
literal_vector conflict;
conflict.push_back(~eq);
TRACE("seq", tout << conflict << "\n";);
set_conflict(dep, conflict);
break;
}
case l_true:
break;
case l_undef:
ctx.mark_as_relevant(eq);
propagate_lit(dep, 0, nullptr, eq);
m_new_propagation = true;
break;
}
}
TRACE("seq", tout << conflict << "\n";);
set_conflict(dep, conflict);
return false;
}
@ -4582,7 +4572,6 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) const {
if (thi && thi->get_lower(ctx.get_enode(e), _lo)) break;
theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
if (thr && thr->get_lower(ctx.get_enode(e), _lo)) break;
TRACE("seq", tout << "no lower bound " << mk_pp(_e, m) << "\n";);
return false;
}
while (false);
@ -4640,7 +4629,6 @@ bool theory_seq::upper_bound(expr* _e, rational& hi) const {
if (thi && thi->get_upper(ctx.get_enode(e), _hi)) break;
theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
if (thr && thr->get_upper(ctx.get_enode(e), _hi)) break;
TRACE("seq", tout << "no upper bound " << mk_pp(_e, m) << "\n";);
return false;
}
while (false);
@ -5163,7 +5151,22 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
}
}
else if (m_util.str.is_contains(e, e1, e2)) {
if (is_true) {
expr_ref_vector disj(m);
// disabled pending regression on issue 1196
if (false && m_seq_rewrite.reduce_contains(e1, e2, disj)) {
literal_vector lits;
literal lit = mk_literal(e);
lits.push_back(~lit);
for (expr* d : disj) {
lits.push_back(mk_literal(d));
}
++m_stats.m_add_axiom;
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
for (expr* d : disj) {
add_axiom(lit, ~mk_literal(d));
}
}
else if (is_true) {
expr_ref f1 = mk_skolem(m_indexof_left, e1, e2);
expr_ref f2 = mk_skolem(m_indexof_right, e1, e2);
f = mk_concat(f1, e2, f2);
@ -5236,6 +5239,7 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
}
void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
TRACE("seq", tout << expr_ref(n1->get_owner(), m) << " = " << expr_ref(n2->get_owner(), m) << "\n";);
if (n1 != n2 && m_util.is_seq(n1->get_owner())) {
theory_var v1 = n1->get_th_var(get_id());
theory_var v2 = n2->get_th_var(get_id());
@ -5263,9 +5267,10 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
enode* n2 = get_enode(v2);
expr_ref e1(n1->get_owner(), m);
expr_ref e2(n2->get_owner(), m);
SASSERT(n1->get_root() != n2->get_root());
m_exclude.update(e1, e2);
expr_ref eq(m.mk_eq(e1, e2), m);
TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";);

12
src/smt/theory_seq.h
View file

@ -375,13 +375,13 @@ namespace smt {
void init_model(expr_ref_vector const& es);
void len_offset(expr* const& e, rational val);
void len_offset(expr* e, rational val);
void prop_arith_to_len_offset();
int find_fst_non_empty_idx(expr_ref_vector const& x) const;
expr* find_fst_non_empty_var(expr_ref_vector const& x) const;
void find_max_eq_len(expr_ref_vector const& ls, expr_ref_vector const& rs);
bool has_len_offset(expr_ref_vector const& ls, expr_ref_vector const& rs, int & diff);
bool find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned const& idx, dependency*& deps, expr_ref_vector & res);
bool find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned idx, dependency*& deps, expr_ref_vector & res);
// final check
bool simplify_and_solve_eqs(); // solve unitary equalities
@ -427,10 +427,10 @@ namespace smt {
bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
bool solve_unit_eq(expr* l, expr* r, dependency* dep);
bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr*& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr*& y);
bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr*& x1, expr_ref_vector& xs, expr*& x2, expr*& y1, expr_ref_vector& ys, expr*& y2);
bool is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr*& x, expr_ref_vector& xs, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1);
bool is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& xs, expr*& x, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1);
bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr_ref& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr_ref& y);
bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
bool is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1);
bool is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1);
bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool propagate_max_length(expr* l, expr* r, dependency* dep);