mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 21:20:52 +00:00
Code Activity

some debugging stuff

Browse source
This commit is contained in:
Ken McMillan 2013-06-27 17:27:36 -07:00
parent ea127c8ab9
commit d8b31773b8
2 changed files with 20 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/interp/iz3translate_direct.cpp
View file

@ -39,6 +39,7 @@ using namespace stl_ext;
static int lemma_count = 0;
static int nll_lemma_count = 0;
#define SHOW_LEMMA_COUNT -1
// One half of a resolution. We need this to distinguish
@ -764,7 +765,8 @@ public:
#if 1
// std::cout << "lemma: " << ++lemma_count << "\n";
++lemma_count;
// std::cout << "lemma: " << lemma_count << "\n";
if(lemma_count == SHOW_LEMMA_COUNT){
for(unsigned i = 0; i < lits.size(); i++)
show_lit(lits[i]);
@ -1337,7 +1339,7 @@ public:
return res;
}
// #define NEW_EXTRACT_TH_LEMMA
//#define NEW_EXTRACT_TH_LEMMA
void get_local_hyps(const ast &proof, std::set<ast> &res){
std::set<ast> hyps = get_hyps(proof);
@ -1372,7 +1374,7 @@ public:
}
}
#ifdef NEW_EXTRACT_TH_LEMMA
bool lemma_nll = nargs > 1;
bool lemma_nll = nprems > 1;
if(nll && !lemma_nll){
lemma_nll = false;
// std::cout << "lemma count = " << nll_lemma_count << "\n";
@ -1394,7 +1396,7 @@ public:
try {
res = extract_th_lemma_common(lits,nll,lemma_nll);
}
#if 0
#if 1
catch (const invalid_lemma &) {
std::cout << "\n\nlemma: " << my_count;
std::cout << "\n\nproof node: \n";