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

unresolved in nla_intervals

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-06 09:21:45 -07:00
parent a4ad71bf33
commit 9ce2733105
4 changed files with 19 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/nla_intervals.cpp Normal file → Executable file
View file

@ -107,15 +107,17 @@ namespace nla {
lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const { lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const {
SASSERT(false); SASSERT(false);
throw;
} }
lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const { lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
SASSERT(false); SASSERT(false);
throw;
} }
bool intervals::product_has_upper_bound(int sign, const svector<lpvar>&) const { bool intervals::product_has_upper_bound(int sign, const svector<lpvar>&) const {
interval a; interval a;
throw;
} }
bool intervals::monomial_has_lower_bound(lpvar j) const { bool intervals::monomial_has_lower_bound(lpvar j) const {

17
src/math/lp/nla_intervals.h Normal file → Executable file
View file

@ -19,6 +19,7 @@
--*/ --*/
#pragma once #pragma once
#include "util/dependency.h" #include "util/dependency.h"
#include "util/small_object_allocator.h"
#include "math/lp/nla_common.h" #include "math/lp/nla_common.h"
#include "math/lp/lar_solver.h" #include "math/lp/lar_solver.h"
#include "math/interval/interval.h" #include "math/interval/interval.h"
@ -134,11 +135,14 @@ namespace nla {
} }
}; };
ci_dependency_manager m_dep_manager; small_object_allocator m_alloc;
ci_value_manager m_val_manager;
unsynch_mpq_manager m_num_manager;
ci_dependency_manager m_dep_manager;
im_config m_config; im_config m_config;
interval_manager<im_config> m_imanager; interval_manager<im_config> m_imanager;
region m_region; region m_region;
// lp::lar_solver& m_solver; lp::lar_solver& m_solver;
typedef interval_manager<im_config>::interval interval; typedef interval_manager<im_config>::interval interval;
@ -151,7 +155,14 @@ namespace nla {
bool check(lp::lar_term const& t); bool check(lp::lar_term const& t);
public: public:
intervals(core* c) : m_core(c) {} intervals(core* c, reslimit& lim, lp::lar_solver& s) :
m_core(c),
m_alloc("intervals"),
m_dep_manager(m_val_manager, m_alloc),
m_config(m_num_manager, m_dep_manager),
m_imanager(lim, im_config(m_num_manager, m_dep_manager)),
m_solver(s)
{}
bool check(); bool check();
bool monomial_has_lower_bound(lpvar j) const; bool monomial_has_lower_bound(lpvar j) const;
bool monomial_has_upper_bound(lpvar j) const; bool monomial_has_upper_bound(lpvar j) const;

2
src/math/lp/nla_solver.cpp
View file

@ -55,7 +55,7 @@ void solver::pop(unsigned n) {
} }
solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core) { solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core, m_res_limit, s) {
} }
solver::~solver() { solver::~solver() {

1
src/math/lp/nla_solver.h
View file

@ -33,6 +33,7 @@ namespace nla {
// nonlinear integer incremental linear solver // nonlinear integer incremental linear solver
class solver { class solver {
core* m_core; core* m_core;
reslimit m_res_limit;
intervals m_intervals; intervals m_intervals;
public: public:
void add_monomial(lpvar v, unsigned sz, lpvar const* vs); void add_monomial(lpvar v, unsigned sz, lpvar const* vs);