3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

merging interpolation and duality changes into unstable

This commit is contained in:
Ken McMillan 2014-02-19 15:36:16 -08:00
commit 75bb495585
9 changed files with 420 additions and 82 deletions

24
src/duality/duality.h Normal file → Executable file
View file

@ -1184,7 +1184,13 @@ namespace Duality {
hash_map<Edge *, Edge *> EdgeCloneMap;
std::vector<expr> alit_stack;
std::vector<unsigned> alit_stack_sizes;
hash_map<Edge *, uptr<LogicSolver> > edge_solvers;
// to let us use one solver per edge
struct edge_solver {
hash_map<ast,expr> AssumptionLits;
uptr<solver> slvr;
};
hash_map<Edge *, edge_solver > edge_solvers;
#ifdef LIMIT_STACK_WEIGHT
struct weight_counter {
@ -1236,19 +1242,23 @@ namespace Duality {
void GetTermTreeAssertionLiteralsRec(TermTree *assumptions);
LogicSolver *SolverForEdge(Edge *edge, bool models);
edge_solver &SolverForEdge(Edge *edge, bool models, bool axioms);
public:
struct scoped_solver_for_edge {
LogicSolver *orig_ls;
solver *orig_slvr;
RPFP_caching *rpfp;
scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){
edge_solver *es;
scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false, bool axioms = false){
rpfp = _rpfp;
orig_ls = rpfp->ls;
rpfp->ls = rpfp->SolverForEdge(edge,models);
orig_slvr = rpfp->ls->slvr;
es = &(rpfp->SolverForEdge(edge,models,axioms));
rpfp->ls->slvr = es->slvr.get();
rpfp->AssumptionLits.swap(es->AssumptionLits);
}
~scoped_solver_for_edge(){
rpfp->ls = orig_ls;
rpfp->ls->slvr = orig_slvr;
rpfp->AssumptionLits.swap(es->AssumptionLits);
}
};

53
src/duality/duality_rpfp.cpp Normal file → Executable file
View file

@ -2711,10 +2711,12 @@ namespace Duality {
const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++)
s.add(theory[i]);
if(s.check(lits.size(),&lits[0]) != unsat)
throw "should be unsat";
for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something!
if(s.check(lits.size(),&lits[0]) == unsat)
goto is_unsat;
throw "should be unsat";
}
is_unsat:
for(unsigned i = 0; i < conjuncts.size(); ){
std::swap(conjuncts[i],conjuncts.back());
std::swap(lits[i],lits.back());
@ -2747,8 +2749,20 @@ namespace Duality {
// verify
check_result res = CheckCore(lits,full_core);
if(res != unsat)
if(res != unsat){
// add the axioms in the off chance they are useful
const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++)
GetAssumptionLits(theory[i],assumps);
lits = assumps;
std::copy(core.begin(),core.end(),std::inserter(lits,lits.end()));
for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something!
if((res = CheckCore(lits,full_core)) == unsat)
goto is_unsat;
throw "should be unsat";
}
is_unsat:
FilterCore(core,full_core);
std::vector<expr> dummy;
@ -2889,13 +2903,20 @@ namespace Duality {
timer_stop("Generalize");
}
RPFP::LogicSolver *RPFP_caching::SolverForEdge(Edge *edge, bool models){
uptr<LogicSolver> &p = edge_solvers[edge];
RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models, bool axioms){
edge_solver &es = edge_solvers[edge];
uptr<solver> &p = es.slvr;
if(!p.get()){
scoped_no_proof no_proofs_please(ctx.m()); // no proofs
p.set(new iZ3LogicSolver(ctx,models)); // no models
p.set(new solver(ctx,true,models)); // no models
if(axioms){
RPFP::LogicSolver *ls = edge->owner->ls;
const std::vector<expr> &axs = ls->get_axioms();
for(unsigned i = 0; i < axs.size(); i++)
p.get()->add(axs[i]);
}
}
return p.get();
return es;
}
@ -3362,6 +3383,8 @@ namespace Duality {
}
}
bool some_labels = false;
// create the edges
for(unsigned i = 0; i < clauses.size(); i++){
@ -3397,17 +3420,23 @@ namespace Duality {
Term labeled = body;
std::vector<label_struct > lbls; // TODO: throw this away for now
body = RemoveLabels(body,lbls);
if(!eq(labeled,body))
some_labels = true; // remember if there are labels, as we then can't do qe_lite
// body = IneqToEq(body); // UFO converts x=y to (x<=y & x >= y). Undo this.
body = body.simplify();
#ifdef USE_QE_LITE
std::set<int> idxs;
for(unsigned j = 0; j < Indparams.size(); j++)
if(Indparams[j].is_var())
idxs.insert(Indparams[j].get_index_value());
body = body.qe_lite(idxs,false);
if(!some_labels){ // can't do qe_lite if we have to reconstruct labels
for(unsigned j = 0; j < Indparams.size(); j++)
if(Indparams[j].is_var())
idxs.insert(Indparams[j].get_index_value());
body = body.qe_lite(idxs,false);
}
hash_map<int,hash_map<ast,Term> > sb_memo;
body = SubstBoundRec(sb_memo,substs[i],0,body);
if(some_labels)
labeled = SubstBoundRec(sb_memo,substs[i],0,labeled);
for(unsigned j = 0; j < Indparams.size(); j++)
Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]);
#endif

29
src/duality/duality_solver.cpp Normal file → Executable file
View file

@ -51,12 +51,17 @@ Revision History:
// #define TOP_DOWN
// #define EFFORT_BOUNDED_STRAT
#define SKIP_UNDERAPPROX_NODES
#define USE_RPFP_CLONE
// #define KEEP_EXPANSIONS
// #define USE_CACHING_RPFP
// #define PROPAGATE_BEFORE_CHECK
#define USE_RPFP_CLONE
#define USE_NEW_GEN_CANDS
//#define NO_PROPAGATE
//#define NO_GENERALIZE
//#define NO_DECISIONS
namespace Duality {
// TODO: must be a better place for this...
@ -129,13 +134,11 @@ namespace Duality {
{
scoped_no_proof no_proofs_please(ctx.m());
#ifdef USE_RPFP_CLONE
clone_ls = new RPFP::iZ3LogicSolver(ctx, false); // no models needed for this one
clone_rpfp = new RPFP_caching(clone_ls);
clone_rpfp = new RPFP_caching(rpfp->ls);
clone_rpfp->Clone(rpfp);
#endif
#ifdef USE_NEW_GEN_CANDS
gen_cands_ls = new RPFP::iZ3LogicSolver(ctx);
gen_cands_rpfp = new RPFP_caching(gen_cands_ls);
gen_cands_rpfp = new RPFP_caching(rpfp->ls);
gen_cands_rpfp->Clone(rpfp);
#endif
}
@ -144,20 +147,16 @@ namespace Duality {
~Duality(){
#ifdef USE_RPFP_CLONE
delete clone_rpfp;
delete clone_ls;
#endif
#ifdef USE_NEW_GEN_CANDS
delete gen_cands_rpfp;
delete gen_cands_ls;
#endif
}
#ifdef USE_RPFP_CLONE
RPFP::LogicSolver *clone_ls;
RPFP_caching *clone_rpfp;
#endif
#ifdef USE_NEW_GEN_CANDS
RPFP::LogicSolver *gen_cands_ls;
RPFP_caching *gen_cands_rpfp;
#endif
@ -1255,7 +1254,7 @@ namespace Duality {
slvr.pop(1);
delete checker;
#else
RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */);
RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
gen_cands_rpfp->Push();
Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
if(gen_cands_rpfp->Check(root) != unsat){
@ -1940,11 +1939,15 @@ namespace Duality {
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
tree->SolveSingleNode(top,node);
#ifdef NO_GENERALIZE
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
#else
if(expansions.size() == 1 && NodeTooComplicated(node))
SimplifyNode(node);
else
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
Generalize(node);
#endif
if(RecordUpdate(node))
update_count++;
else
@ -1984,7 +1987,9 @@ namespace Duality {
if(stack.size() == 1)break;
if(prev_level_used){
Node *node = stack.back().expansions[0];
#ifndef NO_PROPAGATE
if(!Propagate(node)) break;
#endif
if(!RecordUpdate(node)) break; // shouldn't happen!
RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
propagated = true;
@ -2006,11 +2011,13 @@ namespace Duality {
}
else {
was_sat = true;
tree->Push();
tree->Push();
std::vector<Node *> &expansions = stack.back().expansions;
#ifndef NO_DECISIONS
for(unsigned i = 0; i < expansions.size(); i++){
tree->FixCurrentState(expansions[i]->Outgoing);
}
#endif
#if 0
if(tree->slvr().check() == unsat)
throw "help!";

0
src/duality/duality_wrapper.cpp Normal file → Executable file
View file

23
src/interp/iz3mgr.cpp Normal file → Executable file
View file

@ -249,6 +249,9 @@ iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector<ast> &_args){
void iz3mgr::show(ast t){
if(t.null()){
std::cout << "(null)" << std::endl;
}
params_ref p;
p.set_bool("flat_assoc",false);
std::cout << mk_pp(t.raw(), m(), p) << std::endl;
@ -693,10 +696,13 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
throw "not an inequality";
}
}
Qrhs = make(Times,c,Qrhs);
bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
if(pstrict && qstrict && round_off)
bool pstrict = op(P) == Lt;
if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
Qrhs = make(Sub,Qrhs,make_int(rational(1)));
qstrict = false;
}
Qrhs = make(Times,c,Qrhs);
bool strict = pstrict || qstrict;
if(strict)
P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
else
@ -881,3 +887,14 @@ iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){
std::vector<ast> bvs; bvs.push_back(var);
return make_quant(quantifier,bvs,e);
}
#if 0
void iz3mgr::get_bound_substitutes(stl_ext::hash_map<ast,bool> &memo, const ast &e, const ast &var, std::vector<ast> &substs){
std::pair<ast,bool> foo(e,false);
std::pair<hash_map<ast,bool>::iterator,bool> bar = memo.insert(foo);
if(bar.second){
if(op(e) ==
}
}
#endif

0
src/interp/iz3mgr.h Normal file → Executable file
View file

255
src/interp/iz3proof_itp.cpp Normal file → Executable file
View file

@ -579,18 +579,36 @@ class iz3proof_itp_impl : public iz3proof_itp {
return is_ineq(ineq);
}
ast destruct_cond_ineq(const ast &ineq, ast &Aproves, ast &Bproves){
ast res = ineq;
opr o = op(res);
if(o == And){
Aproves = my_and(Aproves,arg(res,0));
res = arg(res,1);
o = op(res);
}
if(o == Implies){
Bproves = my_and(Bproves,arg(res,0));
res = arg(res,1);
}
return res;
}
ast simplify_sum(std::vector<ast> &args){
ast Aproves = mk_true(), Bproves = mk_true();
ast ineq = args[0];
ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves);
if(!is_normal_ineq(ineq)) throw cannot_simplify();
sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves);
return my_and(Aproves,my_implies(Bproves,ineq));
}
ast simplify_rotate_sum(const ast &pl, const ast &pf){
ast cond = mk_true();
ast Aproves = mk_true(), Bproves = mk_true();
ast ineq = make(Leq,make_int("0"),make_int("0"));
return rotate_sum_rec(pl,pf,cond,ineq);
ineq = rotate_sum_rec(pl,pf,Aproves,Bproves,ineq);
if(is_true(Aproves) && is_true(Bproves))
return ineq;
return my_and(Aproves,my_implies(Bproves,ineq));
}
bool is_rewrite_chain(const ast &chain){
@ -623,7 +641,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){
opr o = op(ineq2);
if(o == Implies){
if(o == And){
sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves);
Aproves = my_and(Aproves,arg(ineq2,0));
}
else if(o == Implies){
sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves);
Bproves = my_and(Bproves,arg(ineq2,0));
}
@ -683,23 +705,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor));
}
ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){
if(pf == pl)
return my_implies(Bproves,simplify_ineq(ineq));
ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Aproves, ast &Bproves, ast &ineq){
if(pf == pl){
if(sym(ineq) == normal)
return ineq;
return simplify_ineq(ineq);
}
if(op(pf) == Uninterpreted && sym(pf) == sum){
if(arg(pf,2) == pl){
ast Aproves = mk_true();
sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves);
if(!is_true(Aproves))
throw "help!";
ineq = idiv_ineq(ineq,arg(pf,1));
return my_implies(Bproves,ineq);
return ineq;
}
ast Aproves = mk_true();
sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves);
if(!is_true(Aproves))
throw "help!";
return rotate_sum_rec(pl,arg(pf,0),Bproves,ineq);
return rotate_sum_rec(pl,arg(pf,0),Aproves,Bproves,ineq);
}
throw cannot_simplify();
}
@ -749,6 +768,28 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
}
ast unmixed_eq2ineq(const ast &lhs, const ast &rhs, opr comp_op, const ast &equa, ast &cond){
ast ineqs= chain_ineqs(comp_op,LitA,equa,lhs,rhs); // chain must be from lhs to rhs
cond = my_and(cond,chain_conditions(LitA,equa));
ast Bconds = z3_simplify(chain_conditions(LitB,equa));
if(is_true(Bconds) && op(ineqs) != And)
return my_implies(cond,ineqs);
if(op(ineqs) != And)
return my_and(Bconds,my_implies(cond,ineqs));
throw "help!";
}
ast add_mixed_eq2ineq(const ast &lhs, const ast &rhs, const ast &equa, const ast &itp){
if(is_true(equa))
return itp;
std::vector<ast> args(3);
args[0] = itp;
args[1] = make_int("1");
ast ineq = make(Leq,make_int(rational(0)),make_int(rational(0)));
args[2] = make_normal(ineq,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
return simplify_sum(args);
}
ast simplify_rotate_eq2leq(const ast &pl, const ast &neg_equality, const ast &pf){
if(pl == arg(pf,1)){
ast cond = mk_true();
@ -756,20 +797,21 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(is_equivrel_chain(equa)){
ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove
LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs);
if(lhst != LitMixed && rhst != LitMixed){
ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs
cond = my_and(cond,chain_conditions(LitA,equa));
ast Bconds = z3_simplify(chain_conditions(LitB,equa));
if(is_true(Bconds) && op(ineqs) != And)
return my_implies(cond,ineqs);
}
if(lhst != LitMixed && rhst != LitMixed)
return unmixed_eq2ineq(lhs, rhs, op(arg(neg_equality,0)), equa, cond);
else {
ast itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
return make_normal(itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
ast left, left_term, middle, right_term, right;
left = get_left_movers(equa,lhs,middle,left_term);
middle = get_right_movers(middle,rhs,right,right_term);
ast itp = unmixed_eq2ineq(left_term, right_term, op(arg(neg_equality,0)), middle, cond);
// itp = my_implies(cond,itp);
itp = add_mixed_eq2ineq(lhs, left_term, left, itp);
itp = add_mixed_eq2ineq(right_term, rhs, right, itp);
return itp;
}
}
}
throw cannot_simplify();
throw "help!";
}
void reverse_modpon(std::vector<ast> &args){
@ -836,6 +878,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast equa = sep_cond(args[0],cond);
if(is_equivrel_chain(equa))
return my_implies(cond,reverse_chain(equa));
if(is_negation_chain(equa))
return commute_negation_chain(equa);
throw cannot_simplify();
}
@ -909,7 +953,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves);
ast itp;
if(is_rewrite_side(LitA,head)){
itp = ineq1;
itp = make(Leq,make_int("0"),make_int("0"));
linear_comb(itp,make_int("1"),ineq1); // make sure it is normal form
//itp = ineq1;
ast mc = z3_simplify(chain_side_proves(LitB,pref));
Bproves = my_and(Bproves,mc);
}
@ -951,7 +997,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast simplify_modpon(const std::vector<ast> &args){
ast Aproves = mk_true(), Bproves = mk_true();
ast chain = simplify_modpon_fwd(args,Bproves);
ast Q2 = sep_cond(args[2],Bproves);
ast Q2 = destruct_cond_ineq(args[2],Aproves,Bproves);
ast interp;
if(is_normal_ineq(Q2)){ // inequalities are special
ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves);
@ -1450,6 +1496,50 @@ class iz3proof_itp_impl : public iz3proof_itp {
return is_negation_chain(rest);
}
ast commute_negation_chain(const ast &chain){
if(is_true(chain))
return chain;
ast last = chain_last(chain);
ast rest = chain_rest(chain);
if(is_true(rest)){
ast old = rewrite_rhs(last);
if(!(op(old) == Not))
throw "bad negative equality chain";
ast equ = arg(old,0);
if(!is_equivrel(equ))
throw "bad negative equality chain";
last = rewrite_update_rhs(last,top_pos,make(Not,make(op(equ),arg(equ,1),arg(equ,0))),make(True));
return chain_cons(rest,last);
}
ast pos = rewrite_pos(last);
if(pos == top_pos)
throw "bad negative equality chain";
int idx = pos_arg(pos);
if(idx != 0)
throw "bad negative equality chain";
pos = arg(pos,1);
if(pos == top_pos){
ast lhs = rewrite_lhs(last);
ast rhs = rewrite_rhs(last);
if(op(lhs) != Equal || op(rhs) != Equal)
throw "bad negative equality chain";
last = make_rewrite(rewrite_side(last),rewrite_pos(last),rewrite_cond(last),
make(Iff,make(Equal,arg(lhs,1),arg(lhs,0)),make(Equal,arg(rhs,1),arg(rhs,0))));
}
else {
idx = pos_arg(pos);
if(idx == 0)
idx = 1;
else if(idx == 1)
idx = 0;
else
throw "bad negative equality chain";
pos = pos_add(0,pos_add(idx,arg(pos,1)));
last = make_rewrite(rewrite_side(last),pos,rewrite_cond(last),rewrite_equ(last));
}
return chain_cons(commute_negation_chain(rest),last);
}
// split a rewrite chain into head and tail at last top-level rewrite
ast get_head_chain(const ast &chain, ast &tail, bool is_not = true){
ast last = chain_last(chain);
@ -1466,6 +1556,47 @@ class iz3proof_itp_impl : public iz3proof_itp {
return head;
}
// split a rewrite chain into head and tail at last non-mixed term
ast get_right_movers(const ast &chain, const ast &rhs, ast &tail, ast &mid){
if(is_true(chain) || get_term_type(rhs) != LitMixed){
mid = rhs;
tail = mk_true();
return chain;
}
ast last = chain_last(chain);
ast rest = chain_rest(chain);
ast mm = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last));
ast res = get_right_movers(rest,mm,tail,mid);
tail = chain_cons(tail,last);
return res;
}
// split a rewrite chain into head and tail at first non-mixed term
ast get_left_movers(const ast &chain, const ast &lhs, ast &tail, ast &mid){
if(is_true(chain)){
mid = lhs;
if(get_term_type(lhs) != LitMixed){
tail = mk_true();
return chain;
}
return ast();
}
ast last = chain_last(chain);
ast rest = chain_rest(chain);
ast res = get_left_movers(rest,lhs,tail,mid);
if(res.null()){
mid = subst_in_pos(mid,rewrite_pos(last),rewrite_rhs(last));
if(get_term_type(mid) != LitMixed){
tail = mk_true();
return chain;
}
return ast();
}
tail = chain_cons(tail,last);
return res;
}
struct cannot_split {};
/** Split a chain of rewrites two chains, operating on positions 0 and 1.
@ -1668,11 +1799,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){
LitType lhst = get_term_type(lhs);
LitType rhst = get_term_type(rhs);
if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs))
if(lhst == LitMixed && (rhst != LitMixed || ast_id(lhs) < ast_id(rhs)))
return make_normal_step(lhs,rhs,proof);
else
if(rhst == LitMixed && (lhst != LitMixed || ast_id(rhs) < ast_id(lhs)))
return make_normal_step(rhs,lhs,reverse_chain(proof));
throw "help!";
}
ast chain_side_proves(LitType side, const ast &chain){
@ -1692,8 +1825,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast lhs2 = normal_lhs(f2);
int id1 = ast_id(lhs1);
int id2 = ast_id(lhs2);
if(id1 < id2) return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves));
if(id2 < id1) return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves));
if(id1 < id2)
return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves));
if(id2 < id1)
return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves));
ast rhs1 = normal_rhs(f1);
ast rhs2 = normal_rhs(f2);
LitType t1 = get_term_type(rhs1);
@ -1719,9 +1854,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
Aproves = my_and(Aproves,mcB);
ast rep = apply_rewrite_chain(rhs1,Aproof);
new_proof = concat_rewrite_chain(pf1,Aproof);
new_normal = make_normal_step(rhs1,rep,new_proof);
new_normal = make_normal_step(lhs1,rep,new_proof);
ast A_normal = make_normal_step(rhs1,rep,Aproof);
ast res = cons_normal(new_normal,merge_normal_chains_rec(normal_rest(chain1),normal_rest(chain2),trans,Aproves,Bproves));
res = merge_normal_chains_rec(res,cons_normal(A_normal,make(True)),trans,Aproves,Bproves);
return res;
}
else if(t1 == LitA && t2 == LitB)
else if(t1 == LitB && t2 == LitA)
return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves);
else if(t1 == LitA) {
ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2);
@ -1743,17 +1882,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
return chain;
ast f = normal_first(chain);
ast r = normal_rest(chain);
r = trans_normal_chain(r,trans);
ast rhs = normal_rhs(f);
hash_map<ast,ast>::iterator it = trans.find(rhs);
ast new_normal;
if(it != trans.end()){
if(it != trans.end() && get_term_type(normal_lhs(f)) == LitMixed){
const ast &f2 = it->second;
ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2));
new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf);
}
else
new_normal = f;
return cons_normal(new_normal,trans_normal_chain(r,trans));
if(get_term_type(normal_lhs(f)) == LitMixed)
trans[normal_lhs(f)] = new_normal;
return cons_normal(new_normal,r);
}
ast merge_normal_chains(const ast &chain1, const ast &chain2, ast &Aproves, ast &Bproves){
@ -2011,8 +2153,14 @@ class iz3proof_itp_impl : public iz3proof_itp {
/** Make a Reflexivity node. This rule produces |- x = x */
virtual node make_reflexivity(ast con){
throw proof_error();
}
if(get_term_type(con) == LitA)
return mk_false();
if(get_term_type(con) == LitB)
return mk_true();
ast itp = make(And,make(contra,no_proof,mk_false()),
make(contra,mk_true(),mk_not(con)));
return itp;
}
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x. Ditto for ~(x=y) */
@ -2247,10 +2395,19 @@ class iz3proof_itp_impl : public iz3proof_itp {
throw proof_error();
}
}
Qrhs = make(Times,c,Qrhs);
#if 0
bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
if(pstrict && qstrict && round_off)
Qrhs = make(Sub,Qrhs,make_int(rational(1)));
#else
bool pstrict = op(P) == Lt;
if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
Qrhs = make(Sub,Qrhs,make_int(rational(1)));
qstrict = false;
}
Qrhs = make(Times,c,Qrhs);
bool strict = pstrict || qstrict;
#endif
if(strict)
P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
else
@ -2269,8 +2426,14 @@ 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";
if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed){
// std::cerr << "WARNING: mixed term in leq2eq\n";
std::vector<ast> lits;
lits.push_back(con);
lits.push_back(make(Not,xleqy));
lits.push_back(make(Not,yleqx));
return make_axiom(lits);
}
std::vector<ast> conjs; conjs.resize(3);
conjs[0] = mk_not(con);
conjs[1] = xleqy;
@ -2405,7 +2568,15 @@ class iz3proof_itp_impl : public iz3proof_itp {
frng = srng; // this term will be localized
}
else if(o == Plus || o == Times){ // don't want bound variables inside arith ops
frng = erng; // this term will be localized
// std::cout << "WARNING: non-local arithmetic\n";
// frng = erng; // this term will be localized
}
else if(o == Select){ // treat the array term like a function symbol
prover::range srng = pv->ast_scope(arg(e,0));
if(!(srng.lo > srng.hi) && 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;
@ -2434,7 +2605,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
return e; // this term occurs in range, so it's O.K.
if(is_array_type(get_type(e)))
throw "help!";
std::cerr << "WARNING: array quantifier\n";
// choose a frame for the constraint that is close to range
int frame = pv->range_near(pv->ast_scope(e),rng);

View file

@ -188,6 +188,15 @@ public:
get_Z3_lits(con, lits);
iproof->make_axiom(lits);
}
#ifdef LOCALIZATION_KLUDGE
else if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST
&& get_locality_rec(prem(proof,1)) == INT_MAX){
std::vector<ast> lits;
ast con = conc(proof);
get_Z3_lits(con, lits);
iproof->make_axiom(lits);
}
#endif
else {
unsigned nprems = num_prems(proof);
for(unsigned i = 0; i < nprems; i++){
@ -1271,6 +1280,84 @@ public:
return make(Plus,args);
}
ast replace_summands_with_fresh_vars(const ast &t, hash_map<ast,ast> &map){
if(op(t) == Plus){
int nargs = num_args(t);
std::vector<ast> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = replace_summands_with_fresh_vars(arg(t,i),map);
return make(Plus,args);
}
if(op(t) == Times)
return make(Times,arg(t,0),replace_summands_with_fresh_vars(arg(t,1),map));
if(map.find(t) == map.end())
map[t] = mk_fresh_constant("@s",get_type(t));
return map[t];
}
ast painfully_normalize_ineq(const ast &ineq, hash_map<ast,ast> &map){
ast res = normalize_inequality(ineq);
ast lhs = arg(res,0);
lhs = replace_summands_with_fresh_vars(lhs,map);
res = make(op(res),SortSum(lhs),arg(res,1));
return res;
}
Iproof::node painfully_reconstruct_farkas(const std::vector<ast> &prems, const std::vector<Iproof::node> &pfs, const ast &con){
int nprems = prems.size();
std::vector<ast> pcons(nprems),npcons(nprems);
hash_map<ast,ast> pcon_to_pf, npcon_to_pcon, pain_map;
for(int i = 0; i < nprems; i++){
pcons[i] = conc(prems[i]);
npcons[i] = painfully_normalize_ineq(pcons[i],pain_map);
pcon_to_pf[npcons[i]] = pfs[i];
npcon_to_pcon[npcons[i]] = pcons[i];
}
// ast leq = make(Leq,arg(con,0),arg(con,1));
ast ncon = painfully_normalize_ineq(mk_not(con),pain_map);
pcons.push_back(mk_not(con));
npcons.push_back(ncon);
// ast assumps = make(And,pcons);
ast new_proof;
if(is_sat(npcons,new_proof))
throw "Proof error!";
pfrule dk = pr(new_proof);
int nnp = num_prems(new_proof);
std::vector<Iproof::node> my_prems;
std::vector<ast> farkas_coeffs, my_pcons;
if(dk == PR_TH_LEMMA
&& get_theory_lemma_theory(new_proof) == ArithTheory
&& get_theory_lemma_kind(new_proof) == FarkasKind)
get_farkas_coeffs(new_proof,farkas_coeffs);
else if(dk == PR_UNIT_RESOLUTION && nnp == 2){
for(int i = 0; i < nprems; i++)
farkas_coeffs.push_back(make_int(rational(1)));
}
else
throw "cannot reconstruct farkas proof";
for(int i = 0; i < nnp; i++){
ast p = conc(prem(new_proof,i));
p = really_normalize_ineq(p);
if(pcon_to_pf.find(p) != pcon_to_pf.end()){
my_prems.push_back(pcon_to_pf[p]);
my_pcons.push_back(npcon_to_pcon[p]);
}
else if(p == ncon){
my_prems.push_back(iproof->make_hypothesis(mk_not(con)));
my_pcons.push_back(mk_not(con));
}
else
throw "cannot reconstruct farkas proof";
}
Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
return res;
}
ast really_normalize_ineq(const ast &ineq){
ast res = normalize_inequality(ineq);
res = make(op(res),SortSum(arg(res,0)),arg(res,1));
@ -1309,7 +1396,7 @@ public:
farkas_coeffs.push_back(make_int(rational(1)));
}
else
throw "cannot reconstruct farkas proof";
return painfully_reconstruct_farkas(prems,pfs,con);
for(int i = 0; i < nnp; i++){
ast p = conc(prem(new_proof,i));
@ -1452,9 +1539,11 @@ public:
lits.push_back(from_ast(con));
// pattern match some idioms
if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST && pr(prem(proof,1)) == PR_REWRITE ) {
res = iproof->make_axiom(lits);
return res;
if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST){
if(get_locality_rec(prem(proof,1)) == INT_MAX) {
res = iproof->make_axiom(lits);
return res;
}
}
if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or){
Iproof::node clause = translate_main(prem(proof,0),true);
@ -1465,12 +1554,20 @@ public:
if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or)
std::cout << "foo!\n";
#if 0
if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
Iproof::node clause = translate_main(prem(proof,0),true);
res = make(commute,clause,conc(prem(proof,0))); // HACK -- we depend on Iproof::node being same as ast.
return res;
}
if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,0)) == PR_COMMUTATIVITY){
Iproof::node clause = translate_main(prem(proof,1),true);
res = make(commute,clause,conc(prem(proof,1))); // HACK -- we depend on Iproof::node being same as ast.
return res;
}
#endif
if(dk == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){
try {
res = CombineEqPropagate(proof);
@ -1627,9 +1724,10 @@ public:
break;
case ArrayTheory: {// nothing fancy for this
ast store_array;
if(!get_store_array(con,store_array))
throw unsupported();
res = iproof->make_axiom(lits,ast_scope(store_array));
if(get_store_array(con,store_array))
res = iproof->make_axiom(lits,ast_scope(store_array));
else
res = iproof->make_axiom(lits); // for array extensionality axiom
break;
}
default:
@ -1653,6 +1751,12 @@ public:
res = args[0];
break;
}
case PR_COMMUTATIVITY: {
ast comm_equiv = make(op(con),arg(con,0),arg(con,0));
ast pf = iproof->make_reflexivity(comm_equiv);
res = make(commute,pf,comm_equiv);
break;
}
default:
assert(0 && "translate_main: unsupported proof rule");
throw unsupported();

0
src/muz/duality/duality_dl_interface.cpp Normal file → Executable file
View file