mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

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

Browse source
This commit is contained in:
jofleish 2022-08-15 12:08:51 -04:00
parent 5fc6c8151f 88f4664c65
commit 4d1362b6a3
14 changed files with 2081 additions and 1486 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -92,3 +92,4 @@ CMakeSettings.json
# Editor temp files
*.swp
.DS_Store
dbg/**

2
src/api/api_ast.cpp
View file

@ -1178,7 +1178,7 @@ extern "C" {
case OP_BSMOD: return Z3_OP_BSMOD;
case OP_BSDIV0: return Z3_OP_BSDIV0;
case OP_BUDIV0: return Z3_OP_BUDIV0;
case OP_BSREM0: return Z3_OP_BUREM0;
case OP_BSREM0: return Z3_OP_BSREM0;
case OP_BUREM0: return Z3_OP_BUREM0;
case OP_BSMOD0: return Z3_OP_BSMOD0;
case OP_ULEQ: return Z3_OP_ULEQ;

4
src/ast/array_decl_plugin.cpp
View file

@ -326,7 +326,9 @@ func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domai
}
sort * r = to_sort(s->get_parameter(i).get_ast());
parameter param(i);
return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT, 1, &param));
func_decl_info info(func_decl_info(m_family_id, OP_ARRAY_EXT, 1, &param));
info.set_commutative(true);
return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, info);
}

17
src/ast/decl_collector.cpp
View file

@ -48,6 +48,7 @@ bool decl_collector::is_bool(sort * s) {
}
void decl_collector::visit_func(func_decl * n) {
func_decl* g;
if (!m_visited.is_marked(n)) {
family_id fid = n->get_family_id();
if (fid == null_family_id)
@ -57,6 +58,8 @@ void decl_collector::visit_func(func_decl * n) {
recfun::util u(m());
m_todo.push_back(u.get_def(n).get_rhs());
}
else if (m_ar_util.is_as_array(n, g))
m_todo.push_back(g);
m_visited.mark(n, true);
m_trail.push_back(n);
}
@ -65,7 +68,8 @@ void decl_collector::visit_func(func_decl * n) {
decl_collector::decl_collector(ast_manager & m):
m_manager(m),
m_trail(m),
m_dt_util(m) {
m_dt_util(m),
m_ar_util(m) {
m_basic_fid = m_manager.get_basic_family_id();
m_dt_fid = m_dt_util.get_family_id();
recfun::util rec_util(m);
@ -156,8 +160,15 @@ void decl_collector::collect_deps(sort* s, sort_set& set) {
for (unsigned i = 0; i < num_cnstr; i++) {
func_decl * cnstr = m_dt_util.get_datatype_constructors(s)->get(i);
set.insert(cnstr->get_range());
for (unsigned j = 0; j < cnstr->get_arity(); ++j)
set.insert(cnstr->get_domain(j));
for (unsigned j = 0; j < cnstr->get_arity(); ++j) {
sort* n = cnstr->get_domain(j);
set.insert(n);
for (unsigned i = n->get_num_parameters(); i-- > 0; ) {
parameter const& p = n->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast()))
set.insert(to_sort(p.get_ast()));
}
}
}
}

2
src/ast/decl_collector.h
View file

@ -23,6 +23,7 @@ Revision History:
#include "util/lim_vector.h"
#include "ast/ast.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/array_decl_plugin.h"
class decl_collector {
ast_manager & m_manager;
@ -35,6 +36,7 @@ class decl_collector {
family_id m_basic_fid;
family_id m_dt_fid;
datatype_util m_dt_util;
array_util m_ar_util;
family_id m_rec_fid;
ptr_vector<ast> m_todo;

591
src/math/simplex/model_based_opt.cpp
View file

@ -27,7 +27,9 @@ std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
case opt::t_eq: return out << " = ";
case opt::t_lt: return out << " < ";
case opt::t_le: return out << " <= ";
case opt::t_divides: return out << " divides ";
case opt::t_mod: return out << " mod ";
case opt::t_div: return out << " div ";
}
return out;
}
@ -199,7 +201,9 @@ namespace opt {
// values satisfy constraints
PASSERT(index == 0 || r.m_type != t_lt || r.m_value.is_neg());
PASSERT(index == 0 || r.m_type != t_le || !r.m_value.is_pos());
PASSERT(index == 0 || r.m_type != t_mod || (mod(r.m_value, r.m_mod).is_zero()));
PASSERT(index == 0 || r.m_type != t_divides || (mod(r.m_value, r.m_mod).is_zero()));
PASSERT(index == 0 || r.m_type != t_mod || r.m_id < m_var2value.size());
PASSERT(index == 0 || r.m_type != t_div || r.m_id < m_var2value.size());
return true;
}
@ -454,9 +458,8 @@ namespace opt {
}
rational model_based_opt::row::get_coefficient(unsigned var_id) const {
if (m_vars.empty()) {
if (m_vars.empty())
return rational::zero();
}
unsigned lo = 0, hi = m_vars.size();
while (lo < hi) {
unsigned mid = lo + (hi - lo)/2;
@ -466,28 +469,23 @@ namespace opt {
lo = mid;
break;
}
if (id < var_id) {
if (id < var_id)
lo = mid + 1;
}
else {
else
hi = mid;
}
}
if (lo == m_vars.size()) {
if (lo == m_vars.size())
return rational::zero();
}
unsigned id = m_vars[lo].m_id;
if (id == var_id) {
if (id == var_id)
return m_vars[lo].m_coeff;
}
else {
else
return rational::zero();
}
}
model_based_opt::row& model_based_opt::row::normalize() {
#if 0
if (m_type == t_mod)
if (m_type == t_divides || m_type == t_mod || m_type == t_div)
return *this;
rational D(denominator(abs(m_coeff)));
if (D == 0)
@ -526,6 +524,9 @@ namespace opt {
//
// the resolvent is the same in all cases (simpler proof should exist)
//
// assume a1 < 0, -a1 = a2:
// t1 <= a2*div(t2, a2)
//
void model_based_opt::resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x) {
@ -537,7 +538,7 @@ namespace opt {
rational a2 = get_coefficient(row_dst, x);
if (is_int(x)) {
TRACE("opt",
tout << a1 << " " << a2 << ": ";
tout << x << ": " << a1 << " " << a2 << ": ";
display(tout, m_rows[row_dst]);
display(tout, m_rows[row_src]););
if (a1.is_pos() != a2.is_pos() || m_rows[row_src].m_type == opt::t_eq) {
@ -547,7 +548,7 @@ namespace opt {
mul(row_dst, abs(a1));
mul_add(false, row_dst, -abs(a2), row_src);
}
TRACE("opt", display(tout, m_rows[row_dst]););
TRACE("opt", display(tout << "result ", m_rows[row_dst]););
normalize(row_dst);
}
else {
@ -571,12 +572,13 @@ namespace opt {
rational a2 = get_coefficient(row_dst, x);
mul(row_dst, a1);
mul_add(false, row_dst, -a2, row_src);
normalize(row_dst);
SASSERT(get_coefficient(row_dst, x).is_zero());
}
// resolution for integer rows.
void model_based_opt::mul_add(
unsigned x, rational const& src_c, unsigned row_src, rational const& dst_c, unsigned row_dst) {
unsigned x, rational src_c, unsigned row_src, rational dst_c, unsigned row_dst) {
row& dst = m_rows[row_dst];
row const& src = m_rows[row_src];
SASSERT(is_int(x));
@ -593,17 +595,9 @@ namespace opt {
rational src_val = src.m_value - x_val*src_c;
rational distance = abs_src_c * dst_val + abs_dst_c * src_val + slack;
bool use_case1 = distance.is_nonpos() || abs_src_c.is_one() || abs_dst_c.is_one();
bool use_case2 = false && abs_src_c == abs_dst_c && src_c.is_pos() != dst_c.is_pos() && !abs_src_c.is_one() && t_le == dst.m_type && t_le == src.m_type;
bool use_case3 = false && src_c.is_pos() != dst_c.is_pos() && t_le == dst.m_type && t_le == src.m_type;
#if 0
if (distance.is_nonpos() && !abs_src_c.is_one() && !abs_dst_c.is_one()) {
unsigned r = copy_row(row_src);
mul_add(false, r, rational::one(), row_dst);
del_var(r, x);
add(r, slack);
TRACE("qe", tout << m_rows[r];);
SASSERT(!m_rows[r].m_value.is_pos());
}
#endif
if (use_case1) {
TRACE("opt", tout << "slack: " << slack << " " << src_c << " " << dst_val << " " << dst_c << " " << src_val << "\n";);
@ -614,6 +608,54 @@ namespace opt {
return;
}
if (use_case2 || use_case3) {
// case2:
// x*src_c + s <= 0
// -x*src_c + t <= 0
//
// -src_c*div(-s, src_c) + t <= 0
//
// Example:
// t <= 100*x <= s
// Then t <= 100*div(s, 100)
//
// case3:
// x*src_c + s <= 0
// -x*dst_c + t <= 0
// t <= x*dst_c, x*src_c <= -s ->
// t <= dst_c*div(-s, src_c) ->
// -dst_c*div(-s,src_c) + t <= 0
//
bool swapped = false;
if (src_c < 0) {
std::swap(row_src, row_dst);
std::swap(src_c, dst_c);
std::swap(abs_src_c, abs_dst_c);
swapped = true;
}
vector<var> src_coeffs, dst_coeffs;
rational src_coeff = m_rows[row_src].m_coeff;
rational dst_coeff = m_rows[row_dst].m_coeff;
for (auto const& v : m_rows[row_src].m_vars)
if (v.m_id != x)
src_coeffs.push_back(var(v.m_id, -v.m_coeff));
for (auto const& v : m_rows[row_dst].m_vars)
if (v.m_id != x)
dst_coeffs.push_back(v);
unsigned v = UINT_MAX;
if (src_coeffs.empty())
dst_coeff -= abs_dst_c*div(-src_coeff, abs_src_c);
else
v = add_div(src_coeffs, -src_coeff, abs_src_c);
if (v != UINT_MAX) dst_coeffs.push_back(var(v, -abs_dst_c));
if (swapped)
std::swap(row_src, row_dst);
retire_row(row_dst);
add_constraint(dst_coeffs, dst_coeff, t_le);
return;
}
//
// create finite disjunction for |b|.
// exists x, z in [0 .. |b|-2] . b*x + s + z = 0 && ax + t <= 0 && bx + s <= 0
@ -669,13 +711,15 @@ namespace opt {
}
void model_based_opt::mul(unsigned dst, rational const& c) {
if (c.is_one()) return;
if (c.is_one())
return;
row& r = m_rows[dst];
for (auto & v : r.m_vars) {
for (auto & v : r.m_vars)
v.m_coeff *= c;
}
r.m_mod *= c;
r.m_coeff *= c;
r.m_value *= c;
if (r.m_type != t_div && r.m_type != t_mod)
r.m_value *= c;
}
void model_based_opt::add(unsigned dst, rational const& c) {
@ -690,28 +734,18 @@ namespace opt {
r.m_value -= c;
}
void model_based_opt::del_var(unsigned dst, unsigned x) {
row& r = m_rows[dst];
unsigned j = 0;
for (var & v : r.m_vars) {
if (v.m_id == x) {
r.m_value -= eval(x)*r.m_coeff;
}
else {
r.m_vars[j++] = v;
}
}
r.m_vars.shrink(j);
}
void model_based_opt::normalize(unsigned row_id) {
row& r = m_rows[row_id];
if (r.m_vars.empty()) {
retire_row(row_id);
return;
}
if (r.m_type == t_mod) return;
if (r.m_type == t_divides)
return;
if (r.m_type == t_mod)
return;
if (r.m_type == t_div)
return;
rational g(abs(r.m_vars[0].m_coeff));
bool all_int = g.is_int();
for (unsigned i = 1; all_int && !g.is_one() && i < r.m_vars.size(); ++i) {
@ -741,9 +775,9 @@ namespace opt {
// set row1 <- row1 + c*row2
//
void model_based_opt::mul_add(bool same_sign, unsigned row_id1, rational const& c, unsigned row_id2) {
if (c.is_zero()) {
if (c.is_zero())
return;
}
m_new_vars.reset();
row& r1 = m_rows[row_id1];
@ -758,9 +792,8 @@ namespace opt {
for (; j < r2.m_vars.size(); ++j) {
m_new_vars.push_back(r2.m_vars[j]);
m_new_vars.back().m_coeff *= c;
if (row_id1 != m_objective_id) {
if (row_id1 != m_objective_id)
m_var2row_ids[r2.m_vars[j].m_id].push_back(row_id1);
}
}
break;
}
@ -772,9 +805,8 @@ namespace opt {
m_new_vars.back().m_coeff += c*r2.m_vars[j].m_coeff;
++i;
++j;
if (m_new_vars.back().m_coeff.is_zero()) {
if (m_new_vars.back().m_coeff.is_zero())
m_new_vars.pop_back();
}
}
else if (v1 < v2) {
m_new_vars.push_back(r1.m_vars[i]);
@ -783,9 +815,8 @@ namespace opt {
else {
m_new_vars.push_back(r2.m_vars[j]);
m_new_vars.back().m_coeff *= c;
if (row_id1 != m_objective_id) {
if (row_id1 != m_objective_id)
m_var2row_ids[r2.m_vars[j].m_id].push_back(row_id1);
}
++j;
}
}
@ -793,25 +824,21 @@ namespace opt {
r1.m_vars.swap(m_new_vars);
r1.m_value += c*r2.m_value;
if (!same_sign && r2.m_type == t_lt) {
if (!same_sign && r2.m_type == t_lt)
r1.m_type = t_lt;
}
else if (same_sign && r1.m_type == t_lt && r2.m_type == t_lt) {
else if (same_sign && r1.m_type == t_lt && r2.m_type == t_lt)
r1.m_type = t_le;
}
SASSERT(invariant(row_id1, r1));
}
void model_based_opt::display(std::ostream& out) const {
for (auto const& r : m_rows) {
for (auto const& r : m_rows)
display(out, r);
}
for (unsigned i = 0; i < m_var2row_ids.size(); ++i) {
unsigned_vector const& rows = m_var2row_ids[i];
out << i << ": ";
for (auto const& r : rows) {
for (auto const& r : rows)
out << r << " ";
}
out << "\n";
}
}
@ -819,33 +846,36 @@ namespace opt {
void model_based_opt::display(std::ostream& out, vector<var> const& vars, rational const& coeff) {
unsigned i = 0;
for (var const& v : vars) {
if (i > 0 && v.m_coeff.is_pos()) {
if (i > 0 && v.m_coeff.is_pos())
out << "+ ";
}
++i;
if (v.m_coeff.is_one()) {
if (v.m_coeff.is_one())
out << "v" << v.m_id << " ";
}
else {
else
out << v.m_coeff << "*v" << v.m_id << " ";
}
}
if (coeff.is_pos()) {
if (coeff.is_pos())
out << " + " << coeff << " ";
}
else if (coeff.is_neg()) {
else if (coeff.is_neg())
out << coeff << " ";
}
}
std::ostream& model_based_opt::display(std::ostream& out, row const& r) {
out << (r.m_alive?"a":"d") << " ";
display(out, r.m_vars, r.m_coeff);
if (r.m_type == opt::t_mod) {
switch (r.m_type) {
case opt::t_divides:
out << r.m_type << " " << r.m_mod << " = 0; value: " << r.m_value << "\n";
}
else {
break;
case opt::t_mod:
out << r.m_type << " " << r.m_mod << " = v" << r.m_id << " ; mod: " << mod(r.m_value, r.m_mod) << "\n";
break;
case opt::t_div:
out << r.m_type << " " << r.m_mod << " = v" << r.m_id << " ; div: " << div(r.m_value, r.m_mod) << "\n";
break;
default:
out << r.m_type << " 0; value: " << r.m_value << "\n";
break;
}
return out;
}
@ -910,32 +940,72 @@ namespace opt {
return row_id;
}
unsigned model_based_opt::copy_row(unsigned src) {
unsigned model_based_opt::copy_row(unsigned src, unsigned excl) {
unsigned dst = new_row();
row const& r = m_rows[src];
set_row(dst, r.m_vars, r.m_coeff, r.m_mod, r.m_type);
for (auto const& v : r.m_vars) {
m_var2row_ids[v.m_id].push_back(dst);
if (v.m_id != excl)
m_var2row_ids[v.m_id].push_back(dst);
}
SASSERT(invariant(dst, m_rows[dst]));
return dst;
}
void model_based_opt::add_lower_bound(unsigned x, rational const& lo) {
vector<var> coeffs;
coeffs.push_back(var(x, rational::minus_one()));
add_constraint(coeffs, lo, t_le);
}
void model_based_opt::add_upper_bound(unsigned x, rational const& hi) {
vector<var> coeffs;
coeffs.push_back(var(x, rational::one()));
add_constraint(coeffs, -hi, t_le);
}
void model_based_opt::add_constraint(vector<var> const& coeffs, rational const& c, ineq_type rel) {
add_constraint(coeffs, c, rational::zero(), rel);
add_constraint(coeffs, c, rational::zero(), rel, 0);
}
void model_based_opt::add_divides(vector<var> const& coeffs, rational const& c, rational const& m) {
add_constraint(coeffs, c, m, t_mod);
rational g(c);
for (auto const& [v, coeff] : coeffs)
g = gcd(coeff, g);
if ((g/m).is_int())
return;
add_constraint(coeffs, c, m, t_divides, 0);
}
void model_based_opt::add_constraint(vector<var> const& coeffs, rational const& c, rational const& m, ineq_type rel) {
unsigned model_based_opt::add_mod(vector<var> const& coeffs, rational const& c, rational const& m) {
rational value = c;
for (auto const& var : coeffs)
value += var.m_coeff * m_var2value[var.m_id];
unsigned v = add_var(mod(value, m), true);
add_constraint(coeffs, c, m, t_mod, v);
return v;
}
unsigned model_based_opt::add_div(vector<var> const& coeffs, rational const& c, rational const& m) {
rational value = c;
for (auto const& var : coeffs)
value += var.m_coeff * m_var2value[var.m_id];
unsigned v = add_var(div(value, m), true);
add_constraint(coeffs, c, m, t_div, v);
return v;
}
void model_based_opt::add_constraint(vector<var> const& coeffs, rational const& c, rational const& m, ineq_type rel, unsigned id) {
auto const& r = m_rows.back();
if (r.m_vars == coeffs && r.m_coeff == c && r.m_mod == m && r.m_type == rel && r.m_id == id && r.m_alive)
return;
unsigned row_id = new_row();
set_row(row_id, coeffs, c, m, rel);
for (var const& coeff : coeffs) {
m_rows[row_id].m_id = id;
for (var const& coeff : coeffs)
m_var2row_ids[coeff.m_id].push_back(row_id);
}
SASSERT(invariant(row_id, m_rows[row_id]));
normalize(row_id);
}
void model_based_opt::set_objective(vector<var> const& coeffs, rational const& c) {
@ -943,11 +1013,9 @@ namespace opt {
}
void model_based_opt::get_live_rows(vector<row>& rows) {
for (row & r : m_rows) {
if (r.m_alive) {
for (row & r : m_rows)
if (r.m_alive)
rows.push_back(r.normalize());
}
}
}
//
@ -971,7 +1039,9 @@ namespace opt {
model_based_opt::def model_based_opt::project(unsigned x, bool compute_def) {
unsigned_vector& lub_rows = m_lub;
unsigned_vector& glb_rows = m_glb;
unsigned_vector& divide_rows = m_divides;
unsigned_vector& mod_rows = m_mod;
unsigned_vector& div_rows = m_div;
unsigned lub_index = UINT_MAX, glb_index = UINT_MAX;
bool lub_strict = false, glb_strict = false;
rational lub_val, glb_val;
@ -980,7 +1050,9 @@ namespace opt {
uint_set visited;
lub_rows.reset();
glb_rows.reset();
divide_rows.reset();
mod_rows.reset();
div_rows.reset();
bool lub_is_unit = true, glb_is_unit = true;
unsigned eq_row = UINT_MAX;
// select the lub and glb.
@ -1001,9 +1073,12 @@ namespace opt {
eq_row = row_id;
continue;
}
if (r.m_type == t_mod) {
if (r.m_type == t_mod)
mod_rows.push_back(row_id);
}
else if (r.m_type == t_div)
div_rows.push_back(row_id);
else if (r.m_type == t_divides)
divide_rows.push_back(row_id);
else if (a.is_pos()) {
rational lub_value = x_val - (r.m_value/a);
if (lub_rows.empty() ||
@ -1031,13 +1106,17 @@ namespace opt {
}
}
if (!mod_rows.empty()) {
if (!mod_rows.empty())
return solve_mod(x, mod_rows, compute_def);
}
if (eq_row != UINT_MAX) {
if (!div_rows.empty())
return solve_div(x, div_rows, compute_def);
if (!divide_rows.empty())
return solve_divides(x, divide_rows, compute_def);
if (eq_row != UINT_MAX)
return solve_for(eq_row, x, compute_def);
}
def result;
unsigned lub_size = lub_rows.size();
@ -1047,15 +1126,12 @@ namespace opt {
// There are only upper or only lower bounds.
if (row_index == UINT_MAX) {
if (compute_def) {
if (lub_index != UINT_MAX) {
if (lub_index != UINT_MAX)
result = solve_for(lub_index, x, true);
}
else if (glb_index != UINT_MAX) {
else if (glb_index != UINT_MAX)
result = solve_for(glb_index, x, true);
}
else {
else
result = def() + m_var2value[x];
}
SASSERT(eval(result) == eval(x));
}
else {
@ -1068,12 +1144,10 @@ namespace opt {
SASSERT(lub_index != UINT_MAX);
SASSERT(glb_index != UINT_MAX);
if (compute_def) {
if (lub_size <= glb_size) {
if (lub_size <= glb_size)
result = def(m_rows[lub_index], x);
}
else {
else
result = def(m_rows[glb_index], x);
}
}
// The number of matching lower and upper bounds is small.
@ -1094,27 +1168,286 @@ namespace opt {
}
}
}
for (unsigned row_id : lub_rows) retire_row(row_id);
for (unsigned row_id : lub_rows)
retire_row(row_id);
return result;
}
// General case.
rational coeff = get_coefficient(row_index, x);
for (unsigned row_id : lub_rows) {
if (row_id != row_index) {
for (unsigned row_id : lub_rows)
if (row_id != row_index)
resolve(row_index, coeff, row_id, x);
}
}
for (unsigned row_id : glb_rows) {
if (row_id != row_index) {
for (unsigned row_id : glb_rows)
if (row_id != row_index)
resolve(row_index, coeff, row_id, x);
}
}
retire_row(row_index);
return result;
}
//
// Given v = a*x + b mod K
//
// - remove v = a*x + b mod K
//
// case a = 1:
// - add w = b mod K
// - x |-> K*y + z, 0 <= z < K
// - if z.value + w.value < K:
// add z + w - v = 0
// - if z.value + w.value >= K:
// add z + w - v - K = 0
//
// case a != 1, gcd(a, K) = 1
// - x |-> x*y + a^-1*z, 0 <= z < K
// - add w = b mod K
// if z.value + w.value < K
// add z + w - v = 0
// if z.value + w.value >= K
// add z + w - v - K = 0
//
// case a != 1, gcd(a,K) = g != 1
// - x |-> x*y + a^-1*z, 0 <= z < K
// a*x + b mod K = v is now
// g*z + b mod K = v
// - add w = b mod K
// - 0 <= g*z.value + w.value < K*(g+1)
// - add g*z + w - v - k*K = 0 for suitable k from 0 .. g based on model
//
model_based_opt::def model_based_opt::solve_mod(unsigned x, unsigned_vector const& _mod_rows, bool compute_def) {
def result;
unsigned_vector mod_rows(_mod_rows);
rational K(1);
for (unsigned ri : mod_rows)
K = lcm(K, m_rows[ri].m_mod);
rational x_value = m_var2value[x];
rational y_value = div(x_value, K);
rational z_value = mod(x_value, K);
SASSERT(x_value == K * y_value + z_value);
SASSERT(0 <= z_value && z_value < K);
// add new variables
unsigned z = add_var(z_value, true);
unsigned y = add_var(y_value, true);
uint_set visited;
for (unsigned ri : mod_rows) {
m_rows[ri].m_alive = false;
visited.insert(ri);
}
// replace x by K*y + z in other rows.
for (unsigned ri : m_var2row_ids[x]) {
if (visited.contains(ri))
continue;
replace_var(ri, x, K, y, rational::one(), z);
visited.insert(ri);
normalize(ri);
}
// add bounds for z
add_lower_bound(z, rational::zero());
add_upper_bound(z, K - 1);
for (unsigned ri : mod_rows) {
rational a = get_coefficient(ri, x);
// add w = b mod K
vector<var> coeffs = m_rows[ri].m_vars;
rational coeff = m_rows[ri].m_coeff;
unsigned v = m_rows[ri].m_id;
unsigned w = UINT_MAX;
rational offset(0);
if (coeffs.empty())
offset = mod(coeff, K);
else
w = add_mod(coeffs, coeff, K);
rational w_value = w == UINT_MAX ? offset : m_var2value[w];
// add v = a*z + w - k*K = 0, for k = (a*z_value + w_value) div K
// claim: (= (mod x K) (- x (* K (div x K)))))) is a theorem for every x, K != 0
rational kK = div(a * z_value + w_value, K) * K;
vector<var> mod_coeffs;
mod_coeffs.push_back(var(v, rational::minus_one()));
mod_coeffs.push_back(var(z, a));
if (w != UINT_MAX) mod_coeffs.push_back(var(w, rational::one()));
add_constraint(mod_coeffs, kK + offset, t_eq);
add_lower_bound(v, rational::zero());
add_upper_bound(v, K - 1);
// allow to recycle row.
m_retired_rows.push_back(ri);
project(v, false);
}
def y_def = project(y, compute_def);
def z_def = project(z, compute_def);
if (compute_def) {
result = (y_def * K) + z_def;
m_var2value[x] = eval(result);
}
TRACE("opt", display(tout << "solve_mod\n"));
return result;
}
//
// Given v = a*x + b div K
// Replace x |-> K*y + z
// - w = b div K
// - v = ((a*K*y + a*z) + b) div K
// = a*y + (a*z + b) div K
// = a*y + b div K + (b mod K + a*z) div K
// = a*y + b div K + k
// where k := (b.value mod K + a*z.value) div K
// k is between 0 and a
//
// - k*K <= b mod K + a*z < (k+1)*K
//
// A better version using a^-1
// - v = (a*K*y + a^-1*a*z + b) div K
// = a*y + ((K*A + g)*z + b) div K where we write a*a^-1 = K*A + g
// = a*y + A + (g*z + b) div K
// - k*K <= b Kod m + gz < (k+1)*K
// where k is between 0 and g
// when gcd(a, K) = 1, then there are only two cases.
//
model_based_opt::def model_based_opt::solve_div(unsigned x, unsigned_vector const& _div_rows, bool compute_def) {
def result;
unsigned_vector div_rows(_div_rows);
SASSERT(!div_rows.empty());
rational K(1);
for (unsigned ri : div_rows)
K = lcm(K, m_rows[ri].m_mod);
rational x_value = m_var2value[x];
rational z_value = mod(x_value, K);
rational y_value = div(x_value, K);
SASSERT(x_value == K * y_value + z_value);
SASSERT(0 <= z_value && z_value < K);
// add new variables
unsigned z = add_var(z_value, true);
unsigned y = add_var(y_value, true);
uint_set visited;
for (unsigned ri : div_rows) {
row& r = m_rows[ri];
mul(ri, K / r.m_mod);
r.m_alive = false;
visited.insert(ri);
}
// replace x by K*y + z in other rows.
for (unsigned ri : m_var2row_ids[x]) {
if (visited.contains(ri))
continue;
replace_var(ri, x, K, y, rational::one(), z);
visited.insert(ri);
normalize(ri);
}
// add bounds for z
add_lower_bound(z, rational::zero());
add_upper_bound(z, K - 1);
TRACE("opt", display(tout));
// solve for x_value = K*y_value + z_value, 0 <= z_value < K.
for (unsigned ri : div_rows) {
rational a = get_coefficient(ri, x);
replace_var(ri, x, rational::zero());
// add w = b div m
vector<var> coeffs = m_rows[ri].m_vars;
rational coeff = m_rows[ri].m_coeff;
unsigned w = UINT_MAX;
rational offset(0);
if (coeffs.empty())
offset = div(coeff, K);
else
w = add_div(coeffs, coeff, K);
//
// w = b div K
// v = a*y + w + k
// k = (a*z_value + (b_value mod K)) div K
// k*K <= a*z + b mod K < (k+1)*K
//
/**
* It is based on the following claim (tested for select values of a, K)
* (define-const K Int 13)
* (declare-const b Int)
* (define-const a Int -11)
* (declare-const y Int)
* (declare-const z Int)
* (define-const w Int (div b K))
* (define-const k1 Int (+ (* a z) (mod b K)))
* (define-const k Int (div k1 K))
* (define-const x Int (+ (* K y) z))
* (define-const u Int (+ (* a x) b))
* (define-const v Int (+ (* a y) w k))
* (assert (<= 0 z))
* (assert (< z K))
* (assert (<= (* K k) k1))
* (assert (< k1 (* K (+ k 1))))
* (assert (not (= (div u K) v)))
* (check-sat)
*/
unsigned v = m_rows[ri].m_id;
rational b_value = eval(coeffs) + coeff;
rational k = div(a * z_value + mod(b_value, K), K);
vector<var> div_coeffs;
div_coeffs.push_back(var(v, rational::minus_one()));
div_coeffs.push_back(var(y, a));
if (w != UINT_MAX) div_coeffs.push_back(var(w, rational::one()));
add_constraint(div_coeffs, k + offset, t_eq);
unsigned u = UINT_MAX;
offset = 0;
if (coeffs.empty())
offset = mod(coeff, K);
else
u = add_mod(coeffs, coeff, K);
// add a*z + (b mod K) < (k + 1)*K
vector<var> bound_coeffs;
bound_coeffs.push_back(var(z, a));
if (u != UINT_MAX) bound_coeffs.push_back(var(u, rational::one()));
add_constraint(bound_coeffs, 1 - K * (k + 1) + offset, t_le);
// add k*K <= az + (b mod K)
for (auto& c : bound_coeffs)
c.m_coeff.neg();
add_constraint(bound_coeffs, k * K - offset, t_le);
// allow to recycle row.
m_retired_rows.push_back(ri);
project(v, false);
}
TRACE("opt", display(tout << "solve_div reduced " << y << " " << z << "\n"));
// project internal variables.
def y_def = project(y, compute_def);
def z_def = project(z, compute_def);
if (compute_def) {
result = (y_def * K) + z_def;
m_var2value[x] = eval(result);
}
TRACE("opt", display(tout << "solve_div done v" << x << "\n"));
return result;
}
//
// compute D and u.
//
@ -1130,10 +1463,10 @@ namespace opt {
// x := D*x' + u
//
model_based_opt::def model_based_opt::solve_mod(unsigned x, unsigned_vector const& mod_rows, bool compute_def) {
SASSERT(!mod_rows.empty());
model_based_opt::def model_based_opt::solve_divides(unsigned x, unsigned_vector const& divide_rows, bool compute_def) {
SASSERT(!divide_rows.empty());
rational D(1);
for (unsigned idx : mod_rows) {
for (unsigned idx : divide_rows) {
D = lcm(D, m_rows[idx].m_mod);
}
if (D.is_zero()) {
@ -1144,7 +1477,7 @@ namespace opt {
rational val_x = m_var2value[x];
rational u = mod(val_x, D);
SASSERT(u.is_nonneg() && u < D);
for (unsigned idx : mod_rows) {
for (unsigned idx : divide_rows) {
replace_var(idx, x, u);
SASSERT(invariant(idx, m_rows[idx]));
normalize(idx);
@ -1217,18 +1550,35 @@ namespace opt {
replace_var(row_id, x, B);
r.m_vars.push_back(var(y, coeff*A));
r.m_value += coeff*A*m_var2value[y];
if (!r.m_vars.empty() && r.m_vars.back().m_id > y) {
if (!r.m_vars.empty() && r.m_vars.back().m_id > y)
std::sort(r.m_vars.begin(), r.m_vars.end(), var::compare());
}
m_var2row_ids[y].push_back(row_id);
SASSERT(invariant(row_id, r));
}
// update row with: x |-> A*y + B*z
void model_based_opt::replace_var(unsigned row_id, unsigned x, rational const& A, unsigned y, rational const& B, unsigned z) {
row& r = m_rows[row_id];
rational coeff = get_coefficient(row_id, x);
if (coeff.is_zero() || !r.m_alive)
return;
replace_var(row_id, x, rational::zero());
if (A != 0) r.m_vars.push_back(var(y, coeff*A));
if (B != 0) r.m_vars.push_back(var(z, coeff*B));
r.m_value += coeff*A*m_var2value[y];
r.m_value += coeff*B*m_var2value[z];
std::sort(r.m_vars.begin(), r.m_vars.end(), var::compare());
if (A != 0) m_var2row_ids[y].push_back(row_id);
if (B != 0) m_var2row_ids[z].push_back(row_id);
SASSERT(invariant(row_id, r));
}
// 3x + t = 0 & 7 | (c*x + s) & ax <= u
// 3 | -t & 21 | (-ct + 3s) & a-t <= 3u
model_based_opt::def model_based_opt::solve_for(unsigned row_id1, unsigned x, bool compute_def) {
TRACE("opt", tout << "v" << x << " := " << eval(x) << "\n" << m_rows[row_id1] << "\n";);
TRACE("opt", tout << "v" << x << " := " << eval(x) << "\n" << m_rows[row_id1] << "\n";
display(tout));
rational a = get_coefficient(row_id1, x), b;
row& r1 = m_rows[row_id1];
ineq_type ty = r1.m_type;
@ -1270,7 +1620,7 @@ namespace opt {
case t_le:
solve(row_id1, a, row_id2, x);
break;
case t_mod:
case t_divides:
// mod reduction already done.
UNREACHABLE();
break;
@ -1284,6 +1634,7 @@ namespace opt {
TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
}
retire_row(row_id1);
TRACE("opt", display(tout << "solved v" << x << "\n"));
return result;
}

48
src/math/simplex/model_based_opt.h
View file

@ -30,7 +30,9 @@ namespace opt {
t_eq,
t_lt,
t_le,
t_mod
t_divides,
t_mod,
t_div
};
@ -48,6 +50,14 @@ namespace opt {
return x.m_id < y.m_id;
}
};
bool operator==(var const& other) const {
return m_id == other.m_id && m_coeff == other.m_coeff;
}
bool operator!=(var const& other) const {
return !(*this == other);
}
};
struct row {
row(): m_type(t_le), m_value(0), m_alive(false) {}
@ -57,6 +67,7 @@ namespace opt {
ineq_type m_type; // inequality type
rational m_value; // value of m_vars + m_coeff under interpretation of m_var2value.
bool m_alive; // rows can be marked dead if they have been processed.
unsigned m_id; // variable defined by row (used for mod_t and div_t)
void reset() { m_vars.reset(); m_coeff.reset(); m_value.reset(); }
row& normalize();
@ -85,9 +96,9 @@ namespace opt {
static const unsigned m_objective_id = 0;
vector<unsigned_vector> m_var2row_ids;
vector<rational> m_var2value;
bool_vector m_var2is_int;
bool_vector m_var2is_int;
vector<var> m_new_vars;
unsigned_vector m_lub, m_glb, m_mod;
unsigned_vector m_lub, m_glb, m_divides, m_mod, m_div;
unsigned_vector m_above, m_below;
unsigned_vector m_retired_rows;
@ -114,7 +125,7 @@ namespace opt {
void mul_add(bool same_sign, unsigned row_id1, rational const& c, unsigned row_id2);
void mul_add(unsigned x, rational const& a1, unsigned row_src, rational const& a2, unsigned row_dst);
void mul_add(unsigned x, rational a1, unsigned row_src, rational a2, unsigned row_dst);
void mul(unsigned dst, rational const& c);
@ -122,14 +133,18 @@ namespace opt {
void sub(unsigned dst, rational const& c);
void del_var(unsigned dst, unsigned x);
void set_row(unsigned row_id, vector<var> const& coeffs, rational const& c, rational const& m, ineq_type rel);
void add_constraint(vector<var> const& coeffs, rational const& c, rational const& m, ineq_type r);
void add_lower_bound(unsigned x, rational const& lo);
void add_upper_bound(unsigned x, rational const& hi);
void add_constraint(vector<var> const& coeffs, rational const& c, rational const& m, ineq_type r, unsigned id);
void replace_var(unsigned row_id, unsigned x, rational const& A, unsigned y, rational const& B);
void replace_var(unsigned row_id, unsigned x, rational const& A, unsigned y, rational const& B, unsigned z);
void replace_var(unsigned row_id, unsigned x, rational const& C);
void normalize(unsigned row_id);
@ -138,7 +153,7 @@ namespace opt {
unsigned new_row();
unsigned copy_row(unsigned row_id);
unsigned copy_row(unsigned row_id, unsigned excl = UINT_MAX);
rational n_sign(rational const& b) const;
@ -150,7 +165,11 @@ namespace opt {
def solve_for(unsigned row_id, unsigned x, bool compute_def);
def solve_mod(unsigned x, unsigned_vector const& mod_rows, bool compute_def);
def solve_divides(unsigned x, unsigned_vector const& divide_rows, bool compute_def);
def solve_mod(unsigned x, unsigned_vector const& divide_rows, bool compute_def);
def solve_div(unsigned x, unsigned_vector const& divide_rows, bool compute_def);
bool is_int(unsigned x) const { return m_var2is_int[x]; }
@ -173,6 +192,17 @@ namespace opt {
// add a divisibility constraint. The row should divide m.
void add_divides(vector<var> const& coeffs, rational const& c, rational const& m);
// add sub-expression for modulus
// v = add_mod(coeffs, m) means
// v = coeffs mod m
unsigned add_mod(vector<var> const& coeffs, rational const& c, rational const& m);
// add sub-expression for div
// v = add_div(coeffs, m) means
// v = coeffs div m
unsigned add_div(vector<var> const& coeffs, rational const& c, rational const& m);
// Set the objective function (linear).
void set_objective(vector<var> const& coeffs, rational const& c);

222
src/qe/mbp/mbp_arith.cpp
View file

@ -23,7 +23,6 @@ Revision History:
#include "ast/ast_util.h"
#include "ast/arith_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/expr_functors.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "math/simplex/model_based_opt.h"
@ -35,10 +34,10 @@ namespace mbp {
struct arith_project_plugin::imp {
ast_manager& m;
ast_manager& m;
arith_util a;
bool m_check_purified { true }; // check that variables are properly pure
bool m_apply_projection { false };
bool m_check_purified = true; // check that variables are properly pure
bool m_apply_projection = false;
imp(ast_manager& m) :
@ -65,11 +64,11 @@ namespace mbp {
rational c(0), mul(1);
expr_ref t(m);
opt::ineq_type ty = opt::t_le;
expr* e1, *e2;
expr* e1, * e2;
DEBUG_CODE(expr_ref val(m);
eval(lit, val);
CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
SASSERT(m.limit().is_canceled() || !m.is_false(val)););
eval(lit, val);
CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
SASSERT(m.limit().is_canceled() || !m.is_false(val)););
if (!m.inc())
return false;
@ -86,12 +85,12 @@ namespace mbp {
ty = is_not ? opt::t_lt : opt::t_le;
}
else if ((a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1))) {
linearize(mbo, eval, mul, e1, c, fmls, ts, tids);
linearize(mbo, eval, mul, e1, c, fmls, ts, tids);
linearize(mbo, eval, -mul, e2, c, fmls, ts, tids);
ty = is_not ? opt::t_le: opt::t_lt;
ty = is_not ? opt::t_le : opt::t_lt;
}
else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) {
linearize(mbo, eval, mul, e1, c, fmls, ts, tids);
linearize(mbo, eval, mul, e1, c, fmls, ts, tids);
linearize(mbo, eval, -mul, e2, c, fmls, ts, tids);
ty = opt::t_eq;
}
@ -100,8 +99,6 @@ namespace mbp {
rational r1, r2;
expr_ref val1 = eval(e1);
expr_ref val2 = eval(e2);
//TRACE("qe", tout << mk_pp(e1, m) << " " << val1 << "\n";);
//TRACE("qe", tout << mk_pp(e2, m) << " " << val2 << "\n";);
if (!a.is_numeral(val1, r1)) return false;
if (!a.is_numeral(val2, r2)) return false;
SASSERT(r1 != r2);
@ -109,14 +106,14 @@ namespace mbp {
std::swap(e1, e2);
}
ty = opt::t_lt;
linearize(mbo, eval, mul, e1, c, fmls, ts, tids);
linearize(mbo, eval, mul, e1, c, fmls, ts, tids);
linearize(mbo, eval, -mul, e2, c, fmls, ts, tids);
}
else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) {
expr_ref val(m);
rational r;
app* alit = to_app(lit);
vector<std::pair<expr*,rational> > nums;
vector<std::pair<expr*, rational> > nums;
for (expr* arg : *alit) {
val = eval(arg);
TRACE("qe", tout << mk_pp(arg, m) << " " << val << "\n";);
@ -125,8 +122,8 @@ namespace mbp {
}
std::sort(nums.begin(), nums.end(), compare_second());
for (unsigned i = 0; i + 1 < nums.size(); ++i) {
SASSERT(nums[i].second < nums[i+1].second);
expr_ref fml(a.mk_lt(nums[i].first, nums[i+1].first), m);
SASSERT(nums[i].second < nums[i + 1].second);
expr_ref fml(a.mk_lt(nums[i].first, nums[i + 1].first), m);
if (!linearize(mbo, eval, fml, fmls, tids)) {
return false;
}
@ -139,14 +136,14 @@ namespace mbp {
map<rational, expr*, rational::hash_proc, rational::eq_proc> values;
bool found_eq = false;
for (unsigned i = 0; !found_eq && i < to_app(lit)->get_num_args(); ++i) {
expr* arg1 = to_app(lit)->get_arg(i), *arg2 = nullptr;
expr* arg1 = to_app(lit)->get_arg(i), * arg2 = nullptr;
rational r;
expr_ref val = eval(arg1);
TRACE("qe", tout << mk_pp(arg1, m) << " " << val << "\n";);
if (!a.is_numeral(val, r)) return false;
if (values.find(r, arg2)) {
ty = opt::t_eq;
linearize(mbo, eval, mul, arg1, c, fmls, ts, tids);
linearize(mbo, eval, mul, arg1, c, fmls, ts, tids);
linearize(mbo, eval, -mul, arg2, c, fmls, ts, tids);
found_eq = true;
}
@ -170,14 +167,24 @@ namespace mbp {
// convert linear arithmetic term into an inequality for mbo.
//
void linearize(opt::model_based_opt& mbo, model_evaluator& eval, rational const& mul, expr* t, rational& c,
expr_ref_vector& fmls, obj_map<expr, rational>& ts, obj_map<expr, unsigned>& tids) {
expr* t1, *t2, *t3;
expr_ref_vector& fmls, obj_map<expr, rational>& ts, obj_map<expr, unsigned>& tids) {
expr* t1, * t2, * t3;
rational mul1;
expr_ref val(m);
auto add_def = [&](expr* t1, rational const& m, vars& coeffs) {
obj_map<expr, rational> ts0;
rational mul0(1), c0(0);
linearize(mbo, eval, mul0, t1, c0, fmls, ts0, tids);
extract_coefficients(mbo, eval, ts0, tids, coeffs);
insert_mul(t, mul, ts);
return c0;
};
if (a.is_mul(t, t1, t2) && is_numeral(t1, mul1))
linearize(mbo, eval, mul* mul1, t2, c, fmls, ts, tids);
linearize(mbo, eval, mul * mul1, t2, c, fmls, ts, tids);
else if (a.is_mul(t, t1, t2) && is_numeral(t2, mul1))
linearize(mbo, eval, mul* mul1, t1, c, fmls, ts, tids);
linearize(mbo, eval, mul * mul1, t1, c, fmls, ts, tids);
else if (a.is_uminus(t, t1))
linearize(mbo, eval, -mul, t1, c, fmls, ts, tids);
else if (a.is_numeral(t, mul1))
@ -187,7 +194,7 @@ namespace mbp {
linearize(mbo, eval, mul, arg, c, fmls, ts, tids);
}
else if (a.is_sub(t, t1, t2)) {
linearize(mbo, eval, mul, t1, c, fmls, ts, tids);
linearize(mbo, eval, mul, t1, c, fmls, ts, tids);
linearize(mbo, eval, -mul, t2, c, fmls, ts, tids);
}
@ -210,21 +217,31 @@ namespace mbp {
else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
rational r;
val = eval(t);
if (!a.is_numeral(val, r)) {
if (!a.is_numeral(val, r))
throw default_exception("mbp evaluation didn't produce an integer");
}
c += mul*r;
// t1 mod mul1 == r
rational c0(-r), mul0(1);
obj_map<expr, rational> ts0;
linearize(mbo, eval, mul0, t1, c0, fmls, ts0, tids);
c += mul * r;
rational c0(-r), mul0(1);
obj_map<expr, rational> ts0;
linearize(mbo, eval, mul0, t1, c0, fmls, ts0, tids);
vars coeffs;
extract_coefficients(mbo, eval, ts0, tids, coeffs);
mbo.add_divides(coeffs, c0, mul1);
}
else if (false && a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
// v = t1 mod mul1
vars coeffs;
extract_coefficients(mbo, eval, ts0, tids, coeffs);
mbo.add_divides(coeffs, c0, mul1);
rational c0 = add_def(t1, mul1, coeffs);
tids.insert(t, mbo.add_mod(coeffs, c0, mul1));
}
else {
else if (false && a.is_idiv(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
// v = t1 div mul1
vars coeffs;
rational c0 = add_def(t1, mul1, coeffs);
tids.insert(t, mbo.add_div(coeffs, c0, mul1));
}
else
insert_mul(t, mul, ts);
}
}
bool is_numeral(expr* t, rational& r) {
@ -233,7 +250,7 @@ namespace mbp {
struct compare_second {
bool operator()(std::pair<expr*, rational> const& a,
std::pair<expr*, rational> const& b) const {
std::pair<expr*, rational> const& b) const {
return a.second < b.second;
}
};
@ -243,7 +260,7 @@ namespace mbp {
}
rational n_sign(rational const& b) {
return rational(b.is_pos()?-1:1);
return rational(b.is_pos() ? -1 : 1);
}
bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) {
@ -281,7 +298,7 @@ namespace mbp {
expr_ref_vector pinned(m);
unsigned j = 0;
TRACE("qe", tout << "vars: " << vars << "\n";
for (expr* f : fmls) tout << mk_pp(f, m) << " := " << model(f) << "\n";);
for (expr* f : fmls) tout << mk_pp(f, m) << " := " << model(f) << "\n";);
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls.get(i);
if (!linearize(mbo, eval, fml, fmls, tids)) {
@ -294,8 +311,8 @@ namespace mbp {
}
fmls.shrink(j);
TRACE("qe", tout << "formulas\n" << fmls << "\n";
for (auto const& [e, id] : tids)
tout << mk_pp(e, m) << " -> " << id << "\n";);
for (auto const& [e, id] : tids)
tout << mk_pp(e, m) << " -> " << id << "\n";);
// fmls holds residue,
// mbo holds linear inequalities that are in scope
@ -306,7 +323,7 @@ namespace mbp {
// return those to fmls.
expr_mark var_mark, fmls_mark;
for (app * v : vars) {
for (app* v : vars) {
var_mark.mark(v);
if (is_arith(v) && !tids.contains(v)) {
rational r;
@ -321,9 +338,19 @@ namespace mbp {
}
// bail on variables in non-linear sub-terms
auto is_pure = [&](expr* e) {
expr* x, * y;
rational r;
if (a.is_mod(e, x, y) && a.is_numeral(y))
return true;
if (a.is_idiv(e, x, y) && a.is_numeral(y, r) && r > 0)
return true;
return false;
};
for (auto& kv : tids) {
expr* e = kv.m_key;
if (is_arith(e) && !var_mark.is_marked(e))
if (is_arith(e) && !is_pure(e) && !var_mark.is_marked(e))
mark_rec(fmls_mark, e);
}
if (m_check_purified) {
@ -331,7 +358,7 @@ namespace mbp {
mark_rec(fmls_mark, fml);
for (auto& kv : tids) {
expr* e = kv.m_key;
if (!var_mark.is_marked(e))
if (!var_mark.is_marked(e) && !is_pure(e))
mark_rec(fmls_mark, e);
}
}
@ -351,16 +378,16 @@ namespace mbp {
vars.shrink(j);
TRACE("qe", tout << "remaining vars: " << vars << "\n";
for (unsigned v : real_vars) tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n";
mbo.display(tout););
for (unsigned v : real_vars) tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n";
mbo.display(tout););
vector<opt::model_based_opt::def> defs = mbo.project(real_vars.size(), real_vars.data(), compute_def);
vector<row> rows;
mbo.get_live_rows(rows);
rows2fmls(rows, index2expr, fmls);
TRACE("qe", mbo.display(tout << "mbo result\n");
for (auto const& d : defs) tout << "def: " << d << "\n";
tout << fmls << "\n";);
for (auto const& d : defs) tout << "def: " << d << "\n";
tout << fmls << "\n";);
if (compute_def)
optdefs2mbpdef(defs, index2expr, real_vars, result);
@ -370,9 +397,9 @@ namespace mbp {
TRACE("qe",
for (auto const& [v, t] : result)
tout << v << " := " << t << "\n";
for (auto* f : fmls)
tout << mk_pp(f, m) << " := " << eval(f) << "\n";
tout << "fmls:" << fmls << "\n";);
for (auto* f : fmls)
tout << mk_pp(f, m) << " := " << eval(f) << "\n";
tout << "fmls:" << fmls << "\n";);
return true;
}
@ -399,16 +426,77 @@ namespace mbp {
}
}
void rows2fmls(vector<row> const& rows, ptr_vector<expr> const& index2expr, expr_ref_vector& fmls) {
for (row const& r : rows) {
expr_ref_vector ts(m);
expr_ref t(m), s(m), val(m);
if (r.m_vars.empty()) {
expr_ref id2expr(u_map<row> const& def_vars, ptr_vector<expr> const& index2expr, unsigned id) {
row r;
if (def_vars.find(id, r))
return row2expr(def_vars, index2expr, r);
return expr_ref(index2expr[id], m);
}
expr_ref row2expr(u_map<row> const& def_vars, ptr_vector<expr> const& index2expr, row const& r) {
expr_ref_vector ts(m);
expr_ref t(m);
rational n;
for (var const& v : r.m_vars) {
t = id2expr(def_vars, index2expr, v.m_id);
if (a.is_numeral(t, n) && n == 0)
continue;
else if (a.is_numeral(t, n))
t = a.mk_numeral(v.m_coeff * n, a.is_int(t));
else if (!v.m_coeff.is_one())
t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t);
ts.push_back(t);
}
switch (r.m_type) {
case opt::t_mod:
if (ts.empty()) {
t = a.mk_int(mod(r.m_coeff, r.m_mod));
return t;
}
if (r.m_vars.size() == 1 && r.m_vars[0].m_coeff.is_neg() && r.m_type != opt::t_mod) {
ts.push_back(a.mk_int(r.m_coeff));
t = mk_add(ts);
t = a.mk_mod(t, a.mk_int(r.m_mod));
return t;
case opt::t_div:
if (ts.empty()) {
t = a.mk_int(div(r.m_coeff, r.m_mod));
return t;
}
ts.push_back(a.mk_int(r.m_coeff));
t = mk_add(ts);
t = a.mk_idiv(t, a.mk_int(r.m_mod));
return t;
case opt::t_divides:
ts.push_back(a.mk_int(r.m_coeff));
return mk_add(ts);
default:
return mk_add(ts);
}
}
void rows2fmls(vector<row> const& rows, ptr_vector<expr> const& index2expr, expr_ref_vector& fmls) {
u_map<row> def_vars;
for (row const& r : rows) {
if (r.m_type == opt::t_mod)
def_vars.insert(r.m_id, r);
else if (r.m_type == opt::t_div)
def_vars.insert(r.m_id, r);
}
for (row const& r : rows) {
expr_ref t(m), s(m), val(m);
if (r.m_vars.empty())
continue;
if (r.m_type == opt::t_mod)
continue;
if (r.m_type == opt::t_div)
continue;
if (r.m_vars.size() == 1 && r.m_vars[0].m_coeff.is_neg() && r.m_type != opt::t_divides) {
var const& v = r.m_vars[0];
t = index2expr[v.m_id];
t = id2expr(def_vars, index2expr, v.m_id);
if (!v.m_coeff.is_minus_one()) {
t = a.mk_mul(a.mk_numeral(-v.m_coeff, a.is_int(t)), t);
}
@ -422,24 +510,14 @@ namespace mbp {
fmls.push_back(t);
continue;
}
for (var const& v : r.m_vars) {
t = index2expr[v.m_id];
if (!v.m_coeff.is_one()) {
t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t);
}
ts.push_back(t);
}
t = mk_add(ts);
t = row2expr(def_vars, index2expr, r);
s = a.mk_numeral(-r.m_coeff, r.m_coeff.is_int() && a.is_int(t));
switch (r.m_type) {
case opt::t_lt: t = a.mk_lt(t, s); break;
case opt::t_le: t = a.mk_le(t, s); break;
case opt::t_eq: t = a.mk_eq(t, s); break;
case opt::t_mod:
if (!r.m_coeff.is_zero()) {
t = a.mk_sub(t, s);
}
t = a.mk_eq(a.mk_mod(t, a.mk_numeral(r.m_mod, true)), a.mk_int(0));
case opt::t_divides:
t = a.mk_eq(a.mk_mod(t, a.mk_int(r.m_mod)), a.mk_int(0));
break;
}
fmls.push_back(t);
@ -469,7 +547,7 @@ namespace mbp {
// extract linear constraints
for (expr * fml : fmls) {
for (expr* fml : fmls) {
linearize(mbo, eval, fml, fmls, tids);
}
@ -571,7 +649,7 @@ namespace mbp {
};
arith_project_plugin::arith_project_plugin(ast_manager& m):project_plugin(m) {
arith_project_plugin::arith_project_plugin(ast_manager& m) :project_plugin(m) {
m_imp = alloc(imp, m);
}

50
src/qe/qsat.cpp
View file

@ -241,9 +241,8 @@ namespace qe {
while (sz0 != todo.size()) {
app* a = to_app(todo.back());
todo.pop_back();
if (mark.is_marked(a)) {
if (mark.is_marked(a))
continue;
}
mark.mark(a);
if (m_lit2pred.find(a, p)) {
@ -284,9 +283,8 @@ namespace qe {
m_elevel.insert(r, l);
eq = m.mk_eq(r, a);
defs.push_back(eq);
if (!is_predicate(a, l.max())) {
if (!is_predicate(a, l.max()))
insert(r, l);
}
level.merge(l);
}
}
@ -637,57 +635,55 @@ namespace qe {
check_cancel();
expr_ref_vector asms(m_asms);
m_pred_abs.get_assumptions(m_model.get(), asms);
if (m_model.get()) {
if (m_model.get())
validate_assumptions(*m_model.get(), asms);
}
TRACE("qe", tout << asms << "\n";);
solver& s = get_kernel(m_level).s();
lbool res = s.check_sat(asms);
switch (res) {
case l_true:
s.get_model(m_model);
CTRACE("qe", !m_model, tout << "no model\n");
if (!m_model)
return l_undef;
SASSERT(validate_defs("check_sat"));
SASSERT(!m_model.get() || validate_assumptions(*m_model.get(), asms));
SASSERT(validate_model(asms));
TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
if (m_level == 0) {
if (m_level == 0)
m_model_save = m_model;
}
push();
if (m_level == 1 && m_mode == qsat_maximize) {
if (m_level == 1 && m_mode == qsat_maximize)
maximize_model();
}
break;
case l_false:
switch (m_level) {
case 0:
return l_false;
case 1:
if (m_mode == qsat_sat) {
if (m_mode == qsat_sat)
return l_true;
}
if (m_model.get()) {
SASSERT(validate_assumptions(*m_model.get(), asms));
if (!project_qe(asms)) return l_undef;
if (!project_qe(asms))
return l_undef;
}
else {
else
pop(1);
}
break;
default:
if (m_model.get()) {
if (!project(asms)) return l_undef;
if (!project(asms))
return l_undef;
}
else {
else
pop(1);
}
break;
}
break;
case l_undef:
TRACE("qe", tout << "check-sat is undef\n");
return res;
}
}
@ -833,11 +829,10 @@ namespace qe {
}
}
bool get_core(expr_ref_vector& core, unsigned level) {
void get_core(expr_ref_vector& core, unsigned level) {
SASSERT(validate_defs("get_core"));
get_kernel(level).get_core(core);
m_pred_abs.pred2lit(core);
return true;
}
bool minimize_core(expr_ref_vector& core, unsigned level) {
@ -905,9 +900,7 @@ namespace qe {
SASSERT(m_level == 1);
expr_ref fml(m);
model& mdl = *m_model.get();
if (!get_core(core, m_level)) {
return false;
}
get_core(core, m_level);
SASSERT(validate_core(mdl, core));
get_vars(m_level);
SASSERT(validate_assumptions(mdl, core));
@ -927,7 +920,7 @@ namespace qe {
}
bool project(expr_ref_vector& core) {
if (!get_core(core, m_level)) return false;
get_core(core, m_level);
TRACE("qe", display(tout); display(tout << "core\n", core););
SASSERT(m_level >= 2);
expr_ref fml(m);
@ -950,14 +943,17 @@ namespace qe {
if (level.max() == UINT_MAX) {
num_scopes = 2*(m_level/2);
}
else if (level.max() + 2 > m_level) {
// fishy - this can happen.
TRACE("qe", tout << "max-level: " << level.max() << " level: " << m_level << "\n");
return false;
}
else {
if (level.max() + 2 > m_level) return false;
SASSERT(level.max() + 2 <= m_level);
num_scopes = m_level - level.max();
SASSERT(num_scopes >= 2);
if ((num_scopes % 2) != 0) {
if ((num_scopes % 2) != 0)
--num_scopes;
}
}
pop(num_scopes);

79
src/sat/smt/xor_solver.cpp Normal file
View file

@ -0,0 +1,79 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
xor_solver.h
Abstract:
XOR solver.
Interface outline.
--*/
#include "sat/smt/xor_solver.h"
#include "sat/sat_simplifier_params.hpp"
#include "sat/sat_xor_finder.h"
namespace xr {
solver::solver(euf::solver& ctx):
th_solver(ctx.get_manager(), symbol("xor-solver"), ctx.get_manager().get_family_id("xor-solver"))
{}
euf::th_solver* solver::clone(euf::solver& ctx) {
// and relevant copy internal state
return alloc(solver, ctx);
}
void solver::asserted(sat::literal l) {
}
bool solver::unit_propagate() {
return false;
}
void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx,
sat::literal_vector & r, bool probing) {
}
sat::check_result solver::check() {
return sat::check_result::CR_DONE;
}
void solver::push() {
}
void solver::pop(unsigned n) {
}
// inprocessing
// pre_simplify: decompile all xor constraints to allow other in-processing.
// simplify: recompile clauses to xor constraints
// literals that get added to xor constraints are tagged with the theory.
void solver::pre_simplify() {
}
void solver::simplify() {
}
std::ostream& solver::display(std::ostream& out) const {
return out;
}
std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const {
return out;
}
std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
return out;
}
}

48
src/sat/smt/xor_solver.h Normal file
View file

@ -0,0 +1,48 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
xor_solver.h
Abstract:
XOR solver.
Interface outline.
--*/
#pragma once
#include "sat/smt/euf_solver.h"
namespace xr {
class solver : public euf::th_solver {
public:
solver(euf::solver& ctx);
th_solver* clone(euf::solver& ctx) override;
sat::literal internalize(expr* e, bool sign, bool root, bool redundant) override { UNREACHABLE(); return sat::null_literal; }
void internalize(expr* e, bool redundant) override { UNREACHABLE(); }
void asserted(sat::literal l) override;
bool unit_propagate() override;
void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override;
void pre_simplify() override;
void simplify() override;
sat::check_result check() override;
void push() override;
void pop(unsigned n) override;
std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
};
}

8
src/smt/qi_queue.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast/rewriter/var_subst.h"
#include "smt/smt_context.h"
#include "smt/qi_queue.h"
#include <iostream>
namespace smt {
@ -228,15 +229,12 @@ namespace smt {
TRACE("qi_queue", tout << "new instance:\n" << mk_pp(instance, m) << "\n";);
TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m) << "\n";);
expr_ref s_instance(m);
proof_ref pr(m);
m_context.get_rewriter()(instance, s_instance, pr);
TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << s_instance << "\n";);
if (m.is_true(s_instance)) {
TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m););
STRACE("instance", tout << "Instance reduced to true\n";);
stat -> inc_num_instances_simplify_true();
if (m.has_trace_stream()) {
@ -250,9 +248,11 @@ namespace smt {
std::cout << "instantiate\n";
enode_vector _bindings(num_bindings, bindings);
for (auto * b : _bindings)
std::cout << enode_pp(b, m_context) << " ";
std::cout << mk_pp(b->get_expr(), m) << " ";
std::cout << "\n";
std::cout << mk_pp(q, m) << "\n";
std::cout << "instance\n";
std::cout << instance << "\n";
#endif
TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";);

4
src/smt/smt_model_checker.cpp
View file

@ -218,7 +218,7 @@ namespace smt {
TRACE("model_checker", tout << "Got some value " << sk_value << "\n";);
if (use_inv) {
unsigned sk_term_gen = 0;
unsigned sk_term_gen = 0;
expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen);
if (sk_term != nullptr) {
TRACE("model_checker", tout << "Found inverse " << mk_pp(sk_term, m) << "\n";);
@ -243,6 +243,8 @@ namespace smt {
func_decl * f = nullptr;
if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f) && cex->get_func_interp(f)->get_interp()) {
expr_ref body(cex->get_func_interp(f)->get_interp(), m);
if (contains_model_value(body))
return false;
ptr_vector<sort> sorts(f->get_arity(), f->get_domain());
svector<symbol> names;
for (unsigned i = 0; i < f->get_arity(); ++i) {

21
src/smt/theory_lra.cpp
View file

@ -3507,16 +3507,15 @@ public:
case lp::lp_status::OPTIMAL: {
init_variable_values();
TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
inf_rational val = get_value(v);
// inf_rational val(term_max.x, term_max.y);
auto val = value(v);
blocker = mk_gt(v);
return inf_eps(rational::zero(), val);
return val;
}
case lp::lp_status::FEASIBLE: {
inf_rational val = get_value(v);
auto val = value(v);
TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
blocker = mk_gt(v);
return inf_eps(rational::zero(), val);
return val;
}
default:
SASSERT(st == lp::lp_status::UNBOUNDED);
@ -3533,23 +3532,19 @@ public:
rational r = val.x;
expr_ref e(m);
if (a.is_int(obj->get_sort())) {
if (r.is_int()) {
if (r.is_int())
r += rational::one();
}
else {
else
r = ceil(r);
}
e = a.mk_numeral(r, obj->get_sort());
e = a.mk_ge(obj, e);
}
else {
e = a.mk_numeral(r, obj->get_sort());
if (val.y.is_neg()) {
if (val.y.is_neg())
e = a.mk_ge(obj, e);
}
else {
else
e = a.mk_gt(obj, e);
}
}
TRACE("opt", tout << "v" << v << " " << val << " " << r << " " << e << "\n";);
return e;