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

Merge remote-tracking branch 'upstream/master' into refactoring-arith

Browse source
This commit is contained in:
Murphy Berzish 2018-10-02 12:38:40 -04:00
commit b2f0051114
90 changed files with 419 additions and 460 deletions
Download patch file Download diff file Expand all files Collapse all files

135
src/smt/arith_eq_solver.cpp
View file

@ -12,14 +12,11 @@ Abstract:
Author:
Nikolaj Bjorner (nbjorner) 2012-02-25
--*/
#include "smt/arith_eq_solver.h"
arith_eq_solver::~arith_eq_solver() {
}
arith_eq_solver::arith_eq_solver(ast_manager & m, params_ref const& p):
m(m),
m_params(p),
@ -93,9 +90,9 @@ void arith_eq_solver::gcd_normalize(vector<numeral>& values) {
if (g.is_zero() || g.is_one()) {
return;
}
for (unsigned i = 0; i < values.size(); ++i) {
values[i] = values[i] / g;
SASSERT(values[i].is_int());
for (auto &value : values) {
value /= g;
SASSERT(value.is_int());
}
}
@ -116,9 +113,9 @@ unsigned arith_eq_solver::find_abs_min(vector<numeral>& values) {
#ifdef _TRACE
static void print_row(std::ostream& out, vector<rational> const& row) {
for(unsigned i = 0; i < row.size(); ++i) {
out << row[i] << " ";
}
for(unsigned i = 0; i < row.size(); ++i) {
out << row[i] << " ";
}
out << "\n";
}
@ -165,7 +162,7 @@ bool arith_eq_solver::solve_integer_equation(
bool& is_fresh
)
{
TRACE("arith_eq_solver",
TRACE("arith_eq_solver",
tout << "solving: ";
print_row(tout, values);
);
@ -174,31 +171,31 @@ bool arith_eq_solver::solve_integer_equation(
//
// Given:
// a1*x1 + a2*x2 + .. + a_n*x_n + a_{n+1} = 0
//
//
// Assume gcd(a1,..,a_n,a_{n+1}) = 1
// Assume gcd(a1,...,a_n) divides a_{n+1} (eg. gcd(a1,..,an) = 1)
//
//
// post-condition: values[index] = -1.
//
//
// Let a_index be index of least absolute value.
//
// If |a_index| = 1, then return row and index.
// Otherwise:
// Let m = |a_index| + 1
// Set
//
// m*x_index'
// =
//
// m*x_index'
// =
// ((a1 mod_hat m)*x1 + (a2 mod_hat m)*x2 + .. + (a_n mod_hat m)*x_n + (k mod_hat m))
// =
// =
// (a1'*x1 + a2'*x2 + .. (-)1*x_index + ...)
//
//
// <=> Normalize signs so that sign to x_index is -1.
// (-)a1'*x1 + (-)a2'*x2 + .. -1*x_index + ... + m*x_index' = 0
//
//
// Return row, where the coefficient to x_index is implicit.
// Instead used the coefficient 'm' at position 'index'.
//
//
gcd_normalize(values);
if (!gcd_test(values)) {
@ -216,8 +213,8 @@ bool arith_eq_solver::solve_integer_equation(
return true;
}
if (a.is_one()) {
for (unsigned i = 0; i < values.size(); ++i) {
values[i].neg();
for (auto &value : values) {
value.neg();
}
}
is_fresh = !abs_a.is_one();
@ -225,19 +222,19 @@ bool arith_eq_solver::solve_integer_equation(
if (is_fresh) {
numeral m = abs_a + numeral(1);
for (unsigned i = 0; i < values.size(); ++i) {
values[i] = mod_hat(values[i], m);
for (auto &value : values) {
value = mod_hat(value, m);
}
if (values[index].is_one()) {
for (unsigned i = 0; i < values.size(); ++i) {
values[i].neg();
for (auto &value : values) {
value.neg();
}
}
SASSERT(values[index].is_minus_one());
values[index] = m;
}
TRACE("arith_eq_solver",
TRACE("arith_eq_solver",
tout << "solved at index " << index << ": ";
print_row(tout, values);
);
@ -253,7 +250,7 @@ void arith_eq_solver::substitute(
)
{
SASSERT(1 <= index && index < s.size());
TRACE("arith_eq_solver",
TRACE("arith_eq_solver",
tout << "substitute " << index << ":\n";
print_row(tout, r);
print_row(tout, s);
@ -272,21 +269,21 @@ void arith_eq_solver::substitute(
// s encodes an equation that contains a variable
// with a unit coefficient.
//
// Let
// Let
// c = r[index]
// s = s[index]*x + s'*y = 0
// r = c*x + r'*y = 0
//
// =>
//
// =>
//
// 0
// =
// -sign(s[index])*c*s + r
// =
// =
// -sign(s[index])*c*s + r
// =
// -s[index]*sign(s[index])*c*x - sign(s[index])*c*s'*y + c*x + r'*y
// =
// =
// -c*x - sign(s[index])*c*s'*y + c*x + r'*y
// =
// =
// -sign(s[index])*c*s'*y + r'*y
//
numeral sign_s = s[index].is_pos()?numeral(1):numeral(-1);
@ -301,36 +298,36 @@ void arith_eq_solver::substitute(
//
// s encodes a substitution using an auxiliary variable.
// the auxiliary variable is at position 'index'.
//
// Let
//
// Let
// c = r[index]
// s = s[index]*x + s'*y = 0
// r = c*x + r'*y = 0
//
// s encodes : x |-> s[index]*x' + s'*y
//
// Set:
// Set:
//
// r := c*s + r'*y
//
//
r[index] = numeral(0);
for (unsigned i = 0; i < r.size(); ++i) {
r[i] += c*s[i];
}
}
for (unsigned i = r.size(); i < s.size(); ++i) {
r.push_back(c*s[i]);
}
}
}
TRACE("arith_eq_solver",
TRACE("arith_eq_solver",
tout << "result: ";
print_row(tout, r);
);
}
bool arith_eq_solver::solve_integer_equations(
vector<row>& rows,
vector<row>& rows,
row& unsat_row
)
{
@ -340,10 +337,10 @@ bool arith_eq_solver::solve_integer_equations(
//
// Naive integer equation solver where only units are eliminated.
//
//
bool arith_eq_solver::solve_integer_equations_units(
vector<row>& rows,
vector<row>& rows,
row& unsat_row
)
{
@ -351,7 +348,7 @@ bool arith_eq_solver::solve_integer_equations_units(
TRACE("arith_eq_solver", print_rows(tout << "solving:\n", rows););
unsigned_vector todo, done;
for (unsigned i = 0; i < rows.size(); ++i) {
todo.push_back(i);
row& r = rows[i];
@ -360,9 +357,9 @@ bool arith_eq_solver::solve_integer_equations_units(
unsat_row = r;
TRACE("arith_eq_solver", print_row(tout << "input is unsat: ", unsat_row); );
return false;
}
}
}
for (unsigned i = 0; i < todo.size(); ++i) {
for (unsigned i = 0; i < todo.size(); ++i) {
row& r = rows[todo[i]];
gcd_normalize(r);
if (!gcd_test(r)) {
@ -388,7 +385,7 @@ bool arith_eq_solver::solve_integer_equations_units(
todo.push_back(done[j]);
done.erase(done.begin()+j);
--j;
}
}
}
}
else {
@ -396,7 +393,7 @@ bool arith_eq_solver::solve_integer_equations_units(
}
}
TRACE("arith_eq_solver",
TRACE("arith_eq_solver",
tout << ((done.size()<=1)?"solved ":"incomplete check ") << done.size() << "\n";
for (unsigned i = 0; i < done.size(); ++i) {
print_row(tout, rows[done[i]]);
@ -411,12 +408,12 @@ bool arith_eq_solver::solve_integer_equations_units(
//
// Partial solver based on the omega test equalities.
// unsatisfiability is not preserved when eliminating
// unsatisfiability is not preserved when eliminating
// auxiliary variables.
//
bool arith_eq_solver::solve_integer_equations_omega(
vector<row> & rows,
vector<row> & rows,
row& unsat_row
)
{
@ -460,16 +457,16 @@ bool arith_eq_solver::solve_integer_equations_omega(
//
// solved_row: -x_index + m*sigma + r1 = 0
// unsat_row: k*sigma + r2 = 0
//
// <=>
//
//
// <=>
//
// solved_row: -k*x_index + k*m*sigma + k*r1 = 0
// unsat_row: m*k*sigma + m*r2 = 0
//
// =>
//
// m*k*sigma + m*r2 + k*x_index - k*m*sigma - k*r1 = 0
//
//
for (unsigned l = 0; l < unsat_row.size(); ++l) {
unsat_row[l] *= m;
unsat_row[l] -= k*solved_row[l];
@ -479,7 +476,7 @@ bool arith_eq_solver::solve_integer_equations_omega(
}
gcd_normalize(unsat_row);
TRACE("arith_eq_solver",
TRACE("arith_eq_solver",
tout << "gcd: ";
print_row(tout, solved_row);
print_row(tout, unsat_row);
@ -525,18 +522,18 @@ bool arith_eq_solver::solve_integer_equations_omega(
//
// Eliminate variables by searching for combination of rows where
// the coefficients have gcd = 1.
//
// the coefficients have gcd = 1.
//
bool arith_eq_solver::solve_integer_equations_gcd(
vector<row> & rows,
vector<row> & rows,
row& unsat_row
)
{
{
unsigned_vector live, useful, gcd_pos;
vector<rational> gcds;
rational u, v;
if (rows.empty()) {
return true;
}
@ -548,7 +545,7 @@ bool arith_eq_solver::solve_integer_equations_gcd(
unsat_row = r;
TRACE("arith_eq_solver", print_row(tout << "input is unsat: ", unsat_row); );
return false;
}
}
}
unsigned max_column = rows[0].size();
bool change = true;
@ -579,7 +576,7 @@ bool arith_eq_solver::solve_integer_equations_gcd(
if (j == live.size()) {
continue;
}
change = true;
// found gcd, now identify reduced set of rows with GCD = 1.
g = abs(rows[live[j]][i]);
@ -592,7 +589,7 @@ bool arith_eq_solver::solve_integer_equations_gcd(
useful.push_back(gcd_pos[j]);
g = gcd(g, gcds[j]);
SASSERT(j == 0 || gcd(g,gcds[j-1]).is_one());
}
}
}
//
// we now have a set "useful" of rows whose combined GCD = 1.
@ -600,7 +597,7 @@ bool arith_eq_solver::solve_integer_equations_gcd(
//
row& r0 = rows[useful[0]];
for (j = 1; j < useful.size(); ++j) {
row& r1 = rows[useful[j]];
row& r1 = rows[useful[j]];
g = gcd(r0[i], r1[i], u, v);
for (unsigned k = 0; k < max_column; ++k) {
r0[k] = u*r0[k] + v*r1[k];
@ -626,7 +623,7 @@ bool arith_eq_solver::solve_integer_equations_gcd(
}
}
TRACE("arith_eq_solver",
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]]);

24
src/smt/arith_eq_solver.h
View file

@ -12,7 +12,7 @@ Abstract:
Author:
Nikolaj Bjorner (nbjorner) 2012-02-25
--*/
#ifndef ARITH_EQ_SOLVER_H_
#define ARITH_EQ_SOLVER_H_
@ -35,45 +35,45 @@ class arith_eq_solver {
void prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result);
bool gcd_test(vector<numeral>& value);
bool gcd_test(vector<numeral>& values);
unsigned find_abs_min(vector<numeral>& values);
void gcd_normalize(vector<numeral>& values);
void substitute(vector<numeral>& r, vector<numeral> const& s, unsigned index);
bool solve_integer_equations_units(
vector<vector<numeral> > & rows,
vector<vector<numeral> > & rows,
vector<numeral>& unsat_row
);
bool solve_integer_equations_omega(
vector<vector<numeral> > & rows,
vector<vector<numeral> > & rows,
vector<numeral>& unsat_row
);
void compute_hnf(vector<vector<numeral> >& A);
bool solve_integer_equations_hermite(
vector<vector<numeral> > & rows,
vector<vector<numeral> > & rows,
vector<numeral>& unsat_row
);
bool solve_integer_equations_gcd(
vector<vector<numeral> > & rows,
vector<vector<numeral> > & rows,
vector<numeral>& unsat_row
);
public:
arith_eq_solver(ast_manager & m, params_ref const& p = params_ref());
~arith_eq_solver();
~arith_eq_solver() = default;
// Integer linear solver for a single equation.
// The array values contains integer coefficients
//
//
// Determine integer solutions to:
//
// a+k = 0
//
// where a = sum_i a_i*k_i
//
//
typedef vector<numeral> row;
typedef vector<row> matrix;
@ -90,14 +90,14 @@ public:
// a+k = 0
//
// where a = sum_i a_i*k_i
//
//
// Solution, if there is any, is returned as a substitution.
// The return value is "true".
// If there is no solution, then return "false".
// together with equality "eq_unsat", such that
//
// eq_unsat = 0
//
//
// is implied and is unsatisfiable over the integers.
//

1
src/smt/mam.cpp
View file

@ -2571,6 +2571,7 @@ namespace smt {
m_n1 = m_context.get_enode_eq_to(static_cast<const get_cgr *>(m_pc)->m_label, static_cast<const get_cgr *>(m_pc)->m_num_args, m_args.c_ptr()); \
if (m_n1 == 0 || !m_context.is_relevant(m_n1)) \
goto backtrack; \
update_max_generation(m_n1, nullptr); \
m_registers[static_cast<const get_cgr *>(m_pc)->m_oreg] = m_n1; \
m_pc = m_pc->m_next; \
goto main_loop;

2
src/smt/smt_context.h
View file

@ -565,7 +565,7 @@ namespace smt {
return m_asserted_formulas.has_quantifiers();
}
fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = 0) {
fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = nullptr) {
return m_fingerprints.insert(data, data_hash, num_args, args, def);
}

2
src/smt/smt_model_checker.cpp
View file

@ -577,7 +577,7 @@ namespace smt {
}
if (inst.m_def) {
m_context->internalize_assertion(inst.m_def, 0, gen);
m_context->internalize_assertion(inst.m_def, nullptr, gen);
}
TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";

4
src/smt/tactic/smt_tactic.cpp
View file

@ -217,7 +217,7 @@ public:
model_ref md;
m_ctx->get_model(md);
buffer<symbol> r;
m_ctx->get_relevant_labels(0, r);
m_ctx->get_relevant_labels(nullptr, r);
labels_vec rv;
rv.append(r.size(), r.c_ptr());
model_converter_ref mc;
@ -270,7 +270,7 @@ public:
model_ref md;
m_ctx->get_model(md);
buffer<symbol> r;
m_ctx->get_relevant_labels(0, r);
m_ctx->get_relevant_labels(nullptr, r);
labels_vec rv;
rv.append(r.size(), r.c_ptr());
in->add(model_and_labels2model_converter(md.get(), rv));

19
src/smt/theory_lra.cpp
View file

@ -147,7 +147,7 @@ class theory_lra::imp {
imp& m_imp;
public:
resource_limit(imp& i): m_imp(i) { }
virtual bool get_cancel_flag() { return m_imp.m.canceled(); }
bool get_cancel_flag() override { return m_imp.m.canceled(); }
};
@ -341,7 +341,7 @@ class theory_lra::imp {
}
app_ref cnst(a.mk_numeral(rational(c), is_int), m);
TRACE("arith", tout << "add " << cnst << "\n";);
enode* e = mk_enode(cnst);
mk_enode(cnst);
theory_var v = mk_var(cnst);
var = m_solver->add_var(v, true);
m_theory_var2var_index.setx(v, var, UINT_MAX);
@ -1054,7 +1054,7 @@ public:
// to_int (to_real x) = x
// to_real(to_int(x)) <= x < to_real(to_int(x)) + 1
void mk_to_int_axiom(app* n) {
expr* x = 0, *y = 0;
expr* x = nullptr, *y = nullptr;
VERIFY (a.is_to_int(n, x));
if (a.is_to_real(x, y)) {
mk_axiom(th.mk_eq(y, n, false));
@ -1070,7 +1070,7 @@ public:
// is_int(x) <=> to_real(to_int(x)) = x
void mk_is_int_axiom(app* n) {
expr* x = 0;
expr* x = nullptr;
VERIFY(a.is_is_int(n, x));
literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
literal is_int = ctx().get_literal(n);
@ -1450,7 +1450,7 @@ public:
st = FC_GIVEUP;
break;
}
if (m_not_handled != 0) {
if (m_not_handled != nullptr) {
TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);
st = FC_GIVEUP;
}
@ -1569,7 +1569,6 @@ public:
VERIFY(a.is_idiv(n, p, q));
theory_var v = mk_var(n);
theory_var v1 = mk_var(p);
theory_var v2 = mk_var(q);
rational r1 = get_value(v1);
rational r2;
@ -2080,12 +2079,12 @@ public:
m_core2.push_back(~c);
}
m_core2.push_back(lit);
justification * js = 0;
justification * js = nullptr;
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.c_ptr(),
m_params.size(), m_params.c_ptr());
}
ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, 0);
ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
else {
ctx().assign(
@ -2140,7 +2139,7 @@ public:
rational const& k1 = b.get_value();
lp_bounds & bounds = m_bounds[v];
lp_api::bound* end = 0;
lp_api::bound* end = nullptr;
lp_api::bound* lo_inf = end, *lo_sup = end;
lp_api::bound* hi_inf = end, *hi_sup = end;
@ -2798,7 +2797,7 @@ public:
justification* js =
ctx().mk_justification(
ext_theory_eq_propagation_justification(
get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, 0));
get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr));
TRACE("arith",
for (unsigned i = 0; i < m_core.size(); ++i) {

38
src/smt/theory_pb.cpp
View file

@ -759,18 +759,18 @@ namespace smt {
card& get_card() { return m_card; }
virtual void get_antecedents(conflict_resolution& cr) {
void get_antecedents(conflict_resolution& cr) override {
cr.mark_literal(m_card.lit());
for (unsigned i = m_card.k(); i < m_card.size(); ++i) {
cr.mark_literal(~m_card.lit(i));
}
}
virtual theory_id get_from_theory() const {
theory_id get_from_theory() const override {
return m_fid;
}
virtual proof* mk_proof(smt::conflict_resolution& cr) {
proof* mk_proof(smt::conflict_resolution& cr) override {
ptr_buffer<proof> prs;
ast_manager& m = cr.get_context().get_manager();
expr_ref fact(m);
@ -897,7 +897,7 @@ namespace smt {
void theory_pb::watch_literal(literal lit, card* c) {
init_watch(lit.var());
ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_cwatch[lit.sign()];
if (cards == 0) {
if (cards == nullptr) {
cards = alloc(ptr_vector<card>);
m_var_infos[lit.var()].m_lit_cwatch[lit.sign()] = cards;
}
@ -961,13 +961,13 @@ namespace smt {
void theory_pb::add_clause(card& c, literal_vector const& lits) {
m_stats.m_num_conflicts++;
context& ctx = get_context();
justification* js = 0;
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());
}
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
SASSERT(ctx.inconsistent());
}
@ -1027,7 +1027,7 @@ namespace smt {
}
void theory_pb::assign_eh(bool_var v, bool is_true) {
ptr_vector<ineq>* ineqs = 0;
ptr_vector<ineq>* ineqs = nullptr;
context& ctx = get_context();
literal nlit(v, is_true);
init_watch(v);
@ -1060,7 +1060,7 @@ namespace smt {
}
ptr_vector<card>* cards = m_var_infos[v].m_lit_cwatch[nlit.sign()];
if (cards != 0 && !cards->empty() && !ctx.inconsistent()) {
if (cards != nullptr && !cards->empty() && !ctx.inconsistent()) {
ptr_vector<card>::iterator it = cards->begin(), it2 = it, end = cards->end();
for (; it != end; ++it) {
if (ctx.get_assignment((*it)->lit()) != l_true) {
@ -1088,7 +1088,7 @@ namespace smt {
}
card* crd = m_var_infos[v].m_card;
if (crd != 0 && !ctx.inconsistent()) {
if (crd != nullptr && !ctx.inconsistent()) {
crd->init_watch(*this, is_true);
}
@ -1527,7 +1527,7 @@ namespace smt {
else {
z++;
clear_watch(*c);
m_var_infos[v].m_card = 0;
m_var_infos[v].m_card = nullptr;
dealloc(c);
m_card_trail[i] = null_bool_var;
ctx.remove_watch(v);
@ -1671,7 +1671,7 @@ namespace smt {
if (v != null_bool_var) {
card* c = m_var_infos[v].m_card;
clear_watch(*c);
m_var_infos[v].m_card = 0;
m_var_infos[v].m_card = nullptr;
dealloc(c);
}
}
@ -1774,11 +1774,11 @@ namespace smt {
context& ctx = get_context();
TRACE("pb", tout << "#prop:" << c.m_num_propagations << " - " << lits << "\n";
display(tout, c, true););
justification* js = 0;
justification* js = nullptr;
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, 0);
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
@ -1894,11 +1894,11 @@ namespace smt {
break;
case b_justification::JUSTIFICATION: {
justification* j = js.get_justification();
card_justification* pbj = 0;
card_justification* pbj = nullptr;
if (j->get_from_theory() == get_id()) {
pbj = dynamic_cast<card_justification*>(j);
}
if (pbj != 0) {
if (pbj != nullptr) {
card& c2 = pbj->get_card();
result = card2expr(c2);
}
@ -2170,11 +2170,11 @@ namespace smt {
VERIFY(internalize_card(atl, false));
bool_var abv = ctx.get_bool_var(atl);
m_antecedents.push_back(literal(abv));
justification* js = 0;
justification* js = nullptr;
if (proofs_enabled()) {
js = 0; //
js = nullptr;
}
ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), js, CLS_AUX_LEMMA, 0);
ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
bool theory_pb::resolve_conflict(card& c, literal_vector const& confl) {
@ -2403,7 +2403,7 @@ namespace smt {
}
#endif
SASSERT(validate_antecedents(m_antecedents));
ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, 0)));
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);

2
src/smt/theory_pb.h
View file

@ -258,7 +258,7 @@ namespace smt {
card_watch* m_lit_cwatch[2];
card* m_card;
var_info(): m_var_watch(0), m_ineq(0), m_card(0)
var_info(): m_var_watch(nullptr), m_ineq(nullptr), m_card(nullptr)
{
m_lit_watch[0] = nullptr;
m_lit_watch[1] = nullptr;

8
src/smt/theory_seq.cpp
View file

@ -1120,7 +1120,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
break;
}
if (flag) {
expr* nl_fst = 0;
expr* nl_fst = nullptr;
if (e.rs().size()>1 && is_var(e.rs().get(0)))
nl_fst = e.rs().get(0);
if (nl_fst && nl_fst != r_fst) {
@ -1173,7 +1173,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
break;
}
if (flag) {
expr* nl_fst = 0;
expr* nl_fst = nullptr;
if (e.rs().size()>1 && is_var(e.rs().get(0)))
nl_fst = e.rs().get(0);
if (nl_fst && nl_fst != r_fst) {
@ -1375,8 +1375,8 @@ bool theory_seq::branch_variable_mb() {
continue;
}
rational l1, l2;
for (auto elem : len1) l1 += elem;
for (auto elem : len2) l2 += elem;
for (const auto& elem : len1) l1 += elem;
for (const auto& elem : len2) l2 += elem;
if (l1 != l2) {
TRACE("seq", tout << "lengths are not compatible\n";);
expr_ref l = mk_concat(e.ls());

20
src/smt/theory_str.cpp
View file

@ -110,7 +110,7 @@ namespace smt {
public:
seq_expr_solver(ast_manager& m, smt_params& fp):
m_kernel(m, fp) {}
virtual lbool check_sat(expr* e) {
lbool check_sat(expr* e) override {
m_kernel.push();
m_kernel.assert_expr(e);
lbool r = m_kernel.check();
@ -6712,8 +6712,8 @@ namespace smt {
}
unsigned theory_str::estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2) {
ENSURE(aut1 != NULL);
ENSURE(aut2 != NULL);
ENSURE(aut1 != nullptr);
ENSURE(aut2 != nullptr);
return _qmul(aut1->num_states(), aut2->num_states());
}
@ -6966,7 +6966,7 @@ namespace smt {
* and the equality with 0 is based on whether solutions of length 0 are allowed.
*/
void theory_str::find_automaton_initial_bounds(expr * str_in_re, eautomaton * aut) {
ENSURE(aut != NULL);
ENSURE(aut != nullptr);
context & ctx = get_context();
ast_manager & m = get_manager();
@ -7018,7 +7018,7 @@ namespace smt {
* if it exists, or -1 otherwise.
*/
bool theory_str::refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound) {
ENSURE(aut != NULL);
ENSURE(aut != nullptr);
if (aut->final_states().size() < 1) {
// no solutions at all
@ -7128,7 +7128,7 @@ namespace smt {
* if a shorter solution exists, or -1 otherwise.
*/
bool theory_str::refine_automaton_upper_bound(eautomaton * aut, rational current_upper_bound, rational & refined_upper_bound) {
ENSURE(aut != NULL);
ENSURE(aut != nullptr);
if (aut->final_states().empty()) {
// no solutions at all!
@ -7247,7 +7247,7 @@ namespace smt {
return retval;
} else {
TRACE("str", tout << "ERROR: unrecognized automaton path constraint " << mk_pp(cond, m) << ", cannot translate" << std::endl;);
retval = NULL;
retval = nullptr;
return retval;
}
}
@ -7260,7 +7260,7 @@ namespace smt {
* are returned in `characterConstraints`.
*/
expr_ref theory_str::generate_regex_path_constraints(expr * stringTerm, eautomaton * aut, rational lenVal, expr_ref & characterConstraints) {
ENSURE(aut != NULL);
ENSURE(aut != nullptr);
context & ctx = get_context();
ast_manager & m = get_manager();
@ -10643,8 +10643,10 @@ namespace smt {
if (!u.str.is_string(concat_lhs)) {
lhs_terms.push_back(ctx.mk_eq_atom(concat_lhs, concat_lhs_str));
}
if (!u.str.is_string(concat_rhs)) {
lhs_terms.push_back(ctx.mk_eq_atom(concat_rhs, concat_rhs_str));
}
if (lhs_terms.empty()) {
@ -12216,7 +12218,7 @@ namespace smt {
// - in the same EQC as freeVar
if (term_appears_as_subterm(freeVar, re_str)) {
TRACE("str", tout << "prevent value testing on free var " << mk_pp(freeVar, m) << " as it belongs to one or more regex constraints." << std::endl;);
return NULL;
return nullptr;
}
}
}

2
src/smt/theory_str.h
View file

@ -165,7 +165,7 @@ protected:
rational upper_bound;
public:
regex_automaton_under_assumptions() :
re_term(NULL), aut(NULL), polarity(false),
re_term(nullptr), aut(nullptr), polarity(false),
assume_lower_bound(false), assume_upper_bound(false) {}
regex_automaton_under_assumptions(expr * re_term, eautomaton * aut, bool polarity) :

8
src/smt/watch_list.cpp
View file

@ -36,10 +36,10 @@ namespace smt {
void watch_list::expand() {
if (m_data == nullptr) {
unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE;
unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE;
unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, size));
#ifdef _AMD64_
++mem; // make sure data is aligned in 64 bit machines
++mem; // make sure data is aligned in 64 bit machines
#endif
*mem = 0;
++mem;
@ -62,9 +62,9 @@ namespace smt {
unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, new_capacity + HEADER_SIZE));
unsigned curr_end_cls = end_cls_core();
#ifdef _AMD64_
++mem; // make sure data is aligned in 64 bit machines
++mem; // make sure data is aligned in 64 bit machines
#endif
*mem = curr_end_cls;
*mem = curr_end_cls;
++mem;
SASSERT(bin_bytes <= new_capacity);
unsigned new_begin_bin = new_capacity - bin_bytes;