mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'dev' of https://github.com/nikolajbjorner/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-05-25 08:54:00 -07:00
commit d2b2aedef3
33 changed files with 2400 additions and 1463 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.cpp
View file

@ -1727,7 +1727,6 @@ ast * ast_manager::register_node_core(ast * n) {
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
// increment reference counters

45
src/ast/rewriter/arith_rewriter.cpp
View file

@ -738,9 +738,54 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
result = m_util.mk_idiv0(arg1);
return BR_REWRITE1;
}
expr_ref quot(m());
if (divides(arg1, arg2, quot)) {
result = m_util.mk_mul(quot, m_util.mk_idiv(arg1, arg1));
return BR_REWRITE2;
}
return BR_FAILED;
}
bool arith_rewriter::divides(expr* d, expr* n, expr_ref& quot) {
if (d == n) {
quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
return true;
}
if (m_util.is_mul(n)) {
expr_ref_vector muls(m());
muls.push_back(n);
expr* n1, *n2;
rational r1, r2;
for (unsigned i = 0; i < muls.size(); ++i) {
if (m_util.is_mul(muls[i].get(), n1, n2)) {
muls[i] = n1;
muls.push_back(n2);
--i;
}
}
if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
for (unsigned i = 0; i < muls.size(); ++i) {
if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
return true;
}
}
}
else {
for (unsigned i = 0; i < muls.size(); ++i) {
if (d == muls[i].get()) {
muls[i] = muls.back();
muls.pop_back();
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
return true;
}
}
}
}
return false;
}
br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
set_curr_sort(m().get_sort(arg1));
numeral v1, v2;

1
src/ast/rewriter/arith_rewriter.h
View file

@ -90,6 +90,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
bool is_pi_integer_offset(expr * t, expr * & m);
expr * mk_sin_value(rational const & k);
app * mk_sqrt(rational const & k);
bool divides(expr* d, expr* n, expr_ref& quot);
public:
arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):

45
src/ast/simplifier/arith_simplifier_plugin.cpp
View file

@ -267,10 +267,55 @@ void arith_simplifier_plugin::mk_idiv(expr * arg1, expr * arg2, expr_ref & resul
bool is_int;
if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero())
result = m_util.mk_numeral(div(v1, v2), is_int);
else if (divides(arg2, arg1, result)) {
result = m_util.mk_mul(result, m_util.mk_idiv(arg2, arg2));
}
else
result = m_util.mk_idiv(arg1, arg2);
}
bool arith_simplifier_plugin::divides(expr* d, expr* n, expr_ref& quot) {
ast_manager& m = m_manager;
if (d == n) {
quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
return true;
}
if (m_util.is_mul(n)) {
expr_ref_vector muls(m);
muls.push_back(n);
expr* n1, *n2;
rational r1, r2;
for (unsigned i = 0; i < muls.size(); ++i) {
if (m_util.is_mul(muls[i].get(), n1, n2)) {
muls[i] = n1;
muls.push_back(n2);
--i;
}
}
if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
for (unsigned i = 0; i < muls.size(); ++i) {
if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
return true;
}
}
}
else {
for (unsigned i = 0; i < muls.size(); ++i) {
if (d == muls[i].get()) {
muls[i] = muls.back();
muls.pop_back();
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
return true;
}
}
}
}
return false;
}
void arith_simplifier_plugin::prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result) {
SASSERT(m_util.is_int(e));
SASSERT(k.is_int() && k.is_pos());

1
src/ast/simplifier/arith_simplifier_plugin.h
View file

@ -48,6 +48,7 @@ protected:
void div_monomial(expr_ref_vector& monomials, numeral const& g);
void get_monomial_gcd(expr_ref_vector& monomials, numeral& g);
bool divides(expr* d, expr* n, expr_ref& quot);
public:
arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p);

8
src/nlsat/nlsat_solver.h
View file

@ -21,10 +21,10 @@ Revision History:
#ifndef NLSAT_SOLVER_H_
#define NLSAT_SOLVER_H_
#include"nlsat_types.h"
#include"params.h"
#include"statistics.h"
#include"rlimit.h"
#include"nlsat/nlsat_types.h"
#include"util/params.h"
#include"util/statistics.h"
#include"util/rlimit.h"
namespace nlsat {

8
src/nlsat/nlsat_types.h
View file

@ -19,10 +19,10 @@ Revision History:
#ifndef NLSAT_TYPES_H_
#define NLSAT_TYPES_H_
#include"polynomial.h"
#include"buffer.h"
#include"sat_types.h"
#include"z3_exception.h"
#include"math/polynomial/polynomial.h"
#include"util/buffer.h"
#include"sat/sat_types.h"
#include"util/z3_exception.h"
namespace algebraic_numbers {
class anum;

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

@ -36,7 +36,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'),
('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.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'),

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

@ -23,12 +23,13 @@ Revision History:
#include"params.h"
enum arith_solver_id {
AS_NO_ARITH,
AS_DIFF_LOGIC,
AS_ARITH,
AS_DENSE_DIFF_LOGIC,
AS_UTVPI,
AS_OPTINF
AS_NO_ARITH, // 0
AS_DIFF_LOGIC, // 1
AS_ARITH, // 2
AS_DENSE_DIFF_LOGIC, // 3
AS_UTVPI, // 4
AS_OPTINF, // 5
AS_LRA // 6
};
enum bound_prop_mode {

1
src/smt/smt_model_generator.cpp
View file

@ -388,6 +388,7 @@ namespace smt {
enode * n = *it3;
if (is_uninterp_const(n->get_owner()) && m_context->is_relevant(n)) {
func_decl * d = n->get_owner()->get_decl();
TRACE("mg_top_sort", tout << d->get_name() << " " << (m_hidden_ufs.contains(d)?"hidden":"visible") << "\n";);
if (m_hidden_ufs.contains(d)) continue;
expr * val = get_value(n);
m_model->register_decl(d, val);

5
src/smt/smt_setup.cpp
View file

@ -724,8 +724,6 @@ namespace smt {
}
void setup::setup_r_arith() {
// to disable theory lra
// m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
}
@ -789,6 +787,9 @@ 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:
if (m_params.m_arith_int_only && int_only)
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));

122
src/smt/theory_lra.cpp
View file

@ -366,6 +366,14 @@ namespace smt {
terms[index] = n1;
st.terms_to_internalize().push_back(n2);
}
else if (a.is_mul(n)) {
theory_var v;
internalize_mul(to_app(n), v, r);
coeffs[index] *= r;
coeffs[vars.size()] = coeffs[index];
vars.push_back(v);
++index;
}
else if (a.is_numeral(n, r)) {
coeff += coeffs[index]*r;
++index;
@ -415,6 +423,43 @@ namespace smt {
}
}
void internalize_mul(app* t, theory_var& v, rational& r) {
SASSERT(a.is_mul(t));
bool _has_var = has_var(t);
if (!_has_var) {
internalize_args(t);
mk_enode(t);
}
r = rational::one();
rational r1;
v = mk_var(t);
svector<lean::var_index> vars;
ptr_vector<expr> todo;
todo.push_back(t);
while (!todo.empty()) {
expr* n = todo.back();
todo.pop_back();
expr* n1, *n2;
if (a.is_mul(n, n1, n2)) {
todo.push_back(n1);
todo.push_back(n2);
}
else if (a.is_numeral(n, r1)) {
r *= r1;
}
else {
if (!ctx().e_internalized(n)) {
ctx().internalize(n, false);
}
vars.push_back(get_var_index(mk_var(n)));
}
}
TRACE("arith", tout << mk_pp(t, m) << "\n";);
if (!_has_var) {
m_solver->add_monomial(get_var_index(v), vars);
}
}
enode * mk_enode(app * n) {
if (ctx().e_internalized(n)) {
return get_enode(n);
@ -459,6 +504,14 @@ namespace smt {
return m_arith_params.m_arith_reflect || is_underspecified(n);
}
bool has_var(expr* n) {
if (!ctx().e_internalized(n)) {
return false;
}
enode* e = get_enode(n);
return th.is_attached_to_var(e);
}
theory_var mk_var(expr* n, bool internalize = true) {
if (!ctx().e_internalized(n)) {
ctx().internalize(n, false);
@ -487,7 +540,7 @@ namespace smt {
result = m_theory_var2var_index[v];
}
if (result == UINT_MAX) {
result = m_solver->add_var(v);
result = m_solver->add_var(v, false);
m_theory_var2var_index.setx(v, result, UINT_MAX);
m_var_index2theory_var.setx(result, v, UINT_MAX);
m_var_trail.push_back(v);
@ -1166,18 +1219,41 @@ namespace smt {
else if (m_solver->get_status() != lean::lp_status::OPTIMAL) {
is_sat = make_feasible();
}
final_check_status st = FC_DONE;
switch (is_sat) {
case l_true:
if (delayed_assume_eqs()) {
return FC_CONTINUE;
}
if (assume_eqs()) {
return FC_CONTINUE;
}
if (m_not_handled != 0) {
return FC_GIVEUP;
switch (check_lia()) {
case l_true:
break;
case l_false:
return FC_CONTINUE;
case l_undef:
st = FC_GIVEUP;
break;
}
return FC_DONE;
switch (check_nra()) {
case l_true:
break;
case l_false:
return FC_CONTINUE;
case l_undef:
st = FC_GIVEUP;
break;
}
if (m_not_handled != 0) {
st = FC_GIVEUP;
}
return st;
case l_false:
set_conflict();
return FC_CONTINUE;
@ -1190,6 +1266,28 @@ namespace smt {
return FC_GIVEUP;
}
lbool check_lia() {
if (m.canceled()) return l_undef;
return l_true;
}
lbool check_nra() {
if (m.canceled()) return l_undef;
// return l_true;
// TBD:
switch (m_solver->check_nra(m_variable_values, m_explanation)) {
case lean::final_check_status::DONE:
return l_true;
case lean::final_check_status::CONTINUE:
return l_true; // ?? why have a continue at this level ??
case lean::final_check_status::UNSAT:
set_conflict1();
return l_false;
case lean::final_check_status::GIVEUP:
return l_undef;
}
return l_true;
}
/**
\brief We must redefine this method, because theory of arithmetic contains
@ -2197,11 +2295,15 @@ namespace smt {
}
void set_conflict() {
m_explanation.clear();
m_solver->get_infeasibility_explanation(m_explanation);
set_conflict1();
}
void set_conflict1() {
m_eqs.reset();
m_core.reset();
m_params.reset();
m_explanation.clear();
m_solver->get_infeasibility_explanation(m_explanation);
// m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
/*
static unsigned cn = 0;
@ -2252,7 +2354,10 @@ namespace smt {
model_value_proc * mk_value(enode * n, model_generator & mg) {
theory_var v = n->get_th_var(get_id());
return alloc(expr_wrapper_proc, m_factory->mk_value(get_value(v), m.get_sort(n->get_owner())));
expr* o = n->get_owner();
rational r = get_value(v);
if (a.is_int(o) && !r.is_int()) r = floor(r);
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
}
bool get_value(enode* n, expr_ref& r) {
@ -2278,6 +2383,7 @@ namespace smt {
if (dump_lemmas()) {
ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
}
if (m_arith_params.m_arith_mode == AS_LRA) return true;
context nctx(m, ctx().get_fparams(), ctx().get_params());
add_background(nctx);
bool result = l_true != nctx.check();
@ -2290,6 +2396,7 @@ namespace smt {
if (dump_lemmas()) {
ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
}
if (m_arith_params.m_arith_mode == AS_LRA) return true;
context nctx(m, ctx().get_fparams(), ctx().get_params());
m_core.push_back(~lit);
add_background(nctx);
@ -2301,6 +2408,7 @@ namespace smt {
}
bool validate_eq(enode* x, enode* y) {
if (m_arith_params.m_arith_mode == AS_LRA) return true;
context nctx(m, ctx().get_fparams(), ctx().get_params());
add_background(nctx);
nctx.assert_expr(m.mk_not(m.mk_eq(x->get_owner(), y->get_owner())));

0
src/test/argument_parser.h → src/test/lp/argument_parser.h
View file

51
src/test/lp.cpp → src/test/lp/lp.cpp
View file

@ -2691,8 +2691,8 @@ void test_term() {
lar_solver solver;
unsigned _x = 0;
unsigned _y = 1;
var_index x = solver.add_var(_x);
var_index y = solver.add_var(_y);
var_index x = solver.add_var(_x, false);
var_index y = solver.add_var(_y, false);
vector<std::pair<mpq, var_index>> term_ls;
term_ls.push_back(std::pair<mpq, var_index>((int)1, x));
@ -2705,9 +2705,16 @@ void test_term() {
ls.push_back(std::pair<mpq, var_index>((int)1, z));
solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0));
ls.clear();
ls.push_back(std::pair<mpq, var_index>((int)1, x));
solver.add_constraint(ls, lconstraint_kind::LT, mpq(0));
ls.push_back(std::pair<mpq, var_index>((int)2, y));
solver.add_constraint(ls, lconstraint_kind::GT, mpq(0));
auto status = solver.solve();
std::cout << lp_status_to_string(status) << std::endl;
std::unordered_map<var_index, mpq> model;
if (status != OPTIMAL)
return;
solver.get_model(model);
for (auto & t : model) {
@ -2719,8 +2726,8 @@ void test_term() {
void test_evidence_for_total_inf_simple(argument_parser & args_parser) {
lar_solver solver;
var_index x = solver.add_var(0);
var_index y = solver.add_var(1);
var_index x = solver.add_var(0, false);
var_index y = solver.add_var(1, false);
solver.add_var_bound(x, LE, -mpq(1));
solver.add_var_bound(y, GE, mpq(0));
vector<std::pair<mpq, var_index>> ls;
@ -2754,9 +2761,9 @@ If b becomes basic variable, then it is likely the old solver ends up with a row
return true;
};
lar_solver ls;
unsigned a = ls.add_var(0);
unsigned b = ls.add_var(1);
unsigned c = ls.add_var(2);
unsigned a = ls.add_var(0, false);
unsigned b = ls.add_var(1, false);
unsigned c = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> coeffs;
coeffs.push_back(std::pair<mpq, var_index>(1, a));
coeffs.push_back(std::pair<mpq, var_index>(-1, c));
@ -2819,8 +2826,8 @@ If x9 becomes basic variable, then it is likely the old solver ends up with a ro
}
void test_bound_propagation_one_row() {
lar_solver ls;
unsigned x0 = ls.add_var(0);
unsigned x1 = ls.add_var(1);
unsigned x0 = ls.add_var(0, false);
unsigned x1 = ls.add_var(1, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x0));
c.push_back(std::pair<mpq, var_index>(-1, x1));
@ -2833,8 +2840,8 @@ void test_bound_propagation_one_row() {
}
void test_bound_propagation_one_row_with_bounded_vars() {
lar_solver ls;
unsigned x0 = ls.add_var(0);
unsigned x1 = ls.add_var(1);
unsigned x0 = ls.add_var(0, false);
unsigned x1 = ls.add_var(1, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x0));
c.push_back(std::pair<mpq, var_index>(-1, x1));
@ -2849,8 +2856,8 @@ void test_bound_propagation_one_row_with_bounded_vars() {
}
void test_bound_propagation_one_row_mixed() {
lar_solver ls;
unsigned x0 = ls.add_var(0);
unsigned x1 = ls.add_var(1);
unsigned x0 = ls.add_var(0, false);
unsigned x1 = ls.add_var(1, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x0));
c.push_back(std::pair<mpq, var_index>(-1, x1));
@ -2864,9 +2871,9 @@ void test_bound_propagation_one_row_mixed() {
void test_bound_propagation_two_rows() {
lar_solver ls;
unsigned x = ls.add_var(0);
unsigned y = ls.add_var(1);
unsigned z = ls.add_var(2);
unsigned x = ls.add_var(0, false);
unsigned y = ls.add_var(1, false);
unsigned z = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x));
c.push_back(std::pair<mpq, var_index>(2, y));
@ -2888,9 +2895,9 @@ void test_bound_propagation_two_rows() {
void test_total_case_u() {
std::cout << "test_total_case_u\n";
lar_solver ls;
unsigned x = ls.add_var(0);
unsigned y = ls.add_var(1);
unsigned z = ls.add_var(2);
unsigned x = ls.add_var(0, false);
unsigned y = ls.add_var(1, false);
unsigned z = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x));
c.push_back(std::pair<mpq, var_index>(2, y));
@ -2914,9 +2921,9 @@ bool contains_j_kind(unsigned j, lconstraint_kind kind, const mpq & rs, const ve
void test_total_case_l(){
std::cout << "test_total_case_l\n";
lar_solver ls;
unsigned x = ls.add_var(0);
unsigned y = ls.add_var(1);
unsigned z = ls.add_var(2);
unsigned x = ls.add_var(0, false);
unsigned y = ls.add_var(1, false);
unsigned z = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x));
c.push_back(std::pair<mpq, var_index>(2, y));

14
src/test/lp/lp_main.cpp Normal file
View file

@ -0,0 +1,14 @@
void gparams_register_modules(){}
void mem_initialize() {}
void mem_finalize() {}
#include "util/rational.h"
namespace lean {
void test_lp_local(int argc, char**argv);
}
int main(int argn, char**argv){
rational::initialize();
lean::test_lp_local(argn, argv);
rational::finalize();
return 0;
}

2
src/test/smt_reader.h → src/test/lp/smt_reader.h
View file

@ -376,7 +376,7 @@ namespace lean {
void add_constraint_to_solver(lar_solver * solver, formula_constraint & fc) {
vector<std::pair<mpq, var_index>> ls;
for (auto & it : fc.m_coeffs) {
ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second))));
ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second), false)));
}
solver->add_constraint(ls, fc.m_kind, fc.m_right_side);
}

0
src/test/test_file_reader.h → src/test/lp/test_file_reader.h
View file

89
src/util/lp/init_lar_solver.h → src/util/lp/init_lar_solver.cpp
View file

@ -2,40 +2,44 @@
Copyright (c) 2017 Microsoft Corporation
Author: Lev Nachmanson
*/
// this file represents the intiialization functionality of lar_solver
// here we are inside lean::lar_solver class
bool strategy_is_undecided() const {
#include "util/lp/lar_solver.h"
namespace lean {
bool lar_solver::strategy_is_undecided() const {
return m_settings.simplex_strategy() == simplex_strategy_enum::undecided;
}
var_index add_var(unsigned ext_j) {
var_index lar_solver::add_var(unsigned ext_j, bool is_integer) {
var_index i;
lean_assert (ext_j < m_terms_start_index);
if (ext_j >= m_terms_start_index)
throw 0; // todo : what is the right way to exit?
if (try_get_val(m_ext_vars_to_columns, ext_j, i)) {
return i;
auto it = m_ext_vars_to_columns.find(ext_j);
if (it != m_ext_vars_to_columns.end()) {
return it->second.ext_j();
}
lean_assert(m_vars_to_ul_pairs.size() == A_r().column_count());
i = A_r().column_count();
m_vars_to_ul_pairs.push_back (ul_pair(static_cast<unsigned>(-1)));
add_non_basic_var_to_core_fields(ext_j);
lean_assert(sizes_are_correct());
lean_assert(!column_is_integer(i));
return i;
}
void register_new_ext_var_index(unsigned ext_v) {
void lar_solver::register_new_ext_var_index(unsigned ext_v) {
lean_assert(!contains(m_ext_vars_to_columns, ext_v));
unsigned j = static_cast<unsigned>(m_ext_vars_to_columns.size());
m_ext_vars_to_columns[ext_v] = j;
m_ext_vars_to_columns.insert(std::make_pair(ext_v, ext_var_info(j)));
lean_assert(m_columns_to_ext_vars_or_term_indices.size() == j);
m_columns_to_ext_vars_or_term_indices.push_back(ext_v);
}
void add_non_basic_var_to_core_fields(unsigned ext_j) {
void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j) {
register_new_ext_var_index(ext_j);
m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
m_columns_with_changed_bound.increase_size_by_one();
@ -44,7 +48,7 @@ void add_non_basic_var_to_core_fields(unsigned ext_j) {
add_new_var_to_core_fields_for_doubles(false);
}
void add_new_var_to_core_fields_for_doubles(bool register_in_basis) {
void lar_solver::add_new_var_to_core_fields_for_doubles(bool register_in_basis) {
unsigned j = A_d().column_count();
A_d().add_column();
lean_assert(m_mpq_lar_core_solver.m_d_x.size() == j);
@ -63,7 +67,7 @@ void add_new_var_to_core_fields_for_doubles(bool register_in_basis) {
}
}
void add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
unsigned j = A_r().column_count();
A_r().add_column();
lean_assert(m_mpq_lar_core_solver.m_r_x.size() == j);
@ -88,25 +92,23 @@ void add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
}
var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
const mpq &m_v) {
m_terms.push_back(new lar_term(coeffs, m_v));
m_orig_terms.push_back(new lar_term(coeffs, m_v));
return m_terms_start_index + m_terms.size() - 1;
}
// terms
var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs,
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
const mpq &m_v) {
if (strategy_is_undecided())
return add_term_undecided(coeffs, m_v);
m_terms.push_back(new lar_term(coeffs, m_v));
m_orig_terms.push_back(new lar_term(coeffs, m_v));
unsigned adjusted_term_index = m_terms.size() - 1;
var_index ret = m_terms_start_index + adjusted_term_index;
if (use_tableau() && !coeffs.empty()) {
add_row_for_term(m_orig_terms.back(), ret);
add_row_for_term(m_terms.back(), ret);
if (m_settings.bound_propagation())
m_rows_with_changed_bounds.insert(A_r().row_count() - 1);
}
@ -114,13 +116,13 @@ var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs,
return ret;
}
void add_row_for_term(const lar_term * term, unsigned term_ext_index) {
void lar_solver::add_row_for_term(const lar_term * term, unsigned term_ext_index) {
lean_assert(sizes_are_correct());
add_row_from_term_no_constraint(term, term_ext_index);
lean_assert(sizes_are_correct());
}
void add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) {
void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) {
register_new_ext_var_index(term_ext_index);
// j will be a new variable
unsigned j = A_r().column_count();
@ -140,7 +142,7 @@ void add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_in
fill_last_row_of_A_d(A_d(), term);
}
void add_basic_var_to_core_fields() {
void lar_solver::add_basic_var_to_core_fields() {
bool use_lu = m_mpq_lar_core_solver.need_to_presolve_with_double_solver();
lean_assert(!use_lu || A_r().column_count() == A_d().column_count());
m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
@ -151,7 +153,7 @@ void add_basic_var_to_core_fields() {
add_new_var_to_core_fields_for_doubles(true);
}
constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) {
constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) {
constraint_index ci = m_constraints.size();
if (!is_term(j)) { // j is a var
auto vc = new lar_var_constraint(j, kind, right_side);
@ -164,7 +166,7 @@ constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & r
return ci;
}
void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index) {
void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index) {
switch(m_mpq_lar_core_solver.m_column_types[j]) {
case column_type::free_column:
update_free_column_type_and_bound(j, kind, right_side, constr_index);
@ -186,22 +188,32 @@ void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq
}
}
void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
lean_assert(is_term(j));
unsigned adjusted_term_index = adjust_term_index(j);
unsigned term_j;
if (try_get_val(m_ext_vars_to_columns, j, term_j)) {
mpq rs = right_side - m_orig_terms[adjusted_term_index]->m_v;
m_constraints.push_back(new lar_term_constraint(m_orig_terms[adjusted_term_index], kind, right_side));
auto it = m_ext_vars_to_columns.find(j);
if (it != m_ext_vars_to_columns.end()) {
unsigned term_j = it->second.ext_j();
mpq rs = right_side - m_terms[adjusted_term_index]->m_v;
m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side));
update_column_type_and_bound(term_j, kind, rs, ci);
}
else {
add_constraint_from_term_and_create_new_column_row(j, m_orig_terms[adjusted_term_index], kind, right_side);
add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side);
}
}
constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) {
vector<std::pair<mpq, var_index>> left_side;
mpq rs = - right_side_parm;
substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs);
unsigned term_index = add_term(left_side, zero_of_type<mpq>());
constraint_index ci = m_constraints.size();
add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci);
return ci;
}
void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
lconstraint_kind kind, const mpq & right_side) {
add_row_from_term_no_constraint(term, term_j);
@ -211,7 +223,7 @@ void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const l
lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
}
void decide_on_strategy_and_adjust_initial_state() {
void lar_solver::decide_on_strategy_and_adjust_initial_state() {
lean_assert(strategy_is_undecided());
if (m_vars_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) {
m_settings.simplex_strategy() = simplex_strategy_enum::lu;
@ -221,7 +233,7 @@ void decide_on_strategy_and_adjust_initial_state() {
adjust_initial_state();
}
void adjust_initial_state() {
void lar_solver::adjust_initial_state() {
switch (m_settings.simplex_strategy()) {
case simplex_strategy_enum::lu:
adjust_initial_state_for_lu();
@ -237,7 +249,7 @@ void adjust_initial_state() {
}
}
void adjust_initial_state_for_lu() {
void lar_solver::adjust_initial_state_for_lu() {
copy_from_mpq_matrix(A_d());
unsigned n = A_d().column_count();
m_mpq_lar_core_solver.m_d_x.resize(n);
@ -265,7 +277,7 @@ void adjust_initial_state_for_lu() {
}*/
}
void adjust_initial_state_for_tableau_rows() {
void lar_solver::adjust_initial_state_for_tableau_rows() {
for (unsigned j = 0; j < m_terms.size(); j++) {
if (contains(m_ext_vars_to_columns, j + m_terms_start_index))
continue;
@ -274,7 +286,7 @@ void adjust_initial_state_for_tableau_rows() {
}
// this fills the last row of A_d and sets the basis column: -1 in the last column of the row
void fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls) {
void lar_solver::fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls) {
lean_assert(A.row_count() > 0);
lean_assert(A.column_count() > 0);
unsigned last_row = A.row_count() - 1;
@ -290,7 +302,7 @@ void fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls)
A.set(last_row, basis_j, - 1 );
}
void update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind) {
void lar_solver::update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind) {
mpq y_of_bound(0);
switch (kind) {
case LT:
@ -330,7 +342,7 @@ void update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const
m_columns_with_changed_bound.insert(j);
}
void update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
void lar_solver::update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound);
mpq y_of_bound(0);
switch (kind) {
@ -387,7 +399,7 @@ void update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind
}
}
void update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
void lar_solver::update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::boxed && m_mpq_lar_core_solver.m_r_low_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j]));
mpq y_of_bound(0);
switch (kind) {
@ -457,7 +469,7 @@ void update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, cons
}
}
void update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
void lar_solver::update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::low_bound);
mpq y_of_bound(0);
switch (kind) {
@ -513,7 +525,7 @@ void update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind,
}
}
void update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
void lar_solver::update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::fixed && m_mpq_lar_core_solver.m_r_low_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j]));
lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_r_low_bounds()[j].y.is_zero() && m_mpq_lar_core_solver.m_r_upper_bounds()[j].y.is_zero()));
auto v = numeric_pair<mpq>(right_side, mpq(0));
@ -574,3 +586,4 @@ void update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, cons
}
}
}

6
src/util/lp/int_solver.cpp Normal file
View file

@ -0,0 +1,6 @@
/*
Copyright (c) 2017 Microsoft Corporation
Author: Lev Nachmanson
*/
#include "util/lp/int_solver.h"

44
src/util/lp/int_solver.h Normal file
View file

@ -0,0 +1,44 @@
/*
Copyright (c) 2017 Microsoft Corporation
Author: Lev Nachmanson
*/
#pragma once
#include "util/lp/lp_settings.h"
class lemma; // forward definition
namespace lean {
class lar_solver;
template <typename T, typename X>
struct lp_constraint;
class int_solver {
public:
lar_solver *m_solver;
int_solver(lar_solver* lp);
bool check();// main function to check that solution provided by lar_solver is valid for integral values or can be adjusted.
private:
// how to tighten bounds for integer variables.
// gcd test
// 5*x + 3*y + 6*z = 5
// suppose x is fixed at 2.
// so we have 10 + 3(y + 2z) = 5
// 5 = -3(y + 2z)
// this is unsolvable because 5/3 is not an integer.
// so we create a lemma that rules out this condition.
//
bool gcd_test(lemma& lemma); // returns false in case of failure. Creates a theory lemma in case of failure.
// create goromy cuts
// either creates a conflict or a bound.
// branch and bound:
// decide what to branch and bound on
// creates a fresh inequality.
bool branch(const lp_constraint<mpq, mpq> & new_inequality);
};
}

1408
src/util/lp/lar_solver.cpp Normal file
View file

File diff suppressed because it is too large Load diff

1609
src/util/lp/lar_solver.h
View file

File diff suppressed because it is too large Load diff

17
src/util/lp/lar_solver_instances.cpp Normal file
View file

@ -0,0 +1,17 @@
/*
Copyright (c) 2017 Microsoft Corporation
Author: Lev Nachmanson
*/
#include "util/lp/lar_solver.cpp"
#include "util/lp/init_lar_solver.cpp"
template void lean::lar_solver::copy_from_mpq_matrix<double,double>(class lean::static_matrix<double,double> &);

13
src/util/lp/lp_settings.h
View file

@ -16,6 +16,19 @@ namespace lean {
typedef unsigned var_index;
typedef unsigned constraint_index;
typedef unsigned row_index;
enum class final_check_status {
DONE,
CONTINUE,
UNSAT,
GIVEUP
};
typedef vector<std::pair<mpq, constraint_index>> explanation_t;
typedef std::unordered_map<lean::var_index, rational> nra_model_t;
enum class column_type {
free_column = 0,
low_bound = 1,

10
src/util/lp/mps_reader.h
View file

@ -810,7 +810,7 @@ public:
auto kind = get_lar_relation_from_row(row->m_type);
vector<std::pair<mpq, var_index>> ls;
for (auto s : row->m_row_columns) {
var_index i = solver->add_var(get_var_index(s.first));
var_index i = solver->add_var(get_var_index(s.first), false);
ls.push_back(std::make_pair(s.second, i));
}
solver->add_constraint(ls, kind, row->m_right_side);
@ -828,20 +828,20 @@ public:
void create_low_constraint_for_var(column* col, bound * b, lar_solver *solver) {
vector<std::pair<mpq, var_index>> ls;
var_index i = solver->add_var(col->m_index);
var_index i = solver->add_var(col->m_index, false);
ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
solver->add_constraint(ls, GE, b->m_low);
}
void create_upper_constraint_for_var(column* col, bound * b, lar_solver *solver) {
var_index i = solver->add_var(col->m_index);
var_index i = solver->add_var(col->m_index, false);
vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
solver->add_constraint(ls, LE, b->m_upper);
}
void create_equality_contraint_for_var(column* col, bound * b, lar_solver *solver) {
var_index i = solver->add_var(col->m_index);
var_index i = solver->add_var(col->m_index, false);
vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
solver->add_constraint(ls, EQ, b->m_fixed_value);
@ -850,7 +850,7 @@ public:
void fill_lar_solver_on_columns(lar_solver * solver) {
for (auto s : m_columns) {
mps_reader::column * col = s.second;
solver->add_var(col->m_index);
solver->add_var(col->m_index, false);
auto b = col->m_bound;
if (b == nullptr) return;

275
src/util/lp/nra_solver.cpp Normal file
View file

@ -0,0 +1,275 @@
/*
Copyright (c) 2017 Microsoft Corporation
Author: Lev Nachmanson
*/
#pragma once
#include "util/lp/lar_solver.h"
#include "util/lp/nra_solver.h"
#include "nlsat/nlsat_solver.h"
#include "math/polynomial/polynomial.h"
#include "math/polynomial/algebraic_numbers.h"
#include "util/map.h"
namespace nra {
struct solver::imp {
lean::lar_solver& s;
reslimit m_limit; // TBD: extract from lar_solver
params_ref m_params; // TBD: pass from outside
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
struct mon_eq {
mon_eq(lean::var_index v, unsigned sz, lean::var_index const* vs):
m_v(v), m_vs(sz, vs) {}
lean::var_index m_v;
svector<lean::var_index> m_vs;
};
vector<mon_eq> m_monomials;
unsigned_vector m_lim;
mutable std::unordered_map<lean::var_index, rational> m_variable_values; // current model
imp(lean::lar_solver& s):
s(s) {
}
lean::final_check_status check_feasible(lean::nra_model_t& m, lean::explanation_t& ex) {
if (m_monomials.empty()) {
return lean::final_check_status::DONE;
}
if (check_assignments()) {
return lean::final_check_status::DONE;
}
switch (check_nlsat(m, ex)) {
case l_undef: return lean::final_check_status::GIVEUP;
case l_true: return lean::final_check_status::DONE;
case l_false: return lean::final_check_status::UNSAT;
}
return lean::final_check_status::DONE;
}
void add(lean::var_index v, unsigned sz, lean::var_index const* vs) {
m_monomials.push_back(mon_eq(v, sz, vs));
}
void push() {
m_lim.push_back(m_monomials.size());
}
void pop(unsigned n) {
if (n == 0) return;
m_monomials.shrink(m_lim[m_lim.size() - n]);
m_lim.shrink(m_lim.size() - n);
}
/*
\brief Check if polynomials are well defined.
multiply values for vs and check if they are equal to value for v.
epsilon has been computed.
*/
bool check_assignment(mon_eq const& m) const {
rational r1 = m_variable_values[m.m_v];
rational r2(1);
for (auto w : m.m_vs) {
r2 *= m_variable_values[w];
}
return r1 == r2;
}
bool check_assignments() const {
s.get_model(m_variable_values);
for (auto const& m : m_monomials) {
if (!check_assignment(m)) return false;
}
return true;
}
/**
\brief one-shot nlsat check.
A one shot checker is the least functionality that can
enable non-linear reasoning.
In addition to checking satisfiability we would also need
to identify equalities in the model that should be assumed
with the remaining solver.
TBD: use partial model from lra_solver to prime the state of nlsat_solver.
*/
lbool check_nlsat(lean::nra_model_t& model, lean::explanation_t& ex) {
nlsat::solver solver(m_limit, m_params);
m_lp2nl.reset();
// add linear inequalities from lra_solver
for (unsigned i = 0; i < s.constraint_count(); ++i) {
add_constraint(solver, i);
}
// add polynomial definitions.
for (auto const& m : m_monomials) {
add_monomial_eq(solver, m);
}
// TBD: add variable bounds?
lbool r = solver.check();
TRACE("arith", solver.display(tout << r << "\n"););
switch (r) {
case l_true: {
nlsat::anum_manager& am = solver.am();
model.clear();
for (auto kv : m_lp2nl) {
kv.m_key;
nlsat::anum const& v = solver.value(kv.m_value);
if (is_int(kv.m_key) && !am.is_int(v)) {
// the nlsat solver should already have returned unknown.
TRACE("lp", tout << "Value is not integer " << kv.m_key << "\n";);
return l_undef;
}
if (!am.is_rational(v)) {
// TBD extract and convert model.
TRACE("lp", tout << "Cannot handle algebraic numbers\n";);
return l_undef;
}
rational r;
am.to_rational(v, r);
model[kv.m_key] = r;
}
break;
}
case l_false: {
ex.reset();
vector<nlsat::assumption, false> core;
solver.get_core(core);
for (auto c : core) {
unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
ex.push_back(std::pair<rational, unsigned>(rational(1), idx));
TRACE("arith", tout << "ex: " << idx << "\n";);
}
break;
}
case l_undef:
break;
}
return r;
}
void add_monomial_eq(nlsat::solver& solver, mon_eq const& m) {
polynomial::manager& pm = solver.pm();
svector<polynomial::var> vars;
for (auto v : m.m_vs) {
vars.push_back(lp2nl(solver, v));
}
polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm);
polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(solver, m.m_v), 1), pm);
polynomial::monomial* mls[2] = { m1, m2 };
polynomial::scoped_numeral_vector coeffs(pm.m());
coeffs.push_back(mpz(1));
coeffs.push_back(mpz(-1));
polynomial::polynomial_ref p(pm.mk_polynomial(2, coeffs.c_ptr(), mls), pm);
polynomial::polynomial* ps[1] = { p };
bool even[1] = { false };
nlsat::literal lit = solver.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
solver.mk_clause(1, &lit, 0);
}
void add_constraint(nlsat::solver& solver, unsigned idx) {
auto& c = s.get_constraint(idx);
auto& pm = solver.pm();
auto k = c.m_kind;
auto rhs = c.m_right_side;
auto lhs = c.get_left_side_coefficients();
auto sz = lhs.size();
svector<polynomial::var> vars;
rational den = denominator(rhs);
for (auto kv : lhs) {
vars.push_back(lp2nl(solver, kv.second));
den = lcm(den, denominator(kv.first));
}
vector<rational> coeffs;
for (auto kv : lhs) {
coeffs.push_back(den * kv.first);
}
rhs *= den;
polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.c_ptr(), vars.c_ptr(), -rhs), pm);
polynomial::polynomial* ps[1] = { p };
bool is_even[1] = { false };
nlsat::literal lit;
switch (k) {
case lean::lconstraint_kind::LE:
lit = ~solver.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
break;
case lean::lconstraint_kind::GE:
lit = ~solver.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
break;
case lean::lconstraint_kind::LT:
lit = solver.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
break;
case lean::lconstraint_kind::GT:
lit = solver.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
break;
case lean::lconstraint_kind::EQ:
lit = solver.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
break;
}
nlsat::assumption a = this + idx;
solver.mk_clause(1, &lit, a);
}
bool is_int(lean::var_index v) {
// TBD: is it s.column_is_integer(v), if then the function should take a var_index and not unsigned; s.is_int(v);
return false;
}
polynomial::var lp2nl(nlsat::solver& solver, lean::var_index v) {
polynomial::var r;
if (!m_lp2nl.find(v, r)) {
r = solver.mk_var(is_int(v));
m_lp2nl.insert(v, r);
}
return r;
}
std::ostream& display(std::ostream& out) const {
for (auto m : m_monomials) {
out << "v" << m.m_v << " = ";
for (auto v : m.m_vs) {
out << "v" << v << " ";
}
out << "\n";
}
return out;
}
};
solver::solver(lean::lar_solver& s) {
m_imp = alloc(imp, s);
}
solver::~solver() {
dealloc(m_imp);
}
void solver::add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs) {
m_imp->add(v, sz, vs);
}
lean::final_check_status solver::check(lean::nra_model_t& m, lean::explanation_t& ex) {
return m_imp->check_feasible(m, ex);
}
void solver::push() {
m_imp->push();
}
void solver::pop(unsigned n) {
m_imp->pop(n);
}
std::ostream& solver::display(std::ostream& out) const {
return m_imp->display(out);
}
}

51
src/util/lp/nra_solver.h Normal file
View file

@ -0,0 +1,51 @@
/*
Copyright (c) 2017 Microsoft Corporation
Author: Lev Nachmanson
*/
#pragma once
#include "util/vector.h"
#include "util/lp/lp_settings.h"
namespace lean {
class lar_solver;
}
namespace nra {
class solver {
struct imp;
imp* m_imp;
public:
solver(lean::lar_solver& s);
~solver();
/*
\brief Add a definition v = vs[0]*vs[1]*...*vs[sz-1]
The variable v is equal to the product of variables vs.
*/
void add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs);
/*
\brief Check feasiblity of linear constraints augmented by polynomial definitions
that are added.
*/
lean::final_check_status check(lean::nra_model_t& m, lean::explanation_t& ex);
/*
\brief push and pop scope.
Monomial definitions are retraced when popping scope.
*/
void push();
void pop(unsigned n);
/*
\brief display state
*/
std::ostream& display(std::ostream& out) const;
};
}

4
src/util/lp/quick_xplain.cpp
View file

@ -20,7 +20,7 @@ void quick_xplain::copy_constraint_and_add_constraint_vars(const lar_constraint&
vector < std::pair<mpq, unsigned>> ls;
for (auto & p : lar_c.get_left_side_coefficients()) {
unsigned j = p.second;
unsigned lj = m_qsol.add_var(j);
unsigned lj = m_qsol.add_var(j, false);
ls.push_back(std::make_pair(p.first, lj));
}
m_constraints_in_local_vars.push_back(lar_constraint(ls, lar_c.m_kind, lar_c.m_right_side));
@ -94,7 +94,7 @@ bool quick_xplain::is_feasible(const vector<unsigned> & x, unsigned k) const {
vector < std::pair<mpq, unsigned>> ls;
const lar_constraint & c = m_constraints_in_local_vars[i];
for (auto & p : c.get_left_side_coefficients()) {
unsigned lj = l.add_var(p.second);
unsigned lj = l.add_var(p.second, false);
ls.push_back(std::make_pair(p.first, lj));
}
l.add_constraint(ls, c.m_kind, c.m_right_side);