mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-15 15:57:38 -07:00
parent 90f5595067
commit ccda9d56d7
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/explanation.h
View file

@ -33,6 +33,8 @@ public:
vector<std::pair<mpq, constraint_index>>::const_iterator begin() const { return m_explanation.begin(); } vector<std::pair<mpq, constraint_index>>::const_iterator begin() const { return m_explanation.begin(); }
vector<std::pair<mpq, constraint_index>>::const_iterator end() const { return m_explanation.end(); } vector<std::pair<mpq, constraint_index>>::const_iterator end() const { return m_explanation.end(); }
void push_justification(constraint_index j, const mpq& v) { void push_justification(constraint_index j, const mpq& v) {
if (m_set_of_ci.find(j) != m_set_of_ci.end()) return;
m_set_of_ci.insert(j);
m_explanation.push_back(std::make_pair(v, j)); m_explanation.push_back(std::make_pair(v, j));
} }
void push_justification(constraint_index j) { void push_justification(constraint_index j) {