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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-14 15:16:22 -07:00
commit e9d615e309
204 changed files with 4620 additions and 2435 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;

1
src/smt/params/smt_params.cpp
View file

@ -63,6 +63,7 @@ void smt_params::updt_params(params_ref const & p) {
theory_bv_params::updt_params(p);
theory_pb_params::updt_params(p);
// theory_array_params::updt_params(p);
theory_datatype_params::updt_params(p);
updt_local_params(p);
}

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

@ -94,5 +94,6 @@ def_module_params(module_name='smt',
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none')
('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy')
))

9
src/smt/params/theory_datatype_params.h
View file

@ -19,6 +19,8 @@ Revision History:
#ifndef THEORY_DATATYPE_PARAMS_H_
#define THEORY_DATATYPE_PARAMS_H_
#include "smt/params/smt_params_helper.hpp"
struct theory_datatype_params {
unsigned m_dt_lazy_splits;
@ -26,11 +28,10 @@ struct theory_datatype_params {
m_dt_lazy_splits(1) {
}
#if 0
void register_params(ini_params & p) {
p.register_unsigned_param("dt_lazy_splits", m_dt_lazy_splits, "How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy");
void updt_params(params_ref const & _p) {
smt_params_helper p(_p);
m_dt_lazy_splits = p.dt_lazy_splits();
}
#endif
void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << std::endl; }
};

8
src/smt/smt_arith_value.cpp
View file

@ -1,4 +1,3 @@
/*++
Copyright (c) 2018 Microsoft Corporation
@ -17,7 +16,6 @@ Author:
Revision History:
--*/
#pragma once;
#include "smt/smt_arith_value.h"
#include "smt/theory_lra.h"
@ -96,4 +94,10 @@ namespace smt {
while (next != n);
return false;
}
final_check_status arith_value::final_check() {
family_id afid = a.get_family_id();
theory * th = m_ctx.get_theory(afid);
return th->final_check_eh();
}
};

3
src/smt/smt_arith_value.h
View file

@ -17,7 +17,7 @@ Author:
Revision History:
--*/
#pragma once;
#pragma once
#include "ast/arith_decl_plugin.h"
#include "smt/smt_context.h"
@ -33,5 +33,6 @@ namespace smt {
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);
final_check_status final_check();
};
};

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_context_pp.cpp
View file

@ -426,6 +426,7 @@ namespace smt {
std::stringstream strm;
strm << "lemma_" << (++m_lemma_id) << ".smt2";
std::ofstream out(strm.str());
TRACE("lemma", tout << strm.str() << "\n";);
display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic);
out.close();
return m_lemma_id;
@ -466,6 +467,7 @@ namespace smt {
std::stringstream strm;
strm << "lemma_" << (++m_lemma_id) << ".smt2";
std::ofstream out(strm.str());
TRACE("lemma", tout << strm.str() << "\n";);
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close();
return m_lemma_id;

12
src/smt/smt_farkas_util.cpp
View file

@ -312,6 +312,13 @@ namespace smt {
}
expr_ref farkas_util::get() {
TRACE("arith",
for (unsigned i = 0; i < m_coeffs.size(); ++i) {
tout << m_coeffs[i] << " * (" << mk_pp(m_ineqs[i].get(), m) << ") ";
}
tout << "\n";
);
m_normalize_factor = rational::one();
expr_ref res(m);
if (m_coeffs.empty()) {
@ -330,13 +337,12 @@ namespace smt {
partition_ineqs();
expr_ref_vector lits(m);
unsigned lo = 0;
for (unsigned i = 0; i < m_his.size(); ++i) {
unsigned hi = m_his[i];
for (unsigned hi : m_his) {
lits.push_back(extract_consequence(lo, hi));
lo = hi;
}
bool_rewriter(m).mk_or(lits.size(), lits.c_ptr(), res);
IF_VERBOSE(2, { if (lits.size() > 1) { verbose_stream() << "combined lemma: " << mk_pp(res, m) << "\n"; } });
IF_VERBOSE(2, { if (lits.size() > 1) { verbose_stream() << "combined lemma: " << res << "\n"; } });
}
else {
res = extract_consequence(0, m_coeffs.size());

41
src/smt/smt_internalizer.cpp
View file

@ -216,13 +216,17 @@ namespace smt {
SASSERT(m_manager.is_bool(n));
if (is_gate(m_manager, n)) {
switch(to_app(n)->get_decl_kind()) {
case OP_AND:
UNREACHABLE();
case OP_AND: {
for (expr * arg : *to_app(n)) {
internalize(arg, true);
literal lit = get_literal(arg);
mk_root_clause(1, &lit, pr);
}
break;
}
case OP_OR: {
literal_buffer lits;
unsigned num = to_app(n)->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = to_app(n)->get_arg(i);
for (expr * arg : *to_app(n)) {
internalize(arg, true);
lits.push_back(get_literal(arg));
}
@ -294,8 +298,7 @@ namespace smt {
sort * s = m_manager.get_sort(n->get_arg(0));
sort_ref u(m_manager.mk_fresh_sort("distinct-elems"), m_manager);
func_decl_ref f(m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m_manager);
for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i);
for (expr * arg : *n) {
app_ref fapp(m_manager.mk_app(f, arg), m_manager);
app_ref val(m_manager.mk_fresh_const("unique-value", u), m_manager);
enode * e = mk_enode(val, false, false, true);
@ -826,9 +829,7 @@ namespace smt {
void context::internalize_uninterpreted(app * n) {
SASSERT(!e_internalized(n));
// process args
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = n->get_arg(i);
for (expr * arg : *n) {
internalize(arg, false);
SASSERT(e_internalized(arg));
}
@ -1542,10 +1543,9 @@ namespace smt {
void context::add_and_rel_watches(app * n) {
if (relevancy()) {
relevancy_eh * eh = m_relevancy_propagator->mk_and_relevancy_eh(n);
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
for (expr * arg : *n) {
// if one child is assigned to false, the and-parent must be notified
literal l = get_literal(n->get_arg(i));
literal l = get_literal(arg);
add_rel_watch(~l, eh);
}
}
@ -1554,10 +1554,9 @@ namespace smt {
void context::add_or_rel_watches(app * n) {
if (relevancy()) {
relevancy_eh * eh = m_relevancy_propagator->mk_or_relevancy_eh(n);
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
for (expr * arg : *n) {
// if one child is assigned to true, the or-parent must be notified
literal l = get_literal(n->get_arg(i));
literal l = get_literal(arg);
add_rel_watch(l, eh);
}
}
@ -1588,9 +1587,8 @@ namespace smt {
TRACE("mk_and_cnstr", tout << "l: "; display_literal(tout, l); tout << "\n";);
literal_buffer buffer;
buffer.push_back(l);
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
literal l_arg = get_literal(n->get_arg(i));
for (expr * arg : *n) {
literal l_arg = get_literal(arg);
TRACE("mk_and_cnstr", tout << "l_arg: "; display_literal(tout, l_arg); tout << "\n";);
mk_gate_clause(~l, l_arg);
buffer.push_back(~l_arg);
@ -1602,9 +1600,8 @@ namespace smt {
literal l = get_literal(n);
literal_buffer buffer;
buffer.push_back(~l);
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
literal l_arg = get_literal(n->get_arg(i));
for (expr * arg : *n) {
literal l_arg = get_literal(arg);
mk_gate_clause(l, ~l_arg);
buffer.push_back(l_arg);
}

47
src/smt/smt_model_checker.cpp
View file

@ -47,6 +47,7 @@ namespace smt {
m_model_finder(mf),
m_max_cexs(1),
m_iteration_idx(0),
m_has_rec_fun(false),
m_curr_model(nullptr),
m_pinned_exprs(m) {
}
@ -351,9 +352,7 @@ namespace smt {
bool model_checker::check_rec_fun(quantifier* q, bool strict_rec_fun) {
TRACE("model_checker", tout << mk_pp(q, m) << "\n";);
SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body.
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
SASSERT(is_app(fn));
func_decl* f = to_app(fn)->get_decl();
func_decl* f = m.get_rec_fun_decl(q);
expr_ref_vector args(m);
unsigned num_decls = q->get_num_decls();
@ -433,7 +432,7 @@ namespace smt {
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) {
if (num_failures == 0 && (!m_context->validate_model() || has_rec_under_quantifiers())) {
num_failures = 1;
// this time force expanding recursive function definitions
// that are not forced true in the current model.
@ -450,6 +449,43 @@ namespace smt {
return num_failures == 0;
}
struct has_rec_fun_proc {
obj_hashtable<func_decl>& m_rec_funs;
bool m_has_rec_fun;
bool has_rec_fun() const { return m_has_rec_fun; }
has_rec_fun_proc(obj_hashtable<func_decl>& rec_funs):
m_rec_funs(rec_funs),
m_has_rec_fun(false) {}
void operator()(app* fn) {
m_has_rec_fun |= m_rec_funs.contains(fn->get_decl());
}
void operator()(expr*) {}
};
bool model_checker::has_rec_under_quantifiers() {
if (!m_has_rec_fun) {
return false;
}
obj_hashtable<func_decl> rec_funs;
for (quantifier * q : *m_qm) {
if (m.is_rec_fun_def(q)) {
rec_funs.insert(m.get_rec_fun_decl(q));
}
}
expr_fast_mark1 visited;
has_rec_fun_proc proc(rec_funs);
for (quantifier * q : *m_qm) {
if (!m.is_rec_fun_def(q)) {
quick_for_each_expr(proc, visited, q);
if (proc.has_rec_fun()) return true;
}
}
return false;
}
//
// (repeated from defined_names.cpp)
// NB. The pattern for lambdas is incomplete.
@ -479,6 +515,7 @@ namespace smt {
}
found_relevant = true;
if (m.is_rec_fun_def(q)) {
m_has_rec_fun = true;
if (!check_rec_fun(q, strict_rec_fun)) {
TRACE("model_checker", tout << "checking recursive function failed\n";);
num_failures++;
@ -540,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";

3
src/smt/smt_model_checker.h
View file

@ -51,8 +51,10 @@ namespace smt {
scoped_ptr<context> m_aux_context; // Auxiliary context used for model checking quantifiers.
unsigned m_max_cexs;
unsigned m_iteration_idx;
bool m_has_rec_fun;
proto_model * m_curr_model;
obj_map<expr, expr *> m_value2expr;
friend class instantiation_set;
void init_aux_context();
@ -64,6 +66,7 @@ namespace smt {
bool add_blocking_clause(model * cex, expr_ref_vector & sks);
bool check(quantifier * q);
bool check_rec_fun(quantifier* q, bool strict_rec_fun);
bool has_rec_under_quantifiers();
void check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures);
struct instance {

1
src/smt/smt_theory.h
View file

@ -36,6 +36,7 @@ namespace smt {
unsigned_vector m_var2enode_lim;
friend class context;
friend class arith_value;
protected:
virtual void init(context * ctx);

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

5
src/smt/theory_arith_aux.h
View file

@ -1103,6 +1103,7 @@ namespace smt {
e = m_util.mk_gt(obj, e);
}
}
TRACE("opt", tout << e << "\n";);
return e;
}
@ -1119,6 +1120,8 @@ namespace smt {
std::ostringstream strm;
strm << val << " <= " << mk_pp(get_enode(v)->get_owner(), get_manager());
app* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort());
expr_ref result(b, m);
TRACE("opt", tout << result << "\n";);
if (!ctx.b_internalized(b)) {
fm.hide(b->get_decl());
bool_var bv = ctx.mk_bool_var(b);
@ -1133,7 +1136,7 @@ namespace smt {
TRACE("arith", tout << mk_pp(b, m) << "\n";
display_atom(tout, a, false););
}
return expr_ref(b, m);
return result;
}

9
src/smt/theory_arith_core.h
View file

@ -484,7 +484,6 @@ namespace smt {
void theory_arith<Ext>::mk_idiv_mod_axioms(expr * dividend, expr * divisor) {
if (!m_util.is_zero(divisor)) {
ast_manager & m = get_manager();
bool is_numeral = m_util.is_numeral(divisor);
// 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);
@ -504,9 +503,9 @@ namespace smt {
tout << "lower: " << lower << "\n";
tout << "upper: " << upper << "\n";);
mk_axiom(eqz, eq, !is_numeral);
mk_axiom(eqz, lower, !is_numeral);
mk_axiom(eqz, upper, !is_numeral);
mk_axiom(eqz, eq, true);
mk_axiom(eqz, lower, false);
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
rational k;
context& ctx = get_context();
(void)ctx;
@ -3311,7 +3310,7 @@ namespace smt {
}
template<typename Ext>
bool theory_arith<Ext>::get_upper(enode * n, rational& r, bool& is_strict) {
bool theory_arith<Ext>::get_upper(enode * n, rational& r, bool& is_strict) {
theory_var v = n->get_th_var(get_id());
bound* b = (v == null_theory_var) ? nullptr : upper(v);
return b && (r = b->get_value().get_rational().to_rational(), is_strict = b->get_value().get_infinitesimal().is_neg(), true);

4
src/smt/theory_arith_int.h
View file

@ -396,7 +396,9 @@ namespace smt {
for (; it != end; ++it) {
if (!it->is_dead() && it->m_var != b && is_free(it->m_var)) {
theory_var v = it->m_var;
expr * bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(rational::zero(), is_int(v)));
expr* e = get_enode(v)->get_owner();
bool _is_int = m_util.is_int(e);
expr * bound = m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int));
context & ctx = get_context();
ctx.internalize(bound, true);
ctx.mark_as_relevant(bound);

2
src/smt/theory_arith_pp.h
View file

@ -544,7 +544,7 @@ namespace smt {
char buffer[128];
static int id = 0;
#ifdef _WINDOWS
sprintf_s(buffer, ARRAYSIZE(buffer), "arith_%d.smt", id);
sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "arith_%d.smt", id);
#else
sprintf(buffer, "arith_%d.smt", id);
#endif

49
src/smt/theory_array_full.cpp
View file

@ -339,18 +339,14 @@ namespace smt {
SASSERT(v != null_theory_var);
v = find(v);
var_data* d = m_var_data[v];
TRACE("array", tout << "v" << v << " " << d->m_prop_upward << " " << m_params.m_array_delay_exp_axiom << "\n";);
for (enode * store : d->m_stores) {
SASSERT(is_store(store));
instantiate_default_store_axiom(store);
}
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (enode * store : d->m_parent_stores) {
SASSERT(is_store(store));
if (!m_params.m_array_cg || store->is_cgr()) {
instantiate_default_store_axiom(store);
}
}
instantiate_parent_stores_default(v);
}
}
@ -381,14 +377,13 @@ namespace smt {
}
void theory_array_full::relevant_eh(app* n) {
TRACE("array", tout << mk_pp(n, get_manager()) << "\n";);
TRACE("array", tout << mk_pp(n, get_manager()) << "\n";);
theory_array::relevant_eh(n);
if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)) {
if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)){
return;
}
context & ctx = get_context();
enode* node = ctx.get_enode(n);
if (is_select(n)) {
enode * arg = ctx.get_enode(n->get_arg(0));
theory_var v = arg->get_th_var(get_id());
@ -399,14 +394,18 @@ namespace smt {
enode * arg = ctx.get_enode(n->get_arg(0));
theory_var v = arg->get_th_var(get_id());
SASSERT(v != null_theory_var);
set_prop_upward(v);
add_parent_default(find(v));
}
else if (is_const(n)) {
instantiate_default_const_axiom(node);
theory_var v = node->get_th_var(get_id());
set_prop_upward(v);
add_parent_default(find(v));
}
else if (is_map(n)) {
for (unsigned i = 0; i < n->get_num_args(); ++i) {
enode* arg = ctx.get_enode(n->get_arg(i));
for (expr * e : *n) {
enode* arg = ctx.get_enode(e);
theory_var v_arg = find(arg->get_th_var(get_id()));
add_parent_map(v_arg, node);
set_prop_upward(v_arg);
@ -496,7 +495,7 @@ namespace smt {
app* map = mp->get_owner();
ast_manager& m = get_manager();
context& ctx = get_context();
if (!ctx.add_fingerprint(this, 0, 1, &mp)) {
if (!ctx.add_fingerprint(this, m_default_map_fingerprint, 1, &mp)) {
return false;
}
TRACE("array", tout << mk_bounded_pp(map, get_manager()) << "\n";);
@ -521,7 +520,7 @@ namespace smt {
bool theory_array_full::instantiate_default_const_axiom(enode* cnst) {
context& ctx = get_context();
if (!ctx.add_fingerprint(this, 0, 1, &cnst)) {
if (!ctx.add_fingerprint(this, m_default_const_fingerprint, 1, &cnst)) {
return false;
}
m_stats.m_num_default_const_axiom++;
@ -542,7 +541,7 @@ namespace smt {
return false;
#if 0
context& ctx = get_context();
if (!ctx.add_fingerprint(this, 0, 1, &arr)) {
if (!ctx.add_fingerprint(this, m_default_as_array_fingerprint, 1, &arr)) {
return false;
}
m_stats.m_num_default_as_array_axiom++;
@ -659,7 +658,7 @@ namespace smt {
app* store_app = store->get_owner();
context& ctx = get_context();
ast_manager& m = get_manager();
if (!ctx.add_fingerprint(this, 0, 1, &store)) {
if (!ctx.add_fingerprint(this, m_default_store_fingerprint, 1, &store)) {
return false;
}
@ -732,6 +731,10 @@ namespace smt {
var_data * d = m_var_data[v];
if (d->m_prop_upward && instantiate_axiom_map_for(v))
r = FC_CONTINUE;
if (d->m_prop_upward && !m_params.m_array_weak) {
if (instantiate_parent_stores_default(v))
r = FC_CONTINUE;
}
}
}
while (!m_eqsv.empty()) {
@ -746,6 +749,22 @@ namespace smt {
return r;
}
bool theory_array_full::instantiate_parent_stores_default(theory_var v) {
SASSERT(v != null_theory_var);
TRACE("array", tout << "v" << v << "\n";);
v = find(v);
var_data* d = m_var_data[v];
bool result = false;
for (enode * store : d->m_parent_stores) {
TRACE("array", tout << expr_ref(store->get_owner(), get_manager()) << "\n";);
SASSERT(is_store(store));
if (!m_params.m_array_cg || store->is_cgr()) {
if (instantiate_default_store_axiom(store))
result = true;
}
}
return result;
}
bool theory_array_full::try_assign_eq(expr* v1, expr* v2) {
TRACE("array",

6
src/smt/theory_array_full.h
View file

@ -38,6 +38,11 @@ namespace smt {
ast2ast_trailmap<sort,app> m_sort2epsilon;
obj_pair_map<expr,expr,bool> m_eqs;
svector<literal> m_eqsv;
static unsigned const m_default_map_fingerprint = UINT_MAX - 112;
static unsigned const m_default_store_fingerprint = UINT_MAX - 113;
static unsigned const m_default_const_fingerprint = UINT_MAX - 115;
static unsigned const m_default_as_array_fingerprint = UINT_MAX - 116;
protected:
@ -70,6 +75,7 @@ namespace smt {
bool instantiate_default_store_axiom(enode* store);
bool instantiate_default_map_axiom(enode* map);
bool instantiate_default_as_array_axiom(enode* arr);
bool instantiate_parent_stores_default(theory_var v);
bool has_large_domain(app* array_term);
app* mk_epsilon(sort* s);

536
src/smt/theory_lra.cpp
View file

@ -55,7 +55,7 @@ std::ostream& operator<<(std::ostream& out, bound_kind const& k) {
}
class bound {
smt::bool_var m_bv;
smt::bool_var m_bv;
smt::theory_var m_var;
bool m_is_int;
rational m_value;
@ -129,6 +129,7 @@ class theory_lra::imp {
struct scope {
unsigned m_bounds_lim;
unsigned m_idiv_lim;
unsigned m_asserted_qhead;
unsigned m_asserted_atoms_lim;
unsigned m_underspecified_lim;
@ -146,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(); }
};
@ -154,6 +155,7 @@ class theory_lra::imp {
ast_manager& m;
theory_arith_params& m_arith_params;
arith_util a;
bool m_has_int;
arith_eq_adapter m_arith_eq_adapter;
vector<rational> m_columns;
@ -163,13 +165,13 @@ class theory_lra::imp {
expr_ref_vector m_terms;
vector<rational> m_coeffs;
svector<theory_var> m_vars;
rational m_coeff;
rational m_offset;
ptr_vector<expr> m_terms_to_internalize;
internalize_state(ast_manager& m): m_terms(m) {}
void reset() {
m_terms.reset();
m_coeffs.reset();
m_coeff.reset();
m_offset.reset();
m_vars.reset();
m_terms_to_internalize.reset();
}
@ -195,7 +197,7 @@ class theory_lra::imp {
expr_ref_vector& terms() { return m_st.m_terms; }
vector<rational>& coeffs() { return m_st.m_coeffs; }
svector<theory_var>& vars() { return m_st.m_vars; }
rational& coeff() { return m_st.m_coeff; }
rational& offset() { return m_st.m_offset; }
ptr_vector<expr>& terms_to_internalize() { return m_st.m_terms_to_internalize; }
void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); }
void set_back(unsigned i) {
@ -214,6 +216,10 @@ class theory_lra::imp {
svector<theory_var> m_term_index2theory_var; // reverse map from lp_solver variables to theory variables
var_coeffs m_left_side; // constraint left side
mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model
lp::var_index m_one_var;
lp::var_index m_zero_var;
lp::var_index m_rone_var;
lp::var_index m_rzero_var;
enum constraint_source {
inequality_source,
@ -229,6 +235,7 @@ class theory_lra::imp {
svector<delayed_atom> m_asserted_atoms;
expr* m_not_handled;
ptr_vector<app> m_underspecified;
ptr_vector<expr> m_idiv_terms;
unsigned_vector m_var_trail;
vector<ptr_vector<lp_api::bound> > m_use_list; // bounds where variables are used.
@ -328,6 +335,31 @@ class theory_lra::imp {
}
}
lp::var_index add_const(int c, lp::var_index& var, bool is_int) {
if (var != UINT_MAX) {
return var;
}
app_ref cnst(a.mk_numeral(rational(c), is_int), m);
TRACE("arith", tout << "add " << cnst << "\n";);
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);
m_var_index2theory_var.setx(var, v, UINT_MAX);
m_var_trail.push_back(v);
add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c)));
add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c)));
return var;
}
lp::var_index get_one(bool is_int) {
return add_const(1, is_int ? m_one_var : m_rone_var, is_int);
}
lp::var_index get_zero(bool is_int) {
return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int);
}
void found_not_handled(expr* n) {
m_not_handled = n;
@ -372,7 +404,7 @@ class theory_lra::imp {
expr_ref_vector & terms = st.terms();
svector<theory_var>& vars = st.vars();
vector<rational>& coeffs = st.coeffs();
rational& coeff = st.coeff();
rational& offset = st.offset();
rational r;
expr* n1, *n2;
unsigned index = 0;
@ -412,7 +444,7 @@ class theory_lra::imp {
++index;
}
else if (a.is_numeral(n, r)) {
coeff += coeffs[index]*r;
offset += coeffs[index]*r;
++index;
}
else if (a.is_uminus(n, n1)) {
@ -424,7 +456,6 @@ class theory_lra::imp {
app* t = to_app(n);
internalize_args(t);
mk_enode(t);
theory_var v = mk_var(n);
coeffs[vars.size()] = coeffs[index];
vars.push_back(v);
@ -442,6 +473,7 @@ class theory_lra::imp {
}
else if (a.is_idiv(n, n1, n2)) {
if (!a.is_numeral(n2, r) || r.is_zero()) found_not_handled(n);
m_idiv_terms.push_back(n);
app * mod = a.mk_mod(n1, n2);
ctx().internalize(mod, false);
if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod);
@ -451,6 +483,7 @@ class theory_lra::imp {
if (!is_num) {
found_not_handled(n);
}
#if 0
else {
app_ref div(a.mk_idiv(n1, n2), m);
mk_enode(div);
@ -461,7 +494,8 @@ class theory_lra::imp {
// abs(r) > v >= 0
assert_idiv_mod_axioms(u, v, w, r);
}
if (!ctx().relevancy() && !is_num) mk_idiv_mod_axioms(n1, n2);
#endif
if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2);
}
else if (a.is_rem(n, n1, n2)) {
if (!a.is_numeral(n2, r) || r.is_zero()) found_not_handled(n);
@ -544,6 +578,7 @@ class theory_lra::imp {
}
enode * mk_enode(app * n) {
TRACE("arith", tout << expr_ref(n, m) << "\n";);
if (ctx().e_internalized(n)) {
return get_enode(n);
}
@ -624,6 +659,7 @@ class theory_lra::imp {
}
if (result == UINT_MAX) {
result = m_solver->add_var(v, is_int(v));
m_has_int |= is_int(v);
m_theory_var2var_index.setx(v, result, UINT_MAX);
m_var_index2theory_var.setx(result, v, UINT_MAX);
m_var_trail.push_back(v);
@ -677,7 +713,7 @@ class theory_lra::imp {
m_constraint_sources.setx(index, inequality_source, null_source);
m_inequalities.setx(index, lit, null_literal);
++m_stats.m_add_rows;
TRACE("arith", m_solver->print_constraint(index, tout); tout << "\n";);
TRACE("arith", m_solver->print_constraint(index, tout) << "\n";);
}
void add_def_constraint(lp::constraint_index index) {
@ -692,9 +728,7 @@ class theory_lra::imp {
++m_stats.m_add_rows;
}
void internalize_eq(theory_var v1, theory_var v2) {
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
void internalize_eq(theory_var v1, theory_var v2) {
app_ref term(m.mk_fresh_const("eq", a.mk_real()), m);
scoped_internalize_state st(*this);
st.vars().push_back(v1);
@ -707,8 +741,8 @@ class theory_lra::imp {
add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero()));
TRACE("arith",
{
expr* o1 = n1->get_owner();
expr* o2 = n2->get_owner();
expr* o1 = get_enode(v1)->get_owner();
expr* o2 = get_enode(v2)->get_owner();
tout << "v" << v1 << " = " << "v" << v2 << ": "
<< mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";
});
@ -733,10 +767,19 @@ class theory_lra::imp {
}
bool is_unit_var(scoped_internalize_state& st) {
return st.coeff().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one();
return st.offset().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one();
}
bool is_one(scoped_internalize_state& st) {
return st.offset().is_one() && st.vars().empty();
}
bool is_zero(scoped_internalize_state& st) {
return st.offset().is_zero() && st.vars().empty();
}
theory_var internalize_def(app* term, scoped_internalize_state& st) {
TRACE("arith", tout << expr_ref(term, m) << "\n";);
if (ctx().e_internalized(term)) {
IF_VERBOSE(0, verbose_stream() << "repeated term\n";);
return mk_var(term, false);
@ -766,13 +809,24 @@ class theory_lra::imp {
if (is_unit_var(st)) {
return st.vars()[0];
}
else if (is_one(st)) {
return get_one(a.is_int(term));
}
else if (is_zero(st)) {
return get_zero(a.is_int(term));
}
else {
init_left_side(st);
theory_var v = mk_var(term);
lp::var_index vi = m_theory_var2var_index.get(v, UINT_MAX);
TRACE("arith", tout << mk_pp(term, m) << " " << v << " " << vi << "\n";);
TRACE("arith", tout << mk_pp(term, m) << " v" << v << "\n";);
if (vi == UINT_MAX) {
vi = m_solver->add_term(m_left_side, st.coeff());
rational const& offset = st.offset();
if (!offset.is_zero()) {
m_left_side.push_back(std::make_pair(offset, get_one(a.is_int(term))));
}
SASSERT(!m_left_side.empty());
vi = m_solver->add_term(m_left_side);
m_theory_var2var_index.setx(v, vi, UINT_MAX);
if (m_solver->is_term(vi)) {
m_term_index2theory_var.setx(m_solver->adjust_term_index(vi), v, UINT_MAX);
@ -782,7 +836,7 @@ class theory_lra::imp {
}
m_var_trail.push_back(v);
TRACE("arith_verbose", tout << "v" << v << " := " << mk_pp(term, m) << " slack: " << vi << " scopes: " << m_scopes.size() << "\n";
m_solver->print_term(m_solver->get_term(vi), tout); tout << "\n";);
m_solver->print_term(m_solver->get_term(vi), tout) << "\n";);
}
rational val;
if (a.is_numeral(term, val)) {
@ -798,9 +852,14 @@ public:
th(th), m(m),
m_arith_params(ap),
a(m),
m_has_int(false),
m_arith_eq_adapter(th, ap, a),
m_internalize_head(0),
m_not_handled(0),
m_one_var(UINT_MAX),
m_zero_var(UINT_MAX),
m_rone_var(UINT_MAX),
m_rzero_var(UINT_MAX),
m_not_handled(nullptr),
m_asserted_qhead(0),
m_assume_eq_head(0),
m_num_conflicts(0),
@ -871,16 +930,18 @@ public:
}
return true;
}
bool is_arith(enode* n) {
return n && n->get_th_var(get_id()) != null_theory_var;
}
void internalize_eq_eh(app * atom, bool_var) {
expr* lhs = 0, *rhs = 0;
TRACE("arith_verbose", tout << mk_pp(atom, m) << "\n";);
expr* lhs = nullptr, *rhs = nullptr;
VERIFY(m.is_eq(atom, lhs, rhs));
enode * n1 = get_enode(lhs);
enode * n2 = get_enode(rhs);
if (n1->get_th_var(get_id()) != null_theory_var &&
n2->get_th_var(get_id()) != null_theory_var &&
n1 != n2) {
TRACE("arith_verbose", tout << mk_pp(atom, m) << "\n";);
if (is_arith(n1) && is_arith(n2) && n1 != n2) {
m_arith_eq_adapter.mk_axioms(n1, n2);
}
}
@ -910,6 +971,7 @@ public:
scope& s = m_scopes.back();
s.m_bounds_lim = m_bounds_trail.size();
s.m_asserted_qhead = m_asserted_qhead;
s.m_idiv_lim = m_idiv_terms.size();
s.m_asserted_atoms_lim = m_asserted_atoms.size();
s.m_not_handled = m_not_handled;
s.m_underspecified_lim = m_underspecified.size();
@ -935,6 +997,7 @@ public:
}
m_theory_var2var_index[m_var_trail[i]] = UINT_MAX;
}
m_idiv_terms.shrink(m_scopes[old_size].m_idiv_lim);
m_asserted_atoms.shrink(m_scopes[old_size].m_asserted_atoms_lim);
m_asserted_qhead = m_scopes[old_size].m_asserted_qhead;
m_underspecified.shrink(m_scopes[old_size].m_underspecified_lim);
@ -991,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));
@ -1007,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);
@ -1030,37 +1093,74 @@ public:
add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero()));
add_def_constraint(m_solver->add_var_bound(get_var_index(v), lp::GE, rational::zero()));
add_def_constraint(m_solver->add_var_bound(get_var_index(v), lp::LT, abs(r)));
TRACE("arith", m_solver->print_constraints(tout << term << "\n"););
}
void mk_idiv_mod_axioms(expr * p, expr * q) {
if (a.is_zero(q)) {
return;
}
TRACE("arith", tout << expr_ref(p, m) << " " << expr_ref(q, m) << "\n";);
// if q is zero, then idiv and mod are uninterpreted functions.
expr_ref div(a.mk_idiv(p, q), m);
expr_ref mod(a.mk_mod(p, q), m);
expr_ref zero(a.mk_int(0), m);
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
literal q_le_0 = mk_literal(a.mk_le(q, zero));
// literal eqz = th.mk_eq(q, zero, false);
literal eq = th.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p, false);
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
// q >= 0 or p = (p mod q) + q * (p div q)
// q <= 0 or p = (p mod q) + q * (p div q)
// q >= 0 or (p mod q) >= 0
// q <= 0 or (p mod q) >= 0
// q <= 0 or (p mod q) < q
// q >= 0 or (p mod q) < -q
// enable_trace("mk_bool_var");
mk_axiom(q_ge_0, eq);
mk_axiom(q_le_0, eq);
mk_axiom(q_ge_0, mod_ge_0);
mk_axiom(q_le_0, mod_ge_0);
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
rational k;
if (m_arith_params.m_arith_enum_const_mod && a.is_numeral(q, k) &&
k.is_pos() && k < rational(8)) {
literal div_ge_0 = mk_literal(a.mk_ge(div, zero));
literal div_le_0 = mk_literal(a.mk_le(div, zero));
literal p_ge_0 = mk_literal(a.mk_ge(p, zero));
literal p_le_0 = mk_literal(a.mk_le(p, zero));
rational k(0);
expr_ref upper(m);
if (a.is_numeral(q, k)) {
if (k.is_pos()) {
upper = a.mk_numeral(k - 1, true);
}
else if (k.is_neg()) {
upper = a.mk_numeral(-k - 1, true);
}
}
else {
k = rational::zero();
}
if (!k.is_zero()) {
mk_axiom(eq);
mk_axiom(mod_ge_0);
mk_axiom(mk_literal(a.mk_le(mod, upper)));
if (k.is_pos()) {
mk_axiom(~p_ge_0, div_ge_0);
mk_axiom(~p_le_0, div_le_0);
}
else {
mk_axiom(~p_ge_0, div_le_0);
mk_axiom(~p_le_0, div_ge_0);
}
}
else {
// q >= 0 or p = (p mod q) + q * (p div q)
// q <= 0 or p = (p mod q) + q * (p div q)
// q >= 0 or (p mod q) >= 0
// q <= 0 or (p mod q) >= 0
// q <= 0 or (p mod q) < q
// q >= 0 or (p mod q) < -q
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
literal q_le_0 = mk_literal(a.mk_le(q, zero));
mk_axiom(q_ge_0, eq);
mk_axiom(q_le_0, eq);
mk_axiom(q_ge_0, mod_ge_0);
mk_axiom(q_le_0, mod_ge_0);
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
mk_axiom(q_le_0, ~p_ge_0, div_ge_0);
mk_axiom(q_le_0, ~p_le_0, div_le_0);
mk_axiom(q_ge_0, ~p_ge_0, div_le_0);
mk_axiom(q_ge_0, ~p_le_0, div_ge_0);
}
if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
unsigned _k = k.get_unsigned();
literal_buffer lits;
for (unsigned j = 0; j < _k; ++j) {
@ -1152,7 +1252,6 @@ public:
m_todo_terms.pop_back();
if (m_solver->is_term(vi)) {
const lp::lar_term& term = m_solver->get_term(vi);
result += term.m_v * coeff;
for (const auto & i: term) {
m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
}
@ -1189,7 +1288,6 @@ public:
m_todo_terms.pop_back();
if (m_solver->is_term(wi)) {
const lp::lar_term& term = m_solver->get_term(wi);
result += term.m_v * coeff;
for (const auto & i : term) {
if (m_variable_values.count(i.var()) > 0) {
result += m_variable_values[i.var()] * coeff * i.coeff();
@ -1208,10 +1306,10 @@ public:
}
void init_variable_values() {
reset_variable_values();
if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
reset_variable_values();
TRACE("arith", tout << "update variable values\n";);
m_solver->get_model(m_variable_values);
TRACE("arith", display(tout););
}
}
@ -1314,6 +1412,7 @@ public:
}
final_check_status final_check_eh() {
IF_VERBOSE(2, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
m_use_nra_model = false;
lbool is_sat = l_true;
if (m_solver->get_status() != lp::lp_status::OPTIMAL) {
@ -1328,7 +1427,7 @@ public:
}
if (assume_eqs()) {
return FC_CONTINUE;
}
}
switch (check_lia()) {
case l_true:
@ -1340,7 +1439,7 @@ public:
st = FC_CONTINUE;
break;
}
switch (check_nra()) {
case l_true:
break;
@ -1351,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;
}
@ -1378,6 +1477,18 @@ public:
u_map<rational> coeffs;
term2coeffs(term, coeffs, rational::one(), offset);
offset.neg();
TRACE("arith",
m_solver->print_term(term, tout << "term: ") << "\n";
for (auto const& kv : coeffs) {
tout << "v" << kv.m_key << " * " << kv.m_value << "\n";
}
tout << offset << "\n";
rational g(0);
for (auto const& kv : coeffs) {
g = gcd(g, kv.m_value);
}
tout << "gcd: " << g << "\n";
);
if (is_int) {
// 3x + 6y >= 5 -> x + 3y >= 5/3, then x + 3y >= 2
// 3x + 6y <= 5 -> x + 3y <= 1
@ -1385,10 +1496,12 @@ public:
rational g = gcd_reduce(coeffs);
if (!g.is_one()) {
if (lower_bound) {
offset = div(offset + g - rational::one(), g);
TRACE("arith", tout << "lower: " << offset << " / " << g << " = " << offset / g << " >= " << ceil(offset / g) << "\n";);
offset = ceil(offset / g);
}
else {
offset = div(offset, g);
TRACE("arith", tout << "upper: " << offset << " / " << g << " = " << offset / g << " <= " << floor(offset / g) << "\n";);
offset = floor(offset / g);
}
}
}
@ -1408,27 +1521,246 @@ public:
}
TRACE("arith", tout << t << ": " << atom << "\n";
m_solver->print_term(term, tout << "bound atom: "); tout << (lower_bound?" >= ":" <= ") << k << "\n";);
m_solver->print_term(term, tout << "bound atom: ") << (lower_bound?" >= ":" <= ") << k << "\n";);
ctx().internalize(atom, true);
ctx().mark_as_relevant(atom.get());
return atom;
}
bool make_sure_all_vars_have_bounds() {
if (!m_has_int) {
return true;
}
unsigned nv = std::min(th.get_num_vars(), m_theory_var2var_index.size());
bool all_bounded = true;
for (unsigned v = 0; v < nv; ++v) {
lp::var_index vi = m_theory_var2var_index[v];
if (vi == UINT_MAX)
continue;
if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) {
lp::lar_term term;
term.add_monomial(rational::one(), vi);
app_ref b = mk_bound(term, rational::zero(), true);
TRACE("arith", tout << "added bound " << b << "\n";);
IF_VERBOSE(2, verbose_stream() << "bound: " << b << "\n");
all_bounded = false;
}
}
return all_bounded;
}
/**
* n = (div p q)
*
* (div p q) * q + (mod p q) = p, (mod p q) >= 0
*
* 0 < q => (p/q <= v(p)/v(q) => n <= floor(v(p)/v(q)))
* 0 < q => (v(p)/v(q) <= p/q => v(p)/v(q) - 1 < n)
*
*/
bool check_idiv_bounds() {
if (m_idiv_terms.empty()) {
return true;
}
bool all_divs_valid = true;
init_variable_values();
for (expr* n : m_idiv_terms) {
expr* p = nullptr, *q = nullptr;
VERIFY(a.is_idiv(n, p, q));
theory_var v = mk_var(n);
theory_var v1 = mk_var(p);
rational r1 = get_value(v1);
rational r2;
if (!r1.is_int() || r1.is_neg()) {
// TBD
// r1 = 223/4, r2 = 2, r = 219/8
// take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0
// then
// p/q <= ceil(r1)/floor(r2) => n <= div(ceil(r1), floor(r2))
// p/q >= floor(r1)/ceil(r2) => n >= div(floor(r1), ceil(r2))
continue;
}
if (a.is_numeral(q, r2) && r2.is_pos()) {
if (get_value(v) == div(r1, r2)) continue;
rational div_r = div(r1, r2);
// p <= q * div(r1, q) + q - 1 => div(p, q) <= div(r1, r2)
// p >= q * div(r1, q) => div(r1, q) <= div(p, q)
rational mul(1);
rational hi = r2 * div_r + r2 - 1;
rational lo = r2 * div_r;
// used to normalize inequalities so they
// don't appear as 8*x >= 15, but x >= 2
expr *n1 = nullptr, *n2 = nullptr;
if (a.is_mul(p, n1, n2) && is_numeral(n1, mul) && mul.is_pos()) {
p = n2;
hi = floor(hi/mul);
lo = ceil(lo/mul);
}
literal p_le_r1 = mk_literal(a.mk_le(p, a.mk_numeral(hi, true)));
literal p_ge_r1 = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true)));
literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true)));
literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true)));
mk_axiom(~p_le_r1, n_le_div);
mk_axiom(~p_ge_r1, n_ge_div);
all_divs_valid = false;
TRACE("arith",
tout << r1 << " div " << r2 << "\n";
literal_vector lits;
lits.push_back(~p_le_r1);
lits.push_back(n_le_div);
ctx().display_literals_verbose(tout, lits) << "\n\n";
lits[0] = ~p_ge_r1;
lits[1] = n_ge_div;
ctx().display_literals_verbose(tout, lits) << "\n";);
continue;
}
#if 0
// TBD similar for non-linear division.
// better to deal with in nla_solver:
all_divs_valid = false;
//
// p/q <= r1/r2 => n <= div(r1, r2)
// <=>
// p*r2 <= q*r1 => n <= div(r1, r2)
//
// p/q >= r1/r2 => n >= div(r1, r2)
// <=>
// p*r2 >= r1*q => n >= div(r1, r2)
//
expr_ref zero(a.mk_int(0), m);
expr_ref divc(a.mk_numeral(div(r1, r2), true), m);
expr_ref pqr(a.mk_sub(a.mk_mul(a.mk_numeral(r2, true), p), a.mk_mul(a.mk_numeral(r1, true), q)), m);
literal pq_lhs = ~mk_literal(a.mk_le(pqr, zero));
literal pq_rhs = ~mk_literal(a.mk_ge(pqr, zero));
literal n_le_div = mk_literal(a.mk_le(n, divc));
literal n_ge_div = mk_literal(a.mk_ge(n, divc));
mk_axiom(pq_lhs, n_le_div);
mk_axiom(pq_rhs, n_ge_div);
TRACE("arith",
literal_vector lits;
lits.push_back(pq_lhs);
lits.push_back(n_le_div);
ctx().display_literals_verbose(tout, lits) << "\n";
lits[0] = pq_rhs;
lits[1] = n_ge_div;
ctx().display_literals_verbose(tout, lits) << "\n";);
#endif
}
return all_divs_valid;
}
expr_ref var2expr(lp::var_index v) {
std::ostringstream name;
name << "v" << m_solver->local2external(v);
return expr_ref(m.mk_const(symbol(name.str().c_str()), a.mk_int()), m);
}
expr_ref multerm(rational const& r, expr* e) {
if (r.is_one()) return expr_ref(e, m);
return expr_ref(a.mk_mul(a.mk_numeral(r, true), e), m);
}
expr_ref term2expr(lp::lar_term const& term) {
expr_ref t(m);
expr_ref_vector ts(m);
for (auto const& p : term) {
lp::var_index wi = p.var();
if (m_solver->is_term(wi)) {
ts.push_back(multerm(p.coeff(), term2expr(m_solver->get_term(wi))));
}
else {
ts.push_back(multerm(p.coeff(), var2expr(wi)));
}
}
if (ts.size() == 1) {
t = ts.back();
}
else {
t = a.mk_add(ts.size(), ts.c_ptr());
}
return t;
}
expr_ref constraint2fml(lp::constraint_index ci) {
lp::lar_base_constraint const& c = *m_solver->constraints()[ci];
expr_ref fml(m);
expr_ref_vector ts(m);
rational rhs = c.m_right_side;
for (auto cv : c.get_left_side_coefficients()) {
ts.push_back(multerm(cv.first, var2expr(cv.second)));
}
switch (c.m_kind) {
case lp::LE: fml = a.mk_le(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
case lp::LT: fml = a.mk_lt(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
case lp::GE: fml = a.mk_ge(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
case lp::GT: fml = a.mk_gt(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
case lp::EQ: fml = m.mk_eq(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
}
return fml;
}
void dump_cut_lemma(std::ostream& out, lp::lar_term const& term, lp::mpq const& k, lp::explanation const& ex, bool upper) {
m_solver->print_term(term, out << "bound: ");
out << (upper?" <= ":" >= ") << k << "\n";
for (auto const& p : term) {
lp::var_index wi = p.var();
out << p.coeff() << " * ";
if (m_solver->is_term(wi)) {
m_solver->print_term(m_solver->get_term(wi), out) << "\n";
}
else {
out << "v" << m_solver->local2external(wi) << "\n";
}
}
for (auto const& ev : ex.m_explanation) {
m_solver->print_constraint(ev.second, out << ev.first << ": ");
}
expr_ref_vector fmls(m);
for (auto const& ev : ex.m_explanation) {
fmls.push_back(constraint2fml(ev.second));
}
expr_ref t(term2expr(term), m);
if (upper) {
fmls.push_back(m.mk_not(a.mk_ge(t, a.mk_numeral(k, true))));
}
else {
fmls.push_back(m.mk_not(a.mk_le(t, a.mk_numeral(k, true))));
}
ast_pp_util visitor(m);
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
out << "(check-sat)\n";
}
lbool check_lia() {
if (m.canceled()) {
TRACE("arith", tout << "canceled\n";);
return l_undef;
}
lp::lar_term term;
lp::mpq k;
lp::explanation ex; // TBD, this should be streamlined accross different explanations
bool upper;
switch(m_lia->check(term, k, ex, upper)) {
if (!check_idiv_bounds()) {
TRACE("arith", tout << "idiv bounds check\n";);
return l_false;
}
m_explanation.reset();
switch (m_lia->check()) {
case lp::lia_move::sat:
return l_true;
case lp::lia_move::branch: {
TRACE("arith", tout << "branch\n";);
app_ref b = mk_bound(term, k, !upper);
app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";);
// branch on term >= k + 1
// branch on term <= k
// TBD: ctx().force_phase(ctx().get_literal(b));
@ -1440,11 +1772,13 @@ public:
TRACE("arith", tout << "cut\n";);
++m_stats.m_gomory_cuts;
// m_explanation implies term <= k
app_ref b = mk_bound(term, k, !upper);
app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n");
TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper()););
m_eqs.reset();
m_core.reset();
m_params.reset();
for (auto const& ev : ex.m_explanation) {
for (auto const& ev : m_lia->get_explanation().m_explanation) {
if (!ev.first.is_zero()) {
set_evidence(ev.second);
}
@ -1457,8 +1791,9 @@ public:
return l_false;
}
case lp::lia_move::conflict:
TRACE("arith", tout << "conflict\n";);
// ex contains unsat core
m_explanation = ex.m_explanation;
m_explanation = m_lia->get_explanation().m_explanation;
set_conflict1();
return l_false;
case lp::lia_move::undef:
@ -1744,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(
@ -1804,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;
@ -2062,18 +2397,18 @@ public:
SASSERT(!bounds.empty());
if (bounds.size() == 1) return;
if (m_unassigned_bounds[v] == 0) return;
bool v_is_int = is_int(v);
literal lit1(bv, !is_true);
literal lit2 = null_literal;
bool find_glb = (is_true == (k == lp_api::lower_t));
TRACE("arith", tout << "find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
if (find_glb) {
rational glb;
lp_api::bound* lb = 0;
for (unsigned i = 0; i < bounds.size(); ++i) {
lp_api::bound* b2 = bounds[i];
lp_api::bound* lb = nullptr;
for (lp_api::bound* b2 : bounds) {
if (b2 == &b) continue;
rational const& val2 = b2->get_value();
if ((is_true ? val2 < val : val2 <= val) && (!lb || glb < val2)) {
if (((is_true || v_is_int) ? val2 < val : val2 <= val) && (!lb || glb < val2)) {
lb = b2;
glb = val2;
}
@ -2084,12 +2419,11 @@ public:
}
else {
rational lub;
lp_api::bound* ub = 0;
for (unsigned i = 0; i < bounds.size(); ++i) {
lp_api::bound* b2 = bounds[i];
lp_api::bound* ub = nullptr;
for (lp_api::bound* b2 : bounds) {
if (b2 == &b) continue;
rational const& val2 = b2->get_value();
if ((is_true ? val < val2 : val <= val2) && (!ub || val2 < lub)) {
if (((is_true || v_is_int) ? val < val2 : val <= val2) && (!ub || val2 < lub)) {
ub = b2;
lub = val2;
}
@ -2107,7 +2441,7 @@ public:
m_params.reset();
m_core.reset();
m_eqs.reset();
m_core.push_back(lit2);
m_core.push_back(lit1);
m_params.push_back(parameter(symbol("farkas")));
m_params.push_back(parameter(rational(1)));
m_params.push_back(parameter(rational(1)));
@ -2383,6 +2717,18 @@ public:
}
}
bool var_has_bound(lp::var_index vi, bool is_lower) {
bool is_strict = false;
rational b;
lp::constraint_index ci;
if (is_lower) {
return m_solver->has_lower_bound(vi, ci, b, is_strict);
}
else {
return m_solver->has_upper_bound(vi, ci, b, is_strict);
}
}
bool has_upper_bound(lp::var_index vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, false); }
bool has_lower_bound(lp::var_index vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, true); }
@ -2451,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) {
@ -2606,7 +2952,7 @@ public:
m_todo_terms.push_back(std::make_pair(vi, rational::one()));
TRACE("arith", tout << "v" << v << " := w" << vi << "\n";
m_solver->print_term(m_solver->get_term(vi), tout); tout << "\n";);
m_solver->print_term(m_solver->get_term(vi), tout) << "\n";);
m_nra->am().set(r, 0);
while (!m_todo_terms.empty()) {
@ -2614,13 +2960,13 @@ public:
vi = m_todo_terms.back().first;
m_todo_terms.pop_back();
lp::lar_term const& term = m_solver->get_term(vi);
TRACE("arith", m_solver->print_term(term, tout); tout << "\n";);
TRACE("arith", m_solver->print_term(term, tout) << "\n";);
scoped_anum r1(m_nra->am());
rational c1 = term.m_v * wcoeff;
rational c1(0);
m_nra->am().set(r1, c1.to_mpq());
m_nra->am().add(r, r1, r);
for (auto const & arg : term) {
lp::var_index wi = m_solver->local2external(arg.var());
lp::var_index wi = arg.var();
c1 = arg.coeff() * wcoeff;
if (m_solver->is_term(wi)) {
m_todo_terms.push_back(std::make_pair(wi, c1));
@ -2663,6 +3009,7 @@ public:
if (!can_get_bound(v)) return false;
lp::var_index vi = m_theory_var2var_index[v];
if (m_solver->has_value(vi, val)) {
TRACE("arith", tout << expr_ref(n->get_owner(), m) << " := " << val << "\n";);
if (is_int(n) && !val.is_int()) return false;
return true;
}
@ -2891,7 +3238,6 @@ public:
coeffs.find(w, c0);
coeffs.insert(w, c0 + ti.coeff() * coeff);
}
offset += coeff * term.m_v;
}
app_ref coeffs2app(u_map<rational> const& coeffs, rational const& offset, bool is_int) {
@ -2931,15 +3277,17 @@ public:
rational gcd_reduce(u_map<rational>& coeffs) {
rational g(0);
for (auto const& kv : coeffs) {
g = gcd(g, kv.m_value);
}
if (!g.is_one() && !g.is_zero()) {
for (auto& kv : coeffs) {
kv.m_value /= g;
}
}
return g;
for (auto const& kv : coeffs) {
g = gcd(g, kv.m_value);
}
if (g.is_zero())
return rational::one();
if (!g.is_one()) {
for (auto& kv : coeffs) {
kv.m_value /= g;
}
}
return g;
}
app_ref mk_obj(theory_var v) {
@ -2967,7 +3315,7 @@ public:
}
if (!ctx().b_internalized(b)) {
fm.hide(b->get_decl());
bool_var bv = ctx().mk_bool_var(b);
bool_var bv = ctx().mk_bool_var(b);
ctx().set_var_theory(bv, get_id());
// ctx().set_enode_flag(bv, true);
lp_api::bound_kind bkind = lp_api::bound_kind::lower_t;

2
src/smt/theory_lra.h
View file

@ -78,9 +78,9 @@ namespace smt {
model_value_proc * mk_value(enode * n, model_generator & mg) override;
bool get_value(enode* n, expr_ref& r) override;
bool get_value(enode* n, rational& r);
bool get_lower(enode* n, expr_ref& r);
bool get_upper(enode* n, expr_ref& r);
bool get_value(enode* n, rational& r);
bool get_lower(enode* n, rational& r, bool& is_strict);
bool get_upper(enode* n, rational& r, bool& is_strict);

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;

12
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());
@ -4588,10 +4588,10 @@ bool theory_seq::lower_bound2(expr* _e, rational& lo) {
theory_mi_arith* tha = get_th_arith<theory_mi_arith>(ctx, m_autil.get_family_id(), e);
if (!tha) {
theory_i_arith* thi = get_th_arith<theory_i_arith>(ctx, m_autil.get_family_id(), e);
if (!thi || !thi->get_lower(ctx.get_enode(e), _lo)) return false;
if (!thi || !thi->get_lower(ctx.get_enode(e), _lo) || !m_autil.is_numeral(_lo, lo)) return false;
}
enode *ee = ctx.get_enode(e);
if (!tha->get_lower(ee, _lo) || m_autil.is_numeral(_lo, lo)) {
if (tha && (!tha->get_lower(ee, _lo) || m_autil.is_numeral(_lo, lo))) {
enode *next = ee->get_next();
bool flag = false;
while (next != ee) {

1762
src/smt/theory_str.cpp
View file

File diff suppressed because it is too large Load diff

6
src/smt/theory_str.h
View file

@ -30,6 +30,7 @@
#include "smt/params/theory_str_params.h"
#include "smt/proto_model/value_factory.h"
#include "smt/smt_model_generator.h"
#include "smt/smt_arith_value.h"
#include<set>
#include<stack>
#include<vector>
@ -164,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) :
@ -546,6 +547,7 @@ protected:
void process_concat_eq_unroll(expr * concat, expr * unroll);
// regex automata and length-aware regex
void solve_regex_automata();
unsigned estimate_regex_complexity(expr * re);
unsigned estimate_regex_complexity_under_complement(expr * re);
unsigned estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2);
@ -580,6 +582,8 @@ protected:
bool can_concat_eq_str(expr * concat, zstring& str);
bool can_concat_eq_concat(expr * concat1, expr * concat2);
bool check_concat_len_in_eqc(expr * concat);
void check_eqc_empty_string(expr * lhs, expr * rhs);
void check_eqc_concat_concat(std::set<expr*> & eqc_concat_lhs, std::set<expr*> & eqc_concat_rhs);
bool check_length_consistency(expr * n1, expr * n2);
bool check_length_const_string(expr * n1, expr * constStr);
bool check_length_eq_var_concat(expr * n1, expr * n2);

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;