mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

initial skeletons for nra solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-23 16:26:46 -07:00
parent f1ca1de408
commit db54cab8b2
1 changed files with 37 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/util/lp/nra_solver.cpp
View file

@ -10,11 +10,35 @@ namespace lp {
struct nra_solver::imp { struct nra_solver::imp {
lean::lar_solver& s; lean::lar_solver& s;
imp(lean::lar_solver& s): s(s) {}
svector<lean::var_index> m_vars;
vector<svector<lean::var_index>> m_monomials;
unsigned_vector m_lim;
imp(lean::lar_solver& s): s(s) {
m_lim.push_back(0);
}
lean::final_check_status check_feasible() { lean::final_check_status check_feasible() {
return lean::final_check_status::GIVEUP; 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<lean::var_index>(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) { nra_solver::nra_solver(lean::lar_solver& s) {
@ -25,7 +49,19 @@ namespace lp {
dealloc(m_imp); 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() { lean::final_check_status nra_solver::check_feasible() {
return m_imp->check_feasible(); return m_imp->check_feasible();
} }
void nra_solver::push() {
m_imp->push();
}
void nra_solver::pop(unsigned n) {
m_imp->pop(n);
}
} }