mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

interp handle mystery arith lemmas

Browse source
This commit is contained in:
Ken McMillan 2014-05-13 17:28:22 -07:00
parent 669fded98a
commit c9e9b30af6
2 changed files with 18 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/interp/iz3mgr.h
View file

@ -387,10 +387,13 @@ class iz3mgr {
return UnknownTheory;
}
enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,UnknownKind};
enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,ArithMysteryKind,UnknownKind};
lemma_kind get_theory_lemma_kind(const ast &proof){
symb s = sym(proof);
if(s->get_num_parameters() < 2) {
return ArithMysteryKind; // Bad -- Z3 hasn't told us
}
::symbol p0;
bool ok = s->get_parameter(1).is_symbol(p0);
if(!ok) return UnknownKind;

14
src/interp/iz3translate.cpp
View file

@ -1581,6 +1581,12 @@ public:
return res;
}
ast ArithMysteryRule(const ast &con, const std::vector<ast> &prems, const std::vector<Iproof::node> &args){
// Hope for the best!
Iproof::node guess = reconstruct_farkas(prems,args,con);
return guess;
}
struct CannotCombineEqPropagate {};
void CombineEqPropagateRec(const ast &proof, std::vector<ast> &prems, std::vector<Iproof::node> &args, ast &eqprem){
@ -1892,6 +1898,14 @@ public:
res = EqPropagate(con,prems,args);
break;
}
case ArithMysteryKind: {
// Z3 hasn't told us what kind of lemma this is -- maybe we can guess
std::vector<ast> prems(nprems);
for(unsigned i = 0; i < nprems; i++)
prems[i] = prem(proof,i);
res = ArithMysteryRule(con,prems,args);
break;
}
default:
throw unsupported();
}