mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

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

Browse source
This commit is contained in:
nilsbecker 2019-02-23 12:34:40 +01:00
commit 960708e99e
18 changed files with 1108 additions and 932 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/ast/ast_smt_pp.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include "util/vector.h"
#include "util/smt2_util.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/array_decl_plugin.h"
@ -223,7 +224,7 @@ class smt_printer {
}
}
else if (m_manager.is_ite(d)) {
m_out << "ite";
m_out << "ite";
}
else if (m_manager.is_implies(d)) {
m_out << "=>";
@ -266,7 +267,7 @@ class smt_printer {
else {
m_out << "(_ " << sym << " ";
}
for (unsigned i = 0; i < num_params; ++i) {
parameter const& p = params[i];
if (p.is_ast()) {
@ -320,7 +321,7 @@ class smt_printer {
if (num_sorts > 0) {
m_out << "(";
}
m_out << m_renaming.get_symbol(s->get_name(), false);
m_out << m_renaming.get_symbol(s->get_name(), false);
if (num_sorts > 0) {
for (unsigned i = 0; i < num_sorts; ++i) {
m_out << " ";
@ -388,10 +389,7 @@ class smt_printer {
m_out << "(_ bv" << val << " " << bv_size << ")";
}
else if (m_futil.is_numeral(n, float_val)) {
m_out << "((_ to_fp " <<
float_val.get().get_ebits() << " " <<
float_val.get().get_sbits() << ") RTZ " <<
m_futil.fm().to_string(float_val).c_str() << ")";
m_out << mk_ismt2_pp(n, m_manager);
}
else if (m_bvutil.is_bit2bool(n)) {
unsigned bit = n->get_decl()->get_parameter(0).get_int();
@ -402,7 +400,7 @@ class smt_printer {
else if (m_manager.is_label(n, pos, names) && !names.empty()) {
m_out << "(! ";
pp_marked_expr(n->get_arg(0));
m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")";
m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")";
}
else if (m_manager.is_label_lit(n, names) && !names.empty()) {
m_out << "(! true :lblpos " << m_renaming.get_symbol(names[0], false) << ")";
@ -435,7 +433,7 @@ class smt_printer {
pp_arg(curr, n);
m_out << ")";
}
}
else if (m_manager.is_distinct(decl)) {
ptr_vector<expr> args(num_args, n->get_args());
unsigned idx = 0;
@ -613,7 +611,7 @@ class smt_printer {
pp_id(n);
m_out << " ";
pp_expr(n);
m_out << ")";
m_out << ")";
m_out << ")";
newline();
}
@ -781,7 +779,7 @@ public:
datatype_util util(m_manager);
SASSERT(util.is_datatype(s));
sort_ref_vector ps(m_manager);
sort_ref_vector ps(m_manager);
ptr_vector<datatype::def> defs;
util.get_defs(s, defs);
@ -790,7 +788,7 @@ public:
if (mark.is_marked(sr)) return; // already processed
mark.mark(sr, true);
}
m_out << "(declare-datatypes (";
bool first_def = true;
for (datatype::def* d : defs) {
@ -800,7 +798,7 @@ public:
m_out << ") (";
bool first_sort = true;
for (datatype::def* d : defs) {
if (!first_sort) m_out << "\n "; else first_sort = false;
if (!first_sort) m_out << "\n "; else first_sort = false;
if (!d->params().empty()) {
m_out << "(par (";
bool first_param = true;
@ -814,7 +812,7 @@ public:
bool first_constr = true;
for (datatype::constructor* f : *d) {
if (!first_constr) m_out << " "; else first_constr = false;
m_out << "(";
m_out << "(";
m_out << m_renaming.get_symbol(f->name(), false);
for (datatype::accessor* a : *f) {
m_out << " (" << m_renaming.get_symbol(a->name(), false) << " ";
@ -828,7 +826,7 @@ public:
}
m_out << ")";
}
m_out << "))";
m_out << "))";
newline();
}
@ -864,7 +862,7 @@ public:
}
m_out << ") ";
visit_sort(d->get_range());
m_out << ")";
m_out << ")";
}
void visit_pred(func_decl* d) {

8
src/ast/rewriter/array_rewriter.cpp
View file

@ -375,7 +375,13 @@ br_status array_rewriter::mk_set_intersect(unsigned num_args, expr * const * arg
br_status array_rewriter::mk_set_complement(expr * arg, expr_ref & result) {
return mk_map_core(m().mk_not_decl(), 1, &arg, result);
func_decl* fnot = m().mk_not_decl();
br_status st = mk_map_core(fnot, 1, &arg, result);
if (BR_FAILED == st) {
result = m_util.mk_map(fnot, 1, &arg);
st = BR_DONE;
}
return st;
}
br_status array_rewriter::mk_set_difference(expr * arg1, expr * arg2, expr_ref & result) {

2
src/sat/sat_clause.cpp
View file

@ -38,7 +38,6 @@ namespace sat {
memcpy(m_lits, lits, sizeof(literal) * sz);
mark_strengthened();
SASSERT(check_approx());
SASSERT(sz > 1);
}
var_approx_set clause::approx(unsigned num, literal const * lits) {
@ -83,6 +82,7 @@ namespace sat {
i++;
for (; i < m_size; i++)
m_lits[i-1] = m_lits[i];
m_lits[m_size-1] = l;
m_size--;
mark_strengthened();
}

113
src/sat/sat_drat.cpp
View file

@ -49,10 +49,13 @@ namespace sat {
dealloc(m_bout);
for (unsigned i = 0; i < m_proof.size(); ++i) {
clause* c = m_proof[i];
if (c && (c->size() == 2 || m_status[i] == status::deleted || m_status[i] == status::external)) {
s.dealloc_clause(c);
if (c) {
m_alloc.del_clause(c);
}
}
m_proof.reset();
m_out = nullptr;
m_bout = nullptr;
}
void drat::updt_config() {
@ -75,7 +78,7 @@ namespace sat {
if (st == status::asserted || st == status::external) {
return;
}
char buffer[10000];
char digits[20]; // enough for storing unsigned
char* lastd = digits + sizeof(digits);
@ -166,6 +169,9 @@ namespace sat {
}
void drat::append(literal l, status st) {
TRACE("sat_drat", tout << st << " " << l << "\n";);
declare(l);
IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st););
if (st == status::learned) {
verify(1, &l);
@ -177,13 +183,15 @@ namespace sat {
assign_propagate(l);
}
clause* c = s.alloc_clause(1, &l, st == status::learned);
m_proof.push_back(c);
m_status.push_back(st);
m_units.push_back(l);
}
void drat::append(literal l1, literal l2, status st) {
TRACE("sat_drat", tout << st << " " << l1 << " " << l2 << "\n";);
declare(l1);
declare(l2);
literal lits[2] = { l1, l2 };
IF_VERBOSE(20, trace(verbose_stream(), 2, lits, st););
if (st == status::deleted) {
// noop
@ -193,7 +201,7 @@ namespace sat {
if (st == status::learned) {
verify(2, lits);
}
clause* c = s.alloc_clause(2, lits, st == status::learned);
clause* c = m_alloc.mk_clause(2, lits, st == status::learned);
m_proof.push_back(c);
m_status.push_back(st);
if (!m_check_unsat) return;
@ -214,14 +222,37 @@ namespace sat {
}
}
#if 0
// debugging code
bool drat::is_clause(clause& c, literal l1, literal l2, literal l3, drat::status st1, drat::status st2) {
//if (st1 != st2) return false;
if (c.size() != 3) return false;
if (l1 == c[0]) {
if (l2 == c[1] && l3 == c[2]) return true;
if (l2 == c[2] && l3 == c[1]) return true;
}
if (l2 == c[0]) {
if (l1 == c[1] && l3 == c[2]) return true;
if (l1 == c[2] && l3 == c[1]) return true;
}
if (l3 == c[0]) {
if (l1 == c[1] && l2 == c[2]) return true;
if (l1 == c[2] && l2 == c[1]) return true;
}
return false;
}
#endif
void drat::append(clause& c, status st) {
TRACE("sat_drat", tout << st << " " << c << "\n";);
for (literal lit : c) declare(lit);
unsigned n = c.size();
IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st););
if (st == status::learned) {
verify(c);
}
m_status.push_back(st);
m_proof.push_back(&c);
if (st == status::deleted) {
@ -274,6 +305,7 @@ namespace sat {
}
void drat::declare(literal l) {
if (!m_check) return;
unsigned n = static_cast<unsigned>(l.var());
while (m_assignment.size() <= n) {
m_assignment.push_back(l_undef);
@ -379,7 +411,7 @@ namespace sat {
case l_undef: num_undef++; break;
}
}
CTRACE("sat", num_true == 0 && num_undef == 1, display(tout););
CTRACE("sat_drat", num_true == 0 && num_undef == 1, display(tout););
SASSERT(num_true != 0 || num_undef != 1);
}
}
@ -423,7 +455,7 @@ namespace sat {
exit(0);
UNREACHABLE();
//display(std::cout);
TRACE("sat",
TRACE("sat_drat",
tout << literal_vector(n, c) << "\n";
display(tout);
s.display(tout););
@ -431,16 +463,41 @@ namespace sat {
}
}
bool drat::contains(literal c, justification const& j) {
if (!m_check_sat) {
return true;
}
switch (j.get_kind()) {
case justification::NONE:
return m_units.contains(c);
case justification::BINARY:
return contains(c, j.get_literal());
case justification::TERNARY:
return contains(c, j.get_literal1(), j.get_literal2());
case justification::CLAUSE:
return contains(s.get_clause(j));
default:
return true;
}
}
bool drat::contains(unsigned n, literal const* lits) {
if (!m_check) return true;
unsigned num_add = 0;
unsigned num_del = 0;
for (unsigned i = m_proof.size(); i-- > 0; ) {
clause& c = *m_proof[i];
status st = m_status[i];
if (match(n, lits, c)) {
return st != status::deleted;
if (st == status::deleted) {
num_del++;
}
else {
num_add++;
}
}
}
return false;
return num_add > num_del;
}
bool drat::match(unsigned n, literal const* lits, clause const& c) const {
@ -454,7 +511,9 @@ namespace sat {
break;
}
}
if (!found) return false;
if (!found) {
return false;
}
}
return true;
}
@ -512,7 +571,7 @@ namespace sat {
void drat::assign(literal l) {
lbool new_value = l.sign() ? l_false : l_true;
lbool old_value = value(l);
// TRACE("sat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";);
// TRACE("sat_drat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";);
switch (old_value) {
case l_false:
m_inconsistent = true;
@ -544,7 +603,7 @@ namespace sat {
watched_clause& wc = m_watched_clauses[idx];
clause& c = *wc.m_clause;
//TRACE("sat", tout << "Propagate " << l << " " << c << " watch: " << wc.m_l1 << " " << wc.m_l2 << "\n";);
//TRACE("sat_drat", tout << "Propagate " << l << " " << c << " watch: " << wc.m_l1 << " " << wc.m_l2 << "\n";);
if (wc.m_l1 == ~l) {
std::swap(wc.m_l1, wc.m_l2);
}
@ -596,17 +655,12 @@ namespace sat {
}
}
void drat::add(literal l, bool learned) {
TRACE("sat", tout << "add: " << l << " " << (learned?"l":"t") << "\n";);
declare(l);
status st = get_status(learned);
if (m_out) dump(1, &l, st);
if (m_bout) bdump(1, &l, st);
if (m_check) append(l, st);
}
void drat::add(literal l1, literal l2, bool learned) {
TRACE("sat", tout << "add: " << l1 << " " << l2 << " " << (learned?"l":"t") << "\n";);
declare(l1);
declare(l2);
literal ls[2] = {l1, l2};
status st = get_status(learned);
if (m_out) dump(2, ls, st);
@ -614,12 +668,13 @@ namespace sat {
if (m_check) append(l1, l2, st);
}
void drat::add(clause& c, bool learned) {
TRACE("sat", tout << "add: " << c << "\n";);
for (unsigned i = 0; i < c.size(); ++i) declare(c[i]);
status st = get_status(learned);
if (m_out) dump(c.size(), c.begin(), st);
if (m_bout) bdump(c.size(), c.begin(), st);
if (m_check_unsat) append(c, get_status(learned));
if (m_check) {
clause* cl = m_alloc.mk_clause(c.size(), c.begin(), learned);
append(*cl, get_status(learned));
}
}
void drat::add(literal_vector const& lits, svector<premise> const& premises) {
if (m_check) {
@ -627,7 +682,7 @@ namespace sat {
case 0: add(); break;
case 1: append(lits[0], status::external); break;
default: {
clause* c = s.alloc_clause(lits.size(), lits.c_ptr(), true);
clause* c = m_alloc.mk_clause(lits.size(), lits.c_ptr(), true);
append(*c, status::external);
break;
}
@ -635,16 +690,16 @@ namespace sat {
}
}
void drat::add(literal_vector const& c) {
for (unsigned i = 0; i < c.size(); ++i) declare(c[i]);
if (m_out) dump(c.size(), c.begin(), status::learned);
if (m_bout) bdump(c.size(), c.begin(), status::learned);
if (m_check) {
for (literal lit : c) declare(lit);
switch (c.size()) {
case 0: add(); break;
case 1: append(c[0], status::learned); break;
default: {
verify(c.size(), c.begin());
clause* cl = s.alloc_clause(c.size(), c.c_ptr(), true);
clause* cl = m_alloc.mk_clause(c.size(), c.c_ptr(), true);
append(*cl, status::external);
break;
}
@ -657,8 +712,10 @@ namespace sat {
if (m_bout) bdump(1, &l, status::deleted);
if (m_check_unsat) append(l, status::deleted);
}
void drat::del(literal l1, literal l2) {
literal ls[2] = {l1, l2};
SASSERT(!(l1 == literal(13923, false) && l2 == literal(14020, true)));
if (m_out) dump(2, ls, status::deleted);
if (m_bout) bdump(2, ls, status::deleted);
if (m_check) append(l1, l2, status::deleted);
@ -677,11 +734,11 @@ namespace sat {
}
#endif
TRACE("sat", tout << "del: " << c << "\n";);
//SASSERT(!(c.size() == 2 && c[0] == literal(13923, false) && c[1] == literal(14020, true)));
if (m_out) dump(c.size(), c.begin(), status::deleted);
if (m_bout) bdump(c.size(), c.begin(), status::deleted);
if (m_check) {
clause* c1 = s.alloc_clause(c.size(), c.begin(), c.is_learned());
clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), c.is_learned());
append(*c1, status::deleted);
}
}

4
src/sat/sat_drat.h
View file

@ -45,6 +45,7 @@ namespace sat {
svector<watched_clause> m_watched_clauses;
typedef svector<unsigned> watch;
solver& s;
clause_allocator m_alloc;
std::ostream* m_out;
std::ostream* m_bout;
ptr_vector<clause> m_proof;
@ -61,6 +62,8 @@ namespace sat {
void append(literal l1, literal l2, status st);
void append(clause& c, status st);
bool is_clause(clause& c, literal l1, literal l2, literal l3, status st1, status st2);
friend std::ostream& operator<<(std::ostream & out, status st);
status get_status(bool learned) const;
@ -104,6 +107,7 @@ namespace sat {
bool contains(unsigned n, literal const* c);
bool contains(literal l1, literal l2) { literal lits[2] = {l1, l2}; return contains(2, lits); }
bool contains(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; return contains(3, lits); }
bool contains(literal c, justification const& j);
void check_model(model const& m);
};

2
src/sat/sat_elim_eqs.cpp
View file

@ -207,7 +207,7 @@ namespace sat {
c.update_approx();
}
if (m_solver.m_config.m_drat) {
m_solver.m_drat.add(c, true);
m_solver.m_drat.add(c, true);
drat_delete_clause();
}

3
src/sat/sat_probing.cpp
View file

@ -52,6 +52,9 @@ namespace sat {
unsigned tr_sz = s.m_trail.size();
for (unsigned i = old_tr_sz; i < tr_sz; i++) {
entry.m_lits.push_back(s.m_trail[i]);
if (s.m_config.m_drat) {
s.m_drat.add(~l, s.m_trail[i], true);
}
}
}

24
src/sat/sat_simplifier.cpp
View file

@ -124,9 +124,9 @@ namespace sat {
}
}
inline void simplifier::remove_clause(clause & c) {
inline void simplifier::remove_clause(clause & c, bool is_unique) {
if (!c.was_removed()) {
if (s.m_config.m_drat) {
if (s.m_config.m_drat && is_unique) {
s.m_drat.del(c);
}
for (literal l : c) {
@ -477,7 +477,7 @@ namespace sat {
s.set_learned(c1, false);
}
TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
remove_clause(c2);
remove_clause(c2, false);
m_num_subsumed++;
}
else if (!c2.was_removed()) {
@ -577,7 +577,7 @@ namespace sat {
if (c1.is_learned() && !c2.is_learned())
s.set_learned(c1, false);
TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
remove_clause(c2);
remove_clause(c2, false);
m_num_subsumed++;
}
}
@ -662,7 +662,7 @@ namespace sat {
for (auto it = cs.mk_iterator(); !it.at_end(); ) {
clause & c = it.curr();
it.next();
remove_clause(c);
remove_clause(c, true);
}
cs.reset();
}
@ -674,10 +674,12 @@ namespace sat {
m_num_elim_lits++;
insert_elim_todo(l.var());
if (s.m_config.m_drat && c.contains(l)) {
m_dummy.set(c.size(), c.begin(), c.is_learned());
unsigned sz = c.size();
c.elim(l);
s.m_drat.add(c, true);
s.m_drat.del(*m_dummy.get());
c.restore(sz);
s.m_drat.del(c);
c.shrink(sz-1);
}
else {
c.elim(l);
@ -690,7 +692,7 @@ namespace sat {
if (cleanup_clause(c)) {
// clause was satisfied
TRACE("elim_lit", tout << "clause was satisfied\n";);
remove_clause(c);
remove_clause(c, true);
return;
}
unsigned sz = c.size();
@ -710,7 +712,7 @@ namespace sat {
c.restore(sz0);
s.mk_bin_clause(c[0], c[1], c.is_learned());
m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));
remove_clause(c);
remove_clause(c, sz0 != sz);
break;
default:
if (s.m_config.m_drat && sz0 != sz) {
@ -888,7 +890,7 @@ namespace sat {
if (s.m_trail.size() > m_last_sub_trail_sz) {
unsigned sz0 = c.size();
if (cleanup_clause(c)) {
remove_clause(c);
remove_clause(c, true);
continue;
}
unsigned sz = c.size();
@ -906,7 +908,7 @@ namespace sat {
s.mk_bin_clause(c[0], c[1], c.is_learned());
m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));
c.restore(sz0);
remove_clause(c);
remove_clause(c, sz != sz0);
continue;
default:
if (s.m_config.m_drat && sz != sz0) {

2
src/sat/sat_simplifier.h
View file

@ -133,7 +133,7 @@ namespace sat {
void register_clauses(clause_vector & cs);
void remove_clause(clause & c);
void remove_clause(clause & c, bool is_unique);
void set_learned(clause & c);
void set_learned(literal l1, literal l2);

67
src/sat/sat_solver.cpp
View file

@ -36,19 +36,20 @@ Revision History:
namespace sat {
solver::solver(params_ref const & p, reslimit& l):
solver_core(l),
m_checkpoint_enabled(true),
m_config(p),
m_par(nullptr),
m_cls_allocator_idx(false),
m_drat(*this),
m_cleaner(*this),
m_simplifier(*this, p),
m_scc(*this, p),
m_asymm_branch(*this, p),
m_probing(*this, p),
m_mus(*this),
m_drat(*this),
m_inconsistent(false),
m_searching(false),
m_num_frozen(0),
@ -416,8 +417,6 @@ namespace sat {
clause * r = alloc_clause(3, lits, learned);
bool reinit = attach_ter_clause(*r);
if (reinit && !learned) push_reinit_stack(*r);
if (m_config.m_drat) m_drat.add(*r, learned);
if (learned)
m_learned.push_back(r);
else
@ -427,6 +426,9 @@ namespace sat {
bool solver::attach_ter_clause(clause & c) {
bool reinit = false;
if (m_config.m_drat) m_drat.add(c, c.is_learned());
TRACE("sat", tout << c << "\n";);
SASSERT(!c.was_removed());
m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
@ -462,8 +464,9 @@ namespace sat {
else {
m_clauses.push_back(r);
}
if (m_config.m_drat)
if (m_config.m_drat) {
m_drat.add(*r, learned);
}
return r;
}
@ -2166,6 +2169,36 @@ namespace sat {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";);
}
bool solver::can_delete3(literal l1, literal l2, literal l3) const {
if (value(l1) == l_true &&
value(l2) == l_false &&
value(l3) == l_false) {
justification const& j = m_justification[l1.var()];
if (j.is_ternary_clause()) {
watched w1(l2, l3);
watched w2(j.get_literal1(), j.get_literal2());
return w1 != w2;
}
}
return true;
}
bool solver::can_delete(clause const & c) const {
if (c.on_reinit_stack())
return false;
if (c.size() == 3) {
return
can_delete3(c[0],c[1],c[2]) &&
can_delete3(c[1],c[0],c[2]) &&
can_delete3(c[2],c[0],c[1]);
}
literal l0 = c[0];
if (value(l0) != l_true)
return true;
justification const & jst = m_justification[l0.var()];
return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c;
}
/**
\brief Use gc based on dynamic psm. Clauses are initially frozen.
*/
@ -2384,6 +2417,7 @@ namespace sat {
}
}
m_lemma.reset();
unsigned idx = skip_literals_above_conflict_level();
@ -2404,6 +2438,7 @@ namespace sat {
do {
TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n";
tout << "num_marks: " << num_marks << ", js: " << js << "\n";);
switch (js.get_kind()) {
case justification::NONE:
break;
@ -2458,6 +2493,8 @@ namespace sat {
idx--;
num_marks--;
reset_mark(c_var);
TRACE("sat", display_justification(tout << consequent << " ", js) << "\n";);
}
while (num_marks > 0);
@ -2470,12 +2507,13 @@ namespace sat {
TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
unsigned new_scope_lvl = 0;
bool sub_min = false, res_min = false;
if (!m_lemma.empty()) {
if (m_config.m_minimize_lemmas) {
minimize_lemma();
res_min = minimize_lemma();
reset_lemma_var_marks();
if (m_config.m_dyn_sub_res)
dyn_sub_res();
sub_min = dyn_sub_res();
TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
}
else
@ -2495,12 +2533,12 @@ namespace sat {
m_slow_glue_avg.update(glue);
pop_reinit(m_scope_lvl - new_scope_lvl);
TRACE("sat_conflict_detail", tout << glue << " " << new_scope_lvl << "\n";);
// unsound: m_asymm_branch.minimize(m_scc, m_lemma);
clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true);
if (lemma) {
lemma->set_glue(glue);
if (m_par) m_par->share_clause(*this, *lemma);
}
TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n";);
decay_activity();
updt_phase_counters();
@ -2847,7 +2885,7 @@ namespace sat {
if (m_lvl_set.may_contain(var_lvl)) {
mark(var);
m_unmark.push_back(var);
m_lemma_min_stack.push_back(var);
m_lemma_min_stack.push_back(antecedent);
}
else {
return false;
@ -2865,11 +2903,12 @@ namespace sat {
*/
bool solver::implied_by_marked(literal lit) {
m_lemma_min_stack.reset(); // avoid recursive function
m_lemma_min_stack.push_back(lit.var());
m_lemma_min_stack.push_back(lit);
unsigned old_size = m_unmark.size();
while (!m_lemma_min_stack.empty()) {
bool_var var = m_lemma_min_stack.back();
lit = m_lemma_min_stack.back();
bool_var var = lit.var();
m_lemma_min_stack.pop_back();
justification const& js = m_justification[var];
switch(js.get_kind()) {
@ -2931,6 +2970,8 @@ namespace sat {
UNREACHABLE();
break;
}
TRACE("sat_conflict",
display_justification(tout << var << " ",js) << "\n";);
}
return true;
}
@ -2961,7 +3002,7 @@ namespace sat {
literals that are implied by other literals in m_lemma and/or literals
assigned at level 0.
*/
void solver::minimize_lemma() {
bool solver::minimize_lemma() {
SASSERT(!m_lemma.empty());
SASSERT(m_unmark.empty());
updt_lemma_lvl_set();
@ -2985,6 +3026,7 @@ namespace sat {
reset_unmark(0);
m_lemma.shrink(j);
m_stats.m_minimized_lits += sz - j;
return j < sz;
}
/**
@ -3058,7 +3100,7 @@ namespace sat {
\brief Apply dynamic subsumption resolution to new lemma.
Only binary and ternary clauses are used.
*/
void solver::dyn_sub_res() {
bool solver::dyn_sub_res() {
unsigned sz = m_lemma.size();
for (unsigned i = 0; i < sz; i++) {
mark_lit(m_lemma[i]);
@ -3171,6 +3213,7 @@ namespace sat {
SASSERT(j >= 1);
m_lemma.shrink(j);
return j < sz;
}

23
src/sat/sat_solver.h
View file

@ -85,9 +85,10 @@ namespace sat {
stats m_stats;
scoped_ptr<extension> m_ext;
parallel* m_par;
random_gen m_rand;
drat m_drat; // DRAT for generating proofs
clause_allocator m_cls_allocator[2];
bool m_cls_allocator_idx;
random_gen m_rand;
cleaner m_cleaner;
model m_model;
model_converter m_mc;
@ -97,7 +98,6 @@ namespace sat {
asymm_branch m_asymm_branch;
probing m_probing;
mus m_mus; // MUS for minimal core extraction
drat m_drat; // DRAT for generating proofs
bool m_inconsistent;
bool m_searching;
// A conflict is usually a single justification. That is, a justification
@ -461,17 +461,8 @@ namespace sat {
void gc_dyn_psm();
bool activate_frozen_clause(clause & c);
unsigned psm(clause const & c) const;
bool can_delete(clause const & c) const {
if (c.on_reinit_stack())
return false;
if (c.size() == 3)
return true; // not needed to justify anything.
literal l0 = c[0];
if (value(l0) != l_true)
return true;
justification const & jst = m_justification[l0.var()];
return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c;
}
bool can_delete(clause const & c) const;
bool can_delete3(literal l1, literal l2, literal l3) const;
clause& get_clause(watch_list::iterator it) const {
SASSERT(it->get_kind() == watched::CLAUSE);
@ -522,14 +513,14 @@ namespace sat {
typedef approx_set_tpl<unsigned, u2u, unsigned> level_approx_set;
bool_var_vector m_unmark;
level_approx_set m_lvl_set;
bool_var_vector m_lemma_min_stack;
literal_vector m_lemma_min_stack;
bool process_antecedent_for_minimization(literal antecedent);
bool implied_by_marked(literal lit);
void reset_unmark(unsigned old_size);
void updt_lemma_lvl_set();
void minimize_lemma();
void reset_lemma_var_marks();
void dyn_sub_res();
bool minimize_lemma();
bool dyn_sub_res();
// -----------------------
//

10
src/sat/sat_watched.cpp
View file

@ -86,7 +86,15 @@ namespace sat {
}
}
wlist.set_end(it2);
//VERIFY(found);
#if 0
VERIFY(found);
for (watched const& w2 : wlist) {
if (w2 == w) {
std::cout << l1 << " " << l2 << "\n";
}
//VERIFY(w2 != w);
}
#endif
}
void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {

1
src/sat/tactic/sat_tactic.cpp
View file

@ -200,6 +200,7 @@ public:
throw tactic_exception(ex.msg());
}
catch (z3_exception& ex) {
(void)ex;
TRACE("sat", tout << ex.msg() << "\n";);
throw;
}

258
src/util/buffer.h
View file

@ -1,268 +1,30 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Copyright (c) 2019 Microsoft Corporation
Module Name:
buffer.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2006-10-16.
Revision History:
Daniel Schemmel 2019-2-23
--*/
#ifndef BUFFER_H_
#define BUFFER_H_
#include<string.h>
#include "util/memory_manager.h"
#include "old_buffer.h"
template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
class buffer {
protected:
T * m_buffer;
unsigned m_pos;
unsigned m_capacity;
char m_initial_buffer[INITIAL_SIZE * sizeof(T)];
void free_memory() {
if (m_buffer != reinterpret_cast<T*>(m_initial_buffer)) {
dealloc_svect(m_buffer);
}
}
using buffer = old_buffer<T, CallDestructors, INITIAL_SIZE>;
void expand() {
unsigned new_capacity = m_capacity << 1;
T * new_buffer = reinterpret_cast<T*>(memory::allocate(sizeof(T) * new_capacity));
memcpy(new_buffer, m_buffer, m_pos * sizeof(T));
free_memory();
m_buffer = new_buffer;
m_capacity = new_capacity;
}
void destroy_elements() {
iterator it = begin();
iterator e = end();
for (; it != e; ++it) {
it->~T();
}
}
void destroy() {
if (CallDestructors) {
destroy_elements();
}
free_memory();
}
public:
typedef T data;
typedef T * iterator;
typedef const T * const_iterator;
buffer():
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0),
m_capacity(INITIAL_SIZE) {
}
buffer(const buffer & source):
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0),
m_capacity(INITIAL_SIZE) {
unsigned sz = source.size();
for(unsigned i = 0; i < sz; i++) {
push_back(source.m_buffer[i]);
}
}
buffer(unsigned sz, const T & elem):
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0),
m_capacity(INITIAL_SIZE) {
for (unsigned i = 0; i < sz; i++) {
push_back(elem);
}
SASSERT(size() == sz);
}
~buffer() {
destroy();
}
void reset() {
if (CallDestructors) {
destroy_elements();
}
m_pos = 0;
}
void finalize() {
destroy();
m_buffer = reinterpret_cast<T *>(m_initial_buffer);
m_pos = 0;
m_capacity = INITIAL_SIZE;
}
unsigned size() const {
return m_pos;
}
bool empty() const {
return m_pos == 0;
}
iterator begin() {
return m_buffer;
}
iterator end() {
return m_buffer + size();
}
void set_end(iterator it) {
m_pos = static_cast<unsigned>(it - m_buffer);
if (CallDestructors) {
iterator e = end();
for (; it != e; ++it) {
it->~T();
}
}
}
const_iterator begin() const {
return m_buffer;
}
const_iterator end() const {
return m_buffer + size();
}
void push_back(const T & elem) {
if (m_pos >= m_capacity)
expand();
new (m_buffer + m_pos) T(elem);
m_pos++;
}
void push_back(T && elem) {
if (m_pos >= m_capacity)
expand();
new (m_buffer + m_pos) T(std::move(elem));
m_pos++;
}
void pop_back() {
if (CallDestructors) {
back().~T();
}
m_pos--;
}
const T & back() const {
SASSERT(!empty());
SASSERT(m_pos > 0);
return m_buffer[m_pos - 1];
}
T & back() {
SASSERT(!empty());
SASSERT(m_pos > 0);
return m_buffer[m_pos - 1];
}
T * c_ptr() const {
return m_buffer;
}
void append(unsigned n, T const * elems) {
for (unsigned i = 0; i < n; i++) {
push_back(elems[i]);
}
}
void append(const buffer& source) {
append(source.size(), source.c_ptr());
}
T & operator[](unsigned idx) {
SASSERT(idx < size());
return m_buffer[idx];
}
const T & operator[](unsigned idx) const {
SASSERT(idx < size());
return m_buffer[idx];
}
T & get(unsigned idx) {
SASSERT(idx < size());
return m_buffer[idx];
}
const T & get(unsigned idx) const {
SASSERT(idx < size());
return m_buffer[idx];
}
void set(unsigned idx, T const & val) {
SASSERT(idx < size());
m_buffer[idx] = val;
}
void resize(unsigned nsz, const T & elem=T()) {
unsigned sz = size();
if (nsz > sz) {
for (unsigned i = sz; i < nsz; i++) {
push_back(elem);
}
}
else if (nsz < sz) {
for (unsigned i = nsz; i < sz; i++) {
pop_back();
}
}
SASSERT(size() == nsz);
}
void shrink(unsigned nsz) {
unsigned sz = size();
SASSERT(nsz <= sz);
for (unsigned i = nsz; i < sz; i++)
pop_back();
SASSERT(size() == nsz);
}
buffer & operator=(buffer const & other) {
if (this == &other)
return *this;
reset();
append(other);
return *this;
}
};
// note that the append added in the old_ptr_buffer is actually not an addition over its base class old_buffer,
// which already has an append function with the same signature and implementation
template<typename T, unsigned INITIAL_SIZE=16>
using ptr_buffer = old_ptr_buffer<T, INITIAL_SIZE>;
template<typename T, unsigned INITIAL_SIZE=16>
class ptr_buffer : public buffer<T *, false, INITIAL_SIZE> {
public:
void append(unsigned n, T * const * elems) {
for (unsigned i = 0; i < n; i++) {
this->push_back(elems[i]);
}
}
};
template<typename T, unsigned INITIAL_SIZE=16>
class sbuffer : public buffer<T, false, INITIAL_SIZE> {
public:
sbuffer(): buffer<T, false, INITIAL_SIZE>() {}
sbuffer(unsigned sz, const T& elem) : buffer<T, false, INITIAL_SIZE>(sz,elem) {}
};
using sbuffer = old_sbuffer<T, INITIAL_SIZE>;
#endif /* BUFFER_H_ */

2
src/util/lp/dense_matrix.cpp
View file

@ -35,6 +35,6 @@ template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::dense_matrix(uns
template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >& lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::operator=(lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const&);
template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> > lp::operator*<lp::mpq, lp::numeric_pair<lp::mpq> >(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&, lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
template void lp::dense_matrix<lp::mpq, lp::numeric_pair< lp::mpq> >::apply_from_right( vector< lp::mpq> &);
template void lp::dense_matrix<double,double>::apply_from_right(class vector<double> &);
template void lp::dense_matrix<double,double>::apply_from_right(vector<double> &);
template void lp::dense_matrix<lp::mpq, lp::mpq>::apply_from_left(vector<lp::mpq>&);
#endif

270
src/util/old_buffer.h Normal file
View file

@ -0,0 +1,270 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
old_buffer.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2006-10-16.
Revision History:
2019-2-23 Renamed to old_buffer from buffer to provide new implementation
--*/
#ifndef OLD_BUFFER_H_
#define OLD_BUFFER_H_
#include<string.h>
#include "util/memory_manager.h"
template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
class old_buffer {
protected:
T * m_buffer;
unsigned m_pos;
unsigned m_capacity;
char m_initial_buffer[INITIAL_SIZE * sizeof(T)];
void free_memory() {
if (m_buffer != reinterpret_cast<T*>(m_initial_buffer)) {
dealloc_svect(m_buffer);
}
}
void expand() {
unsigned new_capacity = m_capacity << 1;
T * new_buffer = reinterpret_cast<T*>(memory::allocate(sizeof(T) * new_capacity));
memcpy(new_buffer, m_buffer, m_pos * sizeof(T));
free_memory();
m_buffer = new_buffer;
m_capacity = new_capacity;
}
void destroy_elements() {
iterator it = begin();
iterator e = end();
for (; it != e; ++it) {
it->~T();
}
}
void destroy() {
if (CallDestructors) {
destroy_elements();
}
free_memory();
}
public:
typedef T data;
typedef T * iterator;
typedef const T * const_iterator;
old_buffer():
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0),
m_capacity(INITIAL_SIZE) {
}
old_buffer(const old_buffer & source):
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0),
m_capacity(INITIAL_SIZE) {
unsigned sz = source.size();
for(unsigned i = 0; i < sz; i++) {
push_back(source.m_buffer[i]);
}
}
old_buffer(unsigned sz, const T & elem):
m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0),
m_capacity(INITIAL_SIZE) {
for (unsigned i = 0; i < sz; i++) {
push_back(elem);
}
SASSERT(size() == sz);
}
~old_buffer() {
destroy();
}
void reset() {
if (CallDestructors) {
destroy_elements();
}
m_pos = 0;
}
void finalize() {
destroy();
m_buffer = reinterpret_cast<T *>(m_initial_buffer);
m_pos = 0;
m_capacity = INITIAL_SIZE;
}
unsigned size() const {
return m_pos;
}
bool empty() const {
return m_pos == 0;
}
iterator begin() {
return m_buffer;
}
iterator end() {
return m_buffer + size();
}
void set_end(iterator it) {
m_pos = static_cast<unsigned>(it - m_buffer);
if (CallDestructors) {
iterator e = end();
for (; it != e; ++it) {
it->~T();
}
}
}
const_iterator begin() const {
return m_buffer;
}
const_iterator end() const {
return m_buffer + size();
}
void push_back(const T & elem) {
if (m_pos >= m_capacity)
expand();
new (m_buffer + m_pos) T(elem);
m_pos++;
}
void push_back(T && elem) {
if (m_pos >= m_capacity)
expand();
new (m_buffer + m_pos) T(std::move(elem));
m_pos++;
}
void pop_back() {
if (CallDestructors) {
back().~T();
}
m_pos--;
}
const T & back() const {
SASSERT(!empty());
SASSERT(m_pos > 0);
return m_buffer[m_pos - 1];
}
T & back() {
SASSERT(!empty());
SASSERT(m_pos > 0);
return m_buffer[m_pos - 1];
}
T * c_ptr() const {
return m_buffer;
}
void append(unsigned n, T const * elems) {
for (unsigned i = 0; i < n; i++) {
push_back(elems[i]);
}
}
void append(const old_buffer& source) {
append(source.size(), source.c_ptr());
}
T & operator[](unsigned idx) {
SASSERT(idx < size());
return m_buffer[idx];
}
const T & operator[](unsigned idx) const {
SASSERT(idx < size());
return m_buffer[idx];
}
T & get(unsigned idx) {
SASSERT(idx < size());
return m_buffer[idx];
}
const T & get(unsigned idx) const {
SASSERT(idx < size());
return m_buffer[idx];
}
void set(unsigned idx, T const & val) {
SASSERT(idx < size());
m_buffer[idx] = val;
}
void resize(unsigned nsz, const T & elem=T()) {
unsigned sz = size();
if (nsz > sz) {
for (unsigned i = sz; i < nsz; i++) {
push_back(elem);
}
}
else if (nsz < sz) {
for (unsigned i = nsz; i < sz; i++) {
pop_back();
}
}
SASSERT(size() == nsz);
}
void shrink(unsigned nsz) {
unsigned sz = size();
SASSERT(nsz <= sz);
for (unsigned i = nsz; i < sz; i++)
pop_back();
SASSERT(size() == nsz);
}
old_buffer & operator=(old_buffer const & other) {
if (this == &other)
return *this;
reset();
append(other);
return *this;
}
};
template<typename T, unsigned INITIAL_SIZE=16>
class old_ptr_buffer : public old_buffer<T *, false, INITIAL_SIZE> {
public:
void append(unsigned n, T * const * elems) {
for (unsigned i = 0; i < n; i++) {
this->push_back(elems[i]);
}
}
};
template<typename T, unsigned INITIAL_SIZE=16>
class old_sbuffer : public old_buffer<T, false, INITIAL_SIZE> {
public:
old_sbuffer(): old_buffer<T, false, INITIAL_SIZE>() {}
old_sbuffer(unsigned sz, const T& elem) : old_buffer<T, false, INITIAL_SIZE>(sz,elem) {}
};
#endif /* OLD_BUFFER_H_ */

611
src/util/old_vector.h Normal file
View file

@ -0,0 +1,611 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
old_vector.h
Abstract:
Dynamic array implementation.
Remarks:
- Empty arrays consume only sizeof(T *) bytes.
- There is the option of disabling the destructor invocation for elements stored in the vector.
This is useful for vectors of int.
Author:
Leonardo de Moura (leonardo) 2006-09-11.
Revision History:
2019-2-23 Renamed from vector to old_vector to provide new implementation
--*/
#ifndef OLD_VECTOR_H_
#define OLD_VECTOR_H_
#include "util/debug.h"
#include<algorithm>
#include<type_traits>
#include<memory.h>
#include<functional>
#include "util/memory_manager.h"
#include "util/hash.h"
#include "util/z3_exception.h"
// disable warning for constant 'if' expressions.
// these are used heavily in templates.
#ifdef _MSC_VER
#pragma warning(disable:4127)
#endif
template<typename T, bool CallDestructors=true, typename SZ = unsigned>
class old_vector {
#define SIZE_IDX -1
#define CAPACITY_IDX -2
T * m_data;
void destroy_elements() {
iterator it = begin();
iterator e = end();
for (; it != e; ++it) {
it->~T();
}
}
void free_memory() {
memory::deallocate(reinterpret_cast<char*>(reinterpret_cast<SZ*>(m_data) - 2));
}
void expand_vector() {
if (m_data == nullptr) {
SZ capacity = 2;
SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
*mem = capacity;
mem++;
*mem = 0;
mem++;
m_data = reinterpret_cast<T *>(mem);
}
else {
SASSERT(capacity() > 0);
SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
SZ new_capacity = (3 * old_capacity + 1) >> 1;
SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
throw default_exception("Overflow encountered when expanding old_vector");
}
SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5
if (__has_trivial_copy(T)) {
#else
if (std::is_trivially_copyable<T>::value) {
#endif
mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
m_data = reinterpret_cast<T *>(mem + 2);
} else {
mem = (SZ*)memory::allocate(new_capacity_T);
auto old_data = m_data;
auto old_size = size();
mem[1] = old_size;
m_data = reinterpret_cast<T *>(mem + 2);
for (unsigned i = 0; i < old_size; ++i) {
new (&m_data[i]) T(std::move(old_data[i]));
old_data[i].~T();
}
memory::deallocate(old_mem);
}
*mem = new_capacity;
}
}
void copy_core(old_vector const & source) {
SZ size = source.size();
SZ capacity = source.capacity();
SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
*mem = capacity;
mem++;
*mem = size;
mem++;
m_data = reinterpret_cast<T *>(mem);
const_iterator it = source.begin();
iterator it2 = begin();
SASSERT(it2 == m_data);
const_iterator e = source.end();
for (; it != e; ++it, ++it2) {
new (it2) T(*it);
}
}
void destroy() {
if (m_data) {
if (CallDestructors) {
destroy_elements();
}
free_memory();
}
}
public:
typedef T data;
typedef T * iterator;
typedef const T * const_iterator;
old_vector():
m_data(nullptr) {
}
old_vector(SZ s) {
if (s == 0) {
m_data = nullptr;
return;
}
SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2));
*mem = s;
mem++;
*mem = s;
mem++;
m_data = reinterpret_cast<T *>(mem);
// initialize elements
iterator it = begin();
iterator e = end();
for (; it != e; ++it) {
new (it) T();
}
}
old_vector(SZ s, T const & elem):
m_data(nullptr) {
resize(s, elem);
}
old_vector(old_vector const & source):
m_data(nullptr) {
if (source.m_data) {
copy_core(source);
}
SASSERT(size() == source.size());
}
old_vector(old_vector&& other) : m_data(nullptr) {
std::swap(m_data, other.m_data);
}
old_vector(SZ s, T const * data):
m_data(nullptr) {
for (SZ i = 0; i < s; i++) {
push_back(data[i]);
}
}
~old_vector() {
destroy();
}
void finalize() {
destroy();
m_data = nullptr;
}
bool operator==(old_vector const & other) const {
if (this == &other) {
return true;
}
if (size() != other.size())
return false;
for (unsigned i = 0; i < size(); i++) {
if ((*this)[i] != other[i])
return false;
}
return true;
}
bool operator!=(old_vector const & other) const {
return !(*this == other);
}
old_vector & operator=(old_vector const & source) {
if (this == &source) {
return *this;
}
destroy();
if (source.m_data) {
copy_core(source);
}
else {
m_data = nullptr;
}
return *this;
}
old_vector & operator=(old_vector && source) {
if (this == &source) {
return *this;
}
destroy();
m_data = nullptr;
std::swap(m_data, source.m_data);
return *this;
}
bool containsp(std::function<bool(T)>& predicate) const {
for (auto const& t : *this)
if (predicate(t))
return true;
return false;
}
/**
* retain elements that satisfy predicate. aka 'where'.
*/
old_vector filter_pure(std::function<bool(T)>& predicate) const {
old_vector result;
for (auto& t : *this)
if (predicate(t))
result.push_back(t);
return result;
}
old_vector& filter_update(std::function<bool(T)>& predicate) {
unsigned j = 0;
for (auto& t : *this)
if (predicate(t))
set(j++, t);
shrink(j);
return *this;
}
/**
* update elements using f, aka 'select'
*/
template <typename S>
old_vector<S> map_pure(std::function<S(T)>& f) const {
old_vector<S> result;
for (auto& t : *this)
result.push_back(f(t));
return result;
}
old_vector& map_update(std::function<T(T)>& f) {
unsigned j = 0;
for (auto& t : *this)
set(j++, f(t));
return *this;
}
void reset() {
if (m_data) {
if (CallDestructors) {
destroy_elements();
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = 0;
}
}
void clear() { reset(); }
bool empty() const {
return m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == 0;
}
SZ size() const {
if (m_data == nullptr) {
return 0;
}
return reinterpret_cast<SZ *>(m_data)[SIZE_IDX];
}
SZ capacity() const {
if (m_data == nullptr) {
return 0;
}
return reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
}
iterator begin() {
return m_data;
}
iterator end() {
return m_data + size();
}
const_iterator begin() const {
return m_data;
}
const_iterator end() const {
return m_data + size();
}
class reverse_iterator {
T* v;
public:
reverse_iterator(T* v):v(v) {}
T operator*() { return *v; }
reverse_iterator operator++(int) {
reverse_iterator tmp = *this;
--v;
return tmp;
}
reverse_iterator& operator++() {
--v;
return *this;
}
bool operator==(reverse_iterator const& other) const {
return other.v == v;
}
bool operator!=(reverse_iterator const& other) const {
return other.v != v;
}
};
reverse_iterator rbegin() { return reverse_iterator(end() - 1); }
reverse_iterator rend() { return reverse_iterator(begin() - 1); }
void set_end(iterator it) {
if (m_data) {
SZ new_sz = static_cast<SZ>(it - m_data);
if (CallDestructors) {
iterator e = end();
for(; it != e; ++it) {
it->~T();
}
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = new_sz;
}
else {
SASSERT(it == 0);
}
}
T & operator[](SZ idx) {
SASSERT(idx < size());
return m_data[idx];
}
T const & operator[](SZ idx) const {
SASSERT(idx < size());
return m_data[idx];
}
T & get(SZ idx) {
SASSERT(idx < size());
return m_data[idx];
}
T const & get(SZ idx) const {
SASSERT(idx < size());
return m_data[idx];
}
void set(SZ idx, T const & val) {
SASSERT(idx < size());
m_data[idx] = val;
}
void set(SZ idx, T && val) {
SASSERT(idx < size());
m_data[idx] = std::move(val);
}
T & back() {
SASSERT(!empty());
return operator[](size() - 1);
}
T const & back() const {
SASSERT(!empty());
return operator[](size() - 1);
}
void pop_back() {
SASSERT(!empty());
if (CallDestructors) {
back().~T();
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
}
void push_back(T const & elem) {
if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
expand_vector();
}
new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(elem);
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
}
void push_back(T && elem) {
if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
expand_vector();
}
new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(std::move(elem));
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
}
void insert(T const & elem) {
push_back(elem);
}
void erase(iterator pos) {
SASSERT(pos >= begin() && pos < end());
iterator prev = pos;
++pos;
iterator e = end();
for(; pos != e; ++pos, ++prev) {
*prev = *pos;
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
}
void erase(T const & elem) {
iterator it = std::find(begin(), end(), elem);
if (it != end()) {
erase(it);
}
}
void shrink(SZ s) {
if (m_data) {
SASSERT(s <= reinterpret_cast<SZ *>(m_data)[SIZE_IDX]);
if (CallDestructors) {
iterator it = m_data + s;
iterator e = end();
for(; it != e; ++it) {
it->~T();
}
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
}
else {
SASSERT(s == 0);
}
}
template<typename Args>
void resize(SZ s, Args args...) {
SZ sz = size();
if (s <= sz) { shrink(s); return; }
while (s > capacity()) {
expand_vector();
}
SASSERT(m_data != 0);
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
iterator it = m_data + sz;
iterator end = m_data + s;
for (; it != end; ++it) {
new (it) T(std::forward<Args>(args));
}
}
void resize(SZ s) {
SZ sz = size();
if (s <= sz) { shrink(s); return; }
while (s > capacity()) {
expand_vector();
}
SASSERT(m_data != 0);
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
iterator it = m_data + sz;
iterator end = m_data + s;
for (; it != end; ++it) {
new (it) T();
}
}
void append(old_vector<T, CallDestructors> const & other) {
for(SZ i = 0; i < other.size(); ++i) {
push_back(other[i]);
}
}
void append(SZ sz, T const * data) {
for(SZ i = 0; i < sz; ++i) {
push_back(data[i]);
}
}
T * c_ptr() const {
return m_data;
}
void swap(old_vector & other) {
std::swap(m_data, other.m_data);
}
void reverse() {
SZ sz = size();
for (SZ i = 0; i < sz/2; ++i) {
std::swap(m_data[i], m_data[sz-i-1]);
}
}
void fill(T const & elem) {
iterator i = begin();
iterator e = end();
for (; i != e; ++i) {
*i = elem;
}
}
void fill(unsigned sz, T const & elem) {
resize(sz);
fill(elem);
}
bool contains(T const & elem) const {
const_iterator it = begin();
const_iterator e = end();
for (; it != e; ++it) {
if (*it == elem) {
return true;
}
}
return false;
}
// set pos idx with elem. If idx >= size, then expand using default.
void setx(SZ idx, T const & elem, T const & d) {
if (idx >= size()) {
resize(idx+1, d);
}
m_data[idx] = elem;
}
// return element at position idx, if idx >= size, then return default
T const & get(SZ idx, T const & d) const {
if (idx >= size()) {
return d;
}
return m_data[idx];
}
void reserve(SZ s, T const & d) {
if (s > size())
resize(s, d);
}
void reserve(SZ s) {
if (s > size())
resize(s);
}
};
template<typename T>
class old_ptr_vector : public old_vector<T *, false> {
public:
old_ptr_vector():old_vector<T *, false>() {}
old_ptr_vector(unsigned s):old_vector<T *, false>(s) {}
old_ptr_vector(unsigned s, T * elem):old_vector<T *, false>(s, elem) {}
old_ptr_vector(old_ptr_vector const & source):old_vector<T *, false>(source) {}
old_ptr_vector(old_ptr_vector && other) : old_vector<T*, false>(std::move(other)) {}
old_ptr_vector(unsigned s, T * const * data):old_vector<T *, false>(s, const_cast<T**>(data)) {}
old_ptr_vector & operator=(old_ptr_vector const & source) {
old_vector<T *, false>::operator=(source);
return *this;
}
};
template<typename T, typename SZ = unsigned>
class old_svector : public old_vector<T, false, SZ> {
public:
old_svector():old_vector<T, false, SZ>() {}
old_svector(SZ s):old_vector<T, false, SZ>(s) {}
old_svector(SZ s, T const & elem):old_vector<T, false, SZ>(s, elem) {}
old_svector(old_svector const & source):old_vector<T, false, SZ>(source) {}
old_svector(old_svector && other) : old_vector<T, false, SZ>(std::move(other)) {}
old_svector(SZ s, T const * data):old_vector<T, false, SZ>(s, data) {}
old_svector & operator=(old_svector const & source) {
old_vector<T, false, SZ>::operator=(source);
return *this;
}
};
#endif /* OLD_VECTOR_H_ */

610
src/util/vector.h
View file

@ -1,616 +1,36 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Copyright (c) 2019 Microsoft Corporation
Module Name:
vector.h
Abstract:
Dynamic array implementation.
Remarks:
- Empty arrays consume only sizeof(T *) bytes.
- There is the option of disabling the destructor invocation for elements stored in the vector.
This is useful for vectors of int.
Author:
Leonardo de Moura (leonardo) 2006-09-11.
Revision History:
Daniel Schemmel 2019-2-23
--*/
#ifndef VECTOR_H_
#define VECTOR_H_
#include "util/debug.h"
#include<algorithm>
#include<type_traits>
#include<memory.h>
#include<functional>
#include "util/memory_manager.h"
#include "util/hash.h"
#include "util/z3_exception.h"
// disable warning for constant 'if' expressions.
// these are used heavily in templates.
#ifdef _MSC_VER
#pragma warning(disable:4127)
#endif
#include "old_vector.h"
#include "hash.h"
template<typename T, bool CallDestructors=true, typename SZ = unsigned>
class vector {
#define SIZE_IDX -1
#define CAPACITY_IDX -2
T * m_data;
void destroy_elements() {
iterator it = begin();
iterator e = end();
for (; it != e; ++it) {
it->~T();
}
}
void free_memory() {
memory::deallocate(reinterpret_cast<char*>(reinterpret_cast<SZ*>(m_data) - 2));
}
void expand_vector() {
if (m_data == nullptr) {
SZ capacity = 2;
SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
*mem = capacity;
mem++;
*mem = 0;
mem++;
m_data = reinterpret_cast<T *>(mem);
}
else {
SASSERT(capacity() > 0);
SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
SZ new_capacity = (3 * old_capacity + 1) >> 1;
SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
throw default_exception("Overflow encountered when expanding vector");
}
SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5
if (__has_trivial_copy(T)) {
#else
if (std::is_trivially_copyable<T>::value) {
#endif
mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
m_data = reinterpret_cast<T *>(mem + 2);
} else {
mem = (SZ*)memory::allocate(new_capacity_T);
auto old_data = m_data;
auto old_size = size();
mem[1] = old_size;
m_data = reinterpret_cast<T *>(mem + 2);
for (unsigned i = 0; i < old_size; ++i) {
new (&m_data[i]) T(std::move(old_data[i]));
old_data[i].~T();
}
memory::deallocate(old_mem);
}
*mem = new_capacity;
}
}
void copy_core(vector const & source) {
SZ size = source.size();
SZ capacity = source.capacity();
SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2));
*mem = capacity;
mem++;
*mem = size;
mem++;
m_data = reinterpret_cast<T *>(mem);
const_iterator it = source.begin();
iterator it2 = begin();
SASSERT(it2 == m_data);
const_iterator e = source.end();
for (; it != e; ++it, ++it2) {
new (it2) T(*it);
}
}
void destroy() {
if (m_data) {
if (CallDestructors) {
destroy_elements();
}
free_memory();
}
}
public:
typedef T data;
typedef T * iterator;
typedef const T * const_iterator;
vector():
m_data(nullptr) {
}
vector(SZ s) {
if (s == 0) {
m_data = nullptr;
return;
}
SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2));
*mem = s;
mem++;
*mem = s;
mem++;
m_data = reinterpret_cast<T *>(mem);
// initialize elements
iterator it = begin();
iterator e = end();
for (; it != e; ++it) {
new (it) T();
}
}
vector(SZ s, T const & elem):
m_data(nullptr) {
resize(s, elem);
}
vector(vector const & source):
m_data(nullptr) {
if (source.m_data) {
copy_core(source);
}
SASSERT(size() == source.size());
}
vector(vector&& other) : m_data(nullptr) {
std::swap(m_data, other.m_data);
}
vector(SZ s, T const * data):
m_data(nullptr) {
for (SZ i = 0; i < s; i++) {
push_back(data[i]);
}
}
~vector() {
destroy();
}
void finalize() {
destroy();
m_data = nullptr;
}
bool operator==(vector const & other) const {
if (this == &other) {
return true;
}
if (size() != other.size())
return false;
for (unsigned i = 0; i < size(); i++) {
if ((*this)[i] != other[i])
return false;
}
return true;
}
bool operator!=(vector const & other) const {
return !(*this == other);
}
vector & operator=(vector const & source) {
if (this == &source) {
return *this;
}
destroy();
if (source.m_data) {
copy_core(source);
}
else {
m_data = nullptr;
}
return *this;
}
vector & operator=(vector && source) {
if (this == &source) {
return *this;
}
destroy();
m_data = nullptr;
std::swap(m_data, source.m_data);
return *this;
}
bool containsp(std::function<bool(T)>& predicate) const {
for (auto const& t : *this)
if (predicate(t))
return true;
return false;
}
/**
* retain elements that satisfy predicate. aka 'where'.
*/
vector filter_pure(std::function<bool(T)>& predicate) const {
vector result;
for (auto& t : *this)
if (predicate(t))
result.push_back(t);
return result;
}
vector& filter_update(std::function<bool(T)>& predicate) {
unsigned j = 0;
for (auto& t : *this)
if (predicate(t))
set(j++, t);
shrink(j);
return *this;
}
/**
* update elements using f, aka 'select'
*/
template <typename S>
vector<S> map_pure(std::function<S(T)>& f) const {
vector<S> result;
for (auto& t : *this)
result.push_back(f(t));
return result;
}
vector& map_update(std::function<T(T)>& f) {
unsigned j = 0;
for (auto& t : *this)
set(j++, f(t));
return *this;
}
void reset() {
if (m_data) {
if (CallDestructors) {
destroy_elements();
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = 0;
}
}
void clear() { reset(); }
bool empty() const {
return m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == 0;
}
SZ size() const {
if (m_data == nullptr) {
return 0;
}
return reinterpret_cast<SZ *>(m_data)[SIZE_IDX];
}
SZ capacity() const {
if (m_data == nullptr) {
return 0;
}
return reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
}
iterator begin() {
return m_data;
}
iterator end() {
return m_data + size();
}
const_iterator begin() const {
return m_data;
}
const_iterator end() const {
return m_data + size();
}
class reverse_iterator {
T* v;
public:
reverse_iterator(T* v):v(v) {}
T operator*() { return *v; }
reverse_iterator operator++(int) {
reverse_iterator tmp = *this;
--v;
return tmp;
}
reverse_iterator& operator++() {
--v;
return *this;
}
bool operator==(reverse_iterator const& other) const {
return other.v == v;
}
bool operator!=(reverse_iterator const& other) const {
return other.v != v;
}
};
reverse_iterator rbegin() { return reverse_iterator(end() - 1); }
reverse_iterator rend() { return reverse_iterator(begin() - 1); }
void set_end(iterator it) {
if (m_data) {
SZ new_sz = static_cast<SZ>(it - m_data);
if (CallDestructors) {
iterator e = end();
for(; it != e; ++it) {
it->~T();
}
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = new_sz;
}
else {
SASSERT(it == 0);
}
}
T & operator[](SZ idx) {
SASSERT(idx < size());
return m_data[idx];
}
T const & operator[](SZ idx) const {
SASSERT(idx < size());
return m_data[idx];
}
T & get(SZ idx) {
SASSERT(idx < size());
return m_data[idx];
}
T const & get(SZ idx) const {
SASSERT(idx < size());
return m_data[idx];
}
void set(SZ idx, T const & val) {
SASSERT(idx < size());
m_data[idx] = val;
}
void set(SZ idx, T && val) {
SASSERT(idx < size());
m_data[idx] = std::move(val);
}
T & back() {
SASSERT(!empty());
return operator[](size() - 1);
}
T const & back() const {
SASSERT(!empty());
return operator[](size() - 1);
}
void pop_back() {
SASSERT(!empty());
if (CallDestructors) {
back().~T();
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
}
void push_back(T const & elem) {
if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
expand_vector();
}
new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(elem);
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
}
void push_back(T && elem) {
if (m_data == nullptr || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
expand_vector();
}
new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(std::move(elem));
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
}
void insert(T const & elem) {
push_back(elem);
}
void erase(iterator pos) {
SASSERT(pos >= begin() && pos < end());
iterator prev = pos;
++pos;
iterator e = end();
for(; pos != e; ++pos, ++prev) {
*prev = *pos;
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
}
void erase(T const & elem) {
iterator it = std::find(begin(), end(), elem);
if (it != end()) {
erase(it);
}
}
void shrink(SZ s) {
if (m_data) {
SASSERT(s <= reinterpret_cast<SZ *>(m_data)[SIZE_IDX]);
if (CallDestructors) {
iterator it = m_data + s;
iterator e = end();
for(; it != e; ++it) {
it->~T();
}
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
}
else {
SASSERT(s == 0);
}
}
template<typename Args>
void resize(SZ s, Args args...) {
SZ sz = size();
if (s <= sz) { shrink(s); return; }
while (s > capacity()) {
expand_vector();
}
SASSERT(m_data != 0);
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
iterator it = m_data + sz;
iterator end = m_data + s;
for (; it != end; ++it) {
new (it) T(std::forward<Args>(args));
}
}
void resize(SZ s) {
SZ sz = size();
if (s <= sz) { shrink(s); return; }
while (s > capacity()) {
expand_vector();
}
SASSERT(m_data != 0);
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
iterator it = m_data + sz;
iterator end = m_data + s;
for (; it != end; ++it) {
new (it) T();
}
}
void append(vector<T, CallDestructors> const & other) {
for(SZ i = 0; i < other.size(); ++i) {
push_back(other[i]);
}
}
void append(SZ sz, T const * data) {
for(SZ i = 0; i < sz; ++i) {
push_back(data[i]);
}
}
T * c_ptr() const {
return m_data;
}
void swap(vector & other) {
std::swap(m_data, other.m_data);
}
void reverse() {
SZ sz = size();
for (SZ i = 0; i < sz/2; ++i) {
std::swap(m_data[i], m_data[sz-i-1]);
}
}
void fill(T const & elem) {
iterator i = begin();
iterator e = end();
for (; i != e; ++i) {
*i = elem;
}
}
void fill(unsigned sz, T const & elem) {
resize(sz);
fill(elem);
}
bool contains(T const & elem) const {
const_iterator it = begin();
const_iterator e = end();
for (; it != e; ++it) {
if (*it == elem) {
return true;
}
}
return false;
}
// set pos idx with elem. If idx >= size, then expand using default.
void setx(SZ idx, T const & elem, T const & d) {
if (idx >= size()) {
resize(idx+1, d);
}
m_data[idx] = elem;
}
// return element at position idx, if idx >= size, then return default
T const & get(SZ idx, T const & d) const {
if (idx >= size()) {
return d;
}
return m_data[idx];
}
void reserve(SZ s, T const & d) {
if (s > size())
resize(s, d);
}
void reserve(SZ s) {
if (s > size())
resize(s);
}
};
template<typename T>
class ptr_vector : public vector<T *, false> {
public:
ptr_vector():vector<T *, false>() {}
ptr_vector(unsigned s):vector<T *, false>(s) {}
ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
ptr_vector(ptr_vector const & source):vector<T *, false>(source) {}
ptr_vector(ptr_vector && other) : vector<T*, false>(std::move(other)) {}
ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
ptr_vector & operator=(ptr_vector const & source) {
vector<T *, false>::operator=(source);
return *this;
}
};
using vector = old_vector<T, CallDestructors, SZ>;
template<typename T, typename SZ = unsigned>
class svector : public vector<T, false, SZ> {
public:
svector():vector<T, false, SZ>() {}
svector(SZ s):vector<T, false, SZ>(s) {}
svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
svector(svector const & source):vector<T, false, SZ>(source) {}
svector(svector && other) : vector<T, false, SZ>(std::move(other)) {}
svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
svector & operator=(svector const & source) {
vector<T, false, SZ>::operator=(source);
return *this;
}
};
using svector = old_svector<T, SZ>;
typedef svector<int> int_vector;
typedef svector<unsigned> unsigned_vector;
typedef svector<char> char_vector;
typedef svector<signed char> signed_char_vector;
typedef svector<double> double_vector;
template<typename T>
using ptr_vector = old_ptr_vector<T>;
using int_vector = old_svector<int>;
using unsigned_vector = old_svector<unsigned>;
using char_vector = old_svector<char>;
using signed_char_vector = old_svector<signed char>;
using double_vector = old_svector<double>;
inline std::ostream& operator<<(std::ostream& out, unsigned_vector const& v) {
for (unsigned u : v) out << u << " ";