mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Add forgotten file

Browse source
This commit is contained in:
Lev Nachmanson 2019-04-10 16:01:07 -07:00
parent 7f05907f91
commit 2513deb817
1 changed files with 2 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/util/lp/nla_solver.h
View file

@ -25,39 +25,12 @@ Revision History:
#include "nlsat/nlsat_solver.h"
#include "util/lp/lar_solver.h"
#include "util/lp/monomial.h"
#include "util/lp/nla_core.h"
namespace nla {
struct ineq {
lp::lconstraint_kind m_cmp;
lp::lar_term m_term;
rational m_rs;
ineq(lp::lconstraint_kind cmp, const lp::lar_term& term, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {}
bool operator==(const ineq& a) const {
return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs;
}
const lp::lar_term& term() const { return m_term; };
lp::lconstraint_kind cmp() const { return m_cmp; };
const rational& rs() const { return m_rs; };
};
class lemma {
vector<ineq> m_ineqs;
lp::explanation m_expl;
public:
void push_back(const ineq& i) { m_ineqs.push_back(i);}
size_t size() const { return m_ineqs.size() + m_expl.size(); }
const vector<ineq>& ineqs() const { return m_ineqs; }
vector<ineq>& ineqs() { return m_ineqs; }
lp::explanation& expl() { return m_expl; }
const lp::explanation& expl() const { return m_expl; }
bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); }
};
typedef vector<monomial> polynomial;
// nonlinear integer incremental linear solver
class solver {
struct imp;
imp* m_imp;
core* m_core;
public:
// returns the monomial index
unsigned add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);