mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
added quantifiers in new interpolation
This commit is contained in:
parent
79b0f83ab3
commit
81df4932fb
|
@ -407,6 +407,10 @@ extern "C" {
|
|||
cnsts_vec[i] = a;
|
||||
}
|
||||
Z3_ast tree = parents_vector_to_tree(ctx,num,cnsts,parents);
|
||||
for(int i = 0; i < num_theory; i++){
|
||||
expr *a = to_expr(theory[i]);
|
||||
cnsts_vec.push_back(a);
|
||||
}
|
||||
iz3pp(mk_c(ctx)->m(),cnsts_vec,to_expr(tree),f);
|
||||
Z3_dec_ref(ctx,tree);
|
||||
}
|
||||
|
|
|
@ -640,3 +640,93 @@ iz3mgr::ast iz3mgr::mk_idiv(const ast& t, const ast &d){
|
|||
return mk_idiv(t,r);
|
||||
return make(Idiv,t,d);
|
||||
}
|
||||
|
||||
|
||||
// does variable occur in expression?
|
||||
int iz3mgr::occurs_in1(hash_map<ast,bool> &occurs_in_memo,ast var, ast e){
|
||||
std::pair<ast,bool> foo(e,false);
|
||||
std::pair<hash_map<ast,bool>::iterator,bool> bar = occurs_in_memo.insert(foo);
|
||||
bool &res = bar.first->second;
|
||||
if(bar.second){
|
||||
if(e == var) res = true;
|
||||
int nargs = num_args(e);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
res |= occurs_in1(occurs_in_memo,var,arg(e,i));
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
int iz3mgr::occurs_in(ast var, ast e){
|
||||
hash_map<ast,bool> memo;
|
||||
return occurs_in1(memo,var,e);
|
||||
}
|
||||
|
||||
|
||||
// find a controlling equality for a given variable v in a term
|
||||
// a controlling equality is of the form v = t, which, being
|
||||
// false would force the formula to have the specifid truth value
|
||||
// returns t, or null if no such
|
||||
|
||||
iz3mgr::ast iz3mgr::cont_eq(hash_set<ast> &cont_eq_memo, bool truth, ast v, ast e){
|
||||
if(is_not(e)) return cont_eq(cont_eq_memo, !truth,v,arg(e,0));
|
||||
if(cont_eq_memo.find(e) != cont_eq_memo.end())
|
||||
return ast();
|
||||
cont_eq_memo.insert(e);
|
||||
if(!truth && op(e) == Equal){
|
||||
if(arg(e,0) == v) return(arg(e,1));
|
||||
if(arg(e,1) == v) return(arg(e,0));
|
||||
}
|
||||
if((!truth && op(e) == And) || (truth && op(e) == Or)){
|
||||
int nargs = num_args(e);
|
||||
for(int i = 0; i < nargs; i++){
|
||||
ast res = cont_eq(cont_eq_memo, truth, v, arg(e,i));
|
||||
if(!res.null()) return res;
|
||||
}
|
||||
}
|
||||
if(truth && op(e) == Implies){
|
||||
ast res = cont_eq(cont_eq_memo, !truth, v, arg(e,0));
|
||||
if(!res.null()) return res;
|
||||
res = cont_eq(cont_eq_memo, truth, v, arg(e,1));
|
||||
if(!res.null()) return res;
|
||||
}
|
||||
return ast();
|
||||
}
|
||||
|
||||
// substitute a term t for unbound occurrences of variable v in e
|
||||
|
||||
iz3mgr::ast iz3mgr::subst(hash_map<ast,ast> &subst_memo, ast var, ast t, ast e){
|
||||
if(e == var) return t;
|
||||
std::pair<ast,ast> foo(e,ast());
|
||||
std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);
|
||||
ast &res = bar.first->second;
|
||||
if(bar.second){
|
||||
int nargs = num_args(e);
|
||||
std::vector<ast> args(nargs);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
args[i] = subst(subst_memo,var,t,arg(e,i));
|
||||
opr f = op(e);
|
||||
if(f == Equal && args[0] == args[1]) res = mk_true();
|
||||
else res = clone(e,args);
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
iz3mgr::ast iz3mgr::subst(ast var, ast t, ast e){
|
||||
hash_map<ast,ast> memo;
|
||||
return subst(memo,var,t,e);
|
||||
}
|
||||
|
||||
// apply a quantifier to a formula, with some optimizations
|
||||
// 1) bound variable does not occur -> no quantifier
|
||||
// 2) bound variable must be equal to some term -> substitute
|
||||
|
||||
iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){
|
||||
if(!occurs_in(var,e))return e;
|
||||
hash_set<ast> cont_eq_memo;
|
||||
ast cterm = cont_eq(cont_eq_memo, quantifier == Forall, var, e);
|
||||
if(!cterm.null()){
|
||||
return subst(var,cterm,e);
|
||||
}
|
||||
std::vector<ast> bvs; bvs.push_back(var);
|
||||
return make_quant(quantifier,bvs,e);
|
||||
}
|
||||
|
|
|
@ -612,6 +612,20 @@ class iz3mgr {
|
|||
|
||||
z3pf conc(const z3pf &t){return arg(t,num_prems(t));}
|
||||
|
||||
|
||||
/* quantifier handling */
|
||||
|
||||
// substitute a term t for unbound occurrences of variable v in e
|
||||
|
||||
ast subst(ast var, ast t, ast e);
|
||||
|
||||
// apply a quantifier to a formula, with some optimizations
|
||||
// 1) bound variable does not occur -> no quantifier
|
||||
// 2) bound variable must be equal to some term -> substitute
|
||||
|
||||
ast apply_quant(opr quantifier, ast var, ast e);
|
||||
|
||||
|
||||
/** For debugging */
|
||||
void show(ast);
|
||||
|
||||
|
@ -662,6 +676,11 @@ class iz3mgr {
|
|||
ast mki(family_id fid, decl_kind sk, int n, raw_ast **args);
|
||||
ast make(opr op, int n, raw_ast **args);
|
||||
ast make(symb sym, int n, raw_ast **args);
|
||||
int occurs_in1(stl_ext::hash_map<ast,bool> &occurs_in_memo, ast var, ast e);
|
||||
int occurs_in(ast var, ast e);
|
||||
ast cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, ast v, ast e);
|
||||
ast subst(stl_ext::hash_map<ast,ast> &subst_memo, ast var, ast t, ast e);
|
||||
|
||||
|
||||
family_id m_basic_fid;
|
||||
family_id m_array_fid;
|
||||
|
|
|
@ -2056,11 +2056,26 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
return new_var;
|
||||
}
|
||||
|
||||
ast add_quants(ast e){
|
||||
for(int i = localization_vars.size() - 1; i >= 0; i--){
|
||||
LocVar &lv = localization_vars[i];
|
||||
opr quantifier = (pv->in_range(lv.frame,rng)) ? Exists : Forall;
|
||||
e = apply_quant(quantifier,lv.var,e);
|
||||
}
|
||||
return e;
|
||||
}
|
||||
|
||||
node make_resolution(ast pivot, node premise1, node premise2) {
|
||||
std::vector<ast> lits;
|
||||
return make_resolution(pivot,lits,premise1,premise2);
|
||||
}
|
||||
|
||||
/* Return an interpolant from a proof of false */
|
||||
ast interpolate(const node &pf){
|
||||
// proof of false must be a formula, with quantified symbols
|
||||
return add_quants(pf);
|
||||
}
|
||||
|
||||
ast resolve_with_quantifier(const ast &pivot1, const ast &conj1,
|
||||
const ast &pivot2, const ast &conj2){
|
||||
if(is_not(arg(pivot1,1)))
|
||||
|
|
|
@ -118,6 +118,9 @@ class iz3proof_itp : public iz3mgr {
|
|||
is an affine term divisble by d and c is an integer constant */
|
||||
virtual node make_cut_rule(const ast &tleqc, const ast &d, const ast &con, const ast &prem) = 0;
|
||||
|
||||
/* Return an interpolant from a proof of false */
|
||||
virtual ast interpolate(const node &pf) = 0;
|
||||
|
||||
/** Create proof object to construct an interpolant. */
|
||||
static iz3proof_itp *create(prover *p, const prover::range &r, bool _weak);
|
||||
|
||||
|
|
|
@ -1141,7 +1141,8 @@ public:
|
|||
std::vector<ast> itps;
|
||||
for(int i = 0; i < frames -1; i++){
|
||||
iproof = iz3proof_itp::create(this,range_downward(i),weak_mode());
|
||||
ast itp = translate_main(proof);
|
||||
Iproof::node ipf = translate_main(proof);
|
||||
ast itp = iproof->interpolate(ipf);
|
||||
itps.push_back(itp);
|
||||
delete iproof;
|
||||
clear_translation();
|
||||
|
|
|
@ -219,11 +219,8 @@ public:
|
|||
AstToAst localization_map; // maps terms to their localization vars
|
||||
|
||||
typedef hash_map<ast,bool> AstToBool;
|
||||
AstToBool occurs_in_memo; // memo of occurs_in function
|
||||
|
||||
AstHashSet cont_eq_memo; // memo of cont_eq function
|
||||
|
||||
AstToAst subst_memo; // memo of subst function
|
||||
|
||||
iz3secondary *secondary; // the secondary prover
|
||||
|
||||
|
@ -613,83 +610,6 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
// does variable occur in expression?
|
||||
int occurs_in1(ast var, ast e){
|
||||
std::pair<ast,bool> foo(e,false);
|
||||
std::pair<AstToBool::iterator,bool> bar = occurs_in_memo.insert(foo);
|
||||
bool &res = bar.first->second;
|
||||
if(bar.second){
|
||||
if(e == var) res = true;
|
||||
int nargs = num_args(e);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
res |= occurs_in1(var,arg(e,i));
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
int occurs_in(ast var, ast e){
|
||||
occurs_in_memo.clear();
|
||||
return occurs_in1(var,e);
|
||||
}
|
||||
|
||||
// find a controlling equality for a given variable v in a term
|
||||
// a controlling equality is of the form v = t, which, being
|
||||
// false would force the formula to have the specifid truth value
|
||||
// returns t, or null if no such
|
||||
|
||||
ast cont_eq(bool truth, ast v, ast e){
|
||||
if(is_not(e)) return cont_eq(!truth,v,arg(e,0));
|
||||
if(cont_eq_memo.find(e) != cont_eq_memo.end())
|
||||
return ast();
|
||||
cont_eq_memo.insert(e);
|
||||
if(!truth && op(e) == Equal){
|
||||
if(arg(e,0) == v) return(arg(e,1));
|
||||
if(arg(e,1) == v) return(arg(e,0));
|
||||
}
|
||||
if((!truth && op(e) == And) || (truth && op(e) == Or)){
|
||||
int nargs = num_args(e);
|
||||
for(int i = 0; i < nargs; i++){
|
||||
ast res = cont_eq(truth, v, arg(e,i));
|
||||
if(!res.null()) return res;
|
||||
}
|
||||
}
|
||||
return ast();
|
||||
}
|
||||
|
||||
// substitute a term t for unbound occurrences of variable v in e
|
||||
|
||||
ast subst(ast var, ast t, ast e){
|
||||
if(e == var) return t;
|
||||
std::pair<ast,ast> foo(e,ast());
|
||||
std::pair<AstToAst::iterator,bool> bar = subst_memo.insert(foo);
|
||||
ast &res = bar.first->second;
|
||||
if(bar.second){
|
||||
int nargs = num_args(e);
|
||||
std::vector<ast> args(nargs);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
args[i] = subst(var,t,arg(e,i));
|
||||
opr f = op(e);
|
||||
if(f == Equal && args[0] == args[1]) res = mk_true();
|
||||
else res = clone(e,args);
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
// apply a quantifier to a formula, with some optimizations
|
||||
// 1) bound variable does not occur -> no quantifier
|
||||
// 2) bound variable must be equal to some term -> substitute
|
||||
|
||||
ast apply_quant(opr quantifier, ast var, ast e){
|
||||
if(!occurs_in(var,e))return e;
|
||||
cont_eq_memo.clear();
|
||||
ast cterm = cont_eq(quantifier == Forall, var, e);
|
||||
if(!cterm.null()){
|
||||
subst_memo.clear();
|
||||
return subst(var,cterm,e);
|
||||
}
|
||||
std::vector<ast> bvs; bvs.push_back(var);
|
||||
return make_quant(quantifier,bvs,e);
|
||||
}
|
||||
|
||||
// add quantifiers over the localization vars
|
||||
// to an interpolant for frames lo-hi
|
||||
|
|
Loading…
Reference in a new issue