mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
commit
bb8373151d
|
|
@ -153,8 +153,10 @@ class iz3base : public iz3mgr, public scopes {
|
|||
|
||||
int frames; // number of frames
|
||||
|
||||
protected:
|
||||
void add_frame_range(int frame, ast t);
|
||||
|
||||
private:
|
||||
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);
|
||||
|
|
|
|||
|
|
@ -240,7 +240,9 @@ iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector<ast> &_args){
|
|||
|
||||
|
||||
void iz3mgr::show(ast t){
|
||||
std::cout << mk_pp(t.raw(), m()) << std::endl;
|
||||
params_ref p;
|
||||
p.set_bool("flat_assoc",false);
|
||||
std::cout << mk_pp(t.raw(), m(), p) << std::endl;
|
||||
}
|
||||
|
||||
void iz3mgr::show_symb(symb s){
|
||||
|
|
@ -248,7 +250,9 @@ void iz3mgr::show_symb(symb s){
|
|||
}
|
||||
|
||||
void iz3mgr::print_expr(std::ostream &s, const ast &e){
|
||||
s << mk_pp(e.raw(), m());
|
||||
params_ref p;
|
||||
p.set_bool("flat_assoc",false);
|
||||
s << mk_pp(e.raw(), m(), p);
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -417,7 +417,16 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);
|
||||
ast &res = bar.first->second;
|
||||
if(bar.second){
|
||||
if(sym(e) == rotate_sum && var == get_placeholder(arg(e,0))){
|
||||
symb g = sym(e);
|
||||
if(g == rotate_sum){
|
||||
if(var == get_placeholder(arg(e,0))){
|
||||
res = e;
|
||||
}
|
||||
else
|
||||
res = make(rotate_sum,arg(e,0),subst_term_and_simp_rec(var,t,arg(e,1)));
|
||||
return res;
|
||||
}
|
||||
if(g == concat){
|
||||
res = e;
|
||||
return res;
|
||||
}
|
||||
|
|
@ -453,18 +462,26 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
int nargs = num_args(e);
|
||||
std::vector<ast> args(nargs);
|
||||
bool placeholder_arg = false;
|
||||
symb g = sym(e);
|
||||
if(g == concat){
|
||||
res = e;
|
||||
return res;
|
||||
}
|
||||
for(int i = 0; i < nargs; i++){
|
||||
args[i] = simplify_rec(arg(e,i));
|
||||
if(i == 0 && g == rotate_sum)
|
||||
args[i] = arg(e,i);
|
||||
else
|
||||
args[i] = simplify_rec(arg(e,i));
|
||||
placeholder_arg |= is_placeholder(args[i]);
|
||||
}
|
||||
try {
|
||||
opr f = op(e);
|
||||
if(f == Equal && args[0] == args[1]) res = mk_true();
|
||||
else if(f == And) res = my_and(args);
|
||||
else if(f == Or) res = my_or(args);
|
||||
else if(f == Or)
|
||||
res = my_or(args);
|
||||
else if(f == Idiv) res = mk_idiv(args[0],args[1]);
|
||||
else if(f == Uninterpreted && !placeholder_arg){
|
||||
symb g = sym(e);
|
||||
if(g == rotate_sum) res = simplify_rotate(args);
|
||||
else if(g == symm) res = simplify_symm(args);
|
||||
else if(g == modpon) res = simplify_modpon(args);
|
||||
|
|
@ -1831,6 +1848,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
itp = mk_true();
|
||||
break;
|
||||
default: { // mixed equality
|
||||
if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed)
|
||||
std::cerr << "WARNING: mixed term in leq2eq\n";
|
||||
std::vector<ast> conjs; conjs.resize(3);
|
||||
conjs[0] = mk_not(con);
|
||||
conjs[1] = xleqy;
|
||||
|
|
@ -1943,38 +1962,45 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
hash_map<ast,ast>::iterator it = localization_map.find(e);
|
||||
if(it != localization_map.end()){
|
||||
pf = localization_pf_map[e];
|
||||
return it->second;
|
||||
e = it->second;
|
||||
}
|
||||
|
||||
// if is is non-local, we must first localize the arguments to
|
||||
// the range of its function symbol
|
||||
|
||||
int nargs = num_args(e);
|
||||
if(nargs > 0 /* && (!is_local(e) || flo <= hi || fhi >= lo) */){
|
||||
prover::range frng = rng;
|
||||
if(op(e) == Uninterpreted){
|
||||
symb f = sym(e);
|
||||
prover::range srng = pv->sym_range(f);
|
||||
if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible
|
||||
frng = pv->range_glb(srng,rng);
|
||||
}
|
||||
std::vector<ast> largs(nargs);
|
||||
std::vector<ast> eqs;
|
||||
std::vector<ast> pfs;
|
||||
for(int i = 0; i < nargs; i++){
|
||||
ast argpf;
|
||||
largs[i] = localize_term(arg(e,i),frng,argpf);
|
||||
frng = pv->range_glb(frng,pv->ast_scope(largs[i]));
|
||||
if(largs[i] != arg(e,i)){
|
||||
eqs.push_back(make_equiv(largs[i],arg(e,i)));
|
||||
pfs.push_back(argpf);
|
||||
else {
|
||||
// if it is non-local, we must first localize the arguments to
|
||||
// the range of its function symbol
|
||||
|
||||
int nargs = num_args(e);
|
||||
if(nargs > 0 /* && (!is_local(e) || flo <= hi || fhi >= lo) */){
|
||||
prover::range frng = rng;
|
||||
if(op(e) == Uninterpreted){
|
||||
symb f = sym(e);
|
||||
prover::range srng = pv->sym_range(f);
|
||||
if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible
|
||||
frng = pv->range_glb(srng,rng);
|
||||
else
|
||||
frng = srng; // this term will be localized
|
||||
}
|
||||
std::vector<ast> largs(nargs);
|
||||
std::vector<ast> eqs;
|
||||
std::vector<ast> pfs;
|
||||
for(int i = 0; i < nargs; i++){
|
||||
ast argpf;
|
||||
largs[i] = localize_term(arg(e,i),frng,argpf);
|
||||
frng = pv->range_glb(frng,pv->ast_scope(largs[i]));
|
||||
if(largs[i] != arg(e,i)){
|
||||
eqs.push_back(make_equiv(largs[i],arg(e,i)));
|
||||
pfs.push_back(argpf);
|
||||
}
|
||||
}
|
||||
|
||||
e = clone(e,largs);
|
||||
if(pfs.size())
|
||||
pf = make_congruence(eqs,make_equiv(e,orig_e),pfs);
|
||||
// assert(is_local(e));
|
||||
}
|
||||
|
||||
e = clone(e,largs);
|
||||
if(pfs.size())
|
||||
pf = make_congruence(eqs,make_equiv(e,orig_e),pfs);
|
||||
// assert(is_local(e));
|
||||
|
||||
localization_pf_map[orig_e] = pf;
|
||||
localization_map[orig_e] = e;
|
||||
}
|
||||
|
||||
if(pv->ranges_intersect(pv->ast_scope(e),rng))
|
||||
|
|
@ -1984,7 +2010,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
|
|||
int frame = pv->range_near(pv->ast_scope(e),rng);
|
||||
|
||||
ast new_var = fresh_localization_var(e,frame);
|
||||
localization_map[e] = new_var;
|
||||
localization_map[orig_e] = new_var;
|
||||
std::vector<ast> foo; foo.push_back(make_equiv(new_var,e));
|
||||
ast bar = make_assumption(frame,foo);
|
||||
pf = make_transitivity(new_var,e,orig_e,bar,pf);
|
||||
|
|
|
|||
|
|
@ -105,6 +105,42 @@ public:
|
|||
range rng; // the range of frames in the "A" part of the interpolant
|
||||
#endif
|
||||
|
||||
/* To handle skolemization, we have to scan the proof for skolem
|
||||
symbols and assign each to a frame. THe assignment is heuristic.
|
||||
*/
|
||||
|
||||
void scan_skolems_rec(hash_set<ast> &memo, const ast &proof){
|
||||
std::pair<hash_set<ast>::iterator,bool> bar = memo.insert(proof);
|
||||
if(!bar.second)
|
||||
return;
|
||||
pfrule dk = pr(proof);
|
||||
if(dk == PR_SKOLEMIZE){
|
||||
ast quanted = arg(conc(proof),0);
|
||||
if(op(quanted) == Not)
|
||||
quanted = arg(quanted,0);
|
||||
range r = ast_range(quanted);
|
||||
if(range_is_empty(r))
|
||||
r = ast_scope(quanted);
|
||||
if(range_is_empty(r))
|
||||
throw "can't skolemize";
|
||||
int frame = range_max(r);
|
||||
if(frame >= frames) frame = frames - 1;
|
||||
add_frame_range(frame,arg(conc(proof),1));
|
||||
r = ast_scope(arg(conc(proof),1));
|
||||
}
|
||||
else {
|
||||
unsigned nprems = num_prems(proof);
|
||||
for(unsigned i = 0; i < nprems; i++){
|
||||
scan_skolems_rec(memo,prem(proof,i));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void scan_skolems(const ast &proof){
|
||||
hash_set<ast> memo;
|
||||
scan_skolems_rec(memo,proof);
|
||||
}
|
||||
|
||||
// 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
|
||||
|
|
@ -115,7 +151,8 @@ public:
|
|||
std::pair<AstToInt::iterator, bool> bar = locality.insert(foo);
|
||||
int &res = bar.first->second;
|
||||
if(!bar.second) return res;
|
||||
if(pr(proof) == PR_ASSERTED){
|
||||
pfrule dk = pr(proof);
|
||||
if(dk == PR_ASSERTED){
|
||||
ast ass = conc(proof);
|
||||
res = frame_of_assertion(ass);
|
||||
#ifdef NEW_LOCALITY
|
||||
|
|
@ -125,6 +162,12 @@ public:
|
|||
res = frames-1;
|
||||
#endif
|
||||
}
|
||||
else if(dk == PR_QUANT_INST){
|
||||
std::vector<ast> lits;
|
||||
ast con = conc(proof);
|
||||
get_Z3_lits(con, lits);
|
||||
iproof->make_axiom(lits);
|
||||
}
|
||||
else {
|
||||
unsigned nprems = num_prems(proof);
|
||||
for(unsigned i = 0; i < nprems; i++){
|
||||
|
|
@ -563,6 +606,33 @@ public:
|
|||
return 1;
|
||||
}
|
||||
|
||||
void symbols_out_of_scope_rec(hash_set<ast> &memo, hash_set<symb> &symb_memo, int frame, const ast &t){
|
||||
if(memo.find(t) != memo.end())
|
||||
return;
|
||||
memo.insert(t);
|
||||
if(op(t) == Uninterpreted){
|
||||
symb s = sym(t);
|
||||
range r = sym_range(s);
|
||||
if(!in_range(frame,r) && symb_memo.find(s) == symb_memo.end()){
|
||||
std::cout << string_of_symbol(s) << "\n";
|
||||
symb_memo.insert(s);
|
||||
}
|
||||
}
|
||||
int nargs = num_args(t);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
symbols_out_of_scope_rec(memo,symb_memo,frame,arg(t,i));
|
||||
}
|
||||
|
||||
void symbols_out_of_scope(int frame, const ast &t){
|
||||
hash_set<ast> memo;
|
||||
hash_set<symb> symb_memo;
|
||||
symbols_out_of_scope_rec(memo,symb_memo,frame,t);
|
||||
}
|
||||
|
||||
void conc_symbols_out_of_scope(int frame, const ast &t){
|
||||
symbols_out_of_scope(frame,conc(t));
|
||||
}
|
||||
|
||||
std::vector<ast> lit_trace;
|
||||
hash_set<ast> marked_proofs;
|
||||
|
||||
|
|
@ -634,18 +704,36 @@ public:
|
|||
return !(f == And || f == Or || f == Iff);
|
||||
}
|
||||
|
||||
hash_map<int,ast> asts_by_id;
|
||||
|
||||
void print_lit(const ast &lit){
|
||||
ast abslit = is_not(lit) ? arg(lit,0) : lit;
|
||||
if(!is_literal_or_lit_iff(lit)){
|
||||
if(is_not(lit)) std::cout << "~";
|
||||
std::cout << "[";
|
||||
// print_expr(std::cout,abslit);
|
||||
std::cout << "]";
|
||||
int id = ast_id(abslit);
|
||||
asts_by_id[id] = abslit;
|
||||
std::cout << "[" << id << "]";
|
||||
}
|
||||
else
|
||||
print_expr(std::cout,lit);
|
||||
}
|
||||
|
||||
void expand(int id){
|
||||
if(asts_by_id.find(id) == asts_by_id.end())
|
||||
std::cout << "undefined\n";
|
||||
else {
|
||||
ast lit = asts_by_id[id];
|
||||
std::string s = string_of_symbol(sym(lit));
|
||||
std::cout << "(" << s;
|
||||
unsigned nargs = num_args(lit);
|
||||
for(unsigned i = 0; i < nargs; i++){
|
||||
std::cout << " ";
|
||||
print_lit(arg(lit,i));
|
||||
}
|
||||
std::cout << ")\n";;
|
||||
}
|
||||
}
|
||||
|
||||
void show_lit(const ast &lit){
|
||||
print_lit(lit);
|
||||
std::cout << "\n";
|
||||
|
|
@ -682,6 +770,8 @@ public:
|
|||
print_lit(lits[i]);
|
||||
std::cout << " ";
|
||||
}
|
||||
range r = ast_scope(con);
|
||||
std::cout << " {" << r.lo << "," << r.hi << "}";
|
||||
std::cout << "\n";
|
||||
}
|
||||
|
||||
|
|
@ -753,8 +843,12 @@ public:
|
|||
ast prem0 = prem(proof,0);
|
||||
Iproof::node itp = translate_main(prem0,true);
|
||||
std::vector<ast> clause;
|
||||
get_Z3_lits(conc(prem0),clause);
|
||||
ast conc0 = conc(prem0);
|
||||
int nprems = num_prems(proof);
|
||||
if(nprems == 2 && conc0 == mk_not(conc(prem(proof,1))))
|
||||
clause.push_back(conc0);
|
||||
else
|
||||
get_Z3_lits(conc0,clause);
|
||||
for(int position = 1; position < nprems; position++){
|
||||
ast ante = prem(proof,position);
|
||||
ast pnode = conc(ante);
|
||||
|
|
@ -1215,7 +1309,61 @@ public:
|
|||
return res;
|
||||
}
|
||||
|
||||
|
||||
bool is_eq_propagate(const ast &proof){
|
||||
return pr(proof) == PR_TH_LEMMA && get_theory_lemma_theory(proof) == ArithTheory && get_theory_lemma_kind(proof) == EqPropagateKind;
|
||||
}
|
||||
|
||||
ast EqPropagate(const ast &con, const std::vector<ast> &prems, const std::vector<Iproof::node> &args){
|
||||
Iproof::node fps[2];
|
||||
ast ineq_con[2];
|
||||
for(int i = 0; i < 2; i++){
|
||||
opr o = i == 0 ? Leq : Geq;
|
||||
ineq_con[i] = make(o, arg(con,0), arg(con,1));
|
||||
fps[i] = reconstruct_farkas(prems,args,ineq_con[i]);
|
||||
}
|
||||
ast res = iproof->make_leq2eq(arg(con,0), arg(con,1), ineq_con[0], ineq_con[1]);
|
||||
std::vector<Iproof::node> dummy_clause;
|
||||
for(int i = 0; i < 2; i++)
|
||||
res = iproof->make_resolution(ineq_con[i],dummy_clause,res,fps[i]);
|
||||
return res;
|
||||
}
|
||||
|
||||
struct CannotCombineEqPropagate {};
|
||||
|
||||
void CombineEqPropagateRec(const ast &proof, std::vector<ast> &prems, std::vector<Iproof::node> &args, ast &eqprem){
|
||||
if(pr(proof) == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){
|
||||
CombineEqPropagateRec(prem(proof,0), prems, args, eqprem);
|
||||
ast dummy;
|
||||
CombineEqPropagateRec(prem(proof,1), prems, args, dummy);
|
||||
return;
|
||||
}
|
||||
if(is_eq_propagate(proof)){
|
||||
int nprems = num_prems(proof);
|
||||
for(int i = 0; i < nprems; i++){
|
||||
prems.push_back(prem(proof,i));
|
||||
ast ppf = translate_main(prem(proof,i),false);
|
||||
args.push_back(ppf);
|
||||
}
|
||||
return;
|
||||
}
|
||||
eqprem = proof;
|
||||
}
|
||||
|
||||
ast CombineEqPropagate(const ast &proof){
|
||||
std::vector<ast> prems, args;
|
||||
ast eq1;
|
||||
CombineEqPropagateRec(proof, prems, args, eq1);
|
||||
ast eq2con = conc(proof);
|
||||
if(!eq1.null())
|
||||
eq2con = make(Equal,arg(conc(eq1),1),arg(conc(proof),1));
|
||||
ast eq2 = EqPropagate(eq2con,prems,args);
|
||||
if(!eq1.null()){
|
||||
Iproof::node foo = translate_main(eq1,false);
|
||||
eq2 = iproof->make_transitivity(arg(conc(eq1),0), arg(conc(eq1),1), arg(conc(proof),1), foo, eq2);
|
||||
}
|
||||
return eq2;
|
||||
}
|
||||
|
||||
// translate a Z3 proof term into interpolating proof system
|
||||
|
||||
Iproof::node translate_main(ast proof, bool expect_clause = true){
|
||||
|
|
@ -1290,6 +1438,15 @@ public:
|
|||
res = make(commute,clause,conc(prem(proof,0))); // HACK -- we depend on Iproof::node being same as ast.
|
||||
return res;
|
||||
}
|
||||
|
||||
if(dk == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){
|
||||
try {
|
||||
res = CombineEqPropagate(proof);
|
||||
return res;
|
||||
}
|
||||
catch(const CannotCombineEqPropagate &){
|
||||
}
|
||||
}
|
||||
|
||||
// translate all the premises
|
||||
std::vector<Iproof::node> args(nprems);
|
||||
|
|
@ -1412,20 +1569,10 @@ public:
|
|||
}
|
||||
case EqPropagateKind: {
|
||||
std::vector<ast> prems(nprems);
|
||||
Iproof::node fps[2];
|
||||
ast ineq_con[2];
|
||||
for(int i = 0; i < nprems; i++)
|
||||
for(unsigned i = 0; i < nprems; i++)
|
||||
prems[i] = prem(proof,i);
|
||||
for(int i = 0; i < 2; i++){
|
||||
opr o = i == 0 ? Leq : Geq;
|
||||
ineq_con[i] = make(o, arg(con,0), arg(con,1));
|
||||
fps[i] = reconstruct_farkas(prems,args,ineq_con[i]);
|
||||
}
|
||||
res = iproof->make_leq2eq(arg(con,0), arg(con,1), ineq_con[0], ineq_con[1]);
|
||||
std::vector<Iproof::node> dummy_clause;
|
||||
for(int i = 0; i < 2; i++)
|
||||
res = iproof->make_resolution(ineq_con[i],dummy_clause,res,fps[i]);
|
||||
return res;
|
||||
res = EqPropagate(con,prems,args);
|
||||
break;
|
||||
}
|
||||
default:
|
||||
throw unsupported();
|
||||
|
|
@ -1447,6 +1594,10 @@ public:
|
|||
res = iproof->make_axiom(lits);
|
||||
break;
|
||||
}
|
||||
case PR_DEF_AXIOM: { // this should only happen for formulas resulting from quantifier instantiation
|
||||
res = iproof->make_axiom(lits);
|
||||
break;
|
||||
}
|
||||
default:
|
||||
assert(0 && "translate_main: unsupported proof rule");
|
||||
throw unsupported();
|
||||
|
|
@ -1465,6 +1616,7 @@ public:
|
|||
|
||||
iz3proof::node translate(ast proof, iz3proof &dst){
|
||||
std::vector<ast> itps;
|
||||
scan_skolems(proof);
|
||||
for(int i = 0; i < frames -1; i++){
|
||||
#ifdef NEW_LOCALITY
|
||||
rng = range_downward(i);
|
||||
|
|
@ -1556,6 +1708,17 @@ void iz3translation_full_pfprem(iz3translation_full *p, int i){
|
|||
p->pfprem(i);
|
||||
}
|
||||
|
||||
void iz3translation_full_expand(iz3translation_full *p, int i){
|
||||
p->expand(i);
|
||||
}
|
||||
|
||||
void iz3translation_full_symbols_out_of_scope(iz3translation_full *p, int i, const iz3mgr::ast &t){
|
||||
p->symbols_out_of_scope(i,t);
|
||||
}
|
||||
|
||||
void iz3translation_full_conc_symbols_out_of_scope(iz3translation_full *p, int i, const iz3mgr::ast &t){
|
||||
p->conc_symbols_out_of_scope(i,t);
|
||||
}
|
||||
|
||||
struct stdio_fixer {
|
||||
stdio_fixer(){
|
||||
|
|
|
|||
Loading…
Reference in a new issue