mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
added binary interpolation
This commit is contained in:
parent
ac212ec54c
commit
7ca6c744fd
|
@ -201,6 +201,26 @@ void iz3base::initialize(const std::vector<ast> &_parts, const std::vector<int>
|
|||
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<std::vector<ast> > &_parts, const std::vector<int> &_parents, const std::vector<ast> &_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<ast> &itps, std::vector<ast> &theory){
|
||||
|
|
|
@ -74,6 +74,15 @@ class iz3base : public iz3mgr, public scopes {
|
|||
weak = false;
|
||||
}
|
||||
|
||||
iz3base(const iz3mgr& other,
|
||||
const std::vector<std::vector<ast> > &_cnsts,
|
||||
const std::vector<int> &_parents,
|
||||
const std::vector<ast> &_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<ast,int>::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<ast> &_cnsts,
|
||||
const ast &tree,
|
||||
std::vector<ast> &cnsts,
|
||||
|
@ -132,12 +149,15 @@ class iz3base : public iz3mgr, public scopes {
|
|||
stl_ext::hash_map<symb,range> sym_range_hash;
|
||||
stl_ext::hash_map<ast,ranges> ast_ranges_hash;
|
||||
stl_ext::hash_map<ast,ast> simplify_memo;
|
||||
stl_ext::hash_map<ast,int> frame_map; // map assertions to frames
|
||||
|
||||
int frames; // number of frames
|
||||
|
||||
void add_frame_range(int frame, ast t);
|
||||
|
||||
void initialize(const std::vector<ast> &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory);
|
||||
|
||||
void initialize(const std::vector<std::vector<ast> > &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory);
|
||||
|
||||
bool is_literal(ast n);
|
||||
void gather_conjuncts_rec(ast n, std::vector<ast> &conjuncts, stl_ext::hash_set<ast> &memo);
|
||||
|
|
|
@ -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<std::vector<ast> > 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<std::vector<ast> > 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<iz3translation> tr_killer_i;
|
||||
iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec_vec,std::vector<int>(),theory);
|
||||
tr_killer_i.set(tr);
|
||||
|
||||
// set the translation options, if needed
|
||||
if(options)
|
||||
for(hash_map<std::string,std::string>::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);
|
||||
|
||||
|
|
|
@ -68,7 +68,6 @@ public:
|
|||
typedef std::pair<hash_map<ast,Iproof::node>, hash_map<ast,Iproof::node> > AstToIpf;
|
||||
AstToIpf translation; // Z3 proof nodes to Iproof nodes
|
||||
|
||||
AstToInt frame_map; // map assertions to frames
|
||||
int frames; // number of frames
|
||||
|
||||
typedef std::set<ast> 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<ast,AstSet > foo(proof,AstSet());
|
||||
std::pair<AstToAstSet::iterator, bool> 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<ast> 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<ast> &cnsts,
|
||||
const std::vector<std::vector<ast> > &cnsts,
|
||||
const std::vector<int> &parents,
|
||||
const std::vector<ast> &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<ast> &cnsts,
|
||||
const std::vector<std::vector<ast> > &cnsts,
|
||||
const std::vector<int> &parents,
|
||||
const std::vector<ast> &theory){
|
||||
return new iz3translation_full(mgr,secondary,cnsts,parents,theory);
|
||||
|
|
|
@ -40,15 +40,15 @@ public:
|
|||
|
||||
static iz3translation *create(iz3mgr &mgr,
|
||||
iz3secondary *secondary,
|
||||
const std::vector<ast> &frames,
|
||||
const std::vector<std::vector<ast> > &frames,
|
||||
const std::vector<int> &parents,
|
||||
const std::vector<ast> &theory);
|
||||
|
||||
protected:
|
||||
iz3translation(iz3mgr &mgr,
|
||||
const std::vector<ast> &_cnsts,
|
||||
const std::vector<int> &_parents,
|
||||
const std::vector<ast> &_theory)
|
||||
const std::vector<std::vector<ast> > &_cnsts,
|
||||
const std::vector<int> &_parents,
|
||||
const std::vector<ast> &_theory)
|
||||
: iz3base(mgr,_cnsts,_parents,_theory) {}
|
||||
};
|
||||
|
||||
|
|
|
@ -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<ast> 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<ast,int>(ass,frame));
|
||||
return;
|
||||
|
@ -1655,16 +1650,12 @@ public:
|
|||
|
||||
iz3translation_direct(iz3mgr &mgr,
|
||||
iz3secondary *_secondary,
|
||||
const std::vector<ast> &cnsts,
|
||||
const std::vector<std::vector<ast> > &cnsts,
|
||||
const std::vector<int> &parents,
|
||||
const std::vector<ast> &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<ast> &cnsts,
|
||||
const std::vector<std::vector<ast> > &cnsts,
|
||||
const std::vector<int> &parents,
|
||||
const std::vector<ast> &theory){
|
||||
return new iz3translation_direct(mgr,secondary,cnsts,parents,theory);
|
||||
|
|
Loading…
Reference in a new issue