diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 330799796..1c2927da8 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1636,7 +1636,8 @@ namespace Duality { dont_cares.insert(b); resolve_ite_memo.clear(); timer_start("UnderapproxFormula"); - Term eu = UnderapproxFormula(root->Outgoing->dual,dont_cares); + Term dual = root->Outgoing->dual.null() ? ctx.bool_val(true) : root->Outgoing->dual; + Term eu = UnderapproxFormula(dual,dont_cares); timer_stop("UnderapproxFormula"); /* combine with children */ chu.push_back(eu); @@ -1944,6 +1945,8 @@ namespace Duality { for(unsigned i = 0; i < clauses.size(); i++){ Term &clause = clauses[i]; + if(clause.is_app() && clause.decl().get_decl_kind() == Uninterpreted) + clause = implies(ctx.bool_val(true),clause); if(!canonical_clause(clause)) clause = implies((!clause).simplify(),ctx.bool_val(false)); Term head = clause.arg(1); diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 897c88c30..f716f04fe 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -916,7 +916,7 @@ namespace Duality { return true; } #ifdef UNDERAPPROX_NODES - if(0 && last_decisions > 5000){ + if(UseUnderapprox && last_decisions > 500){ std::cout << "making an underapprox\n"; ExpandNodeFromCoverFail(node); } @@ -1642,7 +1642,7 @@ namespace Duality { std::set old_choices; void ExpansionChoices(std::set &best, bool high_priority){ - if(!underapprox || constrained){ + if(!underapprox || constrained || high_priority){ ExpansionChoicesFull(best, high_priority); return; } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 1048734f7..21ed45479 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -515,39 +515,39 @@ namespace Duality { } friend expr operator+(expr const & a, expr const & b) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_ADD,a,b)); + return a.ctx().make(Plus,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_ADD,a,b)); } friend expr operator*(expr const & a, expr const & b) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_MUL,a,b)); + return a.ctx().make(Times,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_MUL,a,b)); } friend expr operator/(expr const & a, expr const & b) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_DIV,a,b)); + return a.ctx().make(Div,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_DIV,a,b)); } friend expr operator-(expr const & a) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_UMINUS,a)); + return a.ctx().make(Uminus,a); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_UMINUS,a)); } friend expr operator-(expr const & a, expr const & b) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_SUB,a,b)); + return a.ctx().make(Sub,a,b); // expr(a.ctx(),a.m().mk_app(a.ctx().m_arith_fid,OP_SUB,a,b)); } friend expr operator<=(expr const & a, expr const & b) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LE,a,b)); + return a.ctx().make(Leq,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LE,a,b)); } friend expr operator>=(expr const & a, expr const & b) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GE,a,b)); + return a.ctx().make(Geq,a,b); //expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GE,a,b)); } friend expr operator<(expr const & a, expr const & b) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LT,a,b)); + return a.ctx().make(Lt,a,b); expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LT,a,b)); } friend expr operator>(expr const & a, expr const & b) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GT,a,b)); + return a.ctx().make(Gt,a,b); expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GT,a,b)); } expr simplify() const; diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 807c38227..7a787fdea 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -26,6 +26,7 @@ Revision History: #include #include "expr_abstract.h" +#include "params.h" #ifndef WIN32 @@ -145,19 +146,19 @@ iz3mgr::ast iz3mgr::make(symb sym){ return make(sym,0,0); } -iz3mgr::ast iz3mgr::make(symb sym, ast &arg0){ +iz3mgr::ast iz3mgr::make(symb sym, const ast &arg0){ raw_ast *a = arg0.raw(); return make(sym,1,&a); } -iz3mgr::ast iz3mgr::make(symb sym, ast &arg0, ast &arg1){ +iz3mgr::ast iz3mgr::make(symb sym, const ast &arg0, const ast &arg1){ raw_ast *args[2]; args[0] = arg0.raw(); args[1] = arg1.raw(); return make(sym,2,args); } -iz3mgr::ast iz3mgr::make(symb sym, ast &arg0, ast &arg1, ast &arg2){ +iz3mgr::ast iz3mgr::make(symb sym, const ast &arg0, const ast &arg1, const ast &arg2){ raw_ast *args[3]; args[0] = arg0.raw(); args[1] = arg1.raw(); @@ -199,7 +200,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ // FIXME replace this with existing Z3 functionality -iz3mgr::ast iz3mgr::clone(ast &t, const std::vector &_args){ +iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector &_args){ if(_args.size() == 0) return t; @@ -242,6 +243,10 @@ void iz3mgr::show(ast t){ std::cout << mk_pp(t.raw(), m()) << std::endl; } +void iz3mgr::show_symb(symb s){ + std::cout << mk_pp(s, m()) << std::endl; +} + void iz3mgr::print_expr(std::ostream &s, const ast &e){ s << mk_pp(e.raw(), m()); } @@ -431,3 +436,198 @@ void iz3mgr::print_sat_problem(std::ostream &out, const ast &t){ pp.set_simplify_implies(false); pp.display_smt2(out, to_expr(t.raw())); } + +iz3mgr::ast iz3mgr::z3_simplify(const ast &e){ + ::expr * a = to_expr(e.raw()); + params_ref p; + th_rewriter m_rw(m(), p); + expr_ref result(m()); + m_rw(a, result); + return cook(result); +} + + +#if 0 +static rational lcm(const rational &x, const rational &y){ + int a = x.numerator(); + int b = y.numerator(); + return rational(a * b / gcd(a, b)); +} +#endif + +static rational extract_lcd(std::vector &res){ + if(res.size() == 0) return rational(1); // shouldn't happen + rational lcd = denominator(res[0]); + for(unsigned i = 1; i < res.size(); i++) + lcd = lcm(lcd,denominator(res[i])); + for(unsigned i = 0; i < res.size(); i++) + res[i] *= lcd; + return lcd; +} + +void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& coeffs){ + std::vector rats; + get_farkas_coeffs(proof,rats); + coeffs.resize(rats.size()); + for(unsigned i = 0; i < rats.size(); i++){ + sort *is = m().mk_sort(m_arith_fid, INT_SORT); + ast coeff = cook(m_arith_util.mk_numeral(rats[i],is)); + coeffs[i] = coeff; + } +} + +void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& rats){ + symb s = sym(proof); + int numps = s->get_num_parameters(); + rats.resize(numps-2); + for(int i = 2; i < numps; i++){ + rational r; + bool ok = s->get_parameter(i).is_rational(r); + if(!ok) + throw "Bad Farkas coefficient"; + { + ast con = conc(prem(proof,i-2)); + ast temp = make_real(r); // for debugging + opr o = is_not(con) ? op(arg(con,0)) : op(con); + if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt)) + r = -r; + } + rats[i-2] = r; + } + extract_lcd(rats); +} + +void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& coeffs){ + std::vector rats; + get_assign_bounds_coeffs(proof,rats); + coeffs.resize(rats.size()); + for(unsigned i = 0; i < rats.size(); i++){ + coeffs[i] = make_int(rats[i]); + } +} + +void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& rats){ + symb s = sym(proof); + int numps = s->get_num_parameters(); + rats.resize(numps-1); + rats[0] = rational(1); + for(int i = 2; i < numps; i++){ + rational r; + bool ok = s->get_parameter(i).is_rational(r); + if(!ok) + throw "Bad Farkas coefficient"; + { + 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; + } + rats[i-1] = r; + } + extract_lcd(rats); +} + + /** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */ + +void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q){ + ast Qrhs; + bool strict = op(P) == Lt; + if(is_not(Q)){ + ast nQ = arg(Q,0); + switch(op(nQ)){ + case Gt: + Qrhs = make(Sub,arg(nQ,1),arg(nQ,0)); + break; + case Lt: + Qrhs = make(Sub,arg(nQ,0),arg(nQ,1)); + break; + case Geq: + Qrhs = make(Sub,arg(nQ,1),arg(nQ,0)); + strict = true; + break; + case Leq: + Qrhs = make(Sub,arg(nQ,0),arg(nQ,1)); + strict = true; + break; + default: + throw "not an inequality"; + } + } + else { + switch(op(Q)){ + case Leq: + Qrhs = make(Sub,arg(Q,1),arg(Q,0)); + break; + case Geq: + Qrhs = make(Sub,arg(Q,0),arg(Q,1)); + break; + case Lt: + Qrhs = make(Sub,arg(Q,1),arg(Q,0)); + strict = true; + break; + case Gt: + Qrhs = make(Sub,arg(Q,0),arg(Q,1)); + strict = true; + break; + default: + throw "not an inequality"; + } + } + Qrhs = make(Times,c,Qrhs); + if(strict) + P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs)); + else + P = make(Leq,arg(P,0),make(Plus,arg(P,1),Qrhs)); +} + +iz3mgr::ast iz3mgr::sum_inequalities(const std::vector &coeffs, const std::vector &ineqs){ + ast zero = make_int("0"); + ast thing = make(Leq,zero,zero); + for(unsigned i = 0; i < ineqs.size(); i++){ + linear_comb(thing,coeffs[i],ineqs[i]); + } + thing = simplify_ineq(thing); + return thing; +} + +void iz3mgr::mk_idiv(const ast& t, const rational &d, ast &whole, ast &frac){ + opr o = op(t); + if(o == Plus){ + int nargs = num_args(t); + for(int i = 0; i < nargs; i++) + mk_idiv(arg(t,i),d,whole,frac); + return; + } + else if(o == Times){ + rational coeff; + if(is_numeral(arg(t,0),coeff)){ + if(gcd(coeff,d) == d){ + whole = make(Plus,whole,make(Times,make_int(coeff/d),arg(t,1))); + return; + } + } + } + frac = make(Plus,frac,t); +} + +iz3mgr::ast iz3mgr::mk_idiv(const ast& q, const rational &d){ + ast t = z3_simplify(q); + if(d == rational(1)) + return t; + else { + ast whole = make_int("0"); + ast frac = whole; + mk_idiv(t,d,whole,frac); + return z3_simplify(make(Plus,whole,make(Idiv,z3_simplify(frac),make_int(d)))); + } +} + +iz3mgr::ast iz3mgr::mk_idiv(const ast& t, const ast &d){ + rational r; + if(is_numeral(d,r)) + return mk_idiv(t,r); + return make(Idiv,t,d); +} diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 4ae345319..83cd573f3 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -224,11 +224,11 @@ class iz3mgr { ast make(opr op, const ast &arg0, const ast &arg1, const ast &arg2); ast make(symb sym, const std::vector &args); ast make(symb sym); - ast make(symb sym, ast &arg0); - ast make(symb sym, ast &arg0, ast &arg1); - ast make(symb sym, ast &arg0, ast &arg1, ast &arg2); + ast make(symb sym, const ast &arg0); + ast make(symb sym, const ast &arg0, const ast &arg1); + ast make(symb sym, const ast &arg0, const ast &arg1, const ast &arg2); ast make_quant(opr op, const std::vector &bvs, ast &body); - ast clone(ast &t, const std::vector &args); + ast clone(const ast &t, const std::vector &args); ast_manager &m() {return m_manager;} @@ -276,6 +276,12 @@ class iz3mgr { return ast(); } + void get_args(const ast &t, std::vector &res){ + res.resize(num_args(t)); + for(unsigned i = 0; i < res.size(); i++) + res[i] = arg(t,i); + } + symb sym(ast t){ return to_app(t.raw())->get_decl(); } @@ -306,6 +312,19 @@ class iz3mgr { return "NaN"; } + bool is_numeral(const ast& t, rational &r){ + expr* e = to_expr(t.raw()); + assert(e); + return m_arith_util.is_numeral(e, r); + } + + rational get_coeff(const ast& t){ + rational res; + if(op(t) == Times && is_numeral(arg(t,0),res)) + return res; + return rational(1); + } + int get_quantifier_num_bound(const ast &t) { return to_quantifier(t.raw())->get_num_decls(); } @@ -337,6 +356,54 @@ class iz3mgr { return to_func_decl(s)->get_range(); } + int get_num_parameters(const symb &s){ + return to_func_decl(s)->get_num_parameters(); + } + + ast get_ast_parameter(const symb &s, int idx){ + return cook(to_func_decl(s)->get_parameters()[idx].get_ast()); + } + + enum lemma_theory {ArithTheory,UnknownTheory}; + + lemma_theory get_theory_lemma_theory(const ast &proof){ + symb s = sym(proof); + ::symbol p0; + bool ok = s->get_parameter(0).is_symbol(p0); + if(!ok) return UnknownTheory; + std::string foo(p0.bare_str()); + if(foo == "arith") + return ArithTheory; + return UnknownTheory; + } + + enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,UnknownKind}; + + lemma_kind get_theory_lemma_kind(const ast &proof){ + symb s = sym(proof); + ::symbol p0; + bool ok = s->get_parameter(1).is_symbol(p0); + if(!ok) return UnknownKind; + std::string foo(p0.bare_str()); + if(foo == "farkas") + return FarkasKind; + if(foo == "triangle-eq") + return is_not(arg(conc(proof),0)) ? Eq2LeqKind : Leq2EqKind; + if(foo == "gcd-test") + return GCDTestKind; + if(foo == "assign-bounds") + return AssignBoundsKind; + return UnknownKind; + } + + void get_farkas_coeffs(const ast &proof, std::vector& coeffs); + + void get_farkas_coeffs(const ast &proof, std::vector& rats); + + void get_assign_bounds_coeffs(const ast &proof, std::vector& rats); + + void get_assign_bounds_coeffs(const ast &proof, std::vector& rats); + bool is_true(ast t){ return op(t) == True; } @@ -357,6 +424,10 @@ class iz3mgr { return op(t) == Not; } + /** Simplify an expression using z3 simplifier */ + + ast z3_simplify(const ast& e); + // Some constructors that simplify things ast mk_not(ast x){ @@ -389,6 +460,20 @@ class iz3mgr { return make(Or,x,y); } + ast mk_or(const std::vector &x){ + ast res = mk_false(); + for(unsigned i = 0; i < x.size(); i++) + res = mk_or(res,x[i]); + return res; + } + + ast mk_and(const std::vector &x){ + ast res = mk_true(); + for(unsigned i = 0; i < x.size(); i++) + res = mk_and(res,x[i]); + return res; + } + ast mk_equal(ast x, ast y){ if(x == y) return make(True); opr ox = op(x); @@ -419,11 +504,74 @@ class iz3mgr { return cook(m_arith_util.mk_numeral(rational(s.c_str()),r)); } + ast make_int(const rational &s) { + sort *r = m().mk_sort(m_arith_fid, INT_SORT); + return cook(m_arith_util.mk_numeral(s,r)); + } + + ast make_real(const std::string &s) { + sort *r = m().mk_sort(m_arith_fid, REAL_SORT); + return cook(m_arith_util.mk_numeral(rational(s.c_str()),r)); + } + + ast make_real(const rational &s) { + sort *r = m().mk_sort(m_arith_fid, REAL_SORT); + return cook(m_arith_util.mk_numeral(s,r)); + } ast mk_false() { return make(False); } ast mk_true() { return make(True); } + ast mk_fresh_constant(char const * prefix, type s){ + return cook(m().mk_fresh_const(prefix, s)); + } + + type bool_type() { + ::sort *s = m().mk_sort(m_basic_fid, BOOL_SORT); + return s; + } + + type int_type() { + ::sort *s = m().mk_sort(m_arith_fid, INT_SORT); + return s; + } + + type real_type() { + ::sort *s = m().mk_sort(m_arith_fid, REAL_SORT); + return s; + } + + type array_type(type d, type r) { + parameter params[2] = { parameter(d), parameter(to_sort(r)) }; + ::sort * s = m().mk_sort(m_array_fid, ARRAY_SORT, 2, params); + return s; + } + + symb function(const std::string &str_name, unsigned arity, type *domain, type range) { + ::symbol name = ::symbol(str_name.c_str()); + std::vector< ::sort *> sv(arity); + for(unsigned i = 0; i < arity; i++) + sv[i] = domain[i]; + ::func_decl* d = m().mk_func_decl(name,arity,&sv[0],range); + return d; + } + + void linear_comb(ast &P, const ast &c, const ast &Q); + + ast sum_inequalities(const std::vector &coeffs, const std::vector &ineqs); + + ast simplify_ineq(const ast &ineq){ + ast res = make(op(ineq),arg(ineq,0),z3_simplify(arg(ineq,1))); + return res; + } + + void mk_idiv(const ast& t, const rational &d, ast &whole, ast &frac); + + ast mk_idiv(const ast& t, const rational &d); + + ast mk_idiv(const ast& t, const ast &d); + /** methods for destructing proof terms */ pfrule pr(const z3pf &t); @@ -437,6 +585,8 @@ class iz3mgr { /** For debugging */ void show(ast); + void show_symb(symb s); + /** Constructor */ void print_lit(ast lit); diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp new file mode 100644 index 000000000..5cd75bc26 --- /dev/null +++ b/src/interp/iz3proof_itp.cpp @@ -0,0 +1,789 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3proof.cpp + +Abstract: + + This class defines a simple interpolating proof system. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + +#include "iz3proof_itp.h" + +#ifndef WIN32 +using namespace stl_ext; +#endif + + +class iz3proof_itp_impl : public iz3proof_itp { + + prover *pv; + prover::range rng; + bool weak; + + enum LitType {LitA,LitB,LitMixed}; + + hash_map placeholders; + symb farkas; + + ast get_placeholder(ast t){ + hash_map::iterator it = placeholders.find(t); + if(it != placeholders.end()) + return it->second; + ast &res = placeholders[t]; + res = mk_fresh_constant("@p",get_type(t)); + std::cout << "placeholder "; + print_expr(std::cout,res); + std::cout << " = "; + print_expr(std::cout,t); + std::cout << std::endl; + return res; + } + + ast make_farkas(ast &coeff, ast &ineq){ + return make(farkas,coeff,ineq); + } + + LitType get_term_type(const ast &lit){ + prover::range r = pv->ast_scope(lit); + if(pv->range_is_empty(r)) + return LitMixed; + if(weak) { + if(pv->range_min(r) == SHRT_MIN) + return pv->range_contained(r,rng) ? LitA : LitB; + else + return pv->ranges_intersect(r,rng) ? LitA : LitB; + } + else + return pv->range_contained(r,rng) ? LitA : LitB; + } + + /** Make a resolution node with given pivot literal and premises. + The conclusion of premise1 should contain the negation of the + pivot literal, while the conclusion of premise2 should contain the + pivot literal. + */ + node make_resolution(ast pivot, const std::vector &conc, node premise1, node premise2) { + LitType lt = get_term_type(pivot); + if(lt == LitA) + return my_or(premise1,premise2); + if(lt == LitB) + return my_and(premise1,premise2); + + /* 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(); + } + + /* Handles the case of resolution on a mixed equality atom. */ + + ast resolve_equality(const ast &pivot, const std::vector &conc, node premise1, node premise2){ + ast atom = get_lit_atom(pivot); + + /* Get the A term in the mixed equality. */ + ast A_term = arg(atom,0); + if(get_term_type(A_term) != LitA) + A_term = arg(atom,1); + + /* Resolve it out. */ + hash_map memo; + // ast neg_pivot_placeholder = get_placeholder(mk_not(atom)); + ast neg_pivot_placeholder = mk_not(atom); + ast A_term_placeholder = get_placeholder(atom); + if(op(pivot) != Not) + std::swap(premise1,premise2); + return resolve_equality_rec(memo, neg_pivot_placeholder, premise1, A_term_placeholder, premise2); + } + + ast resolve_equality_rec(hash_map &memo, const ast &neg_pivot_placeholder, const ast &premise1, + const ast &A_term, const ast &premise2){ + ast &res = memo[premise1]; + if(!res.null()) + return res; + + if(op(premise1) == And + && num_args(premise1) == 2 + && arg(premise1,1) == neg_pivot_placeholder){ + ast common_term = arg(arg(premise1,0),1); + res = subst_term_and_simp(A_term,common_term,premise2); + } + else { + switch(op(premise1)){ + case Or: + case And: { + unsigned nargs = num_args(premise1); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = resolve_equality_rec(memo, neg_pivot_placeholder, arg(premise1,i), A_term, premise2); + ast foo = premise1; // get rid of const + res = clone(foo,args); + break; + } + default: + res = premise1; + } + } + return res; + } + + /* Handles the case of resolution on a mixed arith atom. */ + + ast resolve_arith(const ast &pivot, const std::vector &conc, node premise1, node premise2){ + ast atom = get_lit_atom(pivot); + hash_map memo; + ast neg_pivot_lit = mk_not(atom); + if(op(pivot) != Not) + std::swap(premise1,premise2); + 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 &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 sum_ineq(const ast &coeff1, const ast &ineq1, const ast &coeff2, const ast &ineq2){ + opr sum_op = Leq; + if(op(ineq1) == Lt || op(ineq2) == Lt) + 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] = 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){ + std::vector 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))); + collect_farkas_resolvents(pivot1,coeff2,conj1,resolvent); + collect_farkas_resolvents(pivot2,coeff1,conj2,resolvent); + return make(And,resolvent); + } + + bool is_farkas_itp(const ast &pivot1, const 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(arg(foo,1) == pivot1){ + pivot2 = foo; + return true; + } + } + else break; + } + } + return false; + } + + ast resolve_arith_rec2(hash_map &memo, const ast &pivot1, const ast &conj1, const ast &itp2){ + ast &res = memo[itp2]; + if(!res.null()) + return res; + + ast pivot2; + if(is_farkas_itp(mk_not(arg(pivot1,1)),itp2,pivot2)) + res = resolve_farkas(pivot1,conj1,pivot2,itp2); + else { + switch(op(itp2)){ + case Or: + case And: { + unsigned nargs = num_args(itp2); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,i)); + ast foo = itp2; // get rid of const + res = clone(foo,args); + break; + } + default: + res = itp2; + } + } + return res; + } + + ast resolve_arith_rec1(hash_map &memo, const ast &neg_pivot_lit, const ast &itp1, const ast &itp2){ + ast &res = memo[itp1]; + if(!res.null()) + return res; + ast pivot1; + if(is_farkas_itp(neg_pivot_lit,itp1,pivot1)){ + hash_map memo2; + res = resolve_arith_rec2(memo2,pivot1,itp1,itp2); + res = resolve_arith_placeholders(pivot1,itp1,res); + } + else { + switch(op(itp1)){ + case Or: + case And: { + unsigned nargs = num_args(itp1); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,i), itp2); + ast foo = itp1; // get rid of const + res = clone(foo,args); + break; + } + default: + res = itp1; + } + } + return res; + } + + ast resolve_arith_placeholders(const ast &pivot1, const ast &conj1, const ast &itp2){ + ast coeff = arg(pivot1,0); + coeff = z3_simplify(coeff); + ast soln = mk_idiv(arg(arg(conj1,0),1),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))); + } + } + ast pl = get_placeholder(mk_not(arg(pivot1,1))); + ast res = subst_term_and_simp(pl,soln,itp2); + return res; + } + + hash_map subst_memo; // memo of subst function + + ast subst_term_and_simp(const ast &var, const ast &t, const ast &e){ + subst_memo.clear(); + return subst_term_and_simp_rec(var,t,e); + } + + ast subst_term_and_simp_rec(const ast &var, const ast &t, const ast &e){ + if(e == var) return t; + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = subst_memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + int nargs = num_args(e); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = subst_term_and_simp_rec(var,t,arg(e,i)); + 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 res = clone(e,args); + } + return res; + } + + + /** Make an assumption node. The given clause is assumed in the given frame. */ + virtual node make_assumption(int frame, const std::vector &assumption){ + if(pv->in_range(frame,rng)){ + std::vector itp_clause; + for(unsigned i = 0; i < assumption.size(); i++) + if(get_term_type(assumption[i]) != LitA) + itp_clause.push_back(assumption[i]); + ast res = my_or(itp_clause); + return res; + } + else { + return mk_true(); + } +} + + /** 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)); + } + } + 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))); + } + else + itp = mk_true(); + } + + /* Resolve it with the premises */ + std::vector 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); + return itp; + } + + /** Make an axiom node. The conclusion must be an instance of an axiom. */ + virtual node make_axiom(const std::vector &conclusion){ + throw proof_error(); +} + + /** Make a Contra node. This rule takes a derivation of the form + Gamma |- False and produces |- \/~Gamma. */ + + virtual node make_contra(node prem, const std::vector &conclusion){ + return prem; + } + + /** Make hypothesis. Creates a node of the form P |- P. */ + + virtual node make_hypothesis(const ast &P){ + if(is_not(P)) + return make_hypothesis(arg(P,0)); + switch(get_term_type(P)){ + case LitA: + return mk_false(); + case LitB: + 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); + return res; + } + default: + throw proof_error(); + } + } + } + + /** Make a Reflexivity node. This rule produces |- x = x */ + + virtual node make_reflexivity(ast con){ + throw proof_error(); +} + + /** Make a Symmetry node. This takes a derivation of |- x = y and + produces | y = x */ + + virtual node make_symmetry(ast con, node prem){ + ast x = arg(con,0); + ast y = arg(con,1); + ast p = make(Equal,y,x); + 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)); + std::vector conc; conc.push_back(con); + itp = make_resolution(p,conc,itp,prem); + return itp; + } + + /** Make a transitivity node. This takes derivations of |- x = y + and |- y = z produces | x = z */ + + virtual node make_transitivity(const ast &x, const ast &y, const ast &z, node prem1, node prem2){ + + /* Interpolate the axiom x=y,y=z,-> x=z */ + ast p = make(Equal,x,y); + ast q = make(Equal,y,z); + ast r = make(Equal,x,z); + ast itp; + if(get_term_type(p) == LitA){ + if(get_term_type(q) == LitA){ + if(get_term_type(r) == LitA) + itp = mk_false(); + else + itp = r; + } + else { + if(get_term_type(r) == LitA) + itp = mk_not(q); + else { + if(get_term_type(r) == LitB) + itp = make(Equal,x,get_placeholder(q)); + else { + ast mid = (get_term_type(y) == LitA) ? get_placeholder(q) : y; + itp = make(And,make(Equal,x,mid),mk_not(r)); + } + } + } + } + else { + if(get_term_type(q) == LitA){ + if(get_term_type(r) == LitA) + itp = mk_not(p); + else { + if(get_term_type(r) == LitB) + itp = make(Equal,get_placeholder(p),z); + else { + ast mid = (get_term_type(y) == LitA) ? get_placeholder(p) : y; + itp = make(And,make(Equal,z,mid),mk_not(r)); + } + } + } + else { + if(get_term_type(r) == LitA){ + ast xr = (get_term_type(x) == LitA) ? get_placeholder(p) : x; + ast zr = (get_term_type(z) == LitA) ? get_placeholder(q) : z; + itp = mk_not(make(Equal,xr,zr)); + } + else { + LitType xt = get_term_type(x); + LitType zt = get_term_type(z); + if(xt == LitA && zt == LitB) + itp = make(And,make(Equal,x,get_placeholder(p)),mk_not(r)); + else if(zt == LitA && xt == LitB) + itp = make(And,make(Equal,z,get_placeholder(q)),mk_not(r)); + else + itp = mk_true(); + } + } + } + + /* Resolve it with the premises */ + std::vector conc; conc.push_back(r); conc.push_back(mk_not(q)); + itp = make_resolution(p,conc,itp,prem1); + conc.pop_back(); + itp = make_resolution(q,conc,itp,prem2); + 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 &hyps, const ast &prem1){ + ast p = make(Equal,x,y); + ast itp; + if(get_term_type(p) == LitA){ + if(get_term_type(con) == LitA) + itp = mk_false(); + else + throw proof_error(); // itp = p; + } + else { + if(get_term_type(con) == LitA) + itp = mk_not(p); + else{ + if(get_term_type(con) == LitB) + itp = mk_true(); + else + itp = make_mixed_congruence(x, y, con, hyps, prem1); + } + } + std::vector conc; conc.push_back(con); + itp = make_resolution(p,conc,itp,prem1); + return itp; + } + + /* Interpolate a mixed congruence axiom. */ + + virtual ast make_mixed_congruence(const ast &x, const ast &y, const ast &con, const std::vector &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); + } + + // find the argument position of x and y + int pos = -1; + int nargs = num_args(arg(con,0)); + for(int i = 0; i < nargs; i++) + if(x == arg(arg(con,0),i) && y == arg(arg(con,1),i)) + pos = i; + if(pos == -1) + throw proof_error(); + + 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; + } + + ast subst_in_arg_pos(int pos, ast term, ast app){ + std::vector args; + get_args(app,args); + args[pos] = term; + return clone(app,args); + } + + /** Make a farkas proof node. */ + + virtual node make_farkas(ast con, const std::vector &prems, const std::vector &prem_cons, + const std::vector &coeffs){ + + /* Compute the interpolant for the clause */ + + ast zero = make_int("0"); + std::vector conjs; conjs.resize(1); + 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); + } + + /* Resolve it with the premises */ + std::vector conc; conc.resize(prem_cons.size()); + for(unsigned i = 0; i < prem_cons.size(); i++) + conc[prem_cons.size()-i-1] = prem_cons[i]; + for(unsigned i = 0; i < prem_cons.size(); i++){ + thing = make_resolution(prem_cons[i],conc,thing,prems[i]); + conc.pop_back(); + } + return thing; + } + + /** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */ + + void linear_comb(ast &P, const ast &c, const ast &Q){ + ast Qrhs; + bool strict = op(P) == Lt; + if(is_not(Q)){ + ast nQ = arg(Q,0); + switch(op(nQ)){ + case Gt: + Qrhs = make(Sub,arg(nQ,1),arg(nQ,0)); + break; + case Lt: + Qrhs = make(Sub,arg(nQ,0),arg(nQ,1)); + break; + case Geq: + Qrhs = make(Sub,arg(nQ,1),arg(nQ,0)); + strict = true; + break; + case Leq: + Qrhs = make(Sub,arg(nQ,0),arg(nQ,1)); + strict = true; + break; + default: + throw proof_error(); + } + } + else { + switch(op(Q)){ + case Leq: + Qrhs = make(Sub,arg(Q,1),arg(Q,0)); + break; + case Geq: + Qrhs = make(Sub,arg(Q,0),arg(Q,1)); + break; + case Lt: + Qrhs = make(Sub,arg(Q,1),arg(Q,0)); + strict = true; + break; + case Gt: + Qrhs = make(Sub,arg(Q,0),arg(Q,1)); + strict = true; + break; + default: + throw proof_error(); + } + } + Qrhs = make(Times,c,Qrhs); + if(strict) + P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs)); + else + P = make(Leq,arg(P,0),make(Plus,arg(P,1),Qrhs)); + } + + /* Make an axiom instance of the form |- x<=y, y<= x -> x =y */ + virtual node make_leq2eq(ast x, ast y, const ast &xleqy, const ast &yleqx){ + ast con = make(Equal,x,y); + ast itp; + switch(get_term_type(con)){ + case LitA: + itp = mk_false(); + break; + case LitB: + 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); + } + } + return itp; + } + + /* Make an axiom instance of the form |- x = y -> x <= y */ + virtual node make_eq2leq(ast x, ast y, const ast &xleqy){ + ast itp; + switch(get_term_type(xleqy)){ + case LitA: + itp = mk_false(); + break; + case LitB: + itp = mk_true(); + break; + default: { // mixed equality + ast mid = get_placeholder(make(Equal,x,y)); + if(get_term_type(y) == LitA){ + std::swap(x,y); + mid = make(Sub,x,mid); + } + else { + mid = make(Sub,mid,x); + } + ast zleqmid = make(Leq,make_int("0"),mid); + ast fark = make(farkas,make_int("1"),mk_not(xleqy)); + itp = make(And,zleqmid,fark); + } + } + return itp; + } + + + /* Make an inference of the form t <= c |- t/d <= floor(c/d) where t + 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){ + ast itp = mk_false(); + switch(get_term_type(con)){ + case LitA: + itp = mk_false(); + break; + case LitB: + itp = mk_true(); + break; + default: { + ast t = arg(tleqc,0); + ast c = arg(tleqc,1); + ast thing = make(farkas,make_int("1"),mk_not(con)); + itp = make(And,make(Leq,make_int("0"),make(Idiv,get_placeholder(tleqc),d)),thing); + } + } + std::vector conc; conc.push_back(con); + itp = make_resolution(tleqc,conc,itp,prem); + return itp; + } + + ast get_farkas_coeff(const ast &f){ + ast c = arg(f,0); + // if(!is_not(arg(f,1))) + // c = make(Uminus,c); + return c; + } + + ast my_or(const ast &a, const ast &b){ + return mk_or(a,b); + } + + ast my_and(const ast &a, const ast &b){ + return mk_and(a,b); + } + + ast my_or(const std::vector &a){ + return mk_or(a); + } + + ast my_and(const std::vector &a){ + return mk_and(a); + } + + ast get_lit_atom(const ast &l){ + if(op(l) == Not) + return arg(l,0); + return l; + } + +public: + iz3proof_itp_impl(prover *p, const prover::range &r, bool w) + : iz3proof_itp(*p) + { + pv = p; + rng = r; + weak = w; + type domain[2] = {int_type(),bool_type()}; + farkas = function("@farkas",2,domain,bool_type()); + } + +}; + +iz3proof_itp *iz3proof_itp::create(prover *p, const prover::range &r, bool w){ + return new iz3proof_itp_impl(p,r,w); +} + diff --git a/src/interp/iz3proof_itp.h b/src/interp/iz3proof_itp.h new file mode 100644 index 000000000..692fb7772 --- /dev/null +++ b/src/interp/iz3proof_itp.h @@ -0,0 +1,130 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3proof.h + +Abstract: + + This class defines a simple interpolating proof system. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + +#ifndef IZ3PROOF_ITP_H +#define IZ3PROOF_ITP_H + +#include + +#include "iz3base.h" +#include "iz3secondary.h" + +// #define CHECK_PROOFS + +/** This class defines a simple proof system. + + As opposed to iz3proof, this class directly computes interpolants, + so the proof representation is just the interpolant itself. + + */ + +class iz3proof_itp : public iz3mgr { + public: + + /** Enumeration of proof rules. */ + enum rule {Resolution,Assumption,Hypothesis,Theory,Axiom,Contra,Lemma,Reflexivity,Symmetry,Transitivity,Congruence,EqContra}; + + /** Interface to prover. */ + typedef iz3base prover; + + /** Ast type. */ + typedef prover::ast ast; + + /** The type of proof nodes (just interpolants). */ + typedef ast node; + + /** Object thrown in case of a proof error. */ + struct proof_error {}; + + + /** Make a resolution node with given pivot literal and premises. + The conclusion of premise1 should contain the negation of the + pivot literal, while the conclusion of premise2 should containe the + pivot literal. + */ + virtual node make_resolution(ast pivot, const std::vector &conc, node premise1, node premise2) = 0; + + /** Make an assumption node. The given clause is assumed in the given frame. */ + virtual node make_assumption(int frame, const std::vector &assumption) = 0; + + /** Make a hypothesis node. If phi is the hypothesis, this is + effectively phi |- phi. */ + virtual node make_hypothesis(const ast &hypothesis) = 0; + + /** Make an axiom node. The conclusion must be an instance of an axiom. */ + virtual node make_axiom(const std::vector &conclusion) = 0; + + /** Make a Contra node. This rule takes a derivation of the form + Gamma |- False and produces |- \/~Gamma. */ + + virtual node make_contra(node prem, const std::vector &conclusion) = 0; + + /** Make a Reflexivity node. This rule produces |- x = x */ + + virtual node make_reflexivity(ast con) = 0; + + /** Make a Symmetry node. This takes a derivation of |- x = y and + produces | y = x */ + + virtual node make_symmetry(ast con, node prem) = 0; + + /** Make a transitivity node. This takes derivations of |- x = y + and |- y = z produces | x = z */ + + virtual node make_transitivity(const ast &x, const ast &y, const ast &z, node prem1, node prem2) = 0; + + /** 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 &hyps, 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; + + /** Make a farkas proof node. */ + + virtual node make_farkas(ast con, const std::vector &prems, const std::vector &prem_cons, const std::vector &coeffs) = 0; + + /* Make an axiom instance of the form |- x<=y, y<= x -> x =y */ + virtual node make_leq2eq(ast x, ast y, const ast &xleqy, const ast &yleqx) = 0; + + /* Make an axiom instance of the form |- x = y -> x <= y */ + virtual node make_eq2leq(ast x, ast y, const ast &xeqy) = 0; + + /* Make an inference of the form t <= c |- t/d <= floor(c/d) where t + 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; + + /** Create proof object to construct an interpolant. */ + static iz3proof_itp *create(prover *p, const prover::range &r, bool _weak); + + protected: + iz3proof_itp(iz3mgr &m) + : iz3mgr(m) + { + } + + public: + virtual ~iz3proof_itp(){ + } +}; + +#endif diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp new file mode 100755 index 000000000..8220fb214 --- /dev/null +++ b/src/interp/iz3translate.cpp @@ -0,0 +1,1164 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3translate.cpp + +Abstract: + + Translate a Z3 proof to in interpolated proof. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + +#include "iz3translate.h" +#include "iz3proof.h" +#include "iz3profiling.h" +#include "iz3interp.h" +#include "iz3proof_itp.h" + +#include +#include +#include +#include +#include +#include +#include + +//using std::vector; +#ifndef WIN32 +using namespace stl_ext; +#endif + + + +/* This translator goes directly from Z3 proofs to interpolated + proofs without an intermediate representation. No secondary + prover is used. +*/ + +class iz3translation_full : public iz3translation { +public: + + + typedef iz3proof_itp Iproof; + + Iproof *iproof; + + /* Here we have lots of hash tables for memoizing various methods and + other such global data structures. + */ + + typedef hash_map AstToInt; + AstToInt locality; // memoizes locality of Z3 proof terms + + typedef std::pair EquivEntry; + typedef hash_map EquivTab; + EquivTab equivs; // maps non-local terms to equivalent local terms, with proof + + typedef hash_set AstHashSet; + AstHashSet equivs_visited; // proofs already checked for equivalences + + typedef pair, hash_map > AstToIpf; + AstToIpf translation; // Z3 proof nodes to Iproof nodes + + AstToInt frame_map; // map assertions to frames + int frames; // number of frames + + typedef std::set AstSet; + typedef hash_map AstToAstSet; + AstToAstSet hyp_map; // map proof terms to hypothesis set + + struct LocVar { // localization vars + ast var; // a fresh variable + ast term; // term it represents + int frame; // frame in which it's defined + LocVar(ast v, ast t, int f){var=v;term=t;frame=f;} + }; + + std::vector localization_vars; // localization vars in order of creation + typedef hash_map AstToAst; + AstToAst localization_map; // maps terms to their localization vars + + typedef hash_map 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 + + public: + + +#define from_ast(x) (x) + + // 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 + // memoized in hash_map "locality" + + int get_locality_rec(ast proof){ + std::pair foo(proof,INT_MAX); + std::pair bar = locality.insert(foo); + int &res = bar.first->second; + 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; + } + else { + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++){ + ast arg = prem(proof,i); + int bar = get_locality_rec(arg); + if(res == INT_MAX || res == bar) res = bar; + else if(bar != INT_MAX) res = -1; + } + } + return res; + } + + + int get_locality(ast proof){ + // if(lia_z3_axioms_only) return -1; + int res = get_locality_rec(proof); + if(res != -1){ + ast con = conc(proof); + range rng = ast_scope(con); + + // hack: if a clause contains "true", it reduces to "true", + // which means we won't compute the range correctly. we handle + // this case by computing the ranges of the literals separately + + if(is_true(con)){ + std::vector lits; + get_Z3_lits(conc(proof),lits); + for(unsigned i = 0; i < lits.size(); i++) + rng = range_glb(rng,ast_scope(lits[i])); + } + + if(!range_is_empty(rng)){ + AstSet &hyps = get_hyps(proof); + for(AstSet::iterator it = hyps.begin(), en = hyps.end(); it != en; ++it){ + ast hyp = *it; + rng = range_glb(rng,ast_scope(hyp)); + } + } + + if(res == INT_MAX){ + if(range_is_empty(rng)) + res = -1; + else res = range_max(rng); + } + else { + if(!in_range(res,rng)) + res = -1; + } + } + return res; + } + + AstSet &get_hyps(ast proof){ + std::pair foo(proof,AstSet()); + std::pair bar = hyp_map.insert(foo); + AstSet &res = bar.first->second; + if(!bar.second) return res; + pfrule dk = pr(proof); + if(dk == PR_HYPOTHESIS){ + ast con = conc(proof); + res.insert(con); + } + else { + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++){ + ast arg = prem(proof,i); + AstSet &arg_hyps = get_hyps(arg); + res.insert(arg_hyps.begin(),arg_hyps.end()); + } + if(dk == PR_LEMMA){ + ast con = conc(proof); + res.erase(mk_not(con)); + if(is_or(con)){ + int clause_size = num_args(con); + for(int i = 0; i < clause_size; i++){ + ast neglit = mk_not(arg(con,i)); + res.erase(neglit); + } + } + } + } +#if 0 + AstSet::iterator it = res.begin(), en = res.end(); + if(it != en){ + AstSet::iterator old = it; + ++it; + for(; it != en; ++it, ++old) + if(!(*old < *it)) + std::cout << "foo!"; + } +#endif + return res; + } + + // Find all the judgements of the form p <-> q, where + // p is local and q is non-local, recording them in "equivs" + // the map equivs_visited is used to record the already visited proof terms + + void find_equivs(ast proof){ + if(equivs_visited.find(proof) != equivs_visited.end()) + return; + equivs_visited.insert(proof); + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++) // do all the sub_terms + find_equivs(prem(proof,i)); + ast con = conc(proof); // get the conclusion + if(is_iff(con)){ + ast iff = con; + for(int i = 0; i < 2; i++) + if(!is_local(arg(iff,i)) && is_local(arg(iff,1-i))){ + std::pair > foo(arg(iff,i),std::pair(arg(iff,1-i),proof)); + equivs.insert(foo); + } + } + } + + // get the lits of a Z3 clause + void get_Z3_lits(ast t, std::vector &lits){ + opr dk = op(t); + if(dk == False) + return; // false = empty clause + if(dk == Or){ + unsigned nargs = num_args(t); + lits.resize(nargs); + for(unsigned i = 0; i < nargs; i++) // do all the sub_terms + lits[i] = arg(t,i); + } + else { + lits.push_back(t); + } + } + + // resolve two clauses represented as vectors of lits. replace first clause + void resolve(ast pivot, std::vector &cls1, std::vector &cls2){ + ast neg_pivot = mk_not(pivot); + for(unsigned i = 0; i < cls1.size(); i++){ + if(cls1[i] == pivot){ + cls1[i] = cls1.back(); + cls1.pop_back(); + bool found_pivot2 = false; + for(unsigned j = 0; j < cls2.size(); j++){ + if(cls2[j] == neg_pivot) + found_pivot2 = true; + else + cls1.push_back(cls2[j]); + } + assert(found_pivot2); + return; + } + } + assert(0 && "resolve failed"); + } + + // get lits resulting from unit resolution up to and including "position" + // TODO: this is quadratic -- fix it + void do_unit_resolution(ast proof, int position, std::vector &lits){ + ast orig_clause = conc(prem(proof,0)); + get_Z3_lits(orig_clause,lits); + for(int i = 1; i <= position; i++){ + std::vector unit(1); + unit[0] = conc(prem(proof,i)); + resolve(mk_not(unit[0]),lits,unit); + } + } + + + // clear the localization variables + void clear_localization(){ + localization_vars.clear(); + localization_map.clear(); + } + + // create a fresh variable for localization + ast fresh_localization_var(ast term, int frame){ + std::ostringstream s; + s << "%" << (localization_vars.size()); + ast var = make_var(s.str().c_str(),get_type(term)); + sym_range(sym(var)) = range_full(); // make this variable global + localization_vars.push_back(LocVar(var,term,frame)); + return var; + } + + + // "localize" a term to a given frame range by + // creating new symbols to represent non-local subterms + + ast localize_term(ast e, const range &rng){ + if(ranges_intersect(ast_scope(e),rng)) + return e; // this term occurs in range, so it's O.K. + AstToAst::iterator it = localization_map.find(e); + if(it != localization_map.end()) + return 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) */){ + range frng = rng; + if(op(e) == Uninterpreted){ + symb f = sym(e); + range srng = sym_range(f); + if(ranges_intersect(srng,rng)) // localize to desired range if possible + frng = range_glb(srng,rng); + } + std::vector largs(nargs); + for(int i = 0; i < nargs; i++){ + largs[i] = localize_term(arg(e,i),frng); + frng = range_glb(frng,ast_scope(largs[i])); + } + e = clone(e,largs); + assert(is_local(e)); + } + + + if(ranges_intersect(ast_scope(e),rng)) + return e; // this term occurs in range, so it's O.K. + + // choose a frame for the constraint that is close to range + int frame = range_near(ast_scope(e),rng); + + ast new_var = fresh_localization_var(e,frame); + localization_map[e] = new_var; + ast cnst = make(Equal,new_var,e); + // antes.push_back(std::pair(cnst,frame)); + return new_var; + } + + // some patterm matching functions + + // match logical or with nargs arguments + // assumes AIG form + bool match_or(ast e, ast *args, int nargs){ + if(op(e) != Or) return false; + int n = num_args(e); + if(n != nargs) return false; + for(int i = 0; i < nargs; i++) + args[i] = arg(e,i); + return true; + } + + // match operator f with exactly nargs arguments + bool match_op(ast e, opr f, ast *args, int nargs){ + if(op(e) != f) return false; + int n = num_args(e); + if(n != nargs) return false; + for(int i = 0; i < nargs; i++) + args[i] = arg(e,i); + return true; + } + + // see if the given formula can be interpreted as + // an axiom instance (e.g., an array axiom instance). + // if so, add it to "antes" in an appropriate frame. + // this may require "localization" + + void get_axiom_instance(ast e){ + + // "store" axiom + // (or (= w q) (= (select (store a1 w y) q) (select a1 q))) + // std::cout << "ax: "; show(e); + ast lits[2],eq_ops_l[2],eq_ops_r[2],sel_ops[2], sto_ops[3], sel_ops2[2] ; + if(match_or(e,lits,2)) + if(match_op(lits[0],Equal,eq_ops_l,2)) + if(match_op(lits[1],Equal,eq_ops_r,2)) + for(int i = 0; i < 2; i++){ // try the second equality both ways + if(match_op(eq_ops_r[0],Select,sel_ops,2)) + if(match_op(sel_ops[0],Store,sto_ops,3)) + if(match_op(eq_ops_r[1],Select,sel_ops2,2)) + for(int j = 0; j < 2; j++){ // try the first equality both ways + if(eq_ops_l[0] == sto_ops[1] + && eq_ops_l[1] == sel_ops[1] + && eq_ops_l[1] == sel_ops2[1] + && sto_ops[0] == sel_ops2[0]) + if(is_local(sel_ops[0])) // store term must be local + { + ast sto = sel_ops[0]; + ast addr = localize_term(eq_ops_l[1],ast_scope(sto)); + ast res = make(Or, + make(Equal,eq_ops_l[0],addr), + make(Equal, + make(Select,sto,addr), + make(Select,sel_ops2[0],addr))); + // int frame = range_min(ast_scope(res)); TODO + // antes.push_back(std::pair(res,frame)); + return; + } + std::swap(eq_ops_l[0],eq_ops_l[1]); + } + std::swap(eq_ops_r[0],eq_ops_r[1]); + } + } + + // a quantifier instantation looks like (~ forall x. P) \/ P[z/x] + // we need to find a time frame for P, then localize P[z/x] in this frame + + void get_quantifier_instance(ast e){ + ast disjs[2]; + if(match_or(e,disjs,2)){ + if(is_local(disjs[0])){ + ast res = localize_term(disjs[1], ast_scope(disjs[0])); + // int frame = range_min(ast_scope(res)); TODO + // antes.push_back(std::pair(res,frame)); + return; + } + } + } + + ast get_judgement(ast proof){ + ast con = from_ast(conc(proof)); + AstSet &hyps = get_hyps(proof); + std::vector hyps_vec; + for(AstSet::iterator it = hyps.begin(), en = hyps.end(); it != en; ++it) + hyps_vec.push_back(*it); + if(hyps_vec.size() == 0) return con; + con = make(Or,mk_not(make(And,hyps_vec)),con); + return con; + } + + // does variable occur in expression? + int occurs_in1(ast var, ast e){ + std::pair foo(e,false); + std::pair 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 foo(e,ast()); + std::pair bar = subst_memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + int nargs = num_args(e); + std::vector 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 bvs; bvs.push_back(var); + return make_quant(quantifier,bvs,e); + } + + // add quantifiers over the localization vars + // to an interpolant for frames lo-hi + + ast add_quants(ast e, int lo, int hi){ + for(int i = localization_vars.size() - 1; i >= 0; i--){ + LocVar &lv = localization_vars[i]; + opr quantifier = (lv.frame >= lo && lv.frame <= hi) ? Exists : Forall; + e = apply_quant(quantifier,lv.var,e); + } + return e; + } + + int get_lits_locality(std::vector &lits){ + range rng = range_full(); + for(std::vector::iterator it = lits.begin(), en = lits.end(); it != en; ++it){ + ast lit = *it; + rng = range_glb(rng,ast_scope(lit)); + } + if(range_is_empty(rng)) return -1; + int hi = range_max(rng); + if(hi >= frames) return frames - 1; + return hi; + } + + int num_lits(ast ast){ + opr dk = op(ast); + if(dk == False) + return 0; + if(dk == Or){ + unsigned nargs = num_args(ast); + int n = 0; + for(unsigned i = 0; i < nargs; i++) // do all the sub_terms + n += num_lits(arg(ast,i)); + return n; + } + else + return 1; + } + + std::vector lit_trace; + hash_set marked_proofs; + + bool proof_has_lit(const ast &proof, const ast &lit){ + AstSet &hyps = get_hyps(proof); + if(hyps.find(mk_not(lit)) != hyps.end()) + return true; + std::vector lits; + ast con = conc(proof); + get_Z3_lits(con, lits); + for(unsigned i = 0; i < lits.size(); i++) + if(lits[i] == lit) + return true; + return false; + } + + + void trace_lit_rec(const ast &lit, const ast &proof, AstHashSet &memo){ + if(memo.find(proof) == memo.end()){ + memo.insert(proof); + AstSet &hyps = get_hyps(proof); + std::vector lits; + for(AstSet::iterator it = hyps.begin(), en = hyps.end(); it != en; ++it) + lits.push_back(mk_not(*it)); + ast con = conc(proof); + get_Z3_lits(con, lits); + for(unsigned i = 0; i < lits.size(); i++){ + if(lits[i] == lit){ + print_expr(std::cout,proof); + std::cout << "\n"; + marked_proofs.insert(proof); + pfrule dk = pr(proof); + if(dk == PR_UNIT_RESOLUTION || dk == PR_LEMMA){ + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++){ + ast arg = prem(proof,i); + trace_lit_rec(lit,arg,memo); + } + } + else + lit_trace.push_back(proof); + } + } + } + } + + ast traced_lit; + + int trace_lit(const ast &lit, const ast &proof){ + marked_proofs.clear(); + lit_trace.clear(); + traced_lit = lit; + AstHashSet memo; + trace_lit_rec(lit,proof,memo); + return lit_trace.size(); + } + + bool is_literal_or_lit_iff(const ast &lit){ + if(my_is_literal(lit)) return true; + if(op(lit) == Iff){ + return my_is_literal(arg(lit,0)) && my_is_literal(arg(lit,1)); + } + return false; + } + + bool my_is_literal(const ast &lit){ + ast abslit = is_not(lit) ? arg(lit,0) : lit; + int f = op(abslit); + return !(f == And || f == Or || f == Iff); + } + + 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 << "]"; + } + else + print_expr(std::cout,lit); + } + + void show_lit(const ast &lit){ + print_lit(lit); + std::cout << "\n"; + } + + void print_z3_lit(const ast &a){ + print_lit(from_ast(a)); + } + + void show_z3_lit(const ast &a){ + print_z3_lit(a); + std::cout << "\n"; + } + + + void show_con(const ast &proof, bool brief){ + if(!traced_lit.null() && proof_has_lit(proof,traced_lit)) + std::cout << "(*) "; + ast con = conc(proof); + AstSet &hyps = get_hyps(proof); + int count = 0; + for(AstSet::iterator it = hyps.begin(), en = hyps.end(); it != en; ++it){ + if(brief && ++count > 5){ + std::cout << "... "; + break; + } + print_lit(*it); + std::cout << " "; + } + std::cout << "|- "; + std::vector lits; + get_Z3_lits(con,lits); + for(unsigned i = 0; i < lits.size(); i++){ + print_lit(lits[i]); + std::cout << " "; + } + std::cout << "\n"; + } + + void show_step(const ast &proof){ + std::cout << "\n"; + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++){ + std::cout << "(" << i << ") "; + ast arg = prem(proof,i); + show_con(arg,true); + } + std::cout << "|------ "; + std::cout << string_of_symbol(sym(proof)) << "\n"; + show_con(proof,false); + } + + void show_marked( const ast &proof){ + std::cout << "\n"; + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++){ + ast arg = prem(proof,i); + if(!traced_lit.null() && proof_has_lit(arg,traced_lit)){ + std::cout << "(" << i << ") "; + show_con(arg,true); + } + } + } + + std::vector pfhist; + int pfhist_pos; + + void pfgoto(const ast &proof){ + if(pfhist.size() == 0) + pfhist_pos = 0; + else pfhist_pos++; + pfhist.resize(pfhist_pos); + pfhist.push_back(proof); + show_step(proof); + } + + + void pfback(){ + if(pfhist_pos > 0){ + pfhist_pos--; + show_step(pfhist[pfhist_pos]); + } + } + + void pffwd(){ + if(pfhist_pos < ((int)pfhist.size()) - 1){ + pfhist_pos++; + show_step(pfhist[pfhist_pos]); + } + } + + void pfprem(int i){ + if(pfhist.size() > 0){ + ast proof = pfhist[pfhist_pos]; + unsigned nprems = num_prems(proof); + if(i >= 0 && i < (int)nprems) + pfgoto(prem(proof,i)); + } + } + + + + // translate a unit resolution sequence + Iproof::node translate_ur(ast proof){ + ast prem0 = prem(proof,0); + Iproof::node itp = translate_main(prem0,true); + std::vector clause; + get_Z3_lits(conc(prem0),clause); + int nprems = num_prems(proof); + for(int position = 1; position < nprems; position++){ + ast ante = prem(proof,position); + ast pnode = conc(ante); + ast pnode_abs = !is_not(pnode) ? pnode : mk_not(pnode); + Iproof::node neg = itp; + Iproof::node pos = translate_main(ante, false); + if(is_not(pnode)){ + pnode = mk_not(pnode); + std::swap(neg,pos); + } + std::vector unit(1); + unit[0] = conc(ante); + resolve(mk_not(conc(ante)),clause,unit); + itp = iproof->make_resolution(pnode,clause,neg,pos); + } + return itp; + } + + // get an inequality in the form 0 <= t where t is a linear term + ast rhs_normalize_inequality(const ast &ineq){ + ast zero = make_int("0"); + ast thing = make(Leq,zero,zero); + linear_comb(thing,make_int("1"),ineq); + thing = simplify_ineq(thing); + return thing; + } + + // get an inequality in the form t <= c or t < c, there t is affine and c constant + ast normalize_inequality(const ast &ineq){ + ast zero = make_int("0"); + ast thing = make(Leq,zero,zero); + linear_comb(thing,make_int("1"),ineq); + thing = simplify_ineq(thing); + ast lhs = arg(thing,0); + ast rhs = arg(thing,1); + opr o = op(rhs); + if(o != Numeral){ + if(op(rhs) == Plus){ + int nargs = num_args(rhs); + ast const_term = zero; + int i = 0; + if(nargs > 0 && op(arg(rhs,0)) == Numeral){ + const_term = arg(rhs,0); + i++; + } + if(i < nargs){ + std::vector non_const; + for(; i < nargs; i++) + non_const.push_back(arg(rhs,i)); + lhs = make(Sub,lhs,make(Plus,non_const)); + } + rhs = const_term; + } + else { + lhs = make(Sub,lhs,make(Plus,rhs)); + rhs = zero; + } + lhs = z3_simplify(lhs); + rhs = z3_simplify(rhs); + thing = make(op(thing),lhs,rhs); + } + return thing; + } + + void get_linear_coefficients(const ast &t, std::vector &coeffs){ + if(op(t) == Plus){ + int nargs = num_args(t); + for(int i = 0; i < nargs; i++) + coeffs.push_back(get_coeff(arg(t,i))); + } + else + coeffs.push_back(get_coeff(t)); + } + + /* given an affine term t, get the GCD of the coefficients in t. */ + ast gcd_of_coefficients(const ast &t){ + std::vector coeffs; + get_linear_coefficients(t,coeffs); + if(coeffs.size() == 0) + return make_int("1"); // arbitrary + rational d = coeffs[0]; + for(unsigned i = 1; i < coeffs.size(); i++){ + d = gcd(d,coeffs[i]); + } + return make_int(d); + } + + Iproof::node GCDtoDivRule(const ast &proof, bool pol, std::vector &coeffs, std::vector &prems, ast &cut_con){ + // gather the summands of the desired polarity + std::vector my_prems; + std::vector my_coeffs; + std::vector my_prem_cons; + for(unsigned i = 0; i < coeffs.size(); i++){ + rational &c = coeffs[i]; + if(pol ? c.is_pos() : c.is_neg()){ + my_prems.push_back(prems[i]); + my_coeffs.push_back(pol ? make_int(c) : make_int(-c)); + my_prem_cons.push_back(conc(prem(proof,i))); + } + } + ast my_con = sum_inequalities(my_coeffs,my_prem_cons); + my_con = normalize_inequality(my_con); + Iproof::node hyp = iproof->make_hypothesis(mk_not(my_con)); + my_prems.push_back(hyp); + my_coeffs.push_back(make_int("1")); + my_prem_cons.push_back(mk_not(my_con)); + Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_prem_cons,my_coeffs); + + ast t = arg(my_con,0); + ast c = arg(my_con,1); + ast d = gcd_of_coefficients(t); + t = z3_simplify(mk_idiv(t,d)); + c = z3_simplify(mk_idiv(c,d)); + cut_con = make(op(my_con),t,c); + return iproof->make_cut_rule(my_con,d,cut_con,res); + } + + + ast divide_inequalities(const ast &x, const ast&y){ + std::vector xcoeffs,ycoeffs; + get_linear_coefficients(arg(x,1),xcoeffs); + get_linear_coefficients(arg(y,1),ycoeffs); + if(xcoeffs.size() != ycoeffs.size() || xcoeffs.size() == 0) + throw "bad assign-bounds lemma"; + rational ratio = xcoeffs[0]/ycoeffs[0]; + return make_int(ratio); // better be integer! + } + + ast AssignBounds2Farkas(const ast &proof, const ast &con){ + std::vector farkas_coeffs; + get_assign_bounds_coeffs(proof,farkas_coeffs); + std::vector lits; + int nargs = num_args(con); + if(nargs != (int)(farkas_coeffs.size())) + throw "bad assign-bounds theory lemma"; +#if 0 + for(int i = 1; i < nargs; i++) + lits.push_back(mk_not(arg(con,i))); + ast sum = sum_inequalities(farkas_coeffs,lits); + ast conseq = rhs_normalize_inequality(arg(con,0)); + ast d = divide_inequalities(sum,conseq); + std::vector my_coeffs; + my_coeffs.push_back(d); + for(unsigned i = 0; i < farkas_coeffs.size(); i++) + my_coeffs.push_back(farkas_coeffs[i]); +#else + std::vector &my_coeffs = farkas_coeffs; +#endif + std::vector my_cons; + for(int i = 0; i < nargs; i++) + my_cons.push_back(mk_not(arg(con,i))); + std::vector 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); + return res; + } + + // translate a Z3 proof term into interpolating proof system + + Iproof::node translate_main(ast proof, bool expect_clause = true){ + AstToIpf &tr = translation; + hash_map &trc = expect_clause ? tr.first : tr.second; + std::pair foo(proof,Iproof::node()); + std::pair::iterator, bool> bar = trc.insert(foo); + Iproof::node &res = bar.first->second; + if(!bar.second) return res; + + // Try the locality rule first + + int frame = get_locality(proof); + if(frame != -1){ + ast e = from_ast(conc(proof)); + if(frame >= frames) frame = frames - 1; + std::vector foo; + if(expect_clause) + get_Z3_lits(conc(proof),foo); + else + foo.push_back(e); + AstSet &hyps = get_hyps(proof); + for(AstSet::iterator it = hyps.begin(), en = hyps.end(); it != en; ++it) + foo.push_back(mk_not(*it)); + res = iproof->make_assumption(frame,foo); + return res; + } + + // If the proof is not local, break it down by proof rule + + pfrule dk = pr(proof); + unsigned nprems = num_prems(proof); + if(dk == PR_UNIT_RESOLUTION){ + res = translate_ur(proof); + } + else if(dk == PR_LEMMA){ + ast contra = prem(proof,0); // this is a proof of false from some hyps + res = translate_main(contra); + if(!expect_clause){ + std::vector foo; // the negations of the hyps form a clause + foo.push_back(from_ast(conc(proof))); + AstSet &hyps = get_hyps(proof); + for(AstSet::iterator it = hyps.begin(), en = hyps.end(); it != en; ++it) + foo.push_back(mk_not(*it)); + res = iproof->make_contra(res,foo); + } + } + else { + std::vector lits; + ast con = conc(proof); + if(expect_clause) + get_Z3_lits(con, lits); + else + lits.push_back(from_ast(con)); + + // translate all the premises + std::vector args(nprems); + for(unsigned i = 0; i < nprems; i++) + args[i] = translate_main(prem(proof,i),false); + + switch(dk){ + case PR_TRANSITIVITY: { + // assume the premises are x = y, y = z + ast x = arg(conc(prem(proof,0)),0); + ast y = arg(conc(prem(proof,0)),1); + ast z = arg(conc(prem(proof,1)),1); + res = iproof->make_transitivity(x,y,z,args[0],args[1]); + break; + } + case PR_MONOTONICITY: { + // assume the premise is x = y + ast x = arg(conc(prem(proof,0)),0); + ast y = arg(conc(prem(proof,0)),1); + AstSet &hyps = get_hyps(proof); + std::vector 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]); + break; + } + case PR_REFLEXIVITY: { + res = iproof->make_reflexivity(con); + break; + } + case PR_SYMMETRY: { + res = iproof->make_symmetry(con,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]); + break; + } + case PR_TH_LEMMA: { + switch(get_theory_lemma_theory(proof)){ + case ArithTheory: + switch(get_theory_lemma_kind(proof)){ + case FarkasKind: { + std::vector farkas_coeffs, prem_cons; + get_farkas_coeffs(proof,farkas_coeffs); + prem_cons.resize(nprems); + for(unsigned i = 0; i < nprems; i++) + prem_cons[i] = conc(prem(proof,i)); + res = iproof->make_farkas(con,args,prem_cons,farkas_coeffs); + break; + } + case Leq2EqKind: { + // conc should be (or x = y (not (leq x y)) (not(leq y z)) ) + ast xeqy = arg(conc(proof),0); + ast x = arg(xeqy,0); + ast y = arg(xeqy,1); + res = iproof->make_leq2eq(x,y,arg(arg(conc(proof),1),0),arg(arg(conc(proof),2),0)); + break; + } + case Eq2LeqKind: { + // conc should be (or (not (= x y)) (leq x y)) + ast xeqy = arg(arg(conc(proof),0),0); + ast xleqy = arg(conc(proof),1); + ast x = arg(xeqy,0); + ast y = arg(xeqy,1); + res = iproof->make_eq2leq(x,y,xleqy); + break; + } + case GCDTestKind: { + std::vector farkas_coeffs; + get_farkas_coeffs(proof,farkas_coeffs); + std::vector my_prems; my_prems.resize(2); + std::vector my_prem_cons; my_prem_cons.resize(2); + std::vector my_farkas_coeffs; my_farkas_coeffs.resize(2); + my_prems[0] = GCDtoDivRule(proof, true, farkas_coeffs, args, my_prem_cons[0]); + my_prems[1] = GCDtoDivRule(proof, false, farkas_coeffs, args, my_prem_cons[1]); + ast con = mk_false(); + my_farkas_coeffs[0] = my_farkas_coeffs[1] = make_int("1"); + res = iproof->make_farkas(con,my_prems,my_prem_cons,my_farkas_coeffs); + break; + } + case AssignBoundsKind: { + res = AssignBounds2Farkas(proof,conc(proof)); + break; + } + default: + throw unsupported(); + } + break; + default: + throw unsupported(); + } + break; + } + case PR_HYPOTHESIS: { + res = iproof->make_hypothesis(conc(proof)); + break; + } + default: + assert(0 && "translate_main: unsupported proof rule"); + throw unsupported(); + } + } + + return res; + } + + // We actually compute the interpolant here and then produce a proof consisting of just a lemma + + iz3proof::node translate(ast proof, iz3proof &dst){ + std::vector itps; + for(int i = 0; i < frames -1; i++){ + iproof = iz3proof_itp::create(this,range_downward(i),weak_mode()); + ast itp = translate_main(proof); + itps.push_back(itp); + delete iproof; + } + // Very simple proof -- lemma of the empty clause with computed interpolation + iz3proof::node Ipf = dst.make_lemma(std::vector(),itps); // builds result in dst + return Ipf; + } + + iz3translation_full(iz3mgr &mgr, + iz3secondary *_secondary, + const std::vector &cnsts, + const std::vector &parents, + const std::vector &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(); + } + + ~iz3translation_full(){ + } +}; + + + + +#ifdef IZ3_TRANSLATE_FULL + +iz3translation *iz3translation::create(iz3mgr &mgr, + iz3secondary *secondary, + const std::vector &cnsts, + const std::vector &parents, + const std::vector &theory){ + return new iz3translation_full(mgr,secondary,cnsts,parents,theory); +} + + +#if 1 + +// This is just to make sure certain methods are compiled, so we can call then from the debugger. + +void iz3translation_full_trace_lit(iz3translation_full *p, iz3mgr::ast lit, iz3mgr::ast proof){ + p->trace_lit(lit, proof); +} + +void iz3translation_full_show_step(iz3translation_full *p, iz3mgr::ast proof){ + p->show_step(proof); +} + +void iz3translation_full_show_marked(iz3translation_full *p, iz3mgr::ast proof){ + p->show_marked(proof); +} + +void iz3translation_full_show_lit(iz3translation_full *p, iz3mgr::ast lit){ + p->show_lit(lit); +} + +void iz3translation_full_show_z3_lit(iz3translation_full *p, iz3mgr::ast a){ + p->show_z3_lit(a); +} + +void iz3translation_full_pfgoto(iz3translation_full *p, iz3mgr::ast proof){ + p->pfgoto(proof); +} + + +void iz3translation_full_pfback(iz3translation_full *p ){ + p->pfback(); +} + +void iz3translation_full_pffwd(iz3translation_full *p ){ + p->pffwd(); +} + +void iz3translation_full_pfprem(iz3translation_full *p, int i){ + p->pfprem(i); +} + + +struct stdio_fixer { + stdio_fixer(){ + std::cout.rdbuf()->pubsetbuf(0,0); + } + +} my_stdio_fixer; + +#endif + +#endif + + diff --git a/src/interp/iz3translate.h b/src/interp/iz3translate.h index 40dc6a165..6663f406b 100755 --- a/src/interp/iz3translate.h +++ b/src/interp/iz3translate.h @@ -34,6 +34,10 @@ public: virtual ast quantify(ast e, const range &rng){return e;} virtual ~iz3translation(){} + /** This is thrown when the proof cannot be translated. */ + struct unsupported { + }; + static iz3translation *create(iz3mgr &mgr, iz3secondary *secondary, const std::vector &frames, @@ -50,6 +54,7 @@ public: //#define IZ3_TRANSLATE_DIRECT2 #define IZ3_TRANSLATE_DIRECT +// #define IZ3_TRANSLATE_FULL #endif