mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix for github issue 83
This commit is contained in:
parent
cd8f82ebc2
commit
caa616f11b
|
@ -556,6 +556,20 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
|
|||
extract_lcd(rats);
|
||||
}
|
||||
|
||||
void iz3mgr::get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats){
|
||||
symb s = sym(proof);
|
||||
int numps = s->get_num_parameters();
|
||||
rats.resize(numps-2);
|
||||
for(int i = 2; i < numps; i++){
|
||||
rational r;
|
||||
bool ok = s->get_parameter(i).is_rational(r);
|
||||
if(!ok)
|
||||
throw "Bad Farkas coefficient";
|
||||
rats[i-2] = r;
|
||||
}
|
||||
extract_lcd(rats);
|
||||
}
|
||||
|
||||
void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& coeffs){
|
||||
std::vector<rational> rats;
|
||||
get_assign_bounds_coeffs(proof,rats);
|
||||
|
|
|
@ -424,6 +424,8 @@ class iz3mgr {
|
|||
|
||||
void get_farkas_coeffs(const ast &proof, std::vector<rational>& rats);
|
||||
|
||||
void get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats);
|
||||
|
||||
void get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& rats);
|
||||
|
||||
void get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& rats);
|
||||
|
|
|
@ -1021,6 +1021,12 @@ public:
|
|||
my_coeffs.push_back(make_int(c));
|
||||
my_prem_cons.push_back(conc(prem(proof,i)));
|
||||
}
|
||||
else if(c.is_neg()){
|
||||
int j = (i % 2 == 0) ? i + 1 : i - 1;
|
||||
my_prems.push_back(prems[j]);
|
||||
my_coeffs.push_back(make_int(-coeffs[j]));
|
||||
my_prem_cons.push_back(conc(prem(proof,j)));
|
||||
}
|
||||
}
|
||||
ast my_con = sum_inequalities(my_coeffs,my_prem_cons);
|
||||
|
||||
|
@ -1884,7 +1890,7 @@ public:
|
|||
}
|
||||
case GCDTestKind: {
|
||||
std::vector<rational> farkas_coeffs;
|
||||
get_farkas_coeffs(proof,farkas_coeffs);
|
||||
get_broken_gcd_test_coeffs(proof,farkas_coeffs);
|
||||
if(farkas_coeffs.size() != nprems){
|
||||
pfgoto(proof);
|
||||
throw unsupported();
|
||||
|
|
Loading…
Reference in a new issue