mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

looking for more farkas rules in interpolation

Browse source
This commit is contained in:
Ken McMillan 2013-11-07 15:40:44 -08:00
parent d9c69f5294
commit cf176af48e
2 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/interp/iz3mgr.cpp
View file

@ -489,11 +489,15 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
symb s = sym(proof); symb s = sym(proof);
int numps = s->get_num_parameters(); int numps = s->get_num_parameters();
rats.resize(numps-2); rats.resize(numps-2);
if(num_prems(proof) < numps-2){
std::cout << "bad farkas rule: " << num_prems(proof) << " premises should be " << numps-2 << "\n";
}
for(int i = 2; i < numps; i++){ for(int i = 2; i < numps; i++){
rational r; rational r;
bool ok = s->get_parameter(i).is_rational(r); bool ok = s->get_parameter(i).is_rational(r);
if(!ok) if(!ok)
throw "Bad Farkas coefficient"; throw "Bad Farkas coefficient";
#if 0
{ {
ast con = conc(prem(proof,i-2)); ast con = conc(prem(proof,i-2));
ast temp = make_real(r); // for debugging ast temp = make_real(r); // for debugging
@ -501,6 +505,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt)) if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt))
r = -r; r = -r;
} }
#endif
rats[i-2] = r; rats[i-2] = r;
} }
#if 0 #if 0

8
src/interp/iz3translate.cpp
View file

@ -1253,6 +1253,10 @@ public:
case FarkasKind: { case FarkasKind: {
std::vector<ast> farkas_coeffs, prem_cons; std::vector<ast> farkas_coeffs, prem_cons;
get_farkas_coeffs(proof,farkas_coeffs); get_farkas_coeffs(proof,farkas_coeffs);
if(farkas_coeffs.size() != nprems){
pfgoto(proof);
throw unsupported();
}
prem_cons.resize(nprems); prem_cons.resize(nprems);
for(unsigned i = 0; i < nprems; i++) for(unsigned i = 0; i < nprems; i++)
prem_cons[i] = conc(prem(proof,i)); prem_cons[i] = conc(prem(proof,i));
@ -1279,6 +1283,10 @@ public:
case GCDTestKind: { case GCDTestKind: {
std::vector<rational> farkas_coeffs; std::vector<rational> farkas_coeffs;
get_farkas_coeffs(proof,farkas_coeffs); get_farkas_coeffs(proof,farkas_coeffs);
if(farkas_coeffs.size() != nprems){
pfgoto(proof);
throw unsupported();
}
std::vector<Iproof::node> my_prems; my_prems.resize(2); std::vector<Iproof::node> my_prems; my_prems.resize(2);
std::vector<ast> my_prem_cons; my_prem_cons.resize(2); std::vector<ast> my_prem_cons; my_prem_cons.resize(2);
std::vector<ast> my_farkas_coeffs; my_farkas_coeffs.resize(2); std::vector<ast> my_farkas_coeffs; my_farkas_coeffs.resize(2);