mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

still working on interpolation of full z3 proofs

Browse source
This commit is contained in:
Ken McMillan 2013-09-15 13:33:20 -07:00
parent 07bb534d65
commit 2c9c5ba1f0
8 changed files with 547 additions and 135 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
scripts/mk_util.py
View file

@ -1496,6 +1496,7 @@ def mk_config():
if test_foci2(CXX,FOCI2LIB):
LDFLAGS = '%s %s' % (LDFLAGS,FOCI2LIB)
SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB)
CPPFLAGS = '%s -D_FOCI2' % CPPFLAGS
else:
print "FAILED\n"
FOCI2 = False

4
src/interp/iz3foci.cpp
View file

@ -308,7 +308,11 @@ public:
int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){
assert((int)cnsts.size() == frames);
std::string lia("lia");
#ifdef _FOCI2
foci = foci2::create(lia);
#else
foci = 0;
#endif
if(!foci){
std::cerr << "iZ3: cannot find foci lia solver.\n";
assert(0);

9
src/interp/iz3mgr.cpp
View file

@ -494,6 +494,12 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
}
rats[i-2] = r;
}
if(rats.size() != 0 && rats[0].is_neg()){
for(unsigned i = 0; i < rats.size(); i++){
assert(rats[i].is_neg());
rats[i] = -rats[i];
}
}
extract_lcd(rats);
}
@ -519,11 +525,10 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& r
{
ast con = arg(conc(proof),i-1);
ast temp = make_real(r); // for debugging
#if 0
opr o = is_not(con) ? op(arg(con,0)) : op(con);
if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt))
#endif
r = -r;
r = -r;
}
rats[i-1] = r;
}

29
src/interp/iz3mgr.h
View file

@ -460,6 +460,17 @@ class iz3mgr {
return make(Or,x,y);
}
ast mk_implies(ast x, ast y){
opr ox = op(x);
opr oy = op(y);
if(ox == True) return y;
if(oy == False) return mk_not(x);
if(ox == False) return mk_true();
if(oy == True) return y;
if(x == y) return mk_true();
return make(Implies,x,y);
}
ast mk_or(const std::vector<ast> &x){
ast res = mk_false();
for(unsigned i = 0; i < x.size(); i++)
@ -468,10 +479,20 @@ class iz3mgr {
}
ast mk_and(const std::vector<ast> &x){
ast res = mk_true();
for(unsigned i = 0; i < x.size(); i++)
res = mk_and(res,x[i]);
return res;
std::vector<ast> conjs;
for(unsigned i = 0; i < x.size(); i++){
const ast &e = x[i];
opr o = op(e);
if(o == False)
return mk_false();
if(o != True)
conjs.push_back(e);
}
if(conjs.size() == 0)
return mk_true();
if(conjs.size() == 1)
return conjs[0];
return make(And,conjs);
}
ast mk_equal(ast x, ast y){

610
src/interp/iz3proof_itp.cpp
View file

@ -33,7 +33,60 @@ class iz3proof_itp_impl : public iz3proof_itp {
enum LitType {LitA,LitB,LitMixed};
hash_map<ast,ast> placeholders;
symb farkas;
// These symbols represent deduction rules
/* This symbol represents a proof by contradiction. That is,
contra(p,l1 /\ ... /\ lk) takes a proof p of
l1,...,lk |- false
and returns a proof of
|- ~l1,...,~l2
*/
symb contra;
/* The summation rule. The term sum(p,c,i) takes a proof p of an
inequality i', an integer coefficient c and an inequality i, and
yieds a proof of i' + ci. */
symb sum;
/* Proof rotation. The proof term rotate(q,p) takes a
proof p of:
Gamma, q |- false
and yields a proof of:
Gamma |- ~q
*/
symb rotate_sum;
/* Inequalities to equality. leq2eq(p, q, r) takes a proof
p of ~x=y, a proof q of x <= y and a proof r of y <= x
and yields a proof of false. */
symb leq2eq;
/* Proof term cong(p,q) takes a proof p of x=y and a proof
q of t != t<y/x> and returns a proof of false. */
symb cong;
/* Excluded middle. exmid(phi,p,q) takes a proof p of phi and a
proof q of ~\phi and returns a proof of false. */
symb exmid;
/* Symmetry. symm(p) takes a proof p of x=y and produces
a proof of y=x. */
symb symm;
/* Modus ponens. modpon(p,e,q) takes proofs p of P, e of P=Q
and q of ~Q and returns a proof of false. */
symb modpon;
// This is used to represent an infinitessimal value
ast epsilon;
ast get_placeholder(ast t){
hash_map<ast,ast>::iterator it = placeholders.find(t);
@ -49,8 +102,17 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
}
ast make_farkas(ast &coeff, ast &ineq){
return make(farkas,coeff,ineq);
ast make_contra_node(const ast &pf, const std::vector<ast> &lits){
if(lits.size() == 0)
return pf;
std::vector<ast> reslits;
reslits.push_back(make(contra,pf,mk_false()));
for(unsigned i = 0; i < lits.size(); i++){
ast bar = make(rotate_sum,lits[i],pf);
ast foo = make(contra,bar,lits[i]);
reslits.push_back(foo);
}
return make(And,reslits);
}
LitType get_term_type(const ast &lit){
@ -81,24 +143,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
/* the mixed case is a bit complicated */
ast atom = get_lit_atom(pivot);
switch(op(atom)){
case Equal:
return resolve_equality(pivot,conc,premise1,premise2);
case Leq:
case Geq:
case Lt:
case Gt:
return resolve_arith(pivot,conc,premise1,premise2);
break;
default:;
}
/* we can resolve on mixed equality and inequality literals,
but nothing else. */
throw proof_error();
return resolve_arith(pivot,conc,premise1,premise2);
}
#if 0
/* Handles the case of resolution on a mixed equality atom. */
ast resolve_equality(const ast &pivot, const std::vector<ast> &conc, node premise1, node premise2){
@ -134,7 +182,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
else {
switch(op(premise1)){
case Or:
case And: {
case And:
case Implies: {
unsigned nargs = num_args(premise1);
std::vector<ast> args; args.resize(nargs);
for(unsigned i = 0; i < nargs; i++)
@ -149,6 +198,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
return res;
}
#endif
/* Handles the case of resolution on a mixed arith atom. */
@ -161,15 +211,21 @@ class iz3proof_itp_impl : public iz3proof_itp {
return resolve_arith_rec1(memo, neg_pivot_lit, premise1, premise2);
}
void collect_farkas_resolvents(const ast &pivot, const ast &coeff, const ast &conj, std::vector<ast> &res){
int nargs = num_args(conj);
for(int i = 1; i < nargs; i++){
ast f = arg(conj,i);
if(!(f == pivot)){
ast newf = make(farkas,make(Times,arg(f,0),coeff),arg(f,1));
res.push_back(newf);
}
ast apply_coeff(const ast &coeff, const ast &t){
#if 0
rational r;
if(!is_integer(coeff,r))
throw "ack!";
ast n = make_int(r.numerator());
ast res = make(Times,n,t);
if(!r.is_int()) {
ast d = make_int(r.numerator());
res = mk_idiv(res,d);
}
return res;
#endif
return make(Times,coeff,t);
}
ast sum_ineq(const ast &coeff1, const ast &ineq1, const ast &coeff2, const ast &ineq2){
@ -178,29 +234,63 @@ class iz3proof_itp_impl : public iz3proof_itp {
sum_op = Lt;
ast sum_sides[2];
for(int i = 0; i < 2; i++){
sum_sides[i] = make(Plus,make(Times,coeff1,arg(ineq1,i)),make(Times,coeff2,arg(ineq2,i)));
sum_sides[i] = make(Plus,apply_coeff(coeff1,arg(ineq1,i)),apply_coeff(coeff2,arg(ineq2,i)));
sum_sides[i] = z3_simplify(sum_sides[i]);
}
return make(sum_op,sum_sides[0],sum_sides[1]);
}
ast resolve_farkas(const ast &pivot1, const ast &conj1, const ast &pivot2, const ast &conj2){
#if 0
ast resolve_farkas(const ast &pivot1, const ast &conj1, const ast &implicant1,
const ast &pivot2, const ast &conj2, const ast &implicant2){
std::vector<ast> resolvent;
ast coeff1 = get_farkas_coeff(pivot1);
ast coeff2 = get_farkas_coeff(pivot2);
resolvent.push_back(sum_ineq(coeff2,arg(conj1,0),coeff1,arg(conj2,0)));
ast s1 = resolve_arith_placeholders(pivot2,conj2,arg(conj1,0));
ast s2 = resolve_arith_placeholders(pivot1,conj1,arg(conj2,0));
resolvent.push_back(sum_ineq(coeff2,s1,coeff1,s2));
collect_farkas_resolvents(pivot1,coeff2,conj1,resolvent);
collect_farkas_resolvents(pivot2,coeff1,conj2,resolvent);
ast res = make(And,resolvent);
if(implicant1.null() && implicant2.null())
return res;
ast i1 = implicant1.null() ? mk_false() : resolve_arith_placeholders(pivot2,conj2,implicant1);
ast i2 = implicant2.null() ? mk_false() : resolve_arith_placeholders(pivot1,conj1,implicant2);
return make(Implies,res,my_or(i1,i2));
}
#endif
void collect_contra_resolvents(int from, const ast &pivot1, const ast &pivot, const ast &conj, std::vector<ast> &res){
int nargs = num_args(conj);
for(int i = from; i < nargs; i++){
ast f = arg(conj,i);
if(!(f == pivot)){
ast ph = get_placeholder(mk_not(arg(pivot1,1)));
ast pf = arg(pivot1,0);
ast thing = subst_term_and_simp(ph,pf,arg(f,0));
ast newf = make(contra,thing,arg(f,1));
res.push_back(newf);
}
}
}
ast resolve_contra(const ast &pivot1, const ast &conj1,
const ast &pivot2, const ast &conj2){
std::vector<ast> resolvent;
collect_contra_resolvents(0,pivot1,pivot2,conj2,resolvent);
collect_contra_resolvents(1,pivot2,pivot1,conj1,resolvent);
if(resolvent.size() == 1) // we have proved a contradiction
return simplify(arg(resolvent[0],0)); // this is the proof -- get interpolant
return make(And,resolvent);
}
bool is_farkas_itp(const ast &pivot1, const ast &itp2, ast &pivot2){
bool is_contra_itp(const ast &pivot1, ast itp2, ast &pivot2){
if(op(itp2) == And){
int nargs = num_args(itp2);
for(int i = 1; i < nargs; i++){
ast foo = arg(itp2,i);
if(op(foo) == Uninterpreted && sym(foo) == farkas){
if(op(foo) == Uninterpreted && sym(foo) == contra){
if(arg(foo,1) == pivot1){
pivot2 = foo;
return true;
@ -218,12 +308,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
ast pivot2;
if(is_farkas_itp(mk_not(arg(pivot1,1)),itp2,pivot2))
res = resolve_farkas(pivot1,conj1,pivot2,itp2);
if(is_contra_itp(mk_not(arg(pivot1,1)),itp2,pivot2))
res = resolve_contra(pivot1,conj1,pivot2,itp2);
else {
switch(op(itp2)){
case Or:
case And: {
case And:
case Implies: {
unsigned nargs = num_args(itp2);
std::vector<ast> args; args.resize(nargs);
for(unsigned i = 0; i < nargs; i++)
@ -244,15 +335,15 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(!res.null())
return res;
ast pivot1;
if(is_farkas_itp(neg_pivot_lit,itp1,pivot1)){
if(is_contra_itp(neg_pivot_lit,itp1,pivot1)){
hash_map<ast,ast> memo2;
res = resolve_arith_rec2(memo2,pivot1,itp1,itp2);
res = resolve_arith_placeholders(pivot1,itp1,res);
}
else {
switch(op(itp1)){
case Or:
case And: {
case And:
case Implies: {
unsigned nargs = num_args(itp1);
std::vector<ast> args; args.resize(nargs);
for(unsigned i = 0; i < nargs; i++)
@ -268,21 +359,26 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
}
#if 0
ast resolve_arith_placeholders(const ast &pivot1, const ast &conj1, const ast &itp2){
ast coeff = arg(pivot1,0);
ast val = arg(arg(conj1,0),1);
if(op(conj1)==Lt)
val = make(Sub,val,epsilon); // represent x < c by x <= c - epsilon
coeff = z3_simplify(coeff);
ast soln = mk_idiv(arg(arg(conj1,0),1),coeff);
ast soln = mk_idiv(val,coeff);
int nargs = num_args(conj1);
for(int i = 1; i < nargs; i++){
ast c = arg(conj1,i);
if(!(c == pivot1)){
soln = make(Plus,soln,get_placeholder(mk_not(c)));
soln = make(Plus,soln,get_placeholder(arg(c,1)));
}
}
ast pl = get_placeholder(mk_not(arg(pivot1,1)));
ast res = subst_term_and_simp(pl,soln,itp2);
return res;
}
#endif
hash_map<ast,ast> subst_memo; // memo of subst function
@ -311,6 +407,197 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
}
/* This is where the real work happens. Here, we simplify the
proof obtained by cut elimination, obtaining a interpolant. */
struct cannot_simplify {};
hash_map<ast,ast> simplify_memo;
ast simplify(const ast &t){
return simplify_rec(t);
}
ast simplify_rec(const ast &e){
std::pair<ast,ast> foo(e,ast());
std::pair<hash_map<ast,ast>::iterator,bool> bar = simplify_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] = simplify_rec(arg(e,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 == Idiv) res = mk_idiv(args[0],args[1]);
else if(f == Uninterpreted){
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);
#if 0
else if(g == cong) res = simplify_cong(args);
else if(g == modpon) res = simplify_modpon(args);
else if(g == leq2eq) res = simplify_leq2eq(args);
else if(g == eq2leq) res = simplify_eq2leq(args);
#endif
else res = clone(e,args);
}
else res = clone(e,args);
}
catch (const cannot_simplify &){
res = clone(e,args);
}
}
return res;
}
ast simplify_rotate(const std::vector<ast> &args){
const ast &pf = args[1];
ast pl = get_placeholder(args[0]);
if(op(pf) == Uninterpreted){
symb g = sym(pf);
if(g == sum) return simplify_rotate_sum(pl,pf);
if(g == leq2eq) return simplify_rotate_leq2eq(pl,args[0],pf);
if(g == cong) return simplify_rotate_cong(pl,args[0],pf);
// if(g == symm) return simplify_rotate_symm(pl,args[0],pf);
}
throw cannot_simplify();
}
ast simplify_rotate_sum(const ast &pl, const ast &pf){
ast cond = mk_true();
ast ineq = make(Leq,make_int("0"),make_int("0"));
rotate_sum_rec(pl,pf,cond,ineq);
return ineq;
}
void sum_cond_ineq(ast &ineq, ast &cond, const ast &coeff2, const ast &ineq2){
opr o = op(ineq2);
if(o == Implies){
sum_cond_ineq(ineq,cond,coeff2,arg(ineq2,1));
cond = my_and(cond,arg(ineq2,0));
}
else if(o == Leq || o == Lt)
ineq = sum_ineq(make_int("1"),ineq,coeff2,ineq2);
else
throw cannot_simplify();
}
// divide both sides of inequality by a non-negative integer divisor
ast idiv_ineq(const ast &ineq, const ast &divisor){
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 &cond, ast &ineq){
if(op(pf) == Uninterpreted && sym(pf) == sum){
if(arg(pf,2) == pl){
sum_cond_ineq(ineq,cond,make_int("1"),arg(pf,0));
ineq = idiv_ineq(ineq,arg(pf,1));
return my_implies(cond,ineq);
}
sum_cond_ineq(ineq,cond,arg(pf,1),arg(pf,2));
return rotate_sum_rec(pl,arg(pf,0),cond,ineq);
}
throw cannot_simplify();
}
ast simplify_rotate_leq2eq(const ast &pl, const ast &neg_equality, const ast &pf){
if(pl == arg(pf,0)){
ast equality = arg(neg_equality,0);
ast x = arg(equality,0);
ast y = arg(equality,1);
ast xleqy = arg(pf,1);
ast yleqx = arg(pf,2);
ast itpeq;
if(get_term_type(x) == LitA)
itpeq = make(Equal,x,make(Plus,x,get_ineq_rhs(xleqy)));
else if(get_term_type(y) == LitA)
itpeq = make(Equal,make(Plus,y,get_ineq_rhs(yleqx)),y);
else
throw cannot_simplify();
ast cond = mk_true();
ast ineq = make(Leq,make_int("0"),make_int("0"));
sum_cond_ineq(ineq,cond,make_int("-1"),xleqy);
sum_cond_ineq(ineq,cond,make_int("-1"),yleqx);
cond = my_and(cond,ineq);
return my_implies(cond,itpeq);
}
throw cannot_simplify();
}
ast get_ineq_rhs(const ast &ineq2){
opr o = op(ineq2);
if(o == Implies)
return get_ineq_rhs(arg(ineq2,1));
else if(o == Leq || o == Lt)
return arg(ineq2,1);
throw cannot_simplify();
}
ast simplify_rotate_cong(const ast &pl, const ast &neg_equality, const ast &pf){
if(pl == arg(pf,2)){
if(op(arg(pf,0)) == True)
return mk_true();
rational pos;
if(is_numeral(arg(pf,1),pos)){
int ipos = pos.get_unsigned();
ast cond = mk_true();
ast equa = sep_cond(arg(pf,0),cond);
if(op(equa) == Equal){
ast pe = mk_not(neg_equality);
ast lhs = subst_in_arg_pos(ipos,arg(equa,0),arg(pe,0));
ast rhs = subst_in_arg_pos(ipos,arg(equa,1),arg(pe,1));
ast res = make(Equal,lhs,rhs);
return my_implies(cond,res);
}
}
}
throw cannot_simplify();
}
ast simplify_symm(const std::vector<ast> &args){
if(op(args[0]) == True)
return mk_true();
ast cond = mk_true();
ast equa = sep_cond(args[0],cond);
if(op(equa) == Equal)
return my_implies(cond,make(Equal,arg(equa,1),arg(equa,0)));
throw cannot_simplify();
}
ast simplify_modpon(const std::vector<ast> &args){
if(op(args[1]) == True){
ast cond = mk_true();
ast P = sep_cond(args[0],cond);
ast notQ = sep_cond(args[2],cond);
ast Q = mk_not(notQ);
ast d = mk_not(delta(P,Q));
return my_implies(cond,d);
}
throw cannot_simplify();
}
ast delta(const ast &x, const ast &y){
if(op(x) != op(y) || (op(x) == Uninterpreted && sym(x) != sym(y)) || num_args(x) != num_args(y))
return make(Equal,x,y);
ast res = mk_true();
int nargs = num_args(x);
for(int i = 0; i < nargs; i++)
res = my_and(res,delta(arg(x,i),arg(y,i)));
return res;
}
ast sep_cond(const ast &t, ast &cond){
if(op(t) == Implies){
cond = my_and(cond,arg(t,0));
return arg(t,1);
}
return t;
}
/** Make an assumption node. The given clause is assumed in the given frame. */
virtual node make_assumption(int frame, const std::vector<ast> &assumption){
@ -327,39 +614,76 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
}
/** Make a modus-ponens node. This takes derivations of |- x
and |- x = y and produces |- y */
virtual node make_mp(const ast &p, const ast &q, const ast &prem1, const ast &prem2){
/* Interpolate the axiom p, p=q -> q */
ast itp;
if(get_term_type(p) == LitA){
if(get_term_type(q) == LitA)
itp = mk_false();
else {
if(get_term_type(make(Equal,p,q)) == LitA)
itp = q;
else
itp = get_placeholder(make(Equal,p,q));
ast triv_interp(const symb &rule, const std::vector<ast> &premises){
std::vector<ast> ps; ps.resize(premises.size());
std::vector<ast> conjs;
for(unsigned i = 0; i < ps.size(); i++){
ast p = premises[i];
switch(get_term_type(p)){
case LitA:
ps[i] = p;
break;
case LitB:
ps[i] = mk_true();
break;
default:
ps[i] = get_placeholder(p);
conjs.push_back(p);
}
}
ast ref = make(rule,ps);
ast res = make_contra_node(ref,conjs);
return res;
}
ast triv_interp(const symb &rule, const ast &p0, const ast &p1, const ast &p2){
std::vector<ast> ps; ps.resize(3);
ps[0] = p0;
ps[1] = p1;
ps[2] = p2;
return triv_interp(rule,ps);
}
/** Make a modus-ponens node. This takes derivations of |- x
and |- x = y and produces |- y */
virtual node make_mp(const ast &p_eq_q, const ast &prem1, const ast &prem2){
/* Interpolate the axiom p, p=q -> q */
ast p = arg(p_eq_q,0);
ast q = arg(p_eq_q,1);
ast itp;
if(get_term_type(p_eq_q) == LitMixed){
itp = triv_interp(modpon,p,p_eq_q,mk_not(q));
}
else {
if(get_term_type(q) == LitA){
if(get_term_type(make(Equal,p,q)) == LitA)
itp = mk_not(p);
else
itp = mk_not(get_placeholder(make(Equal,p,q)));
if(get_term_type(p) == LitA){
if(get_term_type(q) == LitA)
itp = mk_false();
else {
if(get_term_type(p_eq_q) == LitA)
itp = q;
else
throw proof_error();
}
}
else {
if(get_term_type(q) == LitA){
if(get_term_type(make(Equal,p,q)) == LitA)
itp = mk_not(p);
else
throw proof_error();
}
else
itp = mk_true();
}
}
/* Resolve it with the premises */
std::vector<ast> conc; conc.push_back(q); conc.push_back(mk_not(make(Equal,p,q)));
itp = make_resolution(p,conc,itp,prem1);
conc.pop_back();
itp = make_resolution(make(Equal,p,q),conc,itp,prem2);
itp = make_resolution(p_eq_q,conc,itp,prem2);
return itp;
}
@ -387,26 +711,25 @@ class iz3proof_itp_impl : public iz3proof_itp {
return mk_true();
default: // mixed hypothesis
switch(op(P)){
case Equal:
{
ast x = arg(P,0);
ast y = arg(P,1);
ast A_term = (get_term_type(y) == LitA) ? y : x;
ast res = make(And,make(Equal,A_term,get_placeholder(P)),mk_not(P));
return res;
}
case Geq:
case Leq:
case Gt:
case Lt: {
ast zleqz = make(Leq,make_int("0"),make_int("0"));
ast fark1 = make(farkas,make_int("1"),P);
ast fark2 = make(farkas,make_int("1"),mk_not(P));
ast res = make(And,zleqz,fark1,fark2);
ast fark1 = make(sum,zleqz,make_int("1"),get_placeholder(P));
ast fark2 = make(sum,fark1,make_int("1"),get_placeholder(mk_not(P)));
ast res = make(And,make(contra,fark2,mk_false()),
make(contra,get_placeholder(mk_not(P)),P),
make(contra,get_placeholder(P),mk_not(P)));
return res;
}
default: {
ast em = make(exmid,P,get_placeholder(P),get_placeholder(mk_not(P)));
ast res = make(And,make(contra,em,mk_false()),
make(contra,get_placeholder(mk_not(P)),P),
make(contra,get_placeholder(P),mk_not(P)));
return res;
}
default:
throw proof_error();
}
}
}
@ -420,20 +743,31 @@ class iz3proof_itp_impl : public iz3proof_itp {
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x */
virtual node make_symmetry(ast con, node prem){
virtual node make_symmetry(ast con, const ast &premcon, node prem){
ast x = arg(con,0);
ast y = arg(con,1);
ast p = make(Equal,y,x);
ast p = make(op(con),y,x);
if(p == premcon)
std::cout << "ok\n";
if(get_term_type(con) != LitMixed)
return prem; // symmetry shmymmetry...
#if 0
LitType xt = get_term_type(x);
LitType yt = get_term_type(y);
ast A_term;
if(xt == LitA && yt == LitB)
A_term = x;
else if(yt == LitA && xt == LitB)
A_term = y;
else
return prem; // symmetry shmymmetry...
ast itp = make(And,make(Equal,A_term,get_placeholder(p)),mk_not(con));
#endif
ast em = make(exmid,con,make(symm,get_placeholder(p)),get_placeholder(mk_not(con)));
ast itp = make(And,make(contra,em,mk_false()),
make(contra,make(symm,get_placeholder(mk_not(con))),p),
make(contra,make(symm,get_placeholder(p)),mk_not(con)));
std::vector<ast> conc; conc.push_back(con);
itp = make_resolution(p,conc,itp,prem);
return itp;
@ -448,7 +782,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast p = make(Equal,x,y);
ast q = make(Equal,y,z);
ast r = make(Equal,x,z);
ast equiv = make(Iff,p,r);
ast itp;
itp = make_congruence(q,equiv,prem2);
itp = make_mp(equiv,prem1,itp);
#if 0
if(get_term_type(p) == LitA){
if(get_term_type(q) == LitA){
if(get_term_type(r) == LitA)
@ -506,21 +846,24 @@ class iz3proof_itp_impl : public iz3proof_itp {
itp = make_resolution(p,conc,itp,prem1);
conc.pop_back();
itp = make_resolution(q,conc,itp,prem2);
#endif
return itp;
}
/** Make a congruence node. This takes derivations of |- x_i = y_i
and produces |- f(x_1,...,x_n) = f(y_1,...,y_n) */
virtual node make_congruence(const ast &x, const ast &y, const ast &con, const std::vector<ast> &hyps, const ast &prem1){
ast p = make(Equal,x,y);
virtual node make_congruence(const ast &p, const ast &con, const ast &prem1){
ast x = arg(p,0), y = arg(p,1);
ast itp;
if(get_term_type(p) == LitA){
if(get_term_type(con) == LitA)
itp = mk_false();
else
throw proof_error(); // itp = p;
itp = make_mixed_congruence(x, y, p, con, prem1);
}
else {
if(get_term_type(con) == LitA)
@ -529,7 +872,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(get_term_type(con) == LitB)
itp = mk_true();
else
itp = make_mixed_congruence(x, y, con, hyps, prem1);
itp = make_mixed_congruence(x, y, p, con, prem1);
}
}
std::vector<ast> conc; conc.push_back(con);
@ -539,14 +882,19 @@ class iz3proof_itp_impl : public iz3proof_itp {
/* Interpolate a mixed congruence axiom. */
virtual ast make_mixed_congruence(const ast &x, const ast &y, const ast &con, const std::vector<ast> &hyps, const ast &prem1){
ast A_term = x;
ast f_A_term = arg(con,0);
if(get_term_type(y) == LitA){
A_term = y;
f_A_term = arg(con,1);
virtual ast make_mixed_congruence(const ast &x, const ast &y, const ast &p, const ast &con, const ast &prem1){
ast foo = p;
std::vector<ast> conjs;
switch(get_term_type(foo)){
case LitA:
break;
case LitB:
foo = mk_true();
break;
case LitMixed:
conjs.push_back(foo);
foo = get_placeholder(foo);
}
// find the argument position of x and y
int pos = -1;
int nargs = num_args(arg(con,0));
@ -555,10 +903,22 @@ class iz3proof_itp_impl : public iz3proof_itp {
pos = i;
if(pos == -1)
throw proof_error();
ast bar = make(cong,foo,make_int(rational(pos)),get_placeholder(mk_not(con)));
conjs.push_back(mk_not(con));
return make_contra_node(bar,conjs);
#if 0
ast A_term = x;
ast f_A_term = arg(con,0);
if(get_term_type(y) == LitA){
A_term = y;
f_A_term = arg(con,1);
}
ast res = make(Equal,f_A_term,subst_in_arg_pos(pos,get_placeholder(make(Equal,x,y)),f_A_term));
res = make(And,res,mk_not(con));
return res;
#endif
}
ast subst_in_arg_pos(int pos, ast term, ast app){
@ -576,20 +936,22 @@ class iz3proof_itp_impl : public iz3proof_itp {
/* Compute the interpolant for the clause */
ast zero = make_int("0");
std::vector<ast> conjs; conjs.resize(1);
std::vector<ast> conjs;
ast thing = make(Leq,zero,zero);
for(unsigned i = 0; i < prem_cons.size(); i++){
const ast &lit = prem_cons[i];
if(get_term_type(lit) == LitA)
linear_comb(thing,coeffs[i],lit);
else if(get_term_type(lit) != LitB)
conjs.push_back(make(farkas,coeffs[i],prem_cons[i]));
}
thing = simplify_ineq(thing);
if(conjs.size() > 1){
conjs[0] = thing;
thing = make(And,conjs);
for(unsigned i = 0; i < prem_cons.size(); i++){
const ast &lit = prem_cons[i];
if(get_term_type(lit) == LitMixed){
thing = make(sum,thing,coeffs[i],get_placeholder(lit));
conjs.push_back(lit);
}
}
thing = make_contra_node(thing,conjs);
/* Resolve it with the premises */
std::vector<ast> conc; conc.resize(prem_cons.size());
@ -667,24 +1029,15 @@ class iz3proof_itp_impl : public iz3proof_itp {
itp = mk_true();
break;
default: { // mixed equality
ast mid,ante;
if(get_term_type(y) == LitA){
std::swap(x,y);
mid = make(Plus,x,get_placeholder(yleqx));
}
else {
mid = make(Plus,x,get_placeholder(xleqy));
}
ante = make(Uminus,make(Plus,get_placeholder(xleqy),get_placeholder(yleqx)));
ante = mk_not(make(Leq,make_int("0"),ante));
#if 0
ast zleqz = make(Leq,make_int("0"),make_int("0"));
ast fark1 = make(farkas,make_int("1"),xleqy);
ast fark2 = make(farkas,make_int("1"),yleqx);
ast ante = make(And,zleqz,fark1,fark2);
#endif
ast conc = make(And,make(Equal,x,mid),mk_not(con));
itp = my_or(ante,conc);
std::vector<ast> conjs; conjs.resize(3);
conjs[0] = mk_not(con);
conjs[1] = xleqy;
conjs[2] = yleqx;
itp = make_contra_node(make(leq2eq,
get_placeholder(mk_not(con)),
get_placeholder(xleqy),
get_placeholder(yleqx)),
conjs);
}
}
return itp;
@ -710,7 +1063,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
mid = make(Sub,mid,x);
}
ast zleqmid = make(Leq,make_int("0"),mid);
ast fark = make(farkas,make_int("1"),mk_not(xleqy));
ast fark = make(contra,make_int("1"),mk_not(xleqy));
itp = make(And,zleqmid,fark);
}
}
@ -732,7 +1085,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
default: {
ast t = arg(tleqc,0);
ast c = arg(tleqc,1);
ast thing = make(farkas,make_int("1"),mk_not(con));
ast thing = make(contra,make_int("1"),mk_not(con));
itp = make(And,make(Leq,make_int("0"),make(Idiv,get_placeholder(tleqc),d)),thing);
}
}
@ -741,7 +1094,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
return itp;
}
ast get_farkas_coeff(const ast &f){
ast get_contra_coeff(const ast &f){
ast c = arg(f,0);
// if(!is_not(arg(f,1)))
// c = make(Uminus,c);
@ -755,6 +1110,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast my_and(const ast &a, const ast &b){
return mk_and(a,b);
}
ast my_implies(const ast &a, const ast &b){
return mk_implies(a,b);
}
ast my_or(const std::vector<ast> &a){
return mk_or(a);
@ -777,8 +1136,19 @@ public:
pv = p;
rng = r;
weak = w;
type domain[2] = {int_type(),bool_type()};
farkas = function("@farkas",2,domain,bool_type());
type boolintbooldom[3] = {bool_type(),int_type(),bool_type()};
type booldom[1] = {bool_type()};
type boolbooldom[2] = {bool_type(),bool_type()};
type boolboolbooldom[3] = {bool_type(),bool_type(),bool_type()};
contra = function("@contra",2,boolbooldom,bool_type());
sum = function("@sum",3,boolintbooldom,bool_type());
rotate_sum = function("@rotsum",2,boolbooldom,bool_type());
leq2eq = function("@leq2eq",3,boolboolbooldom,bool_type());
cong = function("@cong",3,boolintbooldom,bool_type());
exmid = function("@exmid",3,boolboolbooldom,bool_type());
symm = function("@symm",1,booldom,bool_type());
epsilon = make_var("@eps",int_type());
modpon = function("@mp",3,boolboolbooldom,bool_type());
}
};

6
src/interp/iz3proof_itp.h
View file

@ -82,7 +82,7 @@ class iz3proof_itp : public iz3mgr {
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x */
virtual node make_symmetry(ast con, node prem) = 0;
virtual node make_symmetry(ast con, const ast &premcon, node prem) = 0;
/** Make a transitivity node. This takes derivations of |- x = y
and |- y = z produces | x = z */
@ -92,12 +92,12 @@ class iz3proof_itp : public iz3mgr {
/** Make a congruence node. This takes a derivation of |- x_i = y_i
and produces |- f(...x_i,...) = f(...,y_i,...) */
virtual node make_congruence(const ast &x, const ast &y, const ast &con, const std::vector<ast> &hyps, const ast &prem1) = 0;
virtual node make_congruence(const ast &xi_eq_yi, const ast &con, const ast &prem1) = 0;
/** Make a modus-ponens node. This takes derivations of |- x
and |- x = y and produces |- y */
virtual node make_mp(const ast &x, const ast &y, const ast &prem1, const ast &prem2) = 0;
virtual node make_mp(const ast &x_eq_y, const ast &prem1, const ast &prem2) = 0;
/** Make a farkas proof node. */

18
src/interp/iz3translate.cpp
View file

@ -888,15 +888,21 @@ public:
for(unsigned i = 0; i < farkas_coeffs.size(); i++)
my_coeffs.push_back(farkas_coeffs[i]);
#else
std::vector<ast> &my_coeffs = farkas_coeffs;
std::vector<ast> my_coeffs;
#endif
std::vector<ast> my_cons;
for(int i = 0; i < nargs; i++)
for(int i = 1; i < nargs; i++){
my_cons.push_back(mk_not(arg(con,i)));
my_coeffs.push_back(farkas_coeffs[i]);
}
ast farkas_con = normalize_inequality(sum_inequalities(farkas_coeffs,my_cons));
my_cons.push_back(mk_not(farkas_con));
my_coeffs.push_back(make_int("1"));
std::vector<Iproof::node> my_hyps;
for(int i = 0; i < nargs; i++)
my_hyps.push_back(iproof->make_hypothesis(my_cons[i]));
ast res = iproof->make_farkas(mk_false(),my_hyps,my_cons,my_coeffs);
res = iproof->make_cut_rule(farkas_con,farkas_coeffs[0],arg(con,0),res);
return res;
}
@ -973,10 +979,12 @@ public:
// assume the premise is x = y
ast x = arg(conc(prem(proof,0)),0);
ast y = arg(conc(prem(proof,0)),1);
#if 0
AstSet &hyps = get_hyps(proof);
std::vector<ast> hyps_vec; hyps_vec.resize(hyps.size());
std::copy(hyps.begin(),hyps.end(),hyps_vec.begin());
res = iproof->make_congruence(x,y,con,hyps_vec,args[0]);
#endif
res = iproof->make_congruence(conc(prem(proof,0)),con,args[0]);
break;
}
case PR_REFLEXIVITY: {
@ -984,11 +992,11 @@ public:
break;
}
case PR_SYMMETRY: {
res = iproof->make_symmetry(con,args[0]);
res = iproof->make_symmetry(con,conc(prem(proof,0)),args[0]);
break;
}
case PR_MODUS_PONENS: {
res = iproof->make_mp(conc(prem(proof,0)),arg(conc(prem(proof,1)),1),args[0],args[1]);
res = iproof->make_mp(conc(prem(proof,1)),args[0],args[1]);
break;
}
case PR_TH_LEMMA: {

5
src/interp/iz3translate.h
View file

@ -53,8 +53,11 @@ public:
};
//#define IZ3_TRANSLATE_DIRECT2
#ifndef _FOCI2
#define IZ3_TRANSLATE_DIRECT
// #define IZ3_TRANSLATE_FULL
#else
#define IZ3_TRANSLATE_FULL
#endif
#endif