From 8ecd8a2a521d01e3fff9c9789fd3904628b94115 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 May 2017 18:07:58 -0700 Subject: [PATCH 1/3] Dev (#50) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/util/lp/CMakeLists.txt | 3 +- src/util/lp/nra_solver.cpp | 67 ++++++++++++++++++++++++ src/util/lp/nra_solver.h | 47 +++++++++++++++++ 3 files changed, 116 insertions(+), 1 deletion(-) create mode 100644 src/util/lp/nra_solver.cpp create mode 100644 src/util/lp/nra_solver.h diff --git a/contrib/cmake/src/util/lp/CMakeLists.txt b/contrib/cmake/src/util/lp/CMakeLists.txt index ec9a2e137..75051d68c 100644 --- a/contrib/cmake/src/util/lp/CMakeLists.txt +++ b/contrib/cmake/src/util/lp/CMakeLists.txt @@ -19,8 +19,9 @@ z3_add_component(lp lp_solver_instances.cpp lu_instances.cpp matrix_instances.cpp + nra_solver.cpp permutation_matrix_instances.cpp - quick_xplain.cpp + quick_xplain.cpp row_eta_matrix_instances.cpp scaler_instances.cpp sparse_matrix_instances.cpp diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp new file mode 100644 index 000000000..08b17030c --- /dev/null +++ b/src/util/lp/nra_solver.cpp @@ -0,0 +1,67 @@ +/* + Copyright (c) 2017 Microsoft Corporation + Author: Lev Nachmanson +*/ + +#pragma once +#include "util/lp/nra_solver.h" + +namespace lp { + + struct nra_solver::imp { + lean::lar_solver& s; + + svector m_vars; + vector> m_monomials; + unsigned_vector m_lim; + + imp(lean::lar_solver& s): s(s) { + m_lim.push_back(0); + } + + lean::final_check_status check_feasible() { + return lean::final_check_status::GIVEUP; + } + + void add(lean::var_index v, unsigned sz, lean::var_index const* vs) { + m_vars.push_back(v); + m_monomials.push_back(svector(sz, vs)); + } + + void push() { + m_lim.push_back(m_vars.size()); + } + + void pop(unsigned n) { + SASSERT(n < m_lim.size()); + m_lim.shrink(m_lim.size() - n); + m_vars.shrink(m_lim.back()); + m_monomials.shrink(m_lim.back()); + } + + }; + + nra_solver::nra_solver(lean::lar_solver& s) { + m_imp = alloc(imp, s); + } + + nra_solver::~nra_solver() { + dealloc(m_imp); + } + + void nra_solver::add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs) { + m_imp->add(v, sz, vs); + } + + lean::final_check_status nra_solver::check_feasible() { + return m_imp->check_feasible(); + } + + void nra_solver::push() { + m_imp->push(); + } + + void nra_solver::pop(unsigned n) { + m_imp->pop(n); + } +} diff --git a/src/util/lp/nra_solver.h b/src/util/lp/nra_solver.h new file mode 100644 index 000000000..bae76b0d1 --- /dev/null +++ b/src/util/lp/nra_solver.h @@ -0,0 +1,47 @@ +/* + Copyright (c) 2017 Microsoft Corporation + Author: Lev Nachmanson +*/ + +#pragma once +#include "util/vector.h" +#include "util/lp/lp_settings.h" +#include "util/lp/lar_solver.h" + +namespace lean { + class lar_solver; +} + +namespace lp { + + class nra_solver { + struct imp; + imp* m_imp; + + public: + + nra_solver(lean::lar_solver& s); + + ~nra_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_feasible(); + + /* + \brief push and pop scope. + Monomial definitions are retraced when popping scope. + */ + void push(); + + void pop(unsigned n); + }; +} From 93a3c486b00fe566b2ea70b3062e26a117865ce3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 23 May 2017 18:32:08 -0700 Subject: [PATCH 2/3] small fix in lar_solver.cpp Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index b6315fe5c..aed5e32db 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -1381,7 +1381,8 @@ void lar_solver::shrink_explanation_to_minimum(vectorexplanation_is_correct(explanation)); } -final_check_status check_int_feasibility() { +final_check_status lar_solver::check_int_feasibility() { + std::cout << "lar_solver::check_int_feasibility()\n"; return final_check_status::GIVEUP; } } // namespace lean From 09530bb6bcb09cba18115124496f30ca667716e6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 24 May 2017 10:12:42 -0700 Subject: [PATCH 3/3] adding some content to the new check_int_feasibility() Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 9 +++++++-- src/util/lp/lar_solver.h | 10 ++++++++++ 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index aed5e32db..14d3535af 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -1382,8 +1382,13 @@ void lar_solver::shrink_explanation_to_minimum(vectorsecond.is_integer(); } + + static bool impq_is_int(const impq& v) { + return v.x.is_int() && is_zero(v.y); + } + + inline + bool column_value_is_integer(unsigned j) const { + const impq & v = m_mpq_lar_core_solver.m_r_x[j]; + return impq_is_int(v); + } inline bool column_is_real(unsigned j) const { return !column_is_integer(j); } final_check_status check_int_feasibility(); };