diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index 0fdce156a..6ea8c2d7f 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -201,6 +201,26 @@ void iz3base::initialize(const std::vector &_parts, const std::vector add_frame_range(SHRT_MIN, _theory[i]); add_frame_range(SHRT_MAX, _theory[i]); } + for(unsigned i = 0; i < cnsts.size(); i++) + frame_map[cnsts[i]] = i; + for(unsigned i = 0; i < theory.size(); i++) + frame_map[theory[i]] = INT_MAX; +} + +void iz3base::initialize(const std::vector > &_parts, const std::vector &_parents, const std::vector &_theory){ + cnsts.resize(_parts.size()); + theory = _theory; + for(unsigned i = 0; i < _parts.size(); i++) + for(unsigned j = 0; j < _parts[i].size(); j++){ + cnsts[i] = make(And,_parts[i]); + add_frame_range(i, _parts[i][j]); + frame_map[_parts[i][j]] = i; + } + for(unsigned i = 0; i < _theory.size(); i++){ + add_frame_range(SHRT_MIN, _theory[i]); + add_frame_range(SHRT_MAX, _theory[i]); + frame_map[theory[i]] = INT_MAX; + } } void iz3base::check_interp(const std::vector &itps, std::vector &theory){ diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index da0a3ce4a..0e57cf5e3 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -74,6 +74,15 @@ class iz3base : public iz3mgr, public scopes { weak = false; } + iz3base(const iz3mgr& other, + const std::vector > &_cnsts, + const std::vector &_parents, + const std::vector &_theory) + : iz3mgr(other), scopes(_parents) { + initialize(_cnsts,_parents,_theory); + weak = false; + } + iz3base(const iz3mgr& other) : iz3mgr(other), scopes() { weak = false; @@ -107,6 +116,14 @@ class iz3base : public iz3mgr, public scopes { return make(And,cs); } + int frame_of_assertion(const ast &ass){ + stl_ext::hash_map::iterator it = frame_map.find(ass); + if(it == frame_map.end()) + throw "unknown assertion"; + return it->second; + } + + void to_parents_vec_representation(const std::vector &_cnsts, const ast &tree, std::vector &cnsts, @@ -132,12 +149,15 @@ class iz3base : public iz3mgr, public scopes { stl_ext::hash_map sym_range_hash; stl_ext::hash_map ast_ranges_hash; stl_ext::hash_map simplify_memo; + stl_ext::hash_map frame_map; // map assertions to frames + int frames; // number of frames void add_frame_range(int frame, ast t); void initialize(const std::vector &_parts, const std::vector &_parents, const std::vector &_theory); + void initialize(const std::vector > &_parts, const std::vector &_parents, const std::vector &_theory); bool is_literal(ast n); void gather_conjuncts_rec(ast n, std::vector &conjuncts, stl_ext::hash_set &memo); diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 6767deacf..2ef36f4e2 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -232,8 +232,13 @@ public: iz3secondary *sp = iz3foci::create(this,num,parents_vec.empty()?0:&parents_vec[0]); sp_killer.set(sp); // kill this on exit +#define BINARY_INTERPOLATION +#ifndef BINARY_INTERPOLATION // create a translator - iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory); + std::vector > cnsts_vec_vec(cnsts_vec.size()); + for(unsigned i = 0; i < cnsts_vec.size(); i++) + cnsts_vec_vec[i].push_back(cnsts_vec[i]); + iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec_vec,parents_vec,theory); tr_killer.set(tr); // set the translation options, if needed @@ -258,7 +263,43 @@ public: interps_vec[i] = tr->quantify(interps_vec[i],tr->range_downward(i)); } profiling::timer_stop("Proof interpolation"); - +#else + iz3base the_base(*this,cnsts_vec,parents_vec,theory); + + profiling::timer_stop("Interpolation prep"); + + for(int i = 0; i < num-1; i++){ + range rng = the_base.range_downward(i); + std::vector > cnsts_vec_vec(2); + for(unsigned j = 0; j < cnsts_vec.size(); j++){ + bool is_A = the_base.in_range(j,rng); + cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j]); + } + + killme tr_killer_i; + iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec_vec,std::vector(),theory); + tr_killer_i.set(tr); + + // set the translation options, if needed + if(options) + for(hash_map::iterator it = options->map.begin(), en = options->map.end(); it != en; ++it) + tr->set_option(it->first, it->second); + + // create a proof object to hold the translation + iz3proof pf(tr); + + // translate into an interpolatable proof + profiling::timer_start("Proof translation"); + tr->translate(proof,pf); + profiling::timer_stop("Proof translation"); + + // translate the proof into interpolants + profiling::timer_start("Proof interpolation"); + interps_vec[i] = pf.interpolate(tr->range_downward(0),tr->weak_mode()); + interps_vec[i] = tr->quantify(interps_vec[i],tr->range_downward(0)); + profiling::timer_stop("Proof interpolation"); + } +#endif // put back in the removed frames fr.fix_interpolants(interps_vec); diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 26a1cc8fc..ff5d24228 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -68,7 +68,6 @@ public: typedef std::pair, hash_map > AstToIpf; AstToIpf translation; // Z3 proof nodes to Iproof nodes - AstToInt frame_map; // map assertions to frames int frames; // number of frames typedef std::set AstSet; @@ -98,6 +97,12 @@ public: #define from_ast(x) (x) + // #define NEW_LOCALITY + +#ifdef NEW_LOCALITY + range rng; // the range of frames in the "A" part of the interpolant +#endif + // determine locality of a proof term // return frame of derivation if local, or -1 if not // result INT_MAX means the proof term is a tautology @@ -110,9 +115,13 @@ public: if(!bar.second) return res; if(pr(proof) == PR_ASSERTED){ ast ass = conc(proof); - AstToInt::iterator it = frame_map.find(ass); - assert(it != frame_map.end()); - res = it->second; + res = frame_of_assertion(ass); +#ifdef NEW_LOCALITY + if(in_range(res,rng)) + res = range_max(rng); + else + res = frames-1; +#endif } else { unsigned nprems = num_prems(proof); @@ -166,6 +175,7 @@ public: return res; } + AstSet &get_hyps(ast proof){ std::pair foo(proof,AstSet()); std::pair bar = hyp_map.insert(foo); @@ -279,7 +289,7 @@ public: } } - +#if 0 // clear the localization variables void clear_localization(){ localization_vars.clear(); @@ -534,6 +544,7 @@ public: if(hi >= frames) return frames - 1; return hi; } +#endif int num_lits(ast ast){ opr dk = op(ast); @@ -1197,6 +1208,10 @@ public: iz3proof::node translate(ast proof, iz3proof &dst){ std::vector itps; for(int i = 0; i < frames -1; i++){ +#ifdef NEW_LOCALITY + rng = range_downward(i); + locality.clear(); +#endif iproof = iz3proof_itp::create(this,range_downward(i),weak_mode()); Iproof::node ipf = translate_main(proof); ast itp = iproof->interpolate(ipf); @@ -1211,15 +1226,11 @@ public: iz3translation_full(iz3mgr &mgr, iz3secondary *_secondary, - const std::vector &cnsts, + const std::vector > &cnsts, const std::vector &parents, const std::vector &theory) : iz3translation(mgr, cnsts, parents, theory) { - for(unsigned i = 0; i < cnsts.size(); i++) - frame_map[cnsts[i]] = i; - for(unsigned i = 0; i < theory.size(); i++) - frame_map[theory[i]] = INT_MAX; frames = cnsts.size(); traced_lit = ast(); } @@ -1235,7 +1246,7 @@ public: iz3translation *iz3translation::create(iz3mgr &mgr, iz3secondary *secondary, - const std::vector &cnsts, + const std::vector > &cnsts, const std::vector &parents, const std::vector &theory){ return new iz3translation_full(mgr,secondary,cnsts,parents,theory); diff --git a/src/interp/iz3translate.h b/src/interp/iz3translate.h index 64e3bdea6..6dc01dfa7 100755 --- a/src/interp/iz3translate.h +++ b/src/interp/iz3translate.h @@ -40,15 +40,15 @@ public: static iz3translation *create(iz3mgr &mgr, iz3secondary *secondary, - const std::vector &frames, + const std::vector > &frames, const std::vector &parents, const std::vector &theory); protected: iz3translation(iz3mgr &mgr, - const std::vector &_cnsts, - const std::vector &_parents, - const std::vector &_theory) + const std::vector > &_cnsts, + const std::vector &_parents, + const std::vector &_theory) : iz3base(mgr,_cnsts,_parents,_theory) {} }; diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 037cabee9..44c907d1d 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -200,7 +200,6 @@ public: Iproof *iproof; // the interpolating proof we are constructing - AstToInt frame_map; // map assertions to frames int frames; // number of frames typedef std::set AstSet; @@ -250,9 +249,7 @@ public: if(!bar.second) return res; if(pr(proof) == PR_ASSERTED){ ast ass = conc(proof); - AstToInt::iterator it = frame_map.find(ass); - assert(it != frame_map.end()); - res = it->second; + res = frame_of_assertion(ass); } else { unsigned nprems = num_prems(proof); @@ -590,9 +587,7 @@ public: pfrule dk = pr(proof); if(dk == PR_ASSERTED){ ast ass = conc(proof); - AstToInt::iterator it = frame_map.find(ass); - assert(it != frame_map.end()); - frame = it->second; + frame = frame_of_assertion(ass); if(frame >= frames) frame = frames-1; // can happen if a theory fact antes.push_back(std::pair(ass,frame)); return; @@ -1655,16 +1650,12 @@ public: iz3translation_direct(iz3mgr &mgr, iz3secondary *_secondary, - const std::vector &cnsts, + const std::vector > &cnsts, const std::vector &parents, const std::vector &theory) : iz3translation(mgr, cnsts, parents, theory) { secondary = _secondary; - for(unsigned i = 0; i < cnsts.size(); i++) - frame_map[cnsts[i]] = i; - for(unsigned i = 0; i < theory.size(); i++) - frame_map[theory[i]] = INT_MAX; frames = cnsts.size(); traced_lit = ast(); } @@ -1693,7 +1684,7 @@ public: iz3translation *iz3translation::create(iz3mgr &mgr, iz3secondary *secondary, - const std::vector &cnsts, + const std::vector > &cnsts, const std::vector &parents, const std::vector &theory){ return new iz3translation_direct(mgr,secondary,cnsts,parents,theory);