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

add cutting plane

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-07 01:35:25 -08:00
parent 220b339e5e
commit 31e2d823c9
1 changed files with 15 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_card.cpp
View file

@ -113,6 +113,20 @@ namespace smt {
m_watch_trail.push_back(bv); m_watch_trail.push_back(bv);
} }
static unsigned gcd(unsigned a, unsigned b) {
if (a == 0) return b;
if (b == 0) return a;
while (a != b) {
if (a < b) {
b %= a;
}
else {
a %= b;
}
}
return a;
}
void theory_card::add_card(card* c) { void theory_card::add_card(card* c) {
bool_var abv = c->m_bv; bool_var abv = c->m_bv;
arg_t& args = c->m_args; arg_t& args = c->m_args;
@ -141,7 +155,7 @@ namespace smt {
g = gcd(g, args[i].second); g = gcd(g, args[i].second);
} }
if (g > 1) { if (g > 1) {
unsigned k = c->m_k; int k = c->m_k;
if (k >= 0) { if (k >= 0) {
c->m_k /= g; c->m_k /= g;
} }