mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 11:41:22 +00:00
Code Activity

fix lemma counting and nix NEW_EXTRACT_TH_LEMMA

Browse source
This commit is contained in:
Ken McMillan 2013-09-15 13:40:06 -07:00
commit 6091cb1825
3 changed files with 22 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/interp/iz3interp.cpp
View file

@ -190,6 +190,16 @@ public:
return true; return true;
} }
void test_secondary(const std::vector<ast> &cnsts,
const std::vector<int> &parents,
std::vector<ast> &interps
){
int num = cnsts.size();
iz3secondary *sp = iz3foci::create(this,num,(int *)(parents.empty()?0:&parents[0]));
int res = sp->interpolate(cnsts, interps);
if(res != 0)
throw "secondary failed";
}
void proof_to_interpolant(z3pf proof, void proof_to_interpolant(z3pf proof,
const std::vector<ast> &cnsts, const std::vector<ast> &cnsts,
@ -198,7 +208,10 @@ public:
const std::vector<ast> &theory, const std::vector<ast> &theory,
interpolation_options_struct *options = 0 interpolation_options_struct *options = 0
){ ){
#if 0
test_secondary(cnsts,parents,interps);
return;
#endif
profiling::timer_start("Interpolation prep"); profiling::timer_start("Interpolation prep");
// get rid of frames not used in proof // get rid of frames not used in proof

10
src/interp/iz3translate_direct.cpp
View file

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

3
src/tactic/goal.cpp
View file

@ -255,7 +255,8 @@ void goal::get_formulas(ptr_vector<expr> & result) {
} }
void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) { void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); // KLM: don't know why this assertion is no longer true
// SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent) if (m_inconsistent)
return; return;
if (proofs_enabled()) { if (proofs_enabled()) {