From a5c62bfcc49a4780d9879079fb9ec11d040b917f Mon Sep 17 00:00:00 2001 From: Lev Date: Wed, 8 Aug 2018 15:17:57 +0800 Subject: [PATCH] preparing niil files Signed-off-by: Lev --- src/smt/theory_lra.cpp | 26 +++++++++++++++++------- src/util/lp/CMakeLists.txt | 1 + src/util/lp/lp_params.pyg | 4 +++- src/util/lp/niil_solver.cpp | 40 +++++++++++++++++++++++++++++++++++++ src/util/lp/niil_solver.h | 37 ++++++++++++++++++++++++++++++++++ 5 files changed, 100 insertions(+), 8 deletions(-) create mode 100644 src/util/lp/niil_solver.cpp create mode 100644 src/util/lp/niil_solver.h diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 66175ebaa..de3bff1b5 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -42,6 +42,10 @@ #include "tactic/generic_model_converter.h" #include "math/polynomial/algebraic_numbers.h" #include "math/polynomial/polynomial.h" +#include "ast/ast_pp.h" +#include "util/cancel_eh.h" +#include "util/scoped_timer.h" +#include "util/lp/niil_solver.h" namespace lp_api { enum bound_kind { lower_t, upper_t }; @@ -251,12 +255,14 @@ class theory_lra::imp { svector > m_assume_eq_candidates; unsigned m_assume_eq_head; - unsigned m_num_conflicts; + unsigned m_num_conflicts; // non-linear arithmetic - scoped_ptr m_nra; - bool m_use_nra_model; - scoped_ptr m_a1, m_a2; + scoped_ptr m_nra; + bool m_use_niil; + scoped_ptr m_niil; + bool m_use_nra_model; + scoped_ptr m_a1, m_a2; // integer arithmetic scoped_ptr m_lia; @@ -294,7 +300,6 @@ class theory_lra::imp { resource_limit m_resource_limit; lp_bounds m_new_bounds; - context& ctx() const { return th.get_context(); } theory_id get_id() const { return th.get_id(); } bool is_int(theory_var v) const { return is_int(get_enode(v)); } @@ -303,6 +308,7 @@ class theory_lra::imp { enode* get_enode(expr* e) const { return ctx().get_enode(e); } expr* get_owner(theory_var v) const { return get_enode(v)->get_owner(); } + void init_solver() { if (m_solver) return; @@ -322,6 +328,7 @@ class theory_lra::imp { m_solver->settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; m_solver->settings().set_random_seed(ctx().get_fparams().m_random_seed); + m_use_niil = lp.niil(); m_lia = alloc(lp::int_solver, m_solver.get()); get_one(true); get_zero(true); @@ -560,8 +567,13 @@ class theory_lra::imp { } TRACE("arith", tout << "v" << v << "(" << get_var_index(v) << ") := " << mk_pp(t, m) << " " << _has_var << "\n";); if (!_has_var) { - ensure_nra(); - m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr()); + if (m_use_niil) { + ensure_niil(); + m_niil->add_monomial(get_var_index(v), vars.size(), vars.c_ptr()); + } else { + ensure_nra(); + m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr()); + } } } diff --git a/src/util/lp/CMakeLists.txt b/src/util/lp/CMakeLists.txt index edb73fdab..e2e1c6e7a 100644 --- a/src/util/lp/CMakeLists.txt +++ b/src/util/lp/CMakeLists.txt @@ -21,6 +21,7 @@ z3_add_component(lp lu.cpp lp_utils.cpp matrix.cpp + niil_solver.cpp nra_solver.cpp permutation_matrix.cpp random_updater.cpp diff --git a/src/util/lp/lp_params.pyg b/src/util/lp/lp_params.pyg index 1ef788241..02da979bd 100644 --- a/src/util/lp/lp_params.pyg +++ b/src/util/lp/lp_params.pyg @@ -6,7 +6,9 @@ def_module_params('lp', ('print_stats', BOOL, False, 'print statistic'), ('simplex_strategy', UINT, 0, 'simplex strategy for the solver'), ('enable_hnf', BOOL, True, 'enable hnf cuts'), - ('bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation') + ('bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'), + ('niil', BOOL, False, 'call nonlinear integer solver with incremental linearization') + )) diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp new file mode 100644 index 000000000..526de29b7 --- /dev/null +++ b/src/util/lp/niil_solver.cpp @@ -0,0 +1,40 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + + +Abstract: + + + +Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + +Revision History: + + +--*/ +#include "util/lp/niil_solver.h" +#include "util/map.h" +namespace niil { +struct solver::imp { + imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) + // : + // s(s), + // m_limit(lim), + // m_params(p) + { + } +}; +void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) { + std::cout << "called add_monomial\n"; +} +solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) { + m_imp = alloc(imp, s, lim, p); +} + + +} diff --git a/src/util/lp/niil_solver.h b/src/util/lp/niil_solver.h new file mode 100644 index 000000000..653e52feb --- /dev/null +++ b/src/util/lp/niil_solver.h @@ -0,0 +1,37 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + + +Abstract: + + + +Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + +Revision History: + + +--*/ +#pragma once +#include "util/vector.h" +#include "util/lp/lp_settings.h" +#include "util/rlimit.h" +#include "util/params.h" +#include "nlsat/nlsat_solver.h" +#include "util/lp/lar_solver.h" +namespace niil { +// nonlinear integer incremental linear solver +class solver { +public: + struct imp; + imp* m_imp; + void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs); + solver(lp::lar_solver& s, reslimit& lim, params_ref const& p); + +}; +}