mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 07:27:57 +00:00
Code Activity

synchronizing with main repository

Browse source
This commit is contained in:
nilsbecker 2019-02-22 00:19:43 +01:00
commit ec76efedbe
386 changed files with 10027 additions and 8346 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/arith_eq_solver.cpp
View file

@ -608,8 +608,8 @@ bool arith_eq_solver::solve_integer_equations_gcd(
return false;
}
live.erase(live.begin()+live_pos);
for (j = 0; j < live.size(); ++j) {
row& r = rows[live[j]];
for (unsigned l : live) {
row& r = rows[l];
if (!r[i].is_zero()) {
substitute(r, r0, i);
gcd_normalize(r);
@ -625,10 +625,7 @@ bool arith_eq_solver::solve_integer_equations_gcd(
TRACE("arith_eq_solver",
tout << ((live.size()<=1)?"solved ":"incomplete check ") << live.size() << "\n";
for (unsigned i = 0; i < live.size(); ++i) {
print_row(tout, rows[live[i]]);
}
);
for (unsigned l : live) print_row(tout, rows[l]); );
return true;
}

6
src/smt/asserted_formulas.cpp
View file

@ -449,7 +449,7 @@ void asserted_formulas::propagate_values() {
m_expr2depth.reset();
m_scoped_substitution.push();
unsigned prop = num_prop;
TRACE("propagate_values", tout << "before:\n"; display(tout););
TRACE("propagate_values", display(tout << "before:\n"););
unsigned i = m_qhead;
unsigned sz = m_formulas.size();
for (; i < sz; i++) {
@ -482,15 +482,13 @@ unsigned asserted_formulas::propagate_values(unsigned i) {
expr_ref new_n(m);
proof_ref new_pr(m);
m_rewriter(n, new_n, new_pr);
TRACE("propagate_values", tout << n << "\n" << new_n << "\n";);
if (m.proofs_enabled()) {
proof * pr = m_formulas[i].get_proof();
new_pr = m.mk_modus_ponens(pr, new_pr);
}
justified_expr j(m, new_n, new_pr);
m_formulas[i] = j;
if (m_formulas[i].get_fml() != new_n) {
std::cout << "NOT updated\n";
}
if (m.is_false(j.get_fml())) {
m_inconsistent = true;
}

2
src/smt/mam.cpp
View file

@ -3915,7 +3915,7 @@ namespace smt {
SASSERT(bindings[i]->get_generation() <= max_generation);
}
#endif
unsigned min_gen, max_gen;
unsigned min_gen = 0, max_gen = 0;
m_interpreter.get_min_max_top_generation(min_gen, max_gen);
m_context.add_instance(qa, pat, num_bindings, bindings, nullptr, max_generation, min_gen, max_gen, used_enodes);
}

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

@ -58,8 +58,6 @@ def_module_params(module_name='smt',
('arith.auto_config_simplex', BOOL, False, 'force simplex solver in auto_config'),
('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'),
('pb.enable_simplex', BOOL, False, 'enable simplex to check rational feasibility'),
('array.weak', BOOL, False, 'weak array theory'),
('array.extensional', BOOL, True, 'extensional array theory'),
('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),

6
src/smt/params/theory_pb_params.cpp
View file

@ -23,8 +23,6 @@ void theory_pb_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
m_pb_conflict_frequency = p.pb_conflict_frequency();
m_pb_learn_complements = p.pb_learn_complements();
m_pb_enable_compilation = p.pb_enable_compilation();
m_pb_enable_simplex = p.pb_enable_simplex();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
@ -32,6 +30,4 @@ void theory_pb_params::updt_params(params_ref const & _p) {
void theory_pb_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_pb_conflict_frequency);
DISPLAY_PARAM(m_pb_learn_complements);
DISPLAY_PARAM(m_pb_enable_compilation);
DISPLAY_PARAM(m_pb_enable_simplex);
}
}

6
src/smt/params/theory_pb_params.h
View file

@ -25,13 +25,9 @@ Revision History:
struct theory_pb_params {
unsigned m_pb_conflict_frequency;
bool m_pb_learn_complements;
bool m_pb_enable_compilation;
bool m_pb_enable_simplex;
theory_pb_params(params_ref const & p = params_ref()):
m_pb_conflict_frequency(1000),
m_pb_learn_complements(true),
m_pb_enable_compilation(true),
m_pb_enable_simplex(false)
m_pb_learn_complements(true)
{}
void updt_params(params_ref const & p);

2
src/smt/proto_model/array_factory.cpp
View file

@ -104,7 +104,7 @@ bool array_factory::mk_two_diff_values_for(sort * s) {
bool array_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
value_set * set = nullptr;
if (!m_sort2value_set.find(s, set) || set->size() == 0) {
if (!m_sort2value_set.find(s, set) || set->empty()) {
if (!mk_two_diff_values_for(s))
return false;
}

97
src/smt/smt_arith_value.cpp
View file

@ -18,30 +18,32 @@ Revision History:
--*/
#include "smt/smt_arith_value.h"
#include "smt/theory_lra.h"
#include "smt/theory_arith.h"
namespace smt {
arith_value::arith_value(context& ctx):
m_ctx(ctx), m(ctx.get_manager()), a(m) {}
arith_value::arith_value(ast_manager& m):
m_ctx(nullptr), m(m), a(m) {}
bool arith_value::get_lo(expr* e, rational& lo, bool& is_strict) {
if (!m_ctx.e_internalized(e)) return false;
void arith_value::init(context* ctx) {
m_ctx = ctx;
family_id afid = a.get_family_id();
theory* th = m_ctx->get_theory(afid);
m_tha = dynamic_cast<theory_mi_arith*>(th);
m_thi = dynamic_cast<theory_i_arith*>(th);
m_thr = dynamic_cast<theory_lra*>(th);
}
bool arith_value::get_lo_equiv(expr* e, rational& lo, bool& is_strict) {
if (!m_ctx->e_internalized(e)) return false;
is_strict = false;
enode* next = m_ctx.get_enode(e), *n = next;
enode* next = m_ctx->get_enode(e), *n = next;
bool found = false;
bool is_strict1;
rational lo1;
theory* th = m_ctx.get_theory(afid);
theory_mi_arith* tha = dynamic_cast<theory_mi_arith*>(th);
theory_i_arith* thi = dynamic_cast<theory_i_arith*>(th);
theory_lra* thr = dynamic_cast<theory_lra*>(th);
do {
if ((tha && tha->get_lower(next, lo1, is_strict1)) ||
(thi && thi->get_lower(next, lo1, is_strict1)) ||
(thr && thr->get_lower(next, lo1, is_strict1))) {
if ((m_tha && m_tha->get_lower(next, lo1, is_strict1)) ||
(m_thi && m_thi->get_lower(next, lo1, is_strict1)) ||
(m_thr && m_thr->get_lower(next, lo1, is_strict1))) {
if (!found || lo1 > lo || (lo == lo1 && is_strict1)) lo = lo1, is_strict = is_strict1;
found = true;
}
@ -51,21 +53,16 @@ namespace smt {
return found;
}
bool arith_value::get_up(expr* e, rational& up, bool& is_strict) {
if (!m_ctx.e_internalized(e)) return false;
family_id afid = a.get_family_id();
bool arith_value::get_up_equiv(expr* e, rational& up, bool& is_strict) {
if (!m_ctx->e_internalized(e)) return false;
is_strict = false;
enode* next = m_ctx.get_enode(e), *n = next;
enode* next = m_ctx->get_enode(e), *n = next;
bool found = false, is_strict1;
rational up1;
theory* th = m_ctx.get_theory(afid);
theory_mi_arith* tha = dynamic_cast<theory_mi_arith*>(th);
theory_i_arith* thi = dynamic_cast<theory_i_arith*>(th);
theory_lra* thr = dynamic_cast<theory_lra*>(th);
do {
if ((tha && tha->get_upper(next, up1, is_strict1)) ||
(thi && thi->get_upper(next, up1, is_strict1)) ||
(thr && thr->get_upper(next, up1, is_strict1))) {
if ((m_tha && m_tha->get_upper(next, up1, is_strict1)) ||
(m_thi && m_thi->get_upper(next, up1, is_strict1)) ||
(m_thr && m_thr->get_upper(next, up1, is_strict1))) {
if (!found || up1 < up || (up1 == up && is_strict1)) up = up1, is_strict = is_strict1;
found = true;
}
@ -75,20 +72,46 @@ namespace smt {
return found;
}
bool arith_value::get_value(expr* e, rational& val) {
if (!m_ctx.e_internalized(e)) return false;
bool arith_value::get_up(expr* e, rational& up, bool& is_strict) const {
if (!m_ctx->e_internalized(e)) return false;
is_strict = false;
enode* n = m_ctx->get_enode(e);
if (m_tha) return m_tha->get_upper(n, up, is_strict);
if (m_thi) return m_thi->get_upper(n, up, is_strict);
if (m_thr) return m_thr->get_upper(n, up, is_strict);
return false;
}
bool arith_value::get_lo(expr* e, rational& up, bool& is_strict) const {
if (!m_ctx->e_internalized(e)) return false;
is_strict = false;
enode* n = m_ctx->get_enode(e);
if (m_tha) return m_tha->get_lower(n, up, is_strict);
if (m_thi) return m_thi->get_lower(n, up, is_strict);
if (m_thr) return m_thr->get_lower(n, up, is_strict);
return false;
}
bool arith_value::get_value(expr* e, rational& val) const {
if (!m_ctx->e_internalized(e)) return false;
expr_ref _val(m);
enode* next = m_ctx.get_enode(e), *n = next;
family_id afid = a.get_family_id();
theory* th = m_ctx.get_theory(afid);
theory_mi_arith* tha = dynamic_cast<theory_mi_arith*>(th);
theory_i_arith* thi = dynamic_cast<theory_i_arith*>(th);
theory_lra* thr = dynamic_cast<theory_lra*>(th);
enode* n = m_ctx->get_enode(e);
if (m_tha && m_tha->get_value(n, _val) && a.is_numeral(_val, val)) return true;
if (m_thi && m_thi->get_value(n, _val) && a.is_numeral(_val, val)) return true;
if (m_thr && m_thr->get_value(n, val)) return true;
return false;
}
bool arith_value::get_value_equiv(expr* e, rational& val) const {
if (!m_ctx->e_internalized(e)) return false;
expr_ref _val(m);
enode* next = m_ctx->get_enode(e), *n = next;
do {
e = next->get_owner();
if (tha && tha->get_value(next, _val) && a.is_numeral(_val, val)) return true;
if (thi && thi->get_value(next, _val) && a.is_numeral(_val, val)) return true;
if (thr && thr->get_value(next, val)) return true;
if (m_tha && m_tha->get_value(next, _val) && a.is_numeral(_val, val)) return true;
if (m_thi && m_thi->get_value(next, _val) && a.is_numeral(_val, val)) return true;
if (m_thr && m_thr->get_value(next, val)) return true;
next = next->get_next();
}
while (next != n);
@ -97,7 +120,7 @@ namespace smt {
final_check_status arith_value::final_check() {
family_id afid = a.get_family_id();
theory * th = m_ctx.get_theory(afid);
theory * th = m_ctx->get_theory(afid);
return th->final_check_eh();
}
};

20
src/smt/smt_arith_value.h
View file

@ -21,18 +21,28 @@ Revision History:
#include "ast/arith_decl_plugin.h"
#include "smt/smt_context.h"
#include "smt/theory_lra.h"
#include "smt/theory_arith.h"
namespace smt {
class arith_value {
context& m_ctx;
context* m_ctx;
ast_manager& m;
arith_util a;
theory_mi_arith* m_tha;
theory_i_arith* m_thi;
theory_lra* m_thr;
public:
arith_value(context& ctx);
bool get_lo(expr* e, rational& lo, bool& strict);
bool get_up(expr* e, rational& up, bool& strict);
bool get_value(expr* e, rational& value);
arith_value(ast_manager& m);
void init(context* ctx);
bool get_lo_equiv(expr* e, rational& lo, bool& strict);
bool get_up_equiv(expr* e, rational& up, bool& strict);
bool get_value_equiv(expr* e, rational& value) const;
bool get_lo(expr* e, rational& lo, bool& strict) const;
bool get_up(expr* e, rational& up, bool& strict) const;
bool get_value(expr* e, rational& value) const;
bool get_fixed(expr* e, rational& value) const;
final_check_status final_check();
};
};

26
src/smt/smt_case_split_queue.cpp
View file

@ -80,6 +80,11 @@ namespace smt {
m_queue.decreased(v);
}
void activity_decreased_eh(bool_var v) override {
if (m_queue.contains(v))
m_queue.increased(v);
}
void mk_var_eh(bool_var v) override {
m_queue.reserve(v+1);
SASSERT(!m_queue.contains(v));
@ -167,6 +172,14 @@ namespace smt {
m_delayed_queue.decreased(v);
}
void activity_decreased_eh(bool_var v) override {
act_case_split_queue::activity_decreased_eh(v);
if (m_queue.contains(v))
m_queue.increased(v);
if (m_delayed_queue.contains(v))
m_delayed_queue.increased(v);
}
void mk_var_eh(bool_var v) override {
m_queue.reserve(v+1);
m_delayed_queue.reserve(v+1);
@ -281,7 +294,7 @@ namespace smt {
}
}
if (order == 1) {
if (undef_children.size() == 0) {
if (undef_children.empty()) {
// a bug?
} else if (undef_children.size() == 1) {
undef_child = undef_children[0];
@ -324,6 +337,8 @@ namespace smt {
void activity_increased_eh(bool_var v) override {}
void activity_decreased_eh(bool_var v) override {}
void mk_var_eh(bool_var v) override {}
void del_var_eh(bool_var v) override {}
@ -509,6 +524,8 @@ namespace smt {
void activity_increased_eh(bool_var v) override {}
void activity_decreased_eh(bool_var v) override {}
void mk_var_eh(bool_var v) override {
if (m_context.is_searching()) {
SASSERT(v >= m_bs_num_bool_vars);
@ -753,6 +770,8 @@ namespace smt {
void activity_increased_eh(bool_var v) override {}
void activity_decreased_eh(bool_var v) override {}
void mk_var_eh(bool_var v) override {}
void del_var_eh(bool_var v) override {}
@ -1133,6 +1152,11 @@ namespace smt {
m_queue.decreased(v);
}
void activity_decreased_eh(bool_var v) override {
if (m_queue.contains(v))
m_queue.increased(v);
}
void mk_var_eh(bool_var v) override {
m_queue.reserve(v+1);
m_queue.insert(v);

1
src/smt/smt_case_split_queue.h
View file

@ -32,6 +32,7 @@ namespace smt {
class case_split_queue {
public:
virtual void activity_increased_eh(bool_var v) = 0;
virtual void activity_decreased_eh(bool_var v) = 0;
virtual void mk_var_eh(bool_var v) = 0;
virtual void del_var_eh(bool_var v) = 0;
virtual void assign_lit_eh(literal l) {}

31
src/smt/smt_cg_table.cpp
View file

@ -71,10 +71,7 @@ namespace smt {
void cg_table::display(std::ostream & out) const {
out << "congruence table:\n";
table::iterator it = m_table.begin();
table::iterator end = m_table.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode * n : m_table) {
out << mk_pp(n->get_owner(), m_manager) << "\n";
}
}
@ -82,10 +79,7 @@ namespace smt {
void cg_table::display_compact(std::ostream & out) const {
if (!m_table.empty()) {
out << "congruence table:\n";
table::iterator it = m_table.begin();
table::iterator end = m_table.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode * n : m_table) {
out << "#" << n->get_owner()->get_id() << " ";
}
out << "\n";
@ -94,10 +88,7 @@ namespace smt {
#ifdef Z3DEBUG
bool cg_table::check_invariant() const {
table::iterator it = m_table.begin();
table::iterator end = m_table.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode * n : m_table) {
CTRACE("cg_table", !contains_ptr(n), tout << "#" << n->get_owner_id() << "\n";);
SASSERT(contains_ptr(n));
}
@ -136,9 +127,11 @@ namespace smt {
}
bool cg_table::cg_eq::operator()(enode * n1, enode * n2) const {
SASSERT(n1->get_num_args() == n2->get_num_args());
SASSERT(n1->get_decl() == n2->get_decl());
unsigned num = n1->get_num_args();
if (num != n2->get_num_args()) {
return false;
}
for (unsigned i = 0; i < num; i++)
if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root())
return false;
@ -205,10 +198,7 @@ namespace smt {
}
void cg_table::reset() {
ptr_vector<void>::iterator it = m_tables.begin();
ptr_vector<void>::iterator end = m_tables.end();
for (; it != end; ++it) {
void * t = *it;
for (void* t : m_tables) {
switch (GET_TAG(t)) {
case UNARY:
dealloc(UNTAG(unary_table*, t));
@ -225,10 +215,9 @@ namespace smt {
}
}
m_tables.reset();
obj_map<func_decl, unsigned>::iterator it2 = m_func_decl2id.begin();
obj_map<func_decl, unsigned>::iterator end2 = m_func_decl2id.end();
for (; it2 != end2; ++it2)
m_manager.dec_ref(it2->m_key);
for (auto const& kv : m_func_decl2id) {
m_manager.dec_ref(kv.m_key);
}
m_func_decl2id.reset();
}

2
src/smt/smt_cg_table.h
View file

@ -252,6 +252,8 @@ namespace smt {
enode_bool_pair insert(enode * n) {
// it doesn't make sense to insert a constant.
SASSERT(n->get_num_args() > 0);
SASSERT(!m_manager.is_and(n->get_owner()));
SASSERT(!m_manager.is_or(n->get_owner()));
enode * n_prime;
void * t = get_table(n);
switch (static_cast<table_kind>(GET_TAG(t))) {

20
src/smt/smt_clause.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include "smt/smt_clause.h"
#include "smt/smt_justification.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
namespace smt {
/**
@ -96,22 +97,33 @@ namespace smt {
}
}
void clause::display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
std::ostream& clause::display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
out << "(clause";
for (unsigned i = 0; i < m_num_literals; i++) {
out << " ";
m_lits[i].display(out, m, bool_var2expr_map);
}
out << ")";
return out << ")";
}
void clause::display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
std::ostream& clause::display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
out << "(clause";
for (unsigned i = 0; i < m_num_literals; i++) {
out << " ";
m_lits[i].display_compact(out, bool_var2expr_map);
}
out << ")";
return out << ")";
}
std::ostream& clause::display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
expr_ref_vector args(m);
for (unsigned i = 0; i < m_num_literals; i++) {
literal lit = m_lits[i];
args.push_back(bool_var2expr_map[lit.var()]);
if (lit.sign()) args[args.size()-1] = m.mk_not(args.back());
}
expr_ref disj(m.mk_or(args.size(), args.c_ptr()), m);
return out << disj;
}
};

6
src/smt/smt_clause.h
View file

@ -239,9 +239,11 @@ namespace smt {
set_activity(get_activity() + 1);
}
void display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
std::ostream& display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
std::ostream& display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
void display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
std::ostream& display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
unsigned hash() const {
return get_ptr_hash(this);

12
src/smt/smt_conflict_resolution.cpp
View file

@ -311,7 +311,7 @@ namespace smt {
bool_var var = antecedent.var();
unsigned lvl = m_ctx.get_assign_level(var);
SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
TRACE("conflict_", tout << "processing antecedent (level " << lvl << "):";
m_ctx.display_literal(tout, antecedent);
m_ctx.display_detailed_literal(tout << " ", antecedent) << "\n";);
@ -429,7 +429,7 @@ namespace smt {
void conflict_resolution::finalize_resolve(b_justification conflict, literal not_l) {
unmark_justifications(0);
TRACE("conflict", m_ctx.display_literals(tout << "before minimization:\n", m_lemma) << "\n";);
TRACE("conflict", m_ctx.display_literals(tout << "before minimization:\n", m_lemma) << "\n" << m_lemma << "\n";);
TRACE("conflict_verbose",m_ctx.display_literals_verbose(tout << "before minimization:\n", m_lemma) << "\n";);
@ -484,7 +484,7 @@ namespace smt {
unsigned num_marks = 0;
if (not_l != null_literal) {
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal_verbose(tout, not_l); tout << "\n";);
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal_verbose(tout, not_l) << "\n";);
process_antecedent(not_l, num_marks);
}
@ -497,7 +497,7 @@ namespace smt {
}
TRACE("conflict", tout << "processing consequent id: " << idx << " lit: " << consequent << " "; m_ctx.display_literal(tout, consequent);
m_ctx.display_literal_verbose(tout, consequent) << "\n";
m_ctx.display_literal_verbose(tout << " ", consequent) << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
);
SASSERT(js != null_b_justification);
@ -1372,7 +1372,7 @@ namespace smt {
}
while (true) {
TRACE("unsat_core_bug", tout << consequent << " js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";);
TRACE("unsat_core_bug", tout << consequent << ", idx: " << idx << " " << js.get_kind() << "\n";);
switch (js.get_kind()) {
case b_justification::CLAUSE: {
clause * cls = js.get_clause();
@ -1417,7 +1417,7 @@ namespace smt {
}
while (idx >= 0) {
literal l = m_assigned_literals[idx];
TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";);
CTRACE("unsat_core_bug", m_ctx.is_marked(l.var()), tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << "\n";);
if (m_ctx.get_assign_level(l) < search_lvl)
goto end_unsat_core;
if (m_ctx.is_marked(l.var()))

35
src/smt/smt_context.cpp
View file

@ -1776,7 +1776,7 @@ namespace smt {
void context::set_conflict(const b_justification & js, literal not_l) {
if (!inconsistent()) {
TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout << " ", js); );
TRACE("set_conflict", display_literal_verbose(tout << m_scope_lvl << " ", not_l); display(tout << " ", js); );
m_conflict = js;
m_not_l = not_l;
}
@ -1815,7 +1815,7 @@ namespace smt {
}
/**
\brief Execute next clase split, return false if there are no
\brief Execute next case split, return false if there are no
more case splits to be performed.
*/
bool context::decide() {
@ -1860,7 +1860,7 @@ namespace smt {
if (is_quantifier(m_bool_var2expr[var])) {
// Overriding any decision on how to assign the quantifier.
// assigining a quantifier to false is equivalent to make it irrelevant.
// assigning a quantifier to false is equivalent to make it irrelevant.
phase = l_false;
}
@ -2136,7 +2136,7 @@ namespace smt {
\brief When a clause is reinitialized (see reinit_clauses) enodes and literals may
need to be recreated. When an enode is recreated, I want to use the same generation
number it had before being deleted. Otherwise the generation will be 0, and will affect
the loop prevetion heuristics used to control quantifier instantiation.
the loop prevention heuristics used to control quantifier instantiation.
Thus, I cache the generation number of enodes that will be deleted during backtracking
and recreated by reinit_clauses.
*/
@ -3246,8 +3246,13 @@ namespace smt {
proof * pr = m_manager.mk_asserted(curr_assumption);
internalize_assertion(curr_assumption, pr, 0);
literal l = get_literal(curr_assumption);
if (l == true_literal)
continue;
if (l == false_literal) {
set_conflict(b_justification::mk_axiom());
break;
}
m_literal2assumption.insert(l.index(), orig_assumption);
// mark_as_relevant(l); <<< not needed
// internalize_assertion marked l as relevant.
SASSERT(is_relevant(l));
TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m_manager) << "\n";);
@ -3493,7 +3498,6 @@ namespace smt {
m_case_split_queue ->init_search_eh();
m_next_progress_sample = 0;
TRACE("literal_occ", display_literal_num_occs(tout););
m_timer.start();
}
void context::end_search() {
@ -3874,7 +3878,7 @@ namespace smt {
for (unsigned i = head; i < sz; i++) {
literal l = m_assigned_literals[i];
bool_var v = l.var();
TRACE("forget_phase", tout << "forgeting phase of l: " << l << "\n";);
TRACE("forget_phase", tout << "forgetting phase of l: " << l << "\n";);
m_bdata[v].m_phase_available = false;
}
}
@ -3920,6 +3924,7 @@ namespace smt {
conflict_lvl > m_search_lvl + 1 &&
!m_manager.proofs_enabled() &&
m_units_to_reassert.size() < m_fparams.m_delay_units_threshold;
if (delay_forced_restart) {
new_lvl = conflict_lvl - 1;
}
@ -4419,6 +4424,22 @@ namespace smt {
m = const_cast<model*>(m_model.get());
}
void context::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
unsigned sz = vars.size();
depth.resize(sz);
for (unsigned i = 0; i < sz; ++i) {
expr* v = vars[i];
bool_var bv = m_expr2bool_var.get(v->get_id(), null_bool_var);
depth[i] = bv == null_bool_var ? UINT_MAX : get_assign_level(bv);
}
}
expr_ref_vector context::get_trail() {
expr_ref_vector result(get_manager());
get_assignments(result);
return result;
}
void context::get_proto_model(proto_model_ref & m) const {
m = const_cast<proto_model*>(m_proto_model.get());
}

17
src/smt/smt_context.h
View file

@ -414,10 +414,19 @@ namespace smt {
return m_activity[v];
}
void set_activity(bool_var v, double & act) {
void set_activity(bool_var v, double const & act) {
m_activity[v] = act;
}
void activity_changed(bool_var v, bool increased) {
if (increased) {
m_case_split_queue->activity_increased_eh(v);
}
else {
m_case_split_queue->activity_decreased_eh(v);
}
}
bool is_assumption(bool_var v) const {
return get_bdata(v).m_assumption;
}
@ -1360,7 +1369,7 @@ namespace smt {
void display_profile(std::ostream & out) const;
void display(std::ostream& out, b_justification j) const;
std::ostream& display(std::ostream& out, b_justification j) const;
// -----------------------------------
//
@ -1577,6 +1586,10 @@ namespace smt {
return m_unsat_core.get(idx);
}
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth);
expr_ref_vector get_trail();
void get_model(model_ref & m) const;
bool update_model(bool refinalize);

37
src/smt/smt_context_pp.cpp
View file

@ -160,7 +160,7 @@ namespace smt {
}
void context::display_clause(std::ostream & out, clause const * cls) const {
cls->display_compact(out, m_manager, m_bool_var2expr.c_ptr());
cls->display_smt2(out, m_manager, m_bool_var2expr.c_ptr());
}
void context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
@ -185,11 +185,18 @@ namespace smt {
out << "binary clauses:\n";
first = false;
}
expr_ref t1(m_manager), t2(m_manager);
literal2expr(neg_l1, t1);
literal2expr(l2, t2);
expr_ref disj(m_manager.mk_or(t1, t2), m_manager);
out << disj << "\n";
#if 0
out << "(clause ";
display_literal(out, neg_l1);
out << " ";
display_literal(out, l2);
out << ")\n";
#endif
}
}
}
@ -200,6 +207,7 @@ namespace smt {
out << "current assignment:\n";
for (literal lit : m_assigned_literals) {
display_literal(out, lit);
if (!is_relevant(lit)) out << " n ";
out << ": ";
display_verbose(out, m_manager, 1, &lit, m_bool_var2expr.c_ptr());
out << "\n";
@ -255,7 +263,7 @@ namespace smt {
for (unsigned i = 0; i < sz; i++) {
expr * n = m_b_internalized_stack.get(i);
bool_var v = get_bool_var_of_id(n->get_id());
out << "(#" << n->get_id() << " -> p!" << v << ") ";
out << "(#" << n->get_id() << " -> " << literal(v, false) << ") ";
}
out << "\n";
}
@ -348,9 +356,9 @@ namespace smt {
}
void context::display_unsat_core(std::ostream & out) const {
unsigned sz = m_unsat_core.size();
for (unsigned i = 0; i < sz; i++)
out << mk_pp(m_unsat_core.get(i), m_manager) << "\n";
for (expr* c : m_unsat_core) {
out << mk_pp(c, m_manager) << "\n";
}
}
void context::collect_statistics(::statistics & st) const {
@ -555,23 +563,21 @@ namespace smt {
}
out << "\n";
if (is_app(n)) {
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
todo.push_back(to_app(n)->get_arg(i));
for (expr* arg : *to_app(n)) {
todo.push_back(arg);
}
}
}
}
void context::display(std::ostream& out, b_justification j) const {
std::ostream& context::display(std::ostream& out, b_justification j) const {
switch (j.get_kind()) {
case b_justification::AXIOM:
out << "axiom";
break;
case b_justification::BIN_CLAUSE: {
literal l2 = j.get_literal();
out << "bin-clause ";
display_literal(out, l2);
case b_justification::BIN_CLAUSE:
out << "bin " << j.get_literal();
break;
}
case b_justification::CLAUSE: {
clause * cls = j.get_clause();
out << "clause ";
@ -579,17 +585,16 @@ namespace smt {
break;
}
case b_justification::JUSTIFICATION: {
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(out, lits);
out << "justification " << j.get_justification()->get_from_theory() << ": " << lits;
break;
}
default:
UNREACHABLE();
break;
}
out << "\n";
return out << "\n";
}
void context::trace_assign(literal l, b_justification j, bool decision) const {

2
src/smt/smt_internalizer.cpp
View file

@ -196,7 +196,7 @@ namespace smt {
TRACE("incompleteness_bug", tout << "[internalize-assertion]: #" << n->get_id() << "\n";);
flet<unsigned> l(m_generation, generation);
m_stats.m_max_generation = std::max(m_generation, m_stats.m_max_generation);
if (get_depth(n) > DEEP_EXPR_THRESHOLD) {
if (::get_depth(n) > DEEP_EXPR_THRESHOLD) {
// if the expression is deep, then execute topological sort to avoid
// stack overflow.
// a caveat is that theory internalizers do rely on recursive descent so

36
src/smt/smt_kernel.cpp
View file

@ -146,6 +146,29 @@ namespace smt {
expr * get_unsat_core_expr(unsigned idx) const {
return m_kernel.get_unsat_core_expr(idx);
}
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
m_kernel.get_levels(vars, depth);
}
expr_ref_vector get_trail() {
return m_kernel.get_trail();
}
void set_activity(expr* lit, double act) {
SASSERT(m().is_bool(lit));
m().is_not(lit, lit);
if (!m_kernel.b_internalized(lit)) {
m_kernel.internalize(lit, false);
}
if (!m_kernel.b_internalized(lit)) {
return;
}
auto v = m_kernel.get_bool_var(lit);
double old_act = m_kernel.get_activity(v);
m_kernel.set_activity(v, act);
m_kernel.activity_changed(v, act > old_act);
}
failure last_failure() const {
return m_kernel.get_last_search_failure();
@ -396,4 +419,17 @@ namespace smt {
return m_imp->m_kernel;
}
void kernel::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
m_imp->get_levels(vars, depth);
}
expr_ref_vector kernel::get_trail() {
return m_imp->get_trail();
}
void kernel::set_activity(expr* lit, double activity) {
m_imp->set_activity(lit, activity);
}
};

15
src/smt/smt_kernel.h
View file

@ -219,6 +219,21 @@ namespace smt {
*/
expr* next_decision();
/**
\brief retrieve depth of variables from decision stack.
*/
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth);
/**
\brief retrieve trail of assignment stack.
*/
expr_ref_vector get_trail();
/**
\brief set activity of literal
*/
void set_activity(expr* lit, double activity);
/**
\brief (For debubbing purposes) Prints the state of the kernel
*/

2
src/smt/smt_model_finder.cpp
View file

@ -1703,7 +1703,7 @@ namespace smt {
friend class quantifier_analyzer;
void checkpoint() {
m_mf.checkpoint("quantifer_info");
m_mf.checkpoint("quantifier_info");
}
void insert_qinfo(qinfo * qi) {

130
src/smt/smt_quantifier.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include "ast/ast_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h"
#include "smt/smt_quantifier.h"
#include "smt/smt_context.h"
#include "smt/smt_quantifier_stat.h"
@ -36,14 +36,14 @@ namespace smt {
\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 quantifier_manager::log_justification_to_root(std::ostream & log, enode *en, obj_hashtable<enode> &already_visited, context &ctx, ast_manager &m) {
void quantifier_manager::log_justification_to_root(std::ostream & out, enode *en, obj_hashtable<enode> &visited, context &ctx, ast_manager &m) {
enode *root = en->get_root();
for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
if (already_visited.find(it) == already_visited.end()) already_visited.insert(it);
if (visited.find(it) == visited.end()) visited.insert(it);
else break;
if (!it->m_proof_is_logged) {
log_single_justification(log, it, already_visited, ctx, m);
log_single_justification(out, it, visited, ctx, m);
it->m_proof_is_logged = true;
} else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
@ -52,14 +52,14 @@ namespace smt {
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), already_visited, ctx, m);
log_justification_to_root(log, target->get_arg(i), already_visited, ctx, m);
log_justification_to_root(out, it->get_arg(i), visited, ctx, m);
log_justification_to_root(out, target->get_arg(i), visited, ctx, m);
}
it->m_proof_is_logged = true;
}
}
if (!root->m_proof_is_logged) {
log << "[eq-expl] #" << root->get_owner_id() << " root\n";
out << "[eq-expl] #" << root->get_owner_id() << " root\n";
root->m_proof_is_logged = true;
}
}
@ -68,7 +68,7 @@ namespace smt {
\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 quantifier_manager::log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &already_visited, context &ctx, ast_manager &m) {
void quantifier_manager::log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &visited, context &ctx, ast_manager &m) {
smt::literal lit;
unsigned num_args;
enode *target = en->get_trans_justification().m_target;
@ -87,8 +87,8 @@ namespace smt {
num_args = en->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
log_justification_to_root(out, en->get_arg(i), already_visited, ctx, m);
log_justification_to_root(out, target->get_arg(i), already_visited, ctx, m);
log_justification_to_root(out, en->get_arg(i), visited, ctx, m);
log_justification_to_root(out, target->get_arg(i), visited, ctx, m);
}
out << "[eq-expl] #" << en->get_owner_id() << " cg";
@ -195,6 +195,60 @@ namespace smt {
return m_plugin->is_shared(n);
}
void log_add_instance(
fingerprint* f,
quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
vector<std::tuple<enode *, enode *>> & used_enodes) {
if (pat == nullptr) {
trace_stream() << "[inst-discovered] MBQI " << static_cast<void*>(f) << " #" << q->get_id();
for (unsigned i = 0; i < num_bindings; ++i) {
trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id();
}
trace_stream() << "\n";
} else {
std::ostream & out = trace_stream();
obj_hashtable<enode> already_visited;
// 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], already_visited, m_context, m());
}
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, already_visited, m_context, m());
log_justification_to_root(out, substituted, already_visited, m_context, m());
}
}
// 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[num_bindings - i - 1]->get_owner_id();
}
out << " ;";
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";
}
}
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
@ -211,62 +265,18 @@ namespace smt {
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def);
if (f) {
if (has_trace_stream()) {
if (pat == nullptr) {
trace_stream() << "[inst-discovered] MBQI " << static_cast<void*>(f) << " #" << q->get_id();
for (unsigned i = 0; i < num_bindings; ++i) {
trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id();
}
trace_stream() << "\n";
} else {
std::ostream & out = trace_stream();
obj_hashtable<enode> already_visited;
// 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], already_visited, m_context, m());
}
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, already_visited, m_context, m());
log_justification_to_root(out, substituted, already_visited, m_context, m());
}
}
// 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[num_bindings - i - 1]->get_owner_id();
}
out << " ;";
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";
}
log_add_instance(f, q, pat, num_bindings, bindings, used_enodes);
}
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
m_num_instances++;
}
TRACE("quantifier",
tout << mk_pp(q, m()) << " ";
CTRACE("quantifier_", f != nullptr,
tout << expr_ref(q, m()) << " ";
for (unsigned i = 0; i < num_bindings; ++i) {
tout << mk_pp(bindings[i]->get_owner(), m()) << " ";
tout << expr_ref(bindings[i]->get_owner(), m()) << " ";
}
tout << "\n";
tout << "inserted: " << (f != 0) << "\n";
);
return f != nullptr;
@ -646,7 +656,7 @@ namespace smt {
m_lazy_mam->add_pattern(q, mp);
}
else {
TRACE("quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m) << "\n";);
TRACE("quantifier", tout << "adding:\n" << expr_ref(mp, m) << "\n";);
m_mam->add_pattern(q, mp);
}
if (!unary)

8
src/smt/smt_relevancy.cpp
View file

@ -129,7 +129,7 @@ namespace smt {
struct relevancy_propagator_imp : public relevancy_propagator {
unsigned m_qhead;
expr_ref_vector m_relevant_exprs;
obj_hashtable<expr> m_is_relevant;
uint_set m_is_relevant;
typedef list<relevancy_eh *> relevancy_ehs;
obj_map<expr, relevancy_ehs *> m_relevant_ehs;
obj_map<expr, relevancy_ehs *> m_watches[2];
@ -242,7 +242,7 @@ namespace smt {
}
}
bool is_relevant_core(expr * n) const { return m_is_relevant.contains(n); }
bool is_relevant_core(expr * n) const { return m_is_relevant.contains(n->get_id()); }
bool is_relevant(expr * n) const override {
return !enabled() || is_relevant_core(n);
@ -275,7 +275,7 @@ namespace smt {
while (i != old_lim) {
--i;
expr * n = m_relevant_exprs.get(i);
m_is_relevant.erase(n);
m_is_relevant.remove(n->get_id());
TRACE("propagate_relevancy", tout << "unmarking:\n" << mk_ismt2_pp(n, get_manager()) << "\n";);
}
m_relevant_exprs.shrink(old_lim);
@ -303,7 +303,7 @@ namespace smt {
}
void set_relevant(expr * n) {
m_is_relevant.insert(n);
m_is_relevant.insert(n->get_id());
m_relevant_exprs.push_back(n);
m_context.relevant_eh(n);
}

2
src/smt/smt_setup.cpp
View file

@ -209,7 +209,7 @@ namespace smt {
static void check_no_arithmetic(static_features const & st, char const * logic) {
if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0)
throw default_exception("Benchmark constains arithmetic, but specified logic does not support it.");
throw default_exception("Benchmark constrains arithmetic, but specified logic does not support it.");
}
void setup::setup_QF_UF() {

14
src/smt/smt_solver.cpp
View file

@ -185,7 +185,7 @@ namespace smt {
m_context.pop(n);
}
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override {
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";);
return m_context.check(num_assumptions, assumptions);
}
@ -195,6 +195,18 @@ namespace smt {
return m_context.check(cube, clauses);
}
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
m_context.get_levels(vars, depth);
}
expr_ref_vector get_trail() override {
return m_context.get_trail();
}
void set_activity(expr* lit, double activity) override {
m_context.set_activity(lit, activity);
}
struct scoped_minimize_core {
smt_solver& s;
expr_ref_vector m_assumptions;

4
src/smt/theory_arith_aux.h
View file

@ -548,7 +548,7 @@ namespace smt {
if (!it->is_dead()) {
row const & r = m_rows[it->m_row_id];
theory_var s = r.get_base_var();
if (is_quasi_base(s) && m_var_occs[s].size() == 0)
if (is_quasi_base(s) && m_var_occs[s].empty())
continue;
if (is_int(v)) {
numeral const & c = r[it->m_row_idx].m_coeff;
@ -574,7 +574,7 @@ namespace smt {
TRACE("move_unconstrained_to_base", tout << "before...\n"; display(tout););
int num = get_num_vars();
for (theory_var v = 0; v < num; v++) {
if (m_var_occs[v].size() == 0 && is_free(v)) {
if (m_var_occs[v].empty() && is_free(v)) {
switch (get_var_kind(v)) {
case QUASI_BASE:
break;

14
src/smt/theory_arith_core.h
View file

@ -485,12 +485,12 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::mk_idiv_mod_axioms(expr * dividend, expr * divisor) {
th_rewriter & s = get_context().get_rewriter();
if (!m_util.is_zero(divisor)) {
ast_manager & m = get_manager();
// if divisor is zero, then idiv and mod are uninterpreted functions.
expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m);
expr_ref eqz(m), eq(m), lower(m), upper(m);
th_rewriter & s = get_context().get_rewriter();
div = m_util.mk_idiv(dividend, divisor);
mod = m_util.mk_mod(dividend, divisor);
zero = m_util.mk_int(0);
@ -511,6 +511,17 @@ namespace smt {
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
rational k;
context& ctx = get_context();
if (!m_util.is_numeral(divisor)) {
// (=> (> y 0) (<= (* y (div x y)) x))
// (=> (< y 0) ???)
expr_ref div_ge(m), div_non_pos(m);
div_ge = m_util.mk_ge(m_util.mk_sub(dividend, m_util.mk_mul(divisor, div)), zero);
s(div_ge);
div_non_pos = m_util.mk_le(divisor, zero);
mk_axiom(div_non_pos, div_ge, false);
}
(void)ctx;
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
k.is_pos() && k < rational(8)) {
@ -547,6 +558,7 @@ namespace smt {
}
#endif
}
#if 0
// e-matching is too restrictive for multiplication.
// also suffers from use-after free so formulas have to be pinned in solver.

12
src/smt/theory_array_full.cpp
View file

@ -65,10 +65,14 @@ namespace smt {
bool result = false;
var_data * d = m_var_data[v];
var_data_full * d_full = m_var_data_full[v];
for (enode* pm : d_full->m_parent_maps)
for (enode* ps : d->m_parent_selects)
for (unsigned i = 0; i < d_full->m_parent_maps.size(); ++i) {
enode* pm = d_full->m_parent_maps[i];
for (unsigned j = 0; j < d->m_parent_selects.size(); ++j) {
enode* ps = d->m_parent_selects[j];
if (instantiate_select_map_axiom(ps, pm))
result = true;
result = true;
}
}
return result;
}
@ -137,7 +141,7 @@ namespace smt {
}
void theory_array_full::set_prop_upward(theory_var v, var_data* d) {
if (m_params.m_array_always_prop_upward || d->m_stores.size() >= 1) {
if (m_params.m_array_always_prop_upward || !d->m_stores.empty()) {
theory_array::set_prop_upward(v, d);
}
else {

149
src/smt/theory_bv.cpp
View file

@ -20,9 +20,11 @@ Revision History:
#include "smt/theory_bv.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/bv_decl_plugin.h"
#include "smt/smt_model_generator.h"
#include "util/stats.h"
#define WATCH_DISEQ 0
namespace smt {
@ -52,6 +54,7 @@ namespace smt {
unsigned bv_size = get_bv_size(n);
context & ctx = get_context();
literal_vector & bits = m_bits[v];
TRACE("bv", tout << "v" << v << "\n";);
bits.reset();
for (unsigned i = 0; i < bv_size; i++) {
app * bit = mk_bit2bool(owner, i);
@ -76,6 +79,7 @@ namespace smt {
context & ctx = get_context();
SASSERT(!ctx.b_internalized(n));
TRACE("bv", tout << "bit2bool: " << mk_pp(n, ctx.get_manager()) << "\n";);
expr* first_arg = n->get_arg(0);
if (!ctx.e_internalized(first_arg)) {
@ -93,23 +97,30 @@ namespace smt {
// This will also force the creation of all bits for x.
enode * first_arg_enode = ctx.get_enode(first_arg);
get_var(first_arg_enode);
#if 0
// constant axiomatization moved to catch all case in the end of function.
// numerals are not blasted into bit2bool, so we do this directly.
rational val;
unsigned sz;
if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) {
TRACE("bv", tout << "bit2bool constants\n";);
theory_var v = first_arg_enode->get_th_var(get_id());
app* owner = first_arg_enode->get_owner();
for (unsigned i = 0; i < sz; ++i) {
ctx.internalize(mk_bit2bool(owner, i), true);
app* e = mk_bit2bool(owner, i);
ctx.internalize(e, true);
}
m_bits[v].reset();
rational bit;
for (unsigned i = 0; i < sz; ++i) {
div(val, rational::power_of_two(i), bit);
mod(bit, rational(2), bit);
m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
}
}
#endif
}
enode * arg = ctx.get_enode(first_arg);
@ -134,6 +145,19 @@ namespace smt {
SASSERT(a->m_occs == 0);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
}
// axiomatize bit2bool on constants.
rational val;
unsigned sz;
if (m_util.is_numeral(first_arg, val, sz)) {
rational bit;
unsigned idx = n->get_decl()->get_parameter(0).get_int();
div(val, rational::power_of_two(idx), bit);
mod(bit, rational(2), bit);
literal lit = ctx.get_literal(n);
if (bit.is_zero()) lit.neg();
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
}
}
void theory_bv::process_args(app * n) {
@ -422,16 +446,21 @@ namespace smt {
};
void theory_bv::add_fixed_eq(theory_var v1, theory_var v2) {
++m_stats.m_num_eq_dynamic;
if (v1 > v2) {
std::swap(v1, v2);
}
unsigned sz = get_bv_size(v1);
unsigned act = m_eq_activity[hash_u_u(v1, v2) & 0xFF]++;
if ((act & 0xFF) != 0xFF) {
return;
}
++m_stats.m_num_eq_dynamic;
ast_manager& m = get_manager();
context & ctx = get_context();
app* o1 = get_enode(v1)->get_owner();
app* o2 = get_enode(v2)->get_owner();
literal oeq = mk_eq(o1, o2, true);
unsigned sz = get_bv_size(v1);
TRACE("bv",
tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " "
<< ctx.get_scope_level() << "\n";);
@ -606,8 +635,8 @@ namespace smt {
num *= numeral(2);
}
expr_ref sum(m_autil.mk_add(sz, args.c_ptr()), m);
arith_rewriter arw(m);
ctx.get_rewriter()(sum);
th_rewriter rw(m);
rw(sum);
literal l(mk_eq(n, sum, false));
TRACE("bv",
tout << mk_pp(n, m) << "\n";
@ -628,7 +657,9 @@ namespace smt {
context& ctx = get_context();
process_args(n);
mk_enode(n);
mk_bits(ctx.get_enode(n)->get_th_var(get_id()));
theory_var v = ctx.get_enode(n)->get_th_var(get_id());
mk_bits(v);
if (!ctx.relevancy()) {
assert_int2bv_axiom(n);
}
@ -1094,7 +1125,6 @@ namespace smt {
for (unsigned i = 0; i <= num_args; i++) {
expr* arg = (i == num_args)?n:n->get_arg(i);
sort* s = get_manager().get_sort(arg);
s = get_manager().get_sort(arg);
if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > m_params.m_bv_blast_max_size) {
if (!m_approximates_large_bvs) {
TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, get_manager()) << "\n";);
@ -1133,14 +1163,9 @@ namespace smt {
SASSERT(get_bv_size(v1) == get_bv_size(v2));
context & ctx = get_context();
ast_manager & m = get_manager();
#ifdef _TRACE
unsigned num_bool_vars = ctx.get_num_bool_vars();
#endif
literal_vector & lits = m_tmp_literals;
ptr_vector<expr> exprs;
lits.reset();
literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true);
lits.push_back(eq);
if (v1 > v2) {
std::swap(v1, v2);
}
literal_vector const & bits1 = m_bits[v1];
literal_vector::const_iterator it1 = bits1.begin();
literal_vector::const_iterator end1 = bits1.end();
@ -1148,8 +1173,48 @@ namespace smt {
literal_vector::const_iterator it2 = bits2.begin();
for (; it1 != end1; ++it1, ++it2) {
if (*it1 == ~(*it2))
return; // static diseq
return;
lbool val1 = ctx.get_assignment(*it1);
lbool val2 = ctx.get_assignment(*it2);
if (val1 != l_undef && val2 != l_undef && val1 != val2) {
return;
}
}
#if WATCH_DISEQ
bool_var watch_var = null_bool_var;
it1 = bits1.begin();
it2 = bits2.begin();
unsigned h = hash_u_u(v1, v2);
unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++;
for (; it1 != end1 && ((act & 0x3) != 0x3); ++it1, ++it2) {
lbool val1 = ctx.get_assignment(*it1);
lbool val2 = ctx.get_assignment(*it2);
if (val1 == l_undef) {
watch_var = it1->var();
}
else if (val2 == l_undef) {
watch_var = it2->var();
}
else {
continue;
}
m_diseq_watch.reserve(watch_var+1);
m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
m_diseq_watch_trail.push_back(watch_var);
return;
//m_replay_diseq.push_back(std::make_pair(v1, v2));
}
#endif
literal_vector & lits = m_tmp_literals;
ptr_vector<expr> exprs;
lits.reset();
literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true);
lits.push_back(eq);
it1 = bits1.begin();
it2 = bits2.begin();
for (; it1 != end1; ++it1, ++it2) {
@ -1166,14 +1231,6 @@ namespace smt {
if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_or(exprs.size(), exprs.c_ptr())));
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
TRACE_CODE({
static unsigned num = 0;
static unsigned new_bool_vars = 0;
new_bool_vars += (ctx.get_num_bool_vars() - num_bool_vars);
if (num % 1000 == 0)
TRACE("expand_diseq", tout << "num: " << num << " " << new_bool_vars << "\n";);
num++;
});
}
void theory_bv::assign_eh(bool_var v, bool is_true) {
@ -1195,8 +1252,19 @@ namespace smt {
m_prop_queue.push_back(var_pos(curr->m_var, curr->m_idx));
curr = curr->m_next;
}
TRACE("bv", tout << m_prop_queue.size() << "\n";);
TRACE("bv", tout << "prop queue size: " << m_prop_queue.size() << "\n";);
propagate_bits();
#if WATCH_DISEQ
if (!get_context().inconsistent() && m_diseq_watch.size() > static_cast<unsigned>(v)) {
unsigned sz = m_diseq_watch[v].size();
for (unsigned i = 0; i < sz; ++i) {
auto const & p = m_diseq_watch[v][i];
expand_diseq(p.first, p.second);
}
m_diseq_watch[v].reset();
}
#endif
}
}
@ -1212,7 +1280,7 @@ namespace smt {
literal_vector & bits = m_bits[v];
literal bit = bits[idx];
lbool val = ctx.get_assignment(bit);
lbool val = ctx.get_assignment(bit);
if (val == l_undef) {
continue;
}
@ -1229,6 +1297,7 @@ namespace smt {
SASSERT(bit != ~bit2);
lbool val2 = ctx.get_assignment(bit2);
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
TRACE("bv", tout << bit << " " << bit2 << "\n";);
if (val != val2) {
literal consequent = bit2;
@ -1339,6 +1408,9 @@ namespace smt {
void theory_bv::push_scope_eh() {
theory::push_scope_eh();
m_trail_stack.push_scope();
#if WATCH_DISEQ
m_diseq_watch_lim.push_back(m_diseq_watch_trail.size());
#endif
}
void theory_bv::pop_scope_eh(unsigned num_scopes) {
@ -1348,6 +1420,16 @@ namespace smt {
m_bits.shrink(num_old_vars);
m_wpos.shrink(num_old_vars);
m_zero_one_bits.shrink(num_old_vars);
#if WATCH_DISEQ
unsigned old_trail_sz = m_diseq_watch_lim[m_diseq_watch_lim.size()-num_scopes];
for (unsigned i = m_diseq_watch_trail.size(); i-- > old_trail_sz;) {
if (!m_diseq_watch[m_diseq_watch_trail[i]].empty()) {
m_diseq_watch[m_diseq_watch_trail[i]].pop_back();
}
}
m_diseq_watch_trail.shrink(old_trail_sz);
m_diseq_watch_lim.shrink(m_diseq_watch_lim.size()-num_scopes);
#endif
theory::pop_scope_eh(num_scopes);
}
@ -1390,6 +1472,8 @@ namespace smt {
m_trail_stack(*this),
m_find(*this),
m_approximates_large_bvs(false) {
memset(m_eq_activity, 0, sizeof(m_eq_activity));
memset(m_diseq_activity, 0, sizeof(m_diseq_activity));
}
theory_bv::~theory_bv() {
@ -1512,6 +1596,17 @@ namespace smt {
return true;
}
void theory_bv::propagate() {
unsigned sz = m_replay_diseq.size();
if (sz > 0) {
for (unsigned i = 0; i < sz; ++i) {
auto const& p = m_replay_diseq[i];
expand_diseq(p.first, p.second);
}
m_replay_diseq.reset();
}
}
class bit_eq_justification : public justification {
enode * m_v1;
enode * m_v2;

9
src/smt/theory_bv.h
View file

@ -124,6 +124,13 @@ namespace smt {
value2var m_fixed_var_table;
unsigned char m_eq_activity[256];
unsigned char m_diseq_activity[256];
svector<std::pair<theory_var, theory_var>> m_replay_diseq;
vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
svector<bool_var> m_diseq_watch_trail;
unsigned_vector m_diseq_watch_lim;
literal_vector m_tmp_literals;
svector<var_pos> m_prop_queue;
bool m_approximates_large_bvs;
@ -233,6 +240,8 @@ namespace smt {
bool include_func_interp(func_decl* f) override;
svector<theory_var> m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
bool merge_zero_one_bits(theory_var r1, theory_var r2);
bool can_propagate() override { return !m_replay_diseq.empty(); }
void propagate() override;
// -----------------------------------
//

49
src/smt/theory_datatype.cpp
View file

@ -481,33 +481,46 @@ namespace smt {
return d->m_constructor;
}
void theory_datatype::explain_is_child(enode* parent, enode* child) {
enode * parentc = oc_get_cstor(parent);
if (parent != parentc) {
m_used_eqs.push_back(enode_pair(parent, parentc));
}
// collect equalities on all children that may have been used.
bool found = false;
for (enode * arg : enode::args(parentc)) {
// found an argument which is equal to root
if (arg->get_root() == child->get_root()) {
if (arg != child) {
m_used_eqs.push_back(enode_pair(arg, child));
}
found = true;
}
}
VERIFY(found);
}
// explain the cycle root -> ... -> app -> root
void theory_datatype::occurs_check_explain(enode * app, enode * root) {
TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";);
enode* app_parent = nullptr;
// first: explain that root=v, given that app=cstor(...,v,...)
for (enode * arg : enode::args(oc_get_cstor(app))) {
// found an argument which is equal to root
if (arg->get_root() == root->get_root()) {
if (arg != root)
m_used_eqs.push_back(enode_pair(arg, root));
break;
}
}
explain_is_child(app, root);
// now explain app=cstor(..,v,..) where v=root, and recurse with parent of app
while (app->get_root() != root->get_root()) {
enode * app_cstor = oc_get_cstor(app);
if (app != app_cstor)
m_used_eqs.push_back(enode_pair(app, app_cstor));
app_parent = m_parent[app->get_root()];
app = app_parent;
enode* parent_app = m_parent[app->get_root()];
explain_is_child(parent_app, app);
SASSERT(is_constructor(parent_app));
app = parent_app;
}
SASSERT(app->get_root() == root->get_root());
if (app != root)
if (app != root) {
m_used_eqs.push_back(enode_pair(app, root));
}
TRACE("datatype",
tout << "occurs_check\n";
@ -732,11 +745,11 @@ namespace smt {
sort * s = recognizer->get_decl()->get_domain(0);
if (d->m_recognizers.empty()) {
SASSERT(m_util.is_datatype(s));
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s));
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s), nullptr);
}
SASSERT(d->m_recognizers.size() == m_util.get_datatype_num_constructors(s));
unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl());
if (d->m_recognizers[c_idx] == 0) {
if (d->m_recognizers[c_idx] == nullptr) {
lbool val = ctx.get_assignment(recognizer);
TRACE("datatype", tout << "adding recognizer to v" << v << " rec: #" << recognizer->get_owner_id() << " val: " << val << "\n";);
if (val == l_true) {
@ -808,7 +821,7 @@ namespace smt {
region & reg = ctx.get_region();
TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_owner(), get_manager()) << "\n";
for (literal l : lits) {
ctx.display_detailed_literal(tout, l); tout << "\n";
ctx.display_detailed_literal(tout, l) << "\n";
}
for (auto const& p : eqs) {
tout << enode_eq_pp(p, ctx);

3
src/smt/theory_datatype.h
View file

@ -73,7 +73,7 @@ namespace smt {
void sign_recognizer_conflict(enode * c, enode * r);
typedef enum { ENTER, EXIT } stack_op;
typedef map<enode*, enode*, obj_ptr_hash<enode>, ptr_eq<enode> > parent_tbl;
typedef obj_map<enode, enode*> parent_tbl;
typedef std::pair<stack_op, enode*> stack_entry;
ptr_vector<enode> m_to_unmark;
@ -102,6 +102,7 @@ namespace smt {
bool occurs_check(enode * n);
bool occurs_check_enter(enode * n);
void occurs_check_explain(enode * top, enode * root);
void explain_is_child(enode* parent, enode* child);
void mk_split(theory_var v);

118
src/smt/theory_jobscheduler.cpp
View file

@ -305,7 +305,6 @@ namespace smt {
literal end_ge_lo = mk_ge(ji.m_end, clb);
// Initialization ensures that satisfiable states have completion time below end.
VERIFY(clb <= get_job_resource(j, r).m_end);
ast_manager& m = get_manager();
if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var())));
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
@ -324,6 +323,10 @@ namespace smt {
*/
bool theory_jobscheduler::constrain_end_time_interval(unsigned j, unsigned r) {
unsigned idx1 = 0, idx2 = 0;
if (!job_has_resource(j, r)) {
IF_VERBOSE(0, verbose_stream() << "job " << j << " assigned non-registered resource " << r << "\n");
return false;
}
time_t s = start(j);
job_resource const& jr = get_job_resource(j, r);
TRACE("csp", tout << "job: " << j << " resource: " << r << " start: " << s << "\n";);
@ -457,6 +460,7 @@ namespace smt {
job_info const& ji = m_jobs[j];
VERIFY(u.is_resource(ji.m_job2resource->get_root()->get_owner(), r));
TRACE("csp", tout << "job: " << j << " resource: " << r << "\n";);
std::cout << j << " -o " << r << "\n";
propagate_job2resource(j, r);
}
}
@ -464,8 +468,13 @@ namespace smt {
void theory_jobscheduler::propagate_job2resource(unsigned j, unsigned r) {
job_info const& ji = m_jobs[j];
res_info const& ri = m_resources[r];
job_resource const& jr = get_job_resource(j, r);
literal eq = mk_eq_lit(ji.m_job2resource, ri.m_resource);
if (!job_has_resource(j, r)) {
IF_VERBOSE(0, verbose_stream() << "job " << j << " assigned non-registered resource " << r << "\n");
return;
}
return;
job_resource const& jr = get_job_resource(j, r);
assert_last_end_time(j, r, jr, eq);
assert_last_start_time(j, r, eq);
assert_first_start_time(j, r, eq);
@ -495,7 +504,7 @@ namespace smt {
}
std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const {
return out << "r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_end;
return out << "r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_finite_capacity_end;
for (auto const& s : jr.m_properties) out << " " << s; out << "\n";
}
@ -557,7 +566,8 @@ namespace smt {
}
time_t theory_jobscheduler::get_lo(expr* e) {
arith_value av(get_context());
arith_value av(m);
av.init(&get_context());
rational val;
bool is_strict;
if (av.get_lo(e, val, is_strict) && !is_strict && val.is_uint64()) {
@ -567,7 +577,8 @@ namespace smt {
}
time_t theory_jobscheduler::get_up(expr* e) {
arith_value av(get_context());
arith_value av(m);
av.init(&get_context());
rational val;
bool is_strict;
if (av.get_up(e, val, is_strict) && !is_strict && val.is_uint64()) {
@ -577,9 +588,10 @@ namespace smt {
}
time_t theory_jobscheduler::get_value(expr* e) {
arith_value av(get_context());
arith_value av(get_manager());
av.init(&get_context());
rational val;
if (av.get_value(e, val) && val.is_uint64()) {
if (av.get_value_equiv(e, val) && val.is_uint64()) {
return val.get_uint64();
}
return 0;
@ -623,21 +635,30 @@ namespace smt {
}
void theory_jobscheduler::set_preemptable(unsigned j, bool is_preemptable) {
m_jobs.reserve(j + 1);
m_jobs[j].m_is_preemptable = is_preemptable;
ensure_job(j).m_is_preemptable = is_preemptable;
}
void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned loadpct, uint64_t cap, time_t end, properties const& ps) {
SASSERT(get_context().at_base_level());
SASSERT(0 <= loadpct && loadpct <= 100);
SASSERT(0 <= cap);
m_jobs.reserve(j + 1);
m_resources.reserve(r + 1);
job_info& ji = m_jobs[j];
if (ji.m_resource2index.contains(r)) {
throw default_exception("resource already bound to job");
theory_jobscheduler::res_info& theory_jobscheduler::ensure_resource(unsigned last) {
while (m_resources.size() <= last) {
unsigned r = m_resources.size();
m_resources.push_back(res_info());
res_info& ri = m_resources.back();
context& ctx = get_context();
app_ref res(u.mk_resource(r), m);
if (!ctx.e_internalized(res)) ctx.internalize(res, false);
ri.m_resource = ctx.get_enode(res);
app_ref ms(u.mk_makespan(r), m);
if (!ctx.e_internalized(ms)) ctx.internalize(ms, false);
ri.m_makespan = ctx.get_enode(ms);
}
if (!ji.m_start) {
return m_resources[last];
}
theory_jobscheduler::job_info& theory_jobscheduler::ensure_job(unsigned last) {
while (m_jobs.size() <= last) {
unsigned j = m_jobs.size();
m_jobs.push_back(job_info());
job_info& ji = m_jobs.back();
context& ctx = get_context();
app_ref job(u.mk_job(j), m);
app_ref start(u.mk_start(j), m);
@ -652,10 +673,22 @@ namespace smt {
ji.m_end = ctx.get_enode(end);
ji.m_job2resource = ctx.get_enode(res);
}
return m_jobs[last];
}
void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned loadpct, uint64_t cap, time_t finite_capacity_end, properties const& ps) {
SASSERT(get_context().at_base_level());
SASSERT(0 <= loadpct && loadpct <= 100);
SASSERT(0 <= cap);
job_info& ji = ensure_job(j);
res_info& ri = ensure_resource(r);
if (ji.m_resource2index.contains(r)) {
throw default_exception("resource already bound to job");
}
ji.m_resource2index.insert(r, ji.m_resources.size());
ji.m_resources.push_back(job_resource(r, cap, loadpct, end, ps));
SASSERT(!m_resources[r].m_jobs.contains(j));
m_resources[r].m_jobs.push_back(j);
ji.m_resources.push_back(job_resource(r, cap, loadpct, finite_capacity_end, ps));
SASSERT(!ri.m_jobs.contains(j));
ri.m_jobs.push_back(j);
}
@ -663,17 +696,7 @@ namespace smt {
SASSERT(get_context().at_base_level());
SASSERT(1 <= max_loadpct && max_loadpct <= 100);
SASSERT(start <= end);
m_resources.reserve(r + 1);
res_info& ri = m_resources[r];
if (!ri.m_resource) {
context& ctx = get_context();
app_ref res(u.mk_resource(r), m);
if (!ctx.e_internalized(res)) ctx.internalize(res, false);
ri.m_resource = ctx.get_enode(res);
app_ref ms(u.mk_makespan(r), m);
if (!ctx.e_internalized(ms)) ctx.internalize(ms, false);
ri.m_makespan = ctx.get_enode(ms);
}
res_info& ri = ensure_resource(r);
ri.m_available.push_back(res_available(max_loadpct, start, end, ps));
}
@ -723,22 +746,37 @@ namespace smt {
for (job_resource const& jr : ji.m_resources) {
unsigned r = jr.m_resource_id;
res_info const& ri = m_resources[r];
if (ri.m_available.empty()) continue;
if (ri.m_available.empty()) {
if (jr.m_capacity == 0) {
start_lb = 0;
end_ub = std::numeric_limits<time_t>::max();
runtime_lb = 0;
}
continue;
}
unsigned idx = 0;
if (first_available(jr, ri, idx)) {
start_lb = std::min(start_lb, ri.m_available[idx].m_start);
}
else {
IF_VERBOSE(0, verbose_stream() << "not first-available\n";);
}
idx = ri.m_available.size();
if (last_available(jr, ri, idx)) {
end_ub = std::max(end_ub, ri.m_available[idx].m_end);
}
else {
IF_VERBOSE(0, verbose_stream() << "not last-available\n";);
}
runtime_lb = std::min(runtime_lb, jr.m_capacity);
// TBD: more accurate estimates for runtime_lb based on gaps
// TBD: correct estimate of runtime_ub taking gaps into account.
}
CTRACE("csp", (start_lb > end_ub), tout << "there is no associated resource working time\n";);
if (start_lb > end_ub) {
IF_VERBOSE(0, verbose_stream() << start_lb << " " << end_ub << "\n");
warning_msg("Job %d has no associated resource working time", job_id);
continue;
}
// start(j) >= start_lb
@ -764,12 +802,14 @@ namespace smt {
// resource(j) = r => end(j) <= end(j, r)
void theory_jobscheduler::assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq) {
#if 0
job_info const& ji = m_jobs[j];
literal l2 = mk_le(ji.m_end, jr.m_end);
literal l2 = mk_le(ji.m_end, jr.m_finite_capacity_end);
context& ctx = get_context();
if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var())));
ctx.mk_th_axiom(get_id(), ~eq, l2);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
#endif
}
// resource(j) = r => start(j) <= lst(j, r, end(j, r))
@ -916,6 +956,10 @@ namespace smt {
}
}
bool theory_jobscheduler::job_has_resource(unsigned j, unsigned r) const {
return m_jobs[j].m_resource2index.contains(r);
}
theory_jobscheduler::job_resource const& theory_jobscheduler::get_job_resource(unsigned j, unsigned r) const {
job_info const& ji = m_jobs[j];
return ji.m_resources[ji.m_resource2index[r]];
@ -1067,7 +1111,9 @@ namespace smt {
bool theory_jobscheduler::resource_available(job_resource const& jr, res_available const& ra) const {
auto const& jps = jr.m_properties;
auto const& rps = ra.m_properties;
if (jps.size() > rps.size()) return false;
if (jps.size() > rps.size()) {
return false;
}
unsigned j = 0, i = 0;
for (; i < jps.size() && j < rps.size(); ) {
if (jps[i] == rps[j]) {

11
src/smt/theory_jobscheduler.h
View file

@ -38,10 +38,10 @@ namespace smt {
unsigned m_resource_id; // id of resource
time_t m_capacity; // amount of resource to use
unsigned m_loadpct; // assuming loadpct
time_t m_end; // must run before
time_t m_finite_capacity_end;
properties m_properties;
job_resource(unsigned r, time_t cap, unsigned loadpct, time_t end, properties const& ps):
m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_end(end), m_properties(ps) {}
m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_finite_capacity_end(end), m_properties(ps) {}
};
struct job_time {
@ -89,10 +89,9 @@ namespace smt {
struct res_info {
unsigned_vector m_jobs; // jobs allocated to run on resource
vector<res_available> m_available; // time intervals where resource is available
time_t m_end; // can't run after
enode* m_resource;
enode* m_makespan;
res_info(): m_end(std::numeric_limits<time_t>::max()), m_resource(nullptr), m_makespan(nullptr) {}
res_info(): m_resource(nullptr), m_makespan(nullptr) {}
};
ast_manager& m;
@ -152,6 +151,9 @@ namespace smt {
theory * mk_fresh(context * new_ctx) override;
res_info& ensure_resource(unsigned r);
job_info& ensure_job(unsigned j);
public:
// set up job/resource global constraints
void set_preemptable(unsigned j, bool is_preemptable);
@ -189,6 +191,7 @@ namespace smt {
time_t capacity_used(unsigned j, unsigned r, time_t start, time_t end); // capacity used between start and end
job_resource const& get_job_resource(unsigned j, unsigned r) const;
bool job_has_resource(unsigned j, unsigned r) const;
// propagation
void propagate_end_time(unsigned j, unsigned r);

82
src/smt/theory_lra.cpp
View file

@ -323,6 +323,10 @@ class theory_lra::imp {
m_solver->settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
m_solver->settings().set_random_seed(ctx().get_fparams().m_random_seed);
m_lia = alloc(lp::int_solver, m_solver.get());
get_one(true);
get_zero(true);
get_one(false);
get_zero(false);
}
void ensure_nra() {
@ -479,22 +483,6 @@ class theory_lra::imp {
if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod);
}
else if (a.is_mod(n, n1, n2)) {
bool is_num = a.is_numeral(n2, r) && !r.is_zero();
if (!is_num) {
found_not_handled(n);
}
#if 0
else {
app_ref div(a.mk_idiv(n1, n2), m);
mk_enode(div);
theory_var w = mk_var(div);
theory_var u = mk_var(n1);
// add axioms:
// u = v + r*w
// abs(r) > v >= 0
assert_idiv_mod_axioms(u, v, w, r);
}
#endif
if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2);
}
else if (a.is_rem(n, n1, n2)) {
@ -2341,16 +2329,14 @@ public:
iterator lo_inf = begin1, lo_sup = begin1;
iterator hi_inf = begin2, hi_sup = begin2;
iterator lo_inf1 = begin1, lo_sup1 = begin1;
iterator hi_inf1 = begin2, hi_sup1 = begin2;
bool flo_inf, fhi_inf, flo_sup, fhi_sup;
ptr_addr_hashtable<lp_api::bound> visited;
for (unsigned i = 0; i < atoms.size(); ++i) {
lp_api::bound* a1 = atoms[i];
lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf);
hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf);
lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup);
hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup);
iterator lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf);
iterator hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf);
iterator lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup);
iterator hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup);
if (lo_inf1 != end) lo_inf = lo_inf1;
if (lo_sup1 != end) lo_sup = lo_sup1;
if (hi_inf1 != end) hi_inf = hi_inf1;
@ -2730,14 +2716,12 @@ public:
if (propagate_eqs()) {
rational const& value = b.get_value();
if (k == lp::GE) {
set_lower_bound(vi, ci, value);
if (has_upper_bound(vi, ci, value)) {
if (set_lower_bound(vi, ci, value) && has_upper_bound(vi, ci, value)) {
fixed_var_eh(b.get_var(), value);
}
}
else if (k == lp::LE) {
set_upper_bound(vi, ci, value);
if (has_lower_bound(vi, ci, value)) {
if (set_upper_bound(vi, ci, value) && has_lower_bound(vi, ci, value)) {
fixed_var_eh(b.get_var(), value);
}
}
@ -2756,25 +2740,39 @@ public:
bool use_tableau() const { return lp_params(ctx().get_params()).simplex_strategy() < 2; }
void set_upper_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { set_bound(vi, ci, v, false); }
bool set_upper_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, false); }
void set_lower_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { set_bound(vi, ci, v, true); }
bool set_lower_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, true); }
void set_bound(lp::var_index vi, lp::constraint_index ci, rational const& v, bool is_lower) {
if (!m_solver->is_term(vi)) {
bool set_bound(lp::var_index vi, lp::constraint_index ci, rational const& v, bool is_lower) {
if (m_solver->is_term(vi)) {
lp::var_index ti = m_solver->adjust_term_index(vi);
auto& vec = is_lower ? m_lower_terms : m_upper_terms;
if (vec.size() <= ti) {
vec.resize(ti + 1, constraint_bound(UINT_MAX, rational()));
}
constraint_bound& b = vec[ti];
if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) {
TRACE("arith", tout << "tighter bound " << vi << "\n";);
ctx().push_trail(vector_value_trail<context, constraint_bound>(vec, ti));
b.first = ci;
b.second = v;
}
return true;
}
else {
TRACE("arith", tout << "not a term " << vi << "\n";);
// m_solver already tracks bounds on proper variables, but not on terms.
return;
}
lp::var_index ti = m_solver->adjust_term_index(vi);
auto& vec = is_lower ? m_lower_terms : m_upper_terms;
if (vec.size() <= ti) {
vec.resize(ti + 1, constraint_bound(UINT_MAX, rational()));
}
constraint_bound& b = vec[ti];
if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) {
ctx().push_trail(vector_value_trail<context, constraint_bound>(vec, ti));
b.first = ci;
b.second = v;
bool is_strict = false;
rational b;
if (is_lower) {
return m_solver->has_lower_bound(vi, ci, b, is_strict) && !is_strict && b == v;
}
else {
return m_solver->has_upper_bound(vi, ci, b, is_strict) && !is_strict && b == v;
}
}
}

622
src/smt/theory_pb.cpp
View file

@ -158,8 +158,6 @@ namespace smt {
m_watch_sz = 0;
m_watch_sum.reset();
m_num_propagations = 0;
m_compilation_threshold = UINT_MAX;
m_compiled = l_false;
m_args[0].reset();
m_args[0].m_k.reset();
m_args[1].reset();
@ -430,10 +428,6 @@ namespace smt {
void theory_pb::card::inc_propagations(theory_pb& th) {
++m_num_propagations;
if (m_compiled == l_false && m_num_propagations >= m_compilation_threshold) {
// m_compiled = l_undef;
// th.m_to_compile.push_back(&c);
}
}
// ------------------------
@ -443,8 +437,6 @@ namespace smt {
theory(m.mk_family_id("pb")),
m_params(p),
pb(m),
m_max_compiled_coeff(rational(8)),
m_cardinality_lemma(false),
m_restart_lim(3),
m_restart_inc(0),
m_antecedent_exprs(m),
@ -452,7 +444,6 @@ namespace smt {
{
m_learn_complements = p.m_pb_learn_complements;
m_conflict_frequency = p.m_pb_conflict_frequency;
m_enable_compilation = p.m_pb_enable_compilation;
}
theory_pb::~theory_pb() {
@ -465,7 +456,8 @@ namespace smt {
bool theory_pb::internalize_atom(app * atom, bool gate_ctx) {
context& ctx = get_context();
TRACE("pb", tout << mk_pp(atom, get_manager()) << "\n";);
ast_manager& m = get_manager();
if (ctx.b_internalized(atom)) {
return true;
}
@ -490,6 +482,38 @@ namespace smt {
unsigned num_args = atom->get_num_args();
bool_var abv = ctx.mk_bool_var(atom);
ctx.set_var_theory(abv, get_id());
literal lit(abv);
if (pb.is_eq(atom)) {
expr_ref_vector args(m), nargs(m);
vector<rational> coeffs;
rational sum(0);
for (unsigned i = 0; i < num_args; ++i) {
args.push_back(atom->get_arg(i));
nargs.push_back(::mk_not(m, atom->get_arg(i)));
rational c = pb.get_coeff(atom, i);
coeffs.push_back(c);
sum += c;
}
rational k = pb.get_k(atom);
// ax + by + cz <= k
// <=>
// -ax - by - cz >= -k
// <=>
// a(1-x) + b(1-y) + c(1-z) >= a + b + c - k
expr_ref le(pb.mk_ge(num_args, coeffs.c_ptr(), nargs.c_ptr(), sum - k), m);
expr_ref ge(pb.mk_ge(num_args, coeffs.c_ptr(), args.c_ptr(), k), m);
ctx.internalize(le, false);
ctx.internalize(ge, false);
literal le_lit = ctx.get_literal(le);
literal ge_lit = ctx.get_literal(ge);
ctx.mark_as_relevant(le_lit);
ctx.mark_as_relevant(ge_lit);
ctx.mk_th_axiom(get_id(), ~lit, le_lit);
ctx.mk_th_axiom(get_id(), ~lit, ge_lit);
ctx.mk_th_axiom(get_id(), ~le_lit, ~ge_lit, lit);
return true;
}
ineq* c = alloc(ineq, m_mpz_mgr, literal(abv), pb.is_eq(atom));
c->m_args[0].m_k = pb.get_k(atom);
@ -512,34 +536,23 @@ namespace smt {
break;
}
}
if (pb.is_at_most_k(atom) || pb.is_le(atom)) {
// turn W <= k into -W >= -k
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = -args[i].second;
}
k = -k;
for (auto& a : args) {
a.first.neg();
k += a.second;
}
}
else {
SASSERT(pb.is_at_least_k(atom) || pb.is_ge(atom) || pb.is_eq(atom));
}
TRACE("pb", display(tout, *c, true););
//app_ref fml1(m), fml2(m);
//fml1 = c->to_expr(ctx, m);
c->unique();
lbool is_true = c->normalize();
c->prune();
c->post_prune();
//fml2 = c->to_expr(ctx, m);
//expr_ref validate_pb = pb_rewriter(m).mk_validate_rewrite(fml1, fml2);
//pb_rewriter(m).dump_pb_rewrite(validate_pb);
literal lit(abv);
TRACE("pb", display(tout, *c); tout << " := " << lit << "\n";);
switch(is_true) {
TRACE("pb", display(tout, *c); tout << " := " << lit << " " << is_true << "\n";);
switch (is_true) {
case l_false:
lit = ~lit;
lit.neg();
// fall-through
case l_true:
ctx.mk_th_axiom(get_id(), 1, &lit);
@ -564,40 +577,18 @@ namespace smt {
// maximal coefficient:
scoped_mpz& max_watch = c->m_max_watch;
max_watch.reset();
for (unsigned i = 0; i < args.size(); ++i) {
mpz const& num = args[i].second.to_mpq().numerator();
for (auto const& a : args) {
mpz const& num = a.second.to_mpq().numerator();
if (m_mpz_mgr.lt(max_watch, num)) {
max_watch = num;
}
}
// pre-compile threshold for cardinality
bool enable_compile = m_enable_compilation && c->is_ge() && !c->k().is_one();
for (unsigned i = 0; enable_compile && i < args.size(); ++i) {
enable_compile = (args[i].second <= m_max_compiled_coeff);
}
if (enable_compile) {
unsigned log = 1, n = 1;
while (n <= args.size()) {
++log;
n *= 2;
}
unsigned th = args.size()*log*log;
c->m_compilation_threshold = th;
IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threshold to " << th << ")\n";);
TRACE("pb", tout << "compilation threshold: " << th << "\n";);
}
else {
c->m_compilation_threshold = UINT_MAX;
}
init_watch_var(*c);
init_watch_ineq(*c);
init_watch(abv);
m_var_infos[abv].m_ineq = c;
m_ineqs_trail.push_back(abv);
TRACE("pb", display(tout, *c););
return true;
}
@ -699,7 +690,6 @@ namespace smt {
}
}
void theory_pb::watch_literal(literal lit, ineq* c) {
init_watch(lit.var());
ptr_vector<ineq>* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
@ -707,27 +697,14 @@ namespace smt {
ineqs = alloc(ptr_vector<ineq>);
m_var_infos[lit.var()].m_lit_watch[lit.sign()] = ineqs;
}
DEBUG_CODE(
for (auto* c1 : *ineqs) {
//if (c1 == c) return;
SASSERT (c1 != c);
});
ineqs->push_back(c);
}
void theory_pb::watch_var(bool_var v, ineq* c) {
init_watch(v);
ptr_vector<ineq>* ineqs = m_var_infos[v].m_var_watch;
if (ineqs == nullptr) {
ineqs = alloc(ptr_vector<ineq>);
m_var_infos[v].m_var_watch = ineqs;
}
ineqs->push_back(c);
}
void theory_pb::unwatch_var(bool_var v, ineq* c) {
ptr_vector<ineq>* ineqs = m_var_infos[v].m_var_watch;
if (ineqs) {
remove(*ineqs, c);
}
}
void theory_pb::unwatch_literal(literal lit, ineq* c) {
ptr_vector<ineq>* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
if (ineqs) {
@ -736,13 +713,14 @@ namespace smt {
}
void theory_pb::remove(ptr_vector<ineq>& ineqs, ineq* c) {
for (unsigned j = 0; j < ineqs.size(); ++j) {
unsigned sz = ineqs.size();
for (unsigned j = 0; j < sz; ++j) {
if (ineqs[j] == c) {
std::swap(ineqs[j], ineqs[ineqs.size()-1]);
std::swap(ineqs[j], ineqs[sz-1]);
ineqs.pop_back();
break;
return;
}
}
}
}
// ----------------------------
@ -792,8 +770,6 @@ namespace smt {
return m.mk_th_lemma(m_fid, fact, prs.size(), prs.c_ptr());
}
}
};
@ -964,9 +940,9 @@ namespace smt {
justification* js = nullptr;
c.inc_propagations(*this);
if (!resolve_conflict(c, lits)) {
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
}
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
}
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
SASSERT(ctx.inconsistent());
@ -997,9 +973,6 @@ namespace smt {
st.update("pb conflicts", m_stats.m_num_conflicts);
st.update("pb propagations", m_stats.m_num_propagations);
st.update("pb predicates", m_stats.m_num_predicates);
st.update("pb compilations", m_stats.m_num_compiles);
st.update("pb compiled clauses", m_stats.m_num_compiled_clauses);
st.update("pb compiled vars", m_stats.m_num_compiled_vars);
}
void theory_pb::reset_eh() {
@ -1012,8 +985,6 @@ namespace smt {
m_card_trail.reset();
m_card_lim.reset();
m_stats.reset();
m_to_compile.reset();
m_cardinality_lemma = false;
}
void theory_pb::new_eq_eh(theory_var v1, theory_var v2) {
@ -1042,21 +1013,10 @@ namespace smt {
}
}
}
ineqs = m_var_infos[v].m_var_watch;
if (ineqs != nullptr) {
for (unsigned i = 0; i < ineqs->size(); ++i) {
ineq* c = (*ineqs)[i];
assign_watch(v, is_true, *c);
}
}
ineq* c = m_var_infos[v].m_ineq;
if (c != nullptr) {
if (c->is_ge()) {
assign_ineq(*c, is_true);
}
else {
assign_eq(*c, is_true);
}
VERIFY(c->is_ge());
assign_ineq(*c, is_true);
}
ptr_vector<card>* cards = m_var_infos[v].m_lit_cwatch[nlit.sign()];
@ -1143,19 +1103,6 @@ namespace smt {
return lits;
}
class theory_pb::rewatch_vars : public trail<context> {
theory_pb& pb;
ineq& c;
public:
rewatch_vars(theory_pb& p, ineq& c): pb(p), c(c) {}
void undo(context& ctx) override {
for (unsigned i = 0; i < c.size(); ++i) {
pb.watch_var(c.lit(i).var(), &c);
}
}
};
class theory_pb::negate_ineq : public trail<context> {
ineq& c;
public:
@ -1176,7 +1123,6 @@ namespace smt {
ctx.push_trail(value_trail<context, scoped_mpz>(c.m_max_sum));
ctx.push_trail(value_trail<context, scoped_mpz>(c.m_min_sum));
ctx.push_trail(value_trail<context, unsigned>(c.m_nfixed));
ctx.push_trail(rewatch_vars(*this, c));
SASSERT(c.is_ge());
unsigned sz = c.size();
@ -1214,10 +1160,15 @@ namespace smt {
// perform unit propagation
if (maxsum >= c.mpz_k() && maxsum - mininc < c.mpz_k()) {
literal_vector& lits = get_unhelpful_literals(c, true);
// for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true);
lits.push_back(c.lit());
// SASSERT(ctx.get_assignment(c.lit()) == l_true);
for (unsigned i = 0; i < sz; ++i) {
DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
add_assign(c, lits, c.lit(i));
literal lit = c.lit(i);
if (ctx.get_assignment(lit) == l_undef) {
DEBUG_CODE(validate_assign(c, lits, lit););
add_assign(c, lits, c.lit(i));
}
}
}
}
@ -1227,104 +1178,7 @@ namespace smt {
*/
void theory_pb::assign_eq(ineq& c, bool is_true) {
SASSERT(c.is_eq());
}
/**
Propagation rules:
nfixed = N & minsum = k -> T
nfixed = N & minsum != k -> F
minsum > k or maxsum < k -> F
minsum = k & = -> fix 0 variables
nfixed+1 = N & = -> fix unassigned variable or conflict
nfixed+1 = N & != -> maybe forced unassigned to ensure disequal
minsum >= k -> T
maxsum < k -> F
*/
void theory_pb::assign_watch(bool_var v, bool is_true, ineq& c) {
context& ctx = get_context();
unsigned i;
literal l = c.lit();
lbool asgn = ctx.get_assignment(l);
if (c.max_sum() < c.mpz_k() && asgn == l_false) {
return;
}
if (c.is_ge() && c.min_sum() >= c.mpz_k() && asgn == l_true) {
return;
}
for (i = 0; i < c.size(); ++i) {
if (c.lit(i).var() == v) {
break;
}
}
TRACE("pb", display(tout << "assign watch " << literal(v,!is_true) << " ", c, true););
SASSERT(i < c.size());
if (c.lit(i).sign() == is_true) {
ctx.push_trail(value_trail<context, scoped_mpz>(c.m_max_sum));
c.m_max_sum -= c.ncoeff(i);
}
else {
ctx.push_trail(value_trail<context, scoped_mpz>(c.m_min_sum));
c.m_min_sum += c.ncoeff(i);
}
DEBUG_CODE(
scoped_mpz sum(m_mpz_mgr);
scoped_mpz maxs(m_mpz_mgr);
for (unsigned i = 0; i < c.size(); ++i) {
if (ctx.get_assignment(c.lit(i)) == l_true) sum += c.ncoeff(i);
if (ctx.get_assignment(c.lit(i)) != l_false) maxs += c.ncoeff(i);
}
CTRACE("pb", (maxs > c.max_sum()), display(tout, c, true););
SASSERT(c.min_sum() <= sum);
SASSERT(sum <= maxs);
SASSERT(maxs <= c.max_sum());
);
SASSERT(c.min_sum() <= c.max_sum());
SASSERT(!m_mpz_mgr.is_neg(c.min_sum()));
ctx.push_trail(value_trail<context, unsigned>(c.m_nfixed));
++c.m_nfixed;
SASSERT(c.nfixed() <= c.size());
if (c.is_ge() && c.min_sum() >= c.mpz_k() && asgn != l_true) {
TRACE("pb", display(tout << "Set " << l << "\n", c, true););
add_assign(c, get_helpful_literals(c, false), l);
}
else if (c.max_sum() < c.mpz_k() && asgn != l_false) {
TRACE("pb", display(tout << "Set " << ~l << "\n", c, true););
add_assign(c, get_unhelpful_literals(c, true), ~l);
}
else if (c.is_eq() && c.nfixed() == c.size() && c.min_sum() == c.mpz_k() && asgn != l_true) {
TRACE("pb", display(tout << "Set " << l << "\n", c, true););
add_assign(c, get_all_literals(c, false), l);
}
else if (c.is_eq() && c.nfixed() == c.size() && c.min_sum() != c.mpz_k() && asgn != l_false) {
TRACE("pb", display(tout << "Set " << ~l << "\n", c, true););
add_assign(c, get_all_literals(c, false), ~l);
}
#if 0
else if (c.is_eq() && c.min_sum() > c.mpz_k() && asgn != l_false) {
TRACE("pb", display(tout << "Set " << ~l << "\n", c, true););
add_assign(c, get_all_literals(c, false), ~l);
}
else if (c.is_eq() && asgn == l_true && c.min_sum() == c.mpz_k() && c.max_sum() > c.mpz_k()) {
literal_vector& lits = get_all_literals(c, false);
lits.push_back(c.lit());
for (unsigned i = 0; i < c.size(); ++i) {
if (ctx.get_assignment(c.lit(i)) == l_undef) {
add_assign(c, lits, ~c.lit(i));
}
}
}
#endif
else {
IF_VERBOSE(14, display(verbose_stream() << "no propagation ", c, true););
}
UNREACHABLE();
}
@ -1479,31 +1333,9 @@ namespace smt {
void theory_pb::inc_propagations(ineq& c) {
++c.m_num_propagations;
if (c.m_compiled == l_false && c.m_num_propagations >= c.m_compilation_threshold) {
c.m_compiled = l_undef;
m_to_compile.push_back(&c);
}
}
void theory_pb::restart_eh() {
for (unsigned i = 0; i < m_to_compile.size(); ++i) {
compile_ineq(*m_to_compile[i]);
}
m_to_compile.reset();
return;
if (m_restart_lim <= m_restart_inc) {
m_restart_inc = 0;
if (gc()) {
m_restart_lim = 3;
}
else {
m_restart_lim *= 4;
m_restart_lim /= 3;
}
}
++m_restart_inc;
}
bool theory_pb::gc() {
@ -1553,7 +1385,7 @@ namespace smt {
}
}
std::cout << "zs: " << z << " nzs: " << nz << " lemmas: " << ctx.get_lemmas().size() << " trail: " << m_card_trail.size() << "\n";
//std::cout << "zs: " << z << " nzs: " << nz << " lemmas: " << ctx.get_lemmas().size() << " trail: " << m_card_trail.size() << "\n";
return z*10 >= nz;
m_occs.reset();
@ -1568,76 +1400,6 @@ namespace smt {
}
void theory_pb::compile_ineq(ineq& c) {
++m_stats.m_num_compiles;
context& ctx = get_context();
// only cardinality constraints are compiled.
SASSERT(c.m_compilation_threshold < UINT_MAX);
DEBUG_CODE(for (unsigned i = 0; i < c.size(); ++i) SASSERT(c.coeff(i).is_int()); );
unsigned k = c.k().get_unsigned();
unsigned num_args = c.size();
literal thl = c.lit();
literal at_least_k;
literal_vector in;
for (unsigned i = 0; i < num_args; ++i) {
rational n = c.coeff(i);
literal lit = c.lit(i);
lbool val = ctx.get_assignment(lit);
if (val != l_undef && ctx.get_assign_level(lit) == ctx.get_base_level()) {
if (val == l_true) {
unsigned m = n.get_unsigned();
if (k < m) {
return;
}
k -= m;
}
continue;
}
while (n.is_pos()) {
in.push_back(c.lit(i));
n -= rational::one();
}
}
TRACE("pb", tout << in << " >= " << k << "\n";);
psort_expr ps(ctx, *this);
psort_nw<psort_expr> sortnw(ps);
sortnw.m_stats.reset();
if (ctx.get_assignment(thl) == l_true &&
ctx.get_assign_level(thl) == ctx.get_base_level()) {
at_least_k = sortnw.ge(false, k, in.size(), in.c_ptr());
TRACE("pb", tout << ~thl << " " << at_least_k << "\n";);
ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k));
}
else {
literal at_least_k = sortnw.ge(true, k, in.size(), in.c_ptr());
TRACE("pb", tout << ~thl << " " << at_least_k << "\n";);
ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k));
ctx.mk_clause(~at_least_k, thl, justify(thl, ~at_least_k));
}
m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars;
m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses;
IF_VERBOSE(2, verbose_stream()
<< "(smt.pb compile sorting network bound: "
<< k << " literals: " << in.size()
<< " clauses: " << sortnw.m_stats.m_num_compiled_clauses
<< " vars: " << sortnw.m_stats.m_num_compiled_vars << ")\n";);
// auxiliary clauses get removed when popping scopes.
// we have to recompile the circuit after back-tracking.
c.m_compiled = l_false;
ctx.push_trail(value_trail<context, lbool>(c.m_compiled));
c.m_compiled = l_true;
}
void theory_pb::init_search_eh() {
}
@ -1657,7 +1419,6 @@ namespace smt {
clear_watch(*c);
m_var_infos[v].m_ineq = nullptr;
m_ineqs_trail.pop_back();
m_to_compile.erase(c);
dealloc(c);
}
m_ineqs_lim.resize(new_lim);
@ -1682,7 +1443,6 @@ namespace smt {
void theory_pb::clear_watch(ineq& c) {
for (unsigned i = 0; i < c.size(); ++i) {
literal w = c.lit(i);
unwatch_var(w.var(), &c);
unwatch_literal(w, &c);
}
c.m_watch_sum.reset();
@ -1728,7 +1488,7 @@ namespace smt {
ctx.push_trail(unwatch_ge(*this, c));
}
void theory_pb::init_watch_var(ineq& c) {
void theory_pb::init_watch_ineq(ineq& c) {
c.m_min_sum.reset();
c.m_max_sum.reset();
c.m_nfixed = 0;
@ -1736,7 +1496,6 @@ namespace smt {
c.m_max_watch.reset();
c.m_watch_sz = 0;
for (unsigned i = 0; i < c.size(); ++i) {
watch_var(c.lit(i).var(), &c);
c.m_max_sum += c.ncoeff(i);
}
}
@ -1858,7 +1617,7 @@ namespace smt {
k.assert_expr(notB);
lbool is_sat = k.check();
validating = false;
std::cout << is_sat << "\n";
// std::cout << is_sat << "\n";
if (is_sat == l_true) {
std::cout << A << "\n";
std::cout << B << "\n";
@ -1978,82 +1737,6 @@ namespace smt {
return true;
}
void theory_pb::add_cardinality_lemma() {
context& ctx = get_context();
normalize_active_coeffs();
int s = 0;
int new_bound = 0;
if (!init_arg_max()) {
return;
}
// TBD: can be optimized
while (s < m_bound) {
int coeff;
int arg = arg_max(coeff);
if (arg == -1) break;
s += coeff;
++new_bound;
}
int slack = m_active_coeffs.empty() ? m_bound : (std::min(m_bound, static_cast<int>(m_active_coeffs[0]) - 1));
reset_arg_max();
while (slack > 0) {
bool found = false;
int v = 0;
int coeff = 0;
for (unsigned i = 0; !found && i < m_active_vars.size(); ++i) {
bool_var v = m_active_vars[i];
coeff = get_abs_coeff(v);
if (0 < coeff && coeff < slack) {
found = true;
}
}
if (!found) {
break;
}
slack -= coeff;
m_coeffs[v] = 0; // deactivate coefficient.
}
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
bool_var v = m_active_vars[i];
int coeff = get_coeff(v);
if (coeff < 0) {
m_coeffs[v] = -1;
}
else if (coeff > 0) {
m_coeffs[v] = 1;
}
}
m_bound = new_bound;
if (!validate_lemma()) {
return;
}
SASSERT(m_bound > 0);
if (m_bound > static_cast<int>(m_active_vars.size())) {
return;
}
if (m_bound == static_cast<int>(m_active_vars.size())) {
return;
}
m_antecedent_exprs.reset();
m_antecedent_signs.reset();
m_cardinality_exprs.reset();
m_cardinality_signs.reset();
for (unsigned i = 0; i < m_antecedents.size(); ++i) {
literal lit = m_antecedents[i];
m_antecedent_exprs.push_back(ctx.bool_var2expr(lit.var()));
m_antecedent_signs.push_back(lit.sign());
}
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
bool_var v = m_active_vars[i];
m_cardinality_exprs.push_back(ctx.bool_var2expr(v));
m_cardinality_signs.push_back(get_coeff(v) < 0);
}
m_cardinality_lemma = true;
}
void theory_pb::normalize_active_coeffs() {
while (!m_active_var_set.empty()) m_active_var_set.erase();
unsigned i = 0, j = 0, sz = m_active_vars.size();
@ -2129,53 +1812,13 @@ namespace smt {
m_coeffs[m_active_vars[i]] /= g;
}
m_bound = (m_bound + g - 1) / g;
std::cout << "CUT " << g << "\n";
TRACE("pb", display_resolved_lemma(tout << "cut\n"););
}
}
bool theory_pb::can_propagate() { return m_cardinality_lemma; }
bool theory_pb::can_propagate() { return false; }
void theory_pb::propagate() {
context& ctx = get_context();
ast_manager& m = get_manager();
if (!m_cardinality_lemma) {
return;
}
m_cardinality_lemma = false;
if (ctx.inconsistent()) {
return;
}
m_antecedents.reset();
for (unsigned i = 0; i < m_antecedent_exprs.size(); ++i) {
expr* a = m_antecedent_exprs[i].get();
if (!ctx.b_internalized(a)) {
std::cout << "not internalized " << mk_pp(a, m) << "\n";
return;
}
m_antecedents.push_back(~literal(ctx.get_bool_var(a), m_antecedent_signs[i]));
}
for (unsigned i = 0; i < m_cardinality_exprs.size(); ++i) {
expr* a = m_cardinality_exprs[i].get();
if (!ctx.b_internalized(a)) {
std::cout << "not internalized " << mk_pp(a, m) << "\n";
return;
}
if (m_cardinality_signs[i]) {
m_cardinality_exprs[i] = m.mk_not(a);
}
}
app_ref atl(pb.mk_at_least_k(m_cardinality_exprs.size(), m_cardinality_exprs.c_ptr(), m_bound), m);
VERIFY(internalize_card(atl, false));
bool_var abv = ctx.get_bool_var(atl);
m_antecedents.push_back(literal(abv));
justification* js = nullptr;
if (proofs_enabled()) {
js = nullptr;
}
ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
void theory_pb::propagate() { }
bool theory_pb::resolve_conflict(card& c, literal_vector const& confl) {
@ -2185,9 +1828,7 @@ namespace smt {
context& ctx = get_context();
ast_manager& m = get_manager();
m_conflict_lvl = 0;
m_cardinality_lemma = false;
for (unsigned i = 0; i < confl.size(); ++i) {
literal lit = confl[i];
for (literal lit : confl) {
SASSERT(ctx.get_assignment(lit) == l_false);
m_conflict_lvl = std::max(m_conflict_lvl, ctx.get_assign_level(lit));
}
@ -2195,8 +1836,6 @@ namespace smt {
return false;
}
// std::cout << c.lit() << "\n";
reset_coeffs();
m_num_marks = 0;
m_bound = c.k();
@ -2285,6 +1924,7 @@ namespace smt {
process_antecedent(~js.get_literal(), offset);
break;
case b_justification::AXIOM:
bound = 0;
break;
case b_justification::JUSTIFICATION: {
justification* j = js.get_justification();
@ -2295,7 +1935,11 @@ namespace smt {
}
if (pbj == nullptr) {
TRACE("pb", tout << "skip justification for " << conseq << "\n";);
inc_coeff(conseq, offset);
bound = 0;
// this is possible when conseq is an assumption.
// The justification of conseq is itself,
// don't increment the cofficient here because it assumes
// conseq is justified further. it isnt'. conseq becomes part of the lemma.
}
else {
card& c2 = pbj->get_card();
@ -2303,7 +1947,6 @@ namespace smt {
bound = c2.k();
}
// std::cout << " offset: " << offset << " bound: " << bound << "\n";
break;
}
default:
@ -2354,66 +1997,42 @@ namespace smt {
slack += get_abs_coeff(v);
}
#if 1
//std::cout << slack << " " << m_bound << "\n";
unsigned i = 0;
literal_vector const& alits = ctx.assigned_literals();
literal alit = get_asserting_literal(~conseq);
slack -= get_abs_coeff(alit.var());
for (i = alits.size(); 0 <= slack && i > 0; ) {
--i;
for (i = alits.size(); 0 <= slack && i-- > 0; ) {
literal lit = alits[i];
bool_var v = lit.var();
// -3*x >= k
if (m_active_var_set.contains(v) && v != alit.var()) {
int coeff = get_coeff(v);
//std::cout << coeff << " " << lit << "\n";
if (coeff < 0 && !lit.sign()) {
slack += coeff;
m_antecedents.push_back(lit);
//std::cout << "ante: " << lit << "\n";
}
else if (coeff > 0 && lit.sign()) {
slack -= coeff;
m_antecedents.push_back(lit);
//std::cout << "ante: " << lit << "\n";
}
}
}
SASSERT(slack < 0);
#else
literal alit = get_asserting_literal(~conseq);
slack -= get_abs_coeff(alit.var());
for (unsigned i = 0; 0 <= slack; ++i) {
SASSERT(i < m_active_vars.size());
bool_var v = m_active_vars[i];
literal lit(v, get_coeff(v) < 0);
if (v != alit.var() && ctx.get_assignment(lit) == l_false) {
m_antecedents.push_back(~lit);
slack -= get_abs_coeff(v);
}
if (slack < 0) {
std::cout << i << " " << m_active_vars.size() << "\n";
}
}
#endif
SASSERT(validate_antecedents(m_antecedents));
TRACE("pb", tout << "antecedents " << m_antecedents << "\n";);
ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, nullptr)));
DEBUG_CODE(
m_antecedents.push_back(~alit);
expr_ref_vector args(m);
for (unsigned i = 0; i < m_antecedents.size(); ++i) {
args.push_back(literal2expr(m_antecedents[i]));
for (literal lit : m_antecedents) {
args.push_back(literal2expr(lit));
}
B = m.mk_not(m.mk_and(args.size(), args.c_ptr()));
validate_implies(A, B); );
// add_cardinality_lemma();
return true;
}
@ -2477,21 +2096,58 @@ namespace smt {
}
void theory_pb::validate_final_check() {
for (unsigned i = 0; i < m_var_infos.size(); ++i) {
ineq* c = m_var_infos[i].m_ineq;
if (c) {
validate_final_check(*c);
TRACE("pb", tout << "validate " << m_var_infos.size() << "\n";);
for (auto & vi : m_var_infos) {
if (vi.m_ineq) {
validate_final_check(*vi.m_ineq);
}
if (vi.m_card) {
validate_final_check(*vi.m_card);
}
}
}
void theory_pb::validate_final_check(card& c) {
context& ctx = get_context();
if (ctx.get_assignment(c.lit()) == l_undef) {
TRACE("pb", display(tout << "is undef ", c, true););
return;
}
if (!ctx.is_relevant(c.lit())) {
TRACE("pb", display(tout << "not relevant ", c, true););
return;
}
unsigned sum = 0, maxsum = 0;
for (unsigned i = 0; i < c.size(); ++i) {
switch(ctx.get_assignment(c.lit(i))) {
case l_true:
++sum;
case l_undef:
++maxsum;
break;
case l_false:
break;
}
}
TRACE("pb_verbose", display(tout << "validate: ", c, true);
tout << "sum: " << sum << " " << maxsum << " ";
tout << ctx.get_assignment(c.lit()) << "\n";);
SASSERT(sum <= maxsum);
SASSERT((sum >= c.k()) == (ctx.get_assignment(c.lit()) == l_true));
SASSERT((maxsum < c.k()) == (ctx.get_assignment(c.lit()) == l_false));
}
void theory_pb::validate_final_check(ineq& c) {
context& ctx = get_context();
if (ctx.get_assignment(c.lit()) == l_undef) {
TRACE("pb", tout << c.lit() << " is undef\n";);
return;
}
if (!ctx.is_relevant(c.lit())) {
TRACE("pb", tout << c.lit() << " is not relevant\n";);
return;
}
numeral sum = numeral::zero(), maxsum = numeral::zero();
@ -2519,8 +2175,8 @@ namespace smt {
bool theory_pb::validate_antecedents(literal_vector const& lits) {
context& ctx = get_context();
for (unsigned i = 0; i < lits.size(); ++i) {
if (ctx.get_assignment(lits[i]) != l_true) {
for (literal lit : lits) {
if (ctx.get_assignment(lit) != l_true) {
return false;
}
}
@ -2530,7 +2186,9 @@ namespace smt {
bool theory_pb::validate_unit_propagation(card const& c) {
context& ctx = get_context();
for (unsigned i = c.k(); i < c.size(); ++i) {
VERIFY(ctx.get_assignment(c.lit(i)) == l_false);
if (ctx.get_assignment(c.lit(i)) != l_false) {
return false;
}
}
return true;
}
@ -2560,15 +2218,11 @@ namespace smt {
void theory_pb::display_resolved_lemma(std::ostream& out) const {
context& ctx = get_context();
bool_var v;
unsigned lvl;
out << "num marks: " << m_num_marks << "\n";
out << "conflict level: " << m_conflict_lvl << "\n";
for (unsigned i = 0; i < m_resolved.size(); ++i) {
v = m_resolved[i].var();
lvl = ctx.get_assign_level(v);
out << lvl << ": " << m_resolved[i] << " ";
ctx.display(out, ctx.get_justification(v));
for (literal r : m_resolved) {
out << ctx.get_assign_level(r) << ": " << r << " ";
ctx.display(out, ctx.get_justification(r.var()));
}
if (!m_antecedents.empty()) {
@ -2757,16 +2411,6 @@ namespace smt {
display_watch(out, vi, false);
display_watch(out, vi, true);
}
for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
ineq_watch const* w = m_var_infos[vi].m_var_watch;
if (!w) continue;
out << "watch (v): " << literal(vi) << " |-> ";
ineq_watch const& wl = *w;
for (unsigned i = 0; i < wl.size(); ++i) {
out << wl[i]->lit() << " ";
}
out << "\n";
}
for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
ineq* c = m_var_infos[vi].m_ineq;
if (c) {

29
src/smt/theory_pb.h
View file

@ -97,9 +97,6 @@ namespace smt {
unsigned m_num_conflicts;
unsigned m_num_propagations;
unsigned m_num_predicates;
unsigned m_num_compiles;
unsigned m_num_compiled_vars;
unsigned m_num_compiled_clauses;
void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); }
};
@ -120,8 +117,6 @@ namespace smt {
scoped_mpz m_max_sum; // maximal possible sum.
scoped_mpz m_min_sum; // minimal possible sum.
unsigned m_num_propagations;
unsigned m_compilation_threshold;
lbool m_compiled;
ineq(unsynch_mpz_manager& m, literal l, bool is_eq) :
m_mpz(m), m_lit(l), m_is_eq(is_eq),
@ -197,8 +192,6 @@ namespace smt {
unsigned m_bound;
unsigned m_num_propagations;
unsigned m_all_propagations;
unsigned m_compilation_threshold;
lbool m_compiled;
bool m_aux;
public:
@ -207,8 +200,6 @@ namespace smt {
m_bound(bound),
m_num_propagations(0),
m_all_propagations(0),
m_compilation_threshold(0),
m_compiled(l_false),
m_aux(is_aux)
{
SASSERT(bound > 0);
@ -252,13 +243,12 @@ namespace smt {
struct var_info {
ineq_watch* m_lit_watch[2];
ineq_watch* m_var_watch;
ineq* m_ineq;
card_watch* m_lit_cwatch[2];
card* m_card;
var_info(): m_var_watch(nullptr), m_ineq(nullptr), m_card(nullptr)
var_info(): m_ineq(nullptr), m_card(nullptr)
{
m_lit_watch[0] = nullptr;
m_lit_watch[1] = nullptr;
@ -269,7 +259,6 @@ namespace smt {
void reset() {
dealloc(m_lit_watch[0]);
dealloc(m_lit_watch[1]);
dealloc(m_var_watch);
dealloc(m_ineq);
dealloc(m_lit_cwatch[0]);
dealloc(m_lit_cwatch[1]);
@ -286,13 +275,9 @@ namespace smt {
literal_vector m_literals; // temporary vector
pb_util pb;
stats m_stats;
ptr_vector<ineq> m_to_compile; // inequalities to compile.
unsigned m_conflict_frequency;
bool m_learn_complements;
bool m_enable_compilation;
rational m_max_compiled_coeff;
bool m_cardinality_lemma;
unsigned m_restart_lim;
unsigned m_restart_inc;
uint_set m_occs;
@ -305,16 +290,13 @@ namespace smt {
void add_watch(ineq& c, unsigned index);
void del_watch(ineq_watch& watch, unsigned index, ineq& c, unsigned ineq_index);
void init_watch_literal(ineq& c);
void init_watch_var(ineq& c);
void init_watch_ineq(ineq& c);
void clear_watch(ineq& c);
void watch_literal(literal lit, ineq* c);
void watch_var(bool_var v, ineq* c);
void unwatch_literal(literal w, ineq* c);
void unwatch_var(bool_var v, ineq* c);
void remove(ptr_vector<ineq>& ineqs, ineq* c);
bool assign_watch_ge(bool_var v, bool is_true, ineq_watch& watch, unsigned index);
void assign_watch(bool_var v, bool is_true, ineq& c);
void assign_ineq(ineq& c, bool is_true);
void assign_eq(ineq& c, bool is_true);
@ -357,11 +339,6 @@ namespace smt {
literal_vector& get_helpful_literals(ineq& c, bool negate);
literal_vector& get_unhelpful_literals(ineq& c, bool negate);
//
// Utilities to compile cardinality
// constraints into a sorting network.
//
void compile_ineq(ineq& c);
void inc_propagations(ineq& c);
//
@ -396,7 +373,6 @@ namespace smt {
void reset_arg_max();
void reset_coeffs();
void add_cardinality_lemma();
literal get_asserting_literal(literal conseq);
bool resolve_conflict(card& c, literal_vector const& conflict_clause);
@ -411,6 +387,7 @@ namespace smt {
bool validate_lemma();
void validate_final_check();
void validate_final_check(ineq& c);
void validate_final_check(card& c);
void validate_assign(ineq const& c, literal_vector const& lits, literal l) const;
void validate_watch(ineq const& c) const;
bool validate_unit_propagation(card const& c);

4
src/smt/theory_recfun.h
View file

@ -69,7 +69,7 @@ namespace smt {
recfun::case_def const * m_cdef;
ptr_vector<expr> m_args;
body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(0), m_args() {
body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(nullptr), m_args() {
m_cdef = &u.get_case_def(n);
m_args.append(n->get_num_args(), n->get_args());
}
@ -125,7 +125,7 @@ namespace smt {
literal mk_eq_lit(expr* l, expr* r);
bool is_standard_order(recfun::vars const& vars) const {
return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0;
return vars.empty() || vars[vars.size()-1]->get_idx() == 0;
}
protected:
void push_case_expand(case_expansion* e) { m_q_case_expand.push_back(e); }

974
src/smt/theory_seq.cpp
View file

File diff suppressed because it is too large Load diff

26
src/smt/theory_seq.h
View file

@ -19,9 +19,7 @@ Revision History:
#ifndef THEORY_SEQ_H_
#define THEORY_SEQ_H_
#include "smt/smt_theory.h"
#include "ast/seq_decl_plugin.h"
#include "smt/theory_seq_empty.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/ast_trail.h"
#include "util/scoped_vector.h"
@ -30,6 +28,9 @@ Revision History:
#include "ast/rewriter/seq_rewriter.h"
#include "util/union_find.h"
#include "util/obj_ref_hashtable.h"
#include "smt/smt_theory.h"
#include "smt/smt_arith_value.h"
#include "smt/theory_seq_empty.h"
namespace smt {
@ -343,14 +344,16 @@ namespace smt {
unsigned m_axioms_head; // index of first axiom to add.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
expr_ref_vector m_int_string;
obj_hashtable<expr> m_si_axioms;
obj_hashtable<expr> m_length; // is length applied
obj_map<expr, rational> m_si_axioms;
obj_hashtable<expr> m_has_length; // is length applied
expr_ref_vector m_length; // length applications themselves
scoped_ptr_vector<apply> m_replay; // set of actions to replay
model_generator* m_mg;
th_rewriter m_rewrite;
seq_rewriter m_seq_rewrite;
seq_util m_util;
arith_util m_autil;
arith_value m_arith_value;
th_trail_stack m_trail_stack;
stats m_stats;
symbol m_prefix, m_suffix, m_accept, m_reject;
@ -401,6 +404,8 @@ namespace smt {
void init_search_eh() override;
void init_model(expr_ref_vector const& es);
app* get_ite_value(expr* a);
void get_ite_concat(expr* e, ptr_vector<expr>& concats);
void len_offset(expr* e, rational val);
void prop_arith_to_len_offset();
@ -415,12 +420,13 @@ namespace smt {
bool reduce_length_eq();
bool branch_unit_variable(); // branch on XYZ = abcdef
bool branch_binary_variable(); // branch on abcX = Ydefg
bool branch_variable(); // branch on
bool branch_ternary_variable1(); // branch on XabcY = Zdefg or XabcY = defgZ
bool branch_ternary_variable2(); // branch on XabcY = defgZmnpq
bool branch_quat_variable(); // branch on XabcY = ZdefgT
bool len_based_split(); // split based on len offset
bool branch_variable_mb(); // branch on a variable, model based on length
bool branch_variable(); // branch on a variable
bool branch_variable_eq(); // branch on a variable, by an alignment among variable boundaries.
bool is_solved();
bool check_length_coherence();
bool check_length_coherence0(expr* e);
@ -428,7 +434,7 @@ namespace smt {
bool fixed_length(bool is_zero = false);
bool fixed_length(expr* e, bool is_zero);
void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
bool branch_variable(eq const& e);
bool branch_variable_eq(eq const& e);
bool branch_binary_variable(eq const& e);
bool eq_unit(expr* const& l, expr* const &r) const;
unsigned_vector overlap(expr_ref_vector const& ls, expr_ref_vector const& rs);
@ -446,6 +452,7 @@ namespace smt {
vector<rational> const& ll, vector<rational> const& rl);
bool set_empty(expr* x);
bool is_complex(eq const& e);
lbool regex_are_equal(expr* r1, expr* r2);
bool check_extensionality();
bool check_contains();
@ -536,8 +543,6 @@ namespace smt {
expr_ref expand1(expr* e, dependency*& eqs);
expr_ref try_expand(expr* e, dependency*& eqs);
void add_dependency(dependency*& dep, enode* a, enode* b);
void get_concat(expr* e, ptr_vector<expr>& concats);
// terms whose meaning are encoded using axioms.
void enque_axiom(expr* e);
@ -558,7 +563,7 @@ namespace smt {
bool is_extract_suffix(expr* s, expr* i, expr* l);
bool has_length(expr *e) const { return m_length.contains(e); }
bool has_length(expr *e) const { return m_has_length.contains(e); }
void add_length(expr* e);
void enforce_length(expr* n);
bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
@ -571,6 +576,7 @@ namespace smt {
expr_ref add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n);
void add_nth_axiom(expr* n);
void add_in_re_axiom(expr* n);
void add_itos_axiom(expr* n);
void add_stoi_axiom(expr* n);
@ -604,7 +610,7 @@ namespace smt {
bool get_length(expr* s, rational& val) const;
void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
expr* coalesce_chars(expr* const& str);
expr_ref coalesce_chars(expr* const& str);
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, expr* e4 = nullptr, sort* range = nullptr);
bool is_skolem(symbol const& s, expr* e) const;

165
src/smt/theory_str.cpp
View file

@ -507,7 +507,7 @@ namespace smt {
app * a = mk_fresh_const(name.c_str(), int_sort);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
SASSERT(ctx.e_internalized(a));
ctx.mark_as_relevant(a);
// I'm assuming that this combination will do the correct thing in the integer theory.
@ -546,7 +546,7 @@ namespace smt {
// I have a hunch that this may not get internalized for free...
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
SASSERT(ctx.e_internalized(a));
// this might help??
mk_var(ctx.get_enode(a));
@ -568,7 +568,7 @@ namespace smt {
m_trail.push_back(a);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
SASSERT(ctx.e_internalized(a));
mk_var(ctx.get_enode(a));
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
@ -619,7 +619,7 @@ namespace smt {
app * a = mk_fresh_const(name.c_str(), string_sort);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
// this might help??
mk_var(ctx.get_enode(a));
@ -712,7 +712,7 @@ namespace smt {
* Returns the simplified concatenation of two expressions,
* where either both expressions are constant strings
* or one expression is the empty string.
* If this precondition does not hold, the function returns NULL.
* If this precondition does not hold, the function returns nullptr.
* (note: this function was strTheory::Concat())
*/
expr * theory_str::mk_concat_const_str(expr * n1, expr * n2) {
@ -1667,53 +1667,66 @@ namespace smt {
}
}
// (str.replace s t t') is the string obtained by replacing the first occurrence
// of t in s, if any, by t'. Note that if t is empty, the result is to prepend
// t' to s; also, if t does not occur in s then the result is s.
void theory_str::instantiate_axiom_Replace(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
TRACE("str", tout << "already set up Replace axiom for " << mk_pp(expr, m) << std::endl;);
app * ex = e->get_owner();
if (axiomatized_terms.contains(ex)) {
TRACE("str", tout << "already set up Replace axiom for " << mk_pp(ex, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
axiomatized_terms.insert(ex);
TRACE("str", tout << "instantiate Replace axiom for " << mk_pp(expr, m) << std::endl;);
TRACE("str", tout << "instantiate Replace axiom for " << mk_pp(ex, m) << std::endl;);
expr_ref x1(mk_str_var("x1"), m);
expr_ref x2(mk_str_var("x2"), m);
expr_ref i1(mk_int_var("i1"), m);
expr_ref result(mk_str_var("result"), m);
expr * replaceS = nullptr;
expr * replaceT = nullptr;
expr * replaceTPrime = nullptr;
VERIFY(u.str.is_replace(ex, replaceS, replaceT, replaceTPrime));
// t empty => result = (str.++ t' s)
expr_ref emptySrcAst(ctx.mk_eq_atom(replaceT, mk_string("")), m);
expr_ref prependTPrimeToS(ctx.mk_eq_atom(result, mk_concat(replaceTPrime, replaceS)), m);
// condAst = Contains(args[0], args[1])
expr_ref condAst(mk_contains(expr->get_arg(0), expr->get_arg(1)), m);
expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
// -----------------------
// true branch
expr_ref_vector thenItems(m);
// args[0] = x1 . args[1] . x2
thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x1, mk_concat(expr->get_arg(1), x2))));
thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x1, mk_concat(ex->get_arg(1), x2))));
// i1 = |x1|
thenItems.push_back(ctx.mk_eq_atom(i1, mk_strlen(x1)));
// args[0] = x3 . x4 /\ |x3| = |x1| + |args[1]| - 1 /\ ! contains(x3, args[1])
expr_ref x3(mk_str_var("x3"), m);
expr_ref x4(mk_str_var("x4"), m);
expr_ref tmpLen(m_autil.mk_add(i1, mk_strlen(expr->get_arg(1)), mk_int(-1)), m);
thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
expr_ref tmpLen(m_autil.mk_add(i1, mk_strlen(ex->get_arg(1)), mk_int(-1)), m);
thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4)));
thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
thenItems.push_back(ctx.mk_eq_atom(result, mk_concat(x1, mk_concat(expr->get_arg(2), x2))));
thenItems.push_back(mk_not(m, mk_contains(x3, ex->get_arg(1))));
thenItems.push_back(ctx.mk_eq_atom(result, mk_concat(x1, mk_concat(ex->get_arg(2), x2))));
// -----------------------
// false branch
expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
expr_ref elseBranch(ctx.mk_eq_atom(result, ex->get_arg(0)), m);
th_rewriter rw(m);
expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
expr_ref breakdownAssert(m.mk_ite(emptySrcAst, prependTPrimeToS,
m.mk_ite(condAst, mk_and(thenItems), elseBranch)), m);
expr_ref breakdownAssert_rw(breakdownAssert, m);
rw(breakdownAssert_rw);
assert_axiom(breakdownAssert_rw);
expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
expr_ref reduceToResult(ctx.mk_eq_atom(ex, result), m);
expr_ref reduceToResult_rw(reduceToResult, m);
rw(reduceToResult_rw);
assert_axiom(reduceToResult_rw);
@ -2154,7 +2167,7 @@ namespace smt {
// Evaluates the concatenation (n1 . n2) with respect to
// the current equivalence classes of n1 and n2.
// Returns a constant string expression representing this concatenation
// if one can be determined, or NULL if this is not possible.
// if one can be determined, or nullptr if this is not possible.
expr * theory_str::eval_concat(expr * n1, expr * n2) {
bool n1HasEqcValue = false;
bool n2HasEqcValue = false;
@ -2228,7 +2241,7 @@ namespace smt {
for (enode_vector::iterator parent_it = current_parents.begin(); parent_it != current_parents.end(); ++parent_it) {
enode * e_parent = *parent_it;
SASSERT(e_parent != NULL);
SASSERT(e_parent != nullptr);
app * a_parent = e_parent->get_owner();
TRACE("str", tout << "considering parent " << mk_ismt2_pp(a_parent, m) << std::endl;);
@ -2507,7 +2520,7 @@ namespace smt {
}
}
if (resolvedMap.size() == 0) {
if (resolvedMap.empty()) {
// no simplification possible
return node;
} else {
@ -4844,6 +4857,7 @@ namespace smt {
bool theory_str::get_arith_value(expr* e, rational& val) const {
context& ctx = get_context();
ast_manager & m = get_manager();
(void)m;
if (!ctx.e_internalized(e)) {
return false;
}
@ -4867,9 +4881,10 @@ namespace smt {
return false;
}
arith_value v(get_context());
arith_value v(get_manager());
v.init(&get_context());
bool strict;
return v.get_lo(_e, lo, strict);
return v.get_lo_equiv(_e, lo, strict);
}
bool theory_str::upper_bound(expr* _e, rational& hi) {
@ -4878,9 +4893,10 @@ namespace smt {
return false;
}
arith_value v(get_context());
arith_value v(get_manager());
v.init(&get_context());
bool strict;
return v.get_up(_e, hi, strict);
return v.get_up_equiv(_e, hi, strict);
}
bool theory_str::get_len_value(expr* e, rational& val) {
@ -5458,7 +5474,7 @@ namespace smt {
}
if (implyR) {
if (litems1.size() == 0) {
if (litems1.empty()) {
assert_axiom(implyR);
} else {
assert_implication(mk_and(litems1), implyR);
@ -5581,7 +5597,7 @@ namespace smt {
tout << " " << mk_pp(el, m);
}
tout << std::endl;
if (constStrAst == NULL) {
if (constStrAst == nullptr) {
tout << "constStrAst = NULL" << std::endl;
} else {
tout << "constStrAst = " << mk_pp(constStrAst, m) << std::endl;
@ -7026,7 +7042,7 @@ namespace smt {
bool theory_str::refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound) {
ENSURE(aut != nullptr);
if (aut->final_states().size() < 1) {
if (aut->final_states().empty()) {
// no solutions at all
refined_lower_bound = rational::minus_one();
return false;
@ -7210,20 +7226,18 @@ namespace smt {
expr_ref theory_str::aut_path_rewrite_constraint(expr * cond, expr * ch_var) {
context & ctx = get_context();
ast_manager & m = get_manager();
bv_util bvu(m);
expr_ref retval(m);
rational char_val;
unsigned int bv_width;
unsigned char_val = 0;
expr * lhs;
expr * rhs;
if (bvu.is_numeral(cond, char_val, bv_width)) {
SASSERT(char_val.is_nonneg() && char_val.get_unsigned() < 256);
if (u.is_const_char(cond, char_val)) {
SASSERT(char_val < 256);
TRACE("str", tout << "rewrite character constant " << char_val << std::endl;);
zstring str_const(char_val.get_unsigned());
zstring str_const(char_val);
retval = u.str.mk_string(str_const);
return retval;
} else if (is_var(cond)) {
@ -7368,23 +7382,20 @@ namespace smt {
} else if (mv.t()->is_range()) {
expr_ref range_lo(mv.t()->get_lo(), m);
expr_ref range_hi(mv.t()->get_hi(), m);
bv_util bvu(m);
rational lo_val, hi_val;
unsigned int bv_width;
unsigned lo_val, hi_val;
if (bvu.is_numeral(range_lo, lo_val, bv_width) && bvu.is_numeral(range_hi, hi_val, bv_width)) {
if (u.is_const_char(range_lo, lo_val) && u.is_const_char(range_hi, hi_val)) {
TRACE("str", tout << "make range predicate from " << lo_val << " to " << hi_val << std::endl;);
expr_ref cond_rhs(m);
if (hi_val < lo_val) {
rational tmp = lo_val;
lo_val = hi_val;
hi_val = tmp;
// NSB: why? The range would be empty.
std::swap(lo_val, hi_val);
}
expr_ref_vector cond_rhs_terms(m);
for (unsigned i = lo_val.get_unsigned(); i <= hi_val.get_unsigned(); ++i) {
for (unsigned i = lo_val; i <= hi_val; ++i) {
zstring str_const(i);
expr_ref str_expr(u.str.mk_string(str_const), m);
cond_rhs_terms.push_back(ctx.mk_eq_atom(ch, str_expr));
@ -7492,15 +7503,12 @@ namespace smt {
expr_ref newConcat(m);
if (arg1 != a1 || arg2 != a2) {
TRACE("str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;);
int iPos = 0;
expr_ref_vector item1(m);
if (a1 != arg1) {
item1.push_back(ctx.mk_eq_atom(a1, arg1));
iPos += 1;
}
if (a2 != arg2) {
item1.push_back(ctx.mk_eq_atom(a2, arg2));
iPos += 1;
}
expr_ref implyL1(mk_and(item1), m);
newConcat = mk_concat(arg1, arg2);
@ -7793,7 +7801,7 @@ namespace smt {
generate_mutual_exclusion(arrangement_disjunction);
}
} /* (arg1Len != 1 || arg2Len != 1) */
} /* if (Concat(arg1, arg2) == NULL) */
} /* if (Concat(arg1, arg2) == nullptr) */
}
}
}
@ -8174,13 +8182,13 @@ namespace smt {
// step 2: Concat == Constant
if (eqc_const_lhs.size() != 0) {
if (!eqc_const_lhs.empty()) {
expr * conStr = *(eqc_const_lhs.begin());
std::set<expr*>::iterator itor2 = eqc_concat_rhs.begin();
for (; itor2 != eqc_concat_rhs.end(); itor2++) {
solve_concat_eq_str(*itor2, conStr);
}
} else if (eqc_const_rhs.size() != 0) {
} else if (!eqc_const_rhs.empty()) {
expr* conStr = *(eqc_const_rhs.begin());
std::set<expr*>::iterator itor1 = eqc_concat_lhs.begin();
for (; itor1 != eqc_concat_lhs.end(); itor1++) {
@ -8254,9 +8262,10 @@ namespace smt {
void theory_str::check_eqc_concat_concat(std::set<expr*> & eqc_concat_lhs, std::set<expr*> & eqc_concat_rhs) {
ast_manager & m = get_manager();
(void)m;
int hasCommon = 0;
if (eqc_concat_lhs.size() != 0 && eqc_concat_rhs.size() != 0) {
if (!eqc_concat_lhs.empty() && !eqc_concat_rhs.empty()) {
std::set<expr*>::iterator itor1 = eqc_concat_lhs.begin();
std::set<expr*>::iterator itor2 = eqc_concat_rhs.begin();
for (; itor1 != eqc_concat_lhs.end(); itor1++) {
@ -8576,13 +8585,13 @@ namespace smt {
obj_map<expr, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin();
while (varItor != cut_var_map.end()) {
std::stack<T_cut*> & val = cut_var_map[varItor->m_key];
while ((val.size() > 0) && (val.top()->level != 0) && (val.top()->level >= sLevel)) {
while ((!val.empty()) && (val.top()->level != 0) && (val.top()->level >= sLevel)) {
// TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout););
// T_cut * aCut = val.top();
val.pop();
// dealloc(aCut);
}
if (val.size() == 0) {
if (val.empty()) {
cutvarmap_removes.insert(varItor->m_key);
}
varItor++;
@ -9408,22 +9417,22 @@ namespace smt {
}
}
if (depMap.size() == 0) {
if (depMap.empty()) {
std::map<expr*, int>::iterator itor = strVarMap.begin();
for (; itor != strVarMap.end(); itor++) {
expr * var = get_alias_index_ast(aliasIndexMap, itor->first);
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1;
} else {
int lrConstainted = 0;
int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1;
lrConstrained = 1;
break;
}
}
if (lrConstainted == 0) {
if (lrConstrained == 0) {
freeVarMap[var] = 1;
}
}
@ -9442,15 +9451,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1;
} else {
int lrConstainted = 0;
int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1;
lrConstrained = 1;
break;
}
}
if (lrConstainted == 0) {
if (lrConstrained == 0) {
freeVarMap[var] = 1;
}
}
@ -9462,15 +9471,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1;
} else {
int lrConstainted = 0;
int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1;
lrConstrained = 1;
break;
}
}
if (lrConstainted == 0) {
if (lrConstrained == 0) {
freeVarMap[var] = 1;
}
}
@ -9491,15 +9500,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1;
} else {
int lrConstainted = 0;
int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1;
lrConstrained = 1;
break;
}
}
if (lrConstainted == 0) {
if (lrConstrained == 0) {
freeVarMap[var] = 1;
}
}
@ -9753,7 +9762,7 @@ namespace smt {
expr_ref concatlenExpr (mk_strlen(concat), m) ;
bool allLeafResolved = true;
if (! get_arith_value(concatlenExpr, lenValue)) {
// the length fo concat is unresolved yet
// the length of concat is unresolved yet
if (get_len_value(concat, lenValue)) {
// but all leaf nodes have length information
TRACE("str", tout << "* length pop-up: " << mk_ismt2_pp(concat, m) << "| = " << lenValue << std::endl;);
@ -10423,12 +10432,12 @@ namespace smt {
}
} // foreach(term in str_in_re_terms)
eautomaton * aut_inter = NULL;
eautomaton * aut_inter = nullptr;
CTRACE("str", !intersect_constraints.empty(), tout << "check intersection of automata constraints for " << mk_pp(str, m) << std::endl;);
for (svector<regex_automaton_under_assumptions>::iterator aut_it = intersect_constraints.begin();
aut_it != intersect_constraints.end(); ++aut_it) {
regex_automaton_under_assumptions aut = *aut_it;
if (aut_inter == NULL) {
if (aut_inter == nullptr) {
// start somewhere
aut_inter = aut.get_automaton();
used_intersect_constraints.push_back(aut);
@ -10478,7 +10487,7 @@ namespace smt {
}
}
} // foreach(entry in intersect_constraints)
if (aut_inter != NULL) {
if (aut_inter != nullptr) {
aut_inter->compress();
}
TRACE("str", tout << "intersected " << used_intersect_constraints.size() << " constraints" << std::endl;);
@ -10509,7 +10518,7 @@ namespace smt {
}
conflict_lhs = mk_and(conflict_terms);
if (used_intersect_constraints.size() > 1 && aut_inter != NULL) {
if (used_intersect_constraints.size() > 1 && aut_inter != nullptr) {
// check whether the intersection is only the empty string
unsigned initial_state = aut_inter->init();
if (aut_inter->final_states().size() == 1 && aut_inter->is_final_state(initial_state)) {
@ -10527,7 +10536,7 @@ namespace smt {
}
}
if (aut_inter != NULL && aut_inter->is_empty()) {
if (aut_inter != nullptr && aut_inter->is_empty()) {
TRACE("str", tout << "product automaton is empty; asserting conflict clause" << std::endl;);
expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m);
assert_axiom(conflict_clause);
@ -10807,7 +10816,7 @@ namespace smt {
expr * var = fvIt2->first;
tmpSet.clear();
get_eqc_allUnroll(var, constValue, tmpSet);
if (tmpSet.size() > 0) {
if (!tmpSet.empty()) {
fv_unrolls_map[var] = tmpSet;
}
}
@ -10941,7 +10950,7 @@ namespace smt {
expr * var = fvIt1->first;
fSimpUnroll.clear();
get_eqc_simpleUnroll(var, constValue, fSimpUnroll);
if (fSimpUnroll.size() == 0) {
if (fSimpUnroll.empty()) {
gen_assign_unroll_reg(fv_unrolls_map[var]);
} else {
expr * toAssert = gen_assign_unroll_Str2Reg(var, fSimpUnroll);
@ -11554,7 +11563,7 @@ namespace smt {
unroll_tries_map[var][unrolls].erase(e);
}
if (unroll_tries_map[var][unrolls].size() == 0) {
if (unroll_tries_map[var][unrolls].empty()) {
unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var());
}
@ -11815,7 +11824,7 @@ namespace smt {
expr_ref assertL(mk_and(and_items_LHS), m);
SASSERT(assertL);
expr * finalAxiom = m.mk_or(m.mk_not(assertL), lenTestAssert.get());
SASSERT(finalAxiom != NULL);
SASSERT(finalAxiom != nullptr);
TRACE("str", tout << "crash avoidance finalAxiom: " << mk_pp(finalAxiom, m) << std::endl;);
return finalAxiom;
} else {
@ -12101,7 +12110,7 @@ namespace smt {
lenTester_fvar_map.insert(indicator, freeVar);
expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum);
SASSERT(lenTestAssert != NULL);
SASSERT(lenTestAssert != nullptr);
return lenTestAssert;
} else {
TRACE("str", tout << "found previous in-scope length assertions" << std::endl;);
@ -12207,7 +12216,7 @@ namespace smt {
testNum = i + 1;
}
expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum);
SASSERT(lenTestAssert != NULL);
SASSERT(lenTestAssert != nullptr);
return lenTestAssert;
} else {
// if we are performing automata-based reasoning and the term associated with

2
src/smt/theory_utvpi_def.h
View file

@ -618,7 +618,7 @@ namespace smt {
th_var v1 = null_theory_var, v2 = null_theory_var;
bool pos1 = true, pos2 = true;
if (terms.size() >= 1) {
if (!terms.empty()) {
v1 = terms[0].first;
pos1 = terms[0].second.is_one();
SASSERT(v1 != null_theory_var);

10
src/smt/theory_wmaxsat.cpp
View file

@ -103,8 +103,8 @@ namespace smt {
m_normalize = true;
bool_var bv = register_var(var, true);
(void)bv;
TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";
tout << wfml << "\n";);
TRACE("opt", tout << "inc: " << ctx.inconsistent() << " enable: v" << m_bool2var[bv]
<< " b" << bv << " " << mk_pp(var, get_manager()) << "\n" << wfml << "\n";);
return var;
}
@ -134,8 +134,10 @@ namespace smt {
theory_var v = mk_var(x);
ctx.attach_th_var(x, this, v);
m_bool2var.insert(bv, v);
SASSERT(v == static_cast<theory_var>(m_var2bool.size()));
m_var2bool.push_back(bv);
while (m_var2bool.size() <= static_cast<unsigned>(v)) {
m_var2bool.push_back(null_bool_var);
}
m_var2bool[v] = bv;
SASSERT(ctx.bool_var2enode(bv));
}
return bv;

6
src/smt/watch_list.cpp
View file

@ -21,7 +21,7 @@ Revision History:
namespace smt {
#define DEFAULT_WATCH_LIST_SIZE (sizeof(clause *) * 4)
#ifdef _AMD64_
#if defined(__LP64__) || defined(_WIN64)
// make sure data is aligned in 64 bit machines
#define HEADER_SIZE (4 * sizeof(unsigned))
#else
@ -38,7 +38,7 @@ namespace smt {
if (m_data == nullptr) {
unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE;
unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, size));
#ifdef _AMD64_
#if defined(__LP64__) || defined(_WIN64)
++mem; // make sure data is aligned in 64 bit machines
#endif
*mem = 0;
@ -61,7 +61,7 @@ namespace smt {
unsigned new_capacity = (((curr_capacity * 3 + sizeof(clause *)) >> 1)+3)&~3U;
unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, new_capacity + HEADER_SIZE));
unsigned curr_end_cls = end_cls_core();
#ifdef _AMD64_
#if defined(__LP64__) || defined(_WIN64)
++mem; // make sure data is aligned in 64 bit machines
#endif
*mem = curr_end_cls;