mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

add nla_lemma.h

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-07 17:42:33 -07:00
parent 7a79397769
commit dae67987b5
1 changed files with 40 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/math/lp/nla_lemma.h Normal file
View file

@ -0,0 +1,40 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
nla_core.h
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
--*/
#pragma once
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(); }
};
}