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 pull request #1715 from levnach/master

Browse source 
merge lar_solver/int_solver
This commit is contained in:
Nikolaj Bjorner 2018-07-01 12:20:02 -07:00 • committed by GitHub
commit 5a2a8d7d5c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
159 changed files with 14144 additions and 9250 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -40,7 +40,7 @@ def_module_params(module_name='smt',
('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),
('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'),
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),

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

@ -25,11 +25,11 @@ Revision History:
enum arith_solver_id {
AS_NO_ARITH, // 0
AS_DIFF_LOGIC, // 1
AS_ARITH, // 2
AS_OLD_ARITH, // 2
AS_DENSE_DIFF_LOGIC, // 3
AS_UTVPI, // 4
AS_OPTINF, // 5
AS_LRA // 6
AS_NEW_ARITH // 6
};
enum bound_prop_mode {
@ -113,7 +113,7 @@ struct theory_arith_params {
theory_arith_params(params_ref const & p = params_ref()):
m_arith_eq2ineq(false),
m_arith_process_all_eqs(false),
m_arith_mode(AS_ARITH),
m_arith_mode(AS_NEW_ARITH),
m_arith_auto_config_simplex(false),
m_arith_blands_rule_threshold(1000),
m_arith_propagate_eqs(true),

1
src/smt/smt_context.cpp
View file

@ -3763,6 +3763,7 @@ namespace smt {
}
m_stats.m_num_final_checks++;
TRACE("final_check_stats", tout << "m_stats.m_num_final_checks = " << m_stats.m_num_final_checks << "\n";);
final_check_status ok = m_qmanager->final_check_eh(false);
if (ok != FC_DONE)

2
src/smt/smt_internalizer.cpp
View file

@ -849,7 +849,7 @@ namespace smt {
std::cerr << v << " ::=\n" << mk_ll_pp(n, m_manager) << "<END-OF-FORMULA>\n";
}
#endif
TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m_manager) << "\n";);
TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m_manager) << " " << n->get_id() << "\n";);
TRACE("mk_var_bug", tout << "mk_bool: " << v << "\n";);
set_bool_var(id, v);
m_bdata.reserve(v+1);

31
src/smt/smt_setup.cpp
View file

@ -740,8 +740,12 @@ namespace smt {
}
void setup::setup_i_arith() {
// m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
if (AS_OLD_ARITH == m_params.m_arith_mode) {
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
}
else {
setup_r_arith();
}
}
void setup::setup_r_arith() {
@ -749,14 +753,21 @@ namespace smt {
}
void setup::setup_mi_arith() {
if (m_params.m_arith_mode == AS_OPTINF) {
switch (m_params.m_arith_mode) {
case AS_OPTINF:
m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params));
}
else {
break;
case AS_NEW_ARITH:
setup_r_arith();
break;
default:
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
break;
}
}
void setup::setup_arith() {
static_features st(m_manager);
IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
@ -810,15 +821,15 @@ namespace smt {
case AS_OPTINF:
m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params));
break;
case AS_LRA:
setup_r_arith();
break;
default:
case AS_OLD_ARITH:
if (m_params.m_arith_int_only && int_only)
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
break;
default:
setup_i_arith();
break;
}
}
@ -978,7 +989,7 @@ namespace smt {
if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) {
if (!st.m_has_real)
setup_QF_UFLIA(st);
else if (!st.m_has_int && st.m_num_non_linear == 0)
else if (!st.m_has_int && st.m_num_non_linear == 0)
setup_QF_UFLRA();
else
setup_unknown();

2
src/smt/theory_arith.h
View file

@ -42,7 +42,7 @@ Revision History:
namespace smt {
struct theory_arith_stats {
unsigned m_conflicts, m_add_rows, m_pivots, m_diseq_cs, m_gomory_cuts, m_branches, m_gcd_tests;
unsigned m_conflicts, m_add_rows, m_pivots, m_diseq_cs, m_gomory_cuts, m_branches, m_gcd_tests, m_patches, m_patches_succ;
unsigned m_assert_lower, m_assert_upper, m_assert_diseq, m_core2th_eqs, m_core2th_diseqs;
unsigned m_th2core_eqs, m_th2core_diseqs, m_bound_props, m_offset_eqs, m_fixed_eqs, m_offline_eqs;
unsigned m_max_min;

6
src/smt/theory_arith_int.h
View file

@ -1335,7 +1335,7 @@ namespace smt {
}
}
});
m_stats.m_patches++;
patch_int_infeasible_vars();
fix_non_base_vars();
@ -1368,6 +1368,7 @@ namespace smt {
theory_var int_var = find_infeasible_int_base_var();
if (int_var == null_theory_var) {
m_stats.m_patches_succ++;
TRACE("arith_int_incomp", tout << "FC_DONE 2...\n"; display(tout););
return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
}
@ -1385,6 +1386,7 @@ namespace smt {
m_branch_cut_counter++;
// TODO: add giveup code
TRACE("gomory_cut", tout << m_branch_cut_counter << ", " << m_params.m_arith_branch_cut_ratio << std::endl;);
if (m_branch_cut_counter % m_params.m_arith_branch_cut_ratio == 0) {
TRACE("opt_verbose", display(tout););
move_non_base_vars_to_bounds();
@ -1399,7 +1401,7 @@ namespace smt {
SASSERT(is_base(int_var));
row const & r = m_rows[get_var_row(int_var)];
if (!mk_gomory_cut(r)) {
// silent failure
TRACE("gomory_cut", tout << "silent failure\n";);
}
return FC_CONTINUE;
}

17
src/smt/theory_arith_pp.h
View file

@ -38,6 +38,8 @@ namespace smt {
st.update("arith gcd tests", m_stats.m_gcd_tests);
st.update("arith ineq splits", m_stats.m_branches);
st.update("arith gomory cuts", m_stats.m_gomory_cuts);
st.update("arith patches", m_stats.m_patches);
st.update("arith patches_succ", m_stats.m_patches_succ);
st.update("arith max-min", m_stats.m_max_min);
st.update("arith grobner", m_stats.m_gb_compute_basis);
st.update("arith pseudo nonlinear", m_stats.m_nl_linear);
@ -389,8 +391,19 @@ namespace smt {
void theory_arith<Ext>::display_vars(std::ostream & out) const {
out << "vars:\n";
int n = get_num_vars();
for (theory_var v = 0; v < n; v++)
display_var(out, v);
int inf_vars = 0;
int int_inf_vars = 0;
for (theory_var v = 0; v < n; v++) {
if ((lower(v) && lower(v)->get_value() > get_value(v))
|| (upper(v) && upper(v)->get_value() < get_value(v)))
inf_vars++;
if (is_int(v) && !get_value(v).is_int())
int_inf_vars++;
}
out << "infeasibles = " << inf_vars << " int_inf = " << int_inf_vars << std::endl;
for (theory_var v = 0; v < n; v++) {
display_var(out, v);
}
}
template<typename Ext>

5219
src/smt/theory_lra.cpp
View file

File diff suppressed because it is too large Load diff

4
src/smt/theory_lra.h
View file

@ -31,7 +31,7 @@ namespace smt {
theory_lra(ast_manager& m, theory_arith_params& ap);
~theory_lra() override;
theory* mk_fresh(context* new_ctx) override;
char const* get_name() const override { return "lra"; }
char const* get_name() const override { return "arithmetic"; }
void init(context * ctx) override;
@ -78,6 +78,8 @@ namespace smt {
model_value_proc * mk_value(enode * n, model_generator & mg) override;
bool get_value(enode* n, expr_ref& r) override;
bool get_lower(enode* n, expr_ref& r);
bool get_upper(enode* n, expr_ref& r);
bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const override;

35
src/smt/theory_seq.cpp
View file

@ -26,6 +26,7 @@ Revision History:
#include "smt/smt_model_generator.h"
#include "smt/theory_seq.h"
#include "smt/theory_arith.h"
#include "smt/theory_lra.h"
#include "smt/smt_kernel.h"
using namespace smt;
@ -4551,6 +4552,8 @@ static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v)
if (tha) return tha->get_value(ctx.get_enode(e), v);
theory_i_arith* thi = get_th_arith<theory_i_arith>(ctx, afid, e);
if (thi) return thi->get_value(ctx.get_enode(e), v);
theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
if (thr) return thr->get_value(ctx.get_enode(e), v);
TRACE("seq", tout << "no arithmetic theory\n";);
return false;
}
@ -4576,12 +4579,18 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) const {
context& ctx = get_context();
expr_ref e(m_util.str.mk_length(_e), m);
expr_ref _lo(m);
theory_mi_arith* tha = get_th_arith<theory_mi_arith>(ctx, m_autil.get_family_id(), e);
if (tha && !tha->get_lower(ctx.get_enode(e), _lo)) return false;
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;
family_id afid = m_autil.get_family_id();
do {
theory_mi_arith* tha = get_th_arith<theory_mi_arith>(ctx, afid, e);
if (tha && tha->get_lower(ctx.get_enode(e), _lo)) break;
theory_i_arith* thi = get_th_arith<theory_i_arith>(ctx, afid, e);
if (thi && thi->get_lower(ctx.get_enode(e), _lo)) break;
theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
if (thr && thr->get_lower(ctx.get_enode(e), _lo)) break;
TRACE("seq", tout << "no lower bound " << mk_pp(_e, m) << "\n";);
return false;
}
while (false);
return m_autil.is_numeral(_lo, lo) && lo.is_int();
}
@ -4627,13 +4636,19 @@ bool theory_seq::lower_bound2(expr* _e, rational& lo) {
bool theory_seq::upper_bound(expr* _e, rational& hi) const {
context& ctx = get_context();
expr_ref e(m_util.str.mk_length(_e), m);
theory_mi_arith* tha = get_th_arith<theory_mi_arith>(ctx, m_autil.get_family_id(), e);
family_id afid = m_autil.get_family_id();
expr_ref _hi(m);
if (tha && !tha->get_upper(ctx.get_enode(e), _hi)) return false;
if (!tha) {
theory_i_arith* thi = get_th_arith<theory_i_arith>(ctx, m_autil.get_family_id(), e);
if (!thi || !thi->get_upper(ctx.get_enode(e), _hi)) return false;
do {
theory_mi_arith* tha = get_th_arith<theory_mi_arith>(ctx, afid, e);
if (tha && tha->get_upper(ctx.get_enode(e), _hi)) break;
theory_i_arith* thi = get_th_arith<theory_i_arith>(ctx, afid, e);
if (thi && thi->get_upper(ctx.get_enode(e), _hi)) break;
theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
if (thr && thr->get_upper(ctx.get_enode(e), _hi)) break;
TRACE("seq", tout << "no upper bound " << mk_pp(_e, m) << "\n";);
return false;
}
while (false);
return m_autil.is_numeral(_hi, hi) && hi.is_int();
}