From 9792f6dd33f51bf6d8e4a2cdd81e5b5c75d3ebd4 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 4 Mar 2013 18:41:30 -0800 Subject: [PATCH] more work on incorporating iz3 --- src/api/api_interp.cpp | 201 ++++ src/api/z3_api.h | 122 ++ src/interp/iz3base.cpp | 9 +- src/interp/iz3base.h | 16 + src/interp/iz3interp.cpp | 256 ++++ src/interp/iz3interp.h | 40 + src/interp/iz3mgr.cpp | 9 +- src/interp/iz3mgr.h | 25 +- src/interp/iz3scopes.cpp | 2 +- src/interp/iz3translate.h | 57 + src/interp/iz3translate_direct.cpp | 1797 ++++++++++++++++++++++++++++ 11 files changed, 2527 insertions(+), 7 deletions(-) create mode 100644 src/api/api_interp.cpp create mode 100755 src/interp/iz3interp.cpp create mode 100644 src/interp/iz3interp.h create mode 100755 src/interp/iz3translate.h create mode 100755 src/interp/iz3translate_direct.cpp diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp new file mode 100644 index 000000000..2768e97e3 --- /dev/null +++ b/src/api/api_interp.cpp @@ -0,0 +1,201 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + api_interp.cpp + +Abstract: + API for interpolation + +Author: + + Ken McMillan + +Revision History: + +--*/ +#include +#include"z3.h" +#include"api_log_macros.h" +#include"api_context.h" +#include"api_tactic.h" +#include"api_solver.h" +#include"api_model.h" +#include"api_stats.h" +#include"api_ast_vector.h" +#include"tactic2solver.h" +#include"scoped_ctrl_c.h" +#include"cancel_eh.h" +#include"scoped_timer.h" +#include"smt_strategic_solver.h" +#include"smt_solver.h" +#include"smt_implied_equalities.h" +#include"iz3interp.h" +#include"iz3profiling.h" + +typedef interpolation_options_struct *Z3_interpolation_options; + +extern "C" { + + Z3_context Z3_mk_interpolation_context(Z3_config cfg){ + if(!cfg) cfg = Z3_mk_config(); + Z3_set_param_value(cfg, "PROOF_MODE", "2"); + Z3_set_param_value(cfg, "MODEL", "true"); + Z3_set_param_value(cfg, "PRE_SIMPLIFIER","false"); + Z3_set_param_value(cfg, "SIMPLIFY_CLAUSES","false"); + + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + return ctx; + } + + void Z3_interpolate_proof(Z3_context ctx, + Z3_ast proof, + int num, + Z3_ast *cnsts, + int *parents, + Z3_interpolation_options options, + Z3_ast *interps, + int num_theory, + Z3_ast *theory + ){ + + if(num > 1){ // if we have interpolants to compute + + ptr_vector pre_cnsts_vec(num); // get constraints in a vector + for(int i = 0; i < num; i++){ + ast *a = to_ast(cnsts[i]); + pre_cnsts_vec[i] = a; + } + + vector pre_parents_vec; // get parents in a vector + if(parents){ + pre_parents_vec.resize(num); + for(int i = 0; i < num; i++) + pre_parents_vec[i] = parents[i]; + } + + ptr_vector theory_vec; // get background theory in a vector + if(theory){ + theory_vec.resize(num_theory); + for(int i = 0; i < num_theory; i++) + theory_vec[i] = to_ast(theory[i]); + } + + ptr_vector interpolants(num-1); // make space for result + + scoped_ptr _m(&mk_c(ctx)->m()); + iz3interpolate(_m, + to_ast(proof), + pre_cnsts_vec, + pre_parents_vec, + interpolants, + theory_vec, + (interpolation_options) options); + + // copy result back + for(unsigned i = 0; i < interpolants.size(); i++) + interps[i] = of_ast(interpolants[i]); + } + + } + + Z3_lbool Z3_interpolate(Z3_context ctx, + int num, + Z3_ast *cnsts, + int *parents, + Z3_interpolation_options options, + Z3_ast *interps, + Z3_model *model, + Z3_literals *labels, + bool incremental, + int num_theory, + Z3_ast *theory + ){ + + + if(!incremental){ + + profiling::timer_start("Z3 assert"); + + Z3_push(ctx); // so we can rewind later + + for(int i = 0; i < num; i++) + Z3_assert_cnstr(ctx,cnsts[i]); // assert all the constraints + + if(theory){ + for(int i = 0; i < num_theory; i++) + Z3_assert_cnstr(ctx,theory[i]); + } + + profiling::timer_stop("Z3 assert"); + } + + + // Get a proof of unsat + + Z3_ast proof; + Z3_lbool result; + + profiling::timer_start("Z3 solving"); + result = Z3_check_assumptions(ctx, 0, 0, model, &proof, 0, 0); + profiling::timer_stop("Z3 solving"); + + switch (result) { + case Z3_L_FALSE: + + Z3_interpolate_proof(ctx, + proof, + num, + cnsts, + parents, + options, + interps, + num_theory, + theory); + break; + + case Z3_L_UNDEF: + if(labels) + *labels = Z3_get_relevant_labels(ctx); + break; + + case Z3_L_TRUE: + if(labels) + *labels = Z3_get_relevant_labels(ctx); + break; + } + + return result; + + } + + static std::string Z3_profile_string; + + Z3_string Z3_interpolation_profile(Z3_context ctx){ + std::ostringstream f; + profiling::print(f); + Z3_profile_string = f.str(); + return Z3_profile_string.c_str(); + } + + + Z3_interpolation_options + Z3_mk_interpolation_options(){ + return (Z3_interpolation_options) new interpolation_options_struct; + } + + void + Z3_del_interpolation_options(Z3_interpolation_options opts){ + delete opts; + } + + void + Z3_set_interpolation_option(Z3_interpolation_options opts, + Z3_string name, + Z3_string value){ + opts->map[name] = value; + } + +}; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ea3b05e40..12db470fd 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -7660,6 +7660,128 @@ END_MLAPI_EXCLUDE /*@}*/ + /** + @name Interpolation + */ + /*@{*/ + + /** \brief This function generates a Z3 context suitable for generation of + interpolants. Formulas can be generated as abstract syntx trees in + this context using the Z3 C API. + + Interpolants are also generated as AST's in this context. + + If cfg is non-null, it will be used as the base configuration + for the Z3 context. This makes it possible to set Z3 options + to be used during interpolation. This feature should be used + with some caution however, as it may be that certain Z3 options + are incompatible with interpolation. + + def_API('Z3_mk_interpolation_context', CONTEXT, (_in(CONFIG),)) + + */ + + Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg); + + +/** Constant reprepresenting a root of a formula tree for tree interpolation */ +#define IZ3_ROOT SHRT_MAX + +/** This function uses Z3 to determine satisfiability of a set of + constraints. If UNSAT, an interpolant is returned, based on the + refutation generated by Z3. If SAT, a model is returned. + + If "parents" is non-null, computes a tree interpolant. The tree is + defined by the array "parents". This array maps each formula in + the tree to its parent, where formulas are indicated by their + integer index in "cnsts". The parent of formula n must have index + greater than n. The last formula is the root of the tree. Its + parent entry should be the constant IZ3_ROOT. + + If "parents" is null, computes a sequence interpolant. + + \param ctx The Z3 context. Must be generated by iz3_mk_context + \param num The number of constraints in the sequence + \param cnsts Array of constraints (AST's in context ctx) + \param parents The parents vector defining the tree structure + \param options Interpolation options (may be NULL) + \param interps Array to return interpolants (size at least num-1, may be NULL) + \param model Returns a Z3 model if constraints SAT (may be NULL) + \param labels Returns relevant labels if SAT (may be NULL) + \param incremental + + VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3 + context ctx. The model and interpolants returned are also + in this context. + + The return code is as in Z3_check_assumptions, that is, + + Z3_L_FALSE = constraints UNSAT (interpolants returned) + Z3_L_TRUE = constraints SAT (model returned) + Z3_L_UNDEF = Z3 produced no result, or interpolation not possible + + Currently, this function supports integer and boolean variables, + as well as arrays over these types, with linear arithmetic, + uninterpreted functions and quantifiers over integers (that is + AUFLIA). Interpolants are produced in AUFLIA. However, some + uses of array operations may cause quantifiers to appear in the + interpolants even when there are no quantifiers in the input formulas. + Although quantifiers may appear in the input formulas, Z3 may give up in + this case, returning Z3_L_UNDEF. + + If "incremental" is true, cnsts must contain exactly the set of + formulas that are currently asserted in the context. If false, + there must be no formulas currently asserted in the context. + Setting "incremental" to true makes it posisble to incrementally + add and remove constraints from the context until the context + becomes UNSAT, at which point an interpolant is computed. Caution + must be used, however. Before popping the context, if you wish to + keep the interolant formulas, you *must* preserve them by using + Z3_persist_ast. Also, if you want to simplify the interpolant + formulas using Z3_simplify, you must first pop all of the + assertions in the context (or use a different context). Otherwise, + the formulas will be simplified *relative* to these constraints, + which is almost certainly not what you want. + + + Current limitations on tree interpolants. In a tree interpolation + problem, each constant (0-ary function symbol) must occur only + along one path from root to leaf. Function symbols (of arity > 0) + are considered to have global scope (i.e., may appear in any + interpolant formula). + + def_API('Z3_interpolate', LBOOL, (_in(CONTEXT),), (_in(INT),), (_in_ptr(AST),), + (_in_ptr(INT),), (_in(PARAMS),), (_in_ptr(AST),), + (_out(MODEL),), (_out(LITERALS),), (_in(BOOL),), (_in(INT),), (_in_ptr(AST,0),)) + + */ + + + Z3_lbool Z3_API Z3_interpolate(Z3_context ctx, + int num, + Z3_ast *cnsts, + int *parents, + Z3_interpolation_options options, + Z3_ast *interps, + Z3_model *model = 0, + Z3_literals *labels = 0, + bool incremental = false, + int num_theory = 0, + Z3_ast *theory = 0); + + /** Return a string summarizing cumulative time used for + interpolation. This string is purely for entertainment purposes + and has no semantics. + + \param ctx The context (currently ignored) + + def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),)) + */ + + Z3_string Z3_API Z3_interpolation_profile(Z3_context ctx); + + + #endif diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index d3b469462..296688086 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -193,13 +193,14 @@ iz3base::ast iz3base::simplify(ast n){ return res; } -void iz3base::initialize(const std::vector &_parts, const std::vector &_parents, const std::vector &theory){ +void iz3base::initialize(const std::vector &_parts, const std::vector &_parents, const std::vector &_theory){ cnsts = _parts; + theory = _theory; for(unsigned i = 0; i < cnsts.size(); i++) add_frame_range(i, cnsts[i]); - for(unsigned i = 0; i < theory.size(); i++){ - add_frame_range(SHRT_MIN, theory[i]); - add_frame_range(SHRT_MAX, theory[i]); + for(unsigned i = 0; i < _theory.size(); i++){ + add_frame_range(SHRT_MIN, _theory[i]); + add_frame_range(SHRT_MAX, _theory[i]); } } diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index 4209f3c67..8a8ad332a 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -65,6 +65,15 @@ class iz3base : public iz3mgr, public scopes { weak = false; } + iz3base(const iz3mgr& other, + const std::vector &_cnsts, + const std::vector &_parents, + const std::vector &_theory) + : iz3mgr(other), scopes(_parents) { + initialize(_cnsts,_parents,_theory); + weak = false; + } + /* Set our options */ void set_option(const std::string &name, const std::string &value){ if(name == "weak" && value == "1") weak = true; @@ -87,6 +96,12 @@ class iz3base : public iz3mgr, public scopes { throw "no interpolator"; } + ast get_proof_check_assump(range &rng){ + std::vector cs(theory); + cs.push_back(cnsts[rng.hi]); + return make(And,cs); + } + private: struct ranges { @@ -106,6 +121,7 @@ class iz3base : public iz3mgr, public scopes { void initialize(const std::vector &_parts, const std::vector &_parents, const std::vector &_theory); std::vector cnsts; + std::vector theory; bool is_literal(ast n); void gather_conjuncts_rec(ast n, std::vector &conjuncts, stl_ext::hash_set &memo); diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp new file mode 100755 index 000000000..15bdf0c22 --- /dev/null +++ b/src/interp/iz3interp.cpp @@ -0,0 +1,256 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3interp.cpp + +Abstract: + + Interpolation based on proof translation. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + +/* Copyright 2011 Microsoft Research. */ +#include +#include +#include +#include +#include +#include +#include + +#include "iz3profiling.h" +#include "iz3translate.h" +#include "iz3foci.h" +#include "iz3proof.h" +#include "iz3hash.h" +#include "iz3interp.h" + + +#ifndef WIN32 +using namespace stl_ext; +#endif + + + +#if 1 + +struct frame_reducer : public iz3mgr { + + int frames; + hash_map frame_map; + std::vector assertions_map; + std::vector orig_parents_copy; + std::vector used_frames; + + + frame_reducer(const iz3mgr &other) + : iz3mgr(other) {} + + void get_proof_assumptions_rec(z3pf proof, hash_set &memo, std::vector &used_frames){ + if(memo.count(proof))return; + memo.insert(proof); + pfrule dk = pr(proof); + if(dk == PR_ASSERTED){ + ast con = conc(proof); + if(frame_map.find(con) != frame_map.end()){ // false for theory facts + int frame = frame_map[con]; + used_frames[frame] = true; + } + } + else { + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++){ + z3pf arg = prem(proof,i); + get_proof_assumptions_rec(arg,memo,used_frames); + } + } + } + + void get_frames(const std::vector &z3_preds, + const std::vector &orig_parents, + std::vector &assertions, + std::vector &parents, + z3pf proof){ + frames = z3_preds.size(); + orig_parents_copy = orig_parents; + for(unsigned i = 0; i < z3_preds.size(); i++) + frame_map[z3_preds[i]] = i; + used_frames.resize(frames); + hash_set memo; + get_proof_assumptions_rec(proof,memo,used_frames); + std::vector assertions_back_map(frames); + + for(unsigned i = 0; i < z3_preds.size(); i++) + if(used_frames[i] || i == z3_preds.size() - 1){ + assertions.push_back(z3_preds[i]); + assertions_map.push_back(i); + assertions_back_map[i] = assertions.size() - 1; + } + + if(orig_parents.size()){ + parents.resize(assertions.size()); + for(unsigned i = 0; i < assertions.size(); i++){ + int p = orig_parents[assertions_map[i]]; + while(p != SHRT_MAX && !used_frames[p]) + p = orig_parents[p]; + parents[i] = p == SHRT_MAX ? p : assertions_back_map[p]; + } + } + + // std::cout << "used frames = " << frames << "\n"; + } + + void fix_interpolants(std::vector &interpolants){ + std::vector unfixed = interpolants; + interpolants.resize(frames - 1); + for(int i = 0; i < frames - 1; i++) + interpolants[i] = mk_true(); + for(unsigned i = 0; i < unfixed.size(); i++) + interpolants[assertions_map[i]] = unfixed[i]; + for(int i = 0; i < frames-2; i++){ + int p = orig_parents_copy.size() == 0 ? i+1 : orig_parents_copy[i]; + if(p < frames - 1 && !used_frames[p]) + interpolants[p] = interpolants[i]; + } + } +}; + +#else +struct frame_reducer { + + + + frame_reducer(context _ctx){ + } + + void get_frames(const std::vector &z3_preds, + const std::vector &orig_parents, + std::vector &assertions, + std::vector &parents, + ast proof){ + assertions = z3_preds; + parents = orig_parents; + } + + void fix_interpolants(std::vector &interpolants){ + } +}; + +#endif + + +#if 0 +static lbool test_secondary(context ctx, + int num, + ast *cnsts, + ast *interps, + int *parents = 0 + ){ + iz3secondary *sp = iz3foci::create(ctx,num,parents); + std::vector frames(num), interpolants(num-1); + std::copy(cnsts,cnsts+num,frames.begin()); + int res = sp->interpolate(frames,interpolants); + if(res == 0) + std::copy(interpolants.begin(),interpolants.end(),interps); + return res ? L_TRUE : L_FALSE; +} +#endif + + +class iz3interp : public iz3mgr { +public: + void proof_to_interpolant(z3pf proof, + const std::vector &cnsts, + const std::vector &parents, + std::vector &interps, + const std::vector &theory, + interpolation_options_struct *options = 0 + ){ + + profiling::timer_start("Interpolation prep"); + + // get rid of frames not used in proof + + std::vector cnsts_vec; + std::vector parents_vec; + frame_reducer fr(*this); + fr.get_frames(cnsts,parents,cnsts_vec,parents_vec,proof); + + int num = cnsts_vec.size(); + std::vector interps_vec(num-1); + + // create a secondary prover + iz3secondary *sp = iz3foci::create(this,num,parents_vec.empty()?0:&parents_vec[0]); + + // create a translator + iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory); + + // set the translation options, if needed + if(options) + for(hash_map::iterator it = options->map.begin(), en = options->map.end(); it != en; ++it) + tr->set_option(it->first, it->second); + + // create a proof object to hold the translation + iz3proof pf(tr); + + profiling::timer_stop("Interpolation prep"); + + // translate into an interpolatable proof + profiling::timer_start("Proof translation"); + tr->translate(proof,pf); + profiling::timer_stop("Proof translation"); + + // translate the proof into interpolants + profiling::timer_start("Proof interpolation"); + for(int i = 0; i < num-1; i++){ + interps_vec[i] = pf.interpolate(tr->range_downward(i),tr->weak_mode()); + interps_vec[i] = tr->quantify(interps_vec[i],tr->range_downward(i)); + } + profiling::timer_stop("Proof interpolation"); + + // put back in the removed frames + fr.fix_interpolants(interps_vec); + + interps = interps_vec; + delete tr; + delete sp; + } + + iz3interp(scoped_ptr &_m_manager) + : iz3mgr(_m_manager) {} +}; + +void iz3interpolate(scoped_ptr &_m_manager, + ast *proof, + const ptr_vector &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector theory, + interpolation_options_struct * options) +{ + std::vector _cnsts(cnsts.size()); + std::vector _parents(parents.size()); + std::vector _interps; + std::vector _theory(theory.size()); + for(unsigned i = 0; i < cnsts.size(); i++) + _cnsts[i] = cnsts[i]; + for(unsigned i = 0; i < parents.size(); i++) + _parents[i] = parents[i]; + for(unsigned i = 0; i < theory.size(); i++) + _theory[i] = theory[i]; + ast_r _proof(proof); + iz3interp itp(_m_manager); + itp.proof_to_interpolant(_proof,_cnsts,_parents,_interps,_theory,options); + interps.resize(_interps.size()); + for(unsigned i = 0; i < interps.size(); i++) + _interps[i] = interps[i]; +} + diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h new file mode 100644 index 000000000..4e76b74fd --- /dev/null +++ b/src/interp/iz3interp.h @@ -0,0 +1,40 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3interp.h + +Abstract: + + Interpolation based on proof translation. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + +#ifndef IZ3_INTERP_H +#define IZ3_INTERP_H + +#include "iz3hash.h" + +struct interpolation_options_struct { + stl_ext::hash_map map; +}; + + +typedef interpolation_options_struct *interpolation_options; + +void iz3interpolate(scoped_ptr &_m_manager, + ast *proof, + const ptr_vector &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector theory, + interpolation_options_struct * options = 0); + +#endif diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index b1f07f5ce..741b26478 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -65,7 +65,7 @@ iz3mgr::ast iz3mgr::make(opr op, ast &arg0){ return make(op,1,&a); } -iz3mgr::ast iz3mgr::make(opr op, ast &arg0, ast &arg1){ +iz3mgr::ast iz3mgr::make(opr op, const ast &arg0, const ast &arg1){ raw_ast *args[2]; args[0] = arg0.raw(); args[1] = arg1.raw(); @@ -367,3 +367,10 @@ iz3mgr::opr iz3mgr::op(ast &t){ } return Other; } + + +iz3mgr::pfrule iz3mgr::pr(const ast &t){ + func_decl *d = to_app(t.raw())->get_decl(); + assert(m_basic_fid == d->get_family_id()); + return d->get_decl_kind(); +} diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 32ec25d70..efcbb0d6f 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -63,9 +63,20 @@ class ast_r { bool eq(const ast_r &other) const { return _ast == other._ast; } + bool lt(const ast_r &other) const { + return _ast < other._ast; + } friend bool operator==(const ast_r &x, const ast_r&y){ return x.eq(y); } + friend bool operator!=(const ast_r &x, const ast_r&y){ + return !x.eq(y); + } + friend bool operator<(const ast_r &x, const ast_r&y){ + return x.lt(y); + } + size_t hash() const {return (size_t)_ast;} + bool null() const {return !_ast;} }; @@ -101,6 +112,8 @@ class iz3mgr { // typedef decl_kind opr; typedef func_decl *symb; typedef sort *type; + typedef ast_r z3pf; + typedef decl_kind pfrule; enum opr { True, @@ -163,7 +176,7 @@ class iz3mgr { ast make(opr op, const std::vector &args); ast make(opr op); ast make(opr op, ast &arg0); - ast make(opr op, ast &arg0, ast &arg1); + ast make(opr op, const ast &arg0, const ast &arg1); ast make(opr op, ast &arg0, ast &arg1, ast &arg2); ast make(symb sym, const std::vector &args); ast make(symb sym); @@ -354,6 +367,16 @@ class iz3mgr { ast mk_true() { return make(True); } + /** methods for destructing proof terms */ + + pfrule pr(const z3pf &t); + + int num_prems(const z3pf &t){return to_app(t.raw())->get_num_args()-1;} + + z3pf prem(const z3pf &t, int n){return arg(t,n);} + + z3pf conc(const z3pf &t){return arg(t,num_prems(t));} + /** For debugging */ void show(ast); diff --git a/src/interp/iz3scopes.cpp b/src/interp/iz3scopes.cpp index 90ff3b829..382779be0 100755 --- a/src/interp/iz3scopes.cpp +++ b/src/interp/iz3scopes.cpp @@ -31,7 +31,7 @@ int scopes::tree_lca(int n1, int n2){ if(n1 == SHRT_MAX || n2 == SHRT_MAX) return SHRT_MAX; while(n1 != n2){ if(n1 == SHRT_MAX || n2 == SHRT_MAX) return SHRT_MAX; - assert(n1 >= 0 && n2 >= 0 && n1 < parents.size() && n2 < parents.size()); + assert(n1 >= 0 && n2 >= 0 && n1 < (int)parents.size() && n2 < (int)parents.size()); if(n1 < n2) n1 = parents[n1]; else n2 = parents[n2]; } diff --git a/src/interp/iz3translate.h b/src/interp/iz3translate.h new file mode 100755 index 000000000..40dc6a165 --- /dev/null +++ b/src/interp/iz3translate.h @@ -0,0 +1,57 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3translate.h + +Abstract: + + Interface for proof translations from Z3 proofs to interpolatable + proofs. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + + +#ifndef IZ3TRANSLATION_H +#define IZ3TRANSLATION_H + +#include "iz3proof.h" +#include "iz3secondary.h" + +// This is a interface class for translation from Z3 proof terms to +// an interpolatable proof + +class iz3translation : public iz3base { +public: + virtual iz3proof::node translate(ast, iz3proof &) = 0; + virtual ast quantify(ast e, const range &rng){return e;} + virtual ~iz3translation(){} + + static iz3translation *create(iz3mgr &mgr, + iz3secondary *secondary, + const std::vector &frames, + const std::vector &parents, + const std::vector &theory); + + protected: + iz3translation(iz3mgr &mgr, + const std::vector &_cnsts, + const std::vector &_parents, + const std::vector &_theory) + : iz3base(mgr,_cnsts,_parents,_theory) {} +}; + +//#define IZ3_TRANSLATE_DIRECT2 +#define IZ3_TRANSLATE_DIRECT + +#endif + + + diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp new file mode 100755 index 000000000..0500d88ab --- /dev/null +++ b/src/interp/iz3translate_direct.cpp @@ -0,0 +1,1797 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3translate_direct.cpp + +Abstract: + + Translate a Z3 proof into the interpolating proof calculus. + Translation is direct, without transformations on the target proof + representaiton. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + +#include "iz3translate.h" +#include "iz3proof.h" +#include "iz3profiling.h" + +#include +#include +#include +#include +#include +#include +#include + +//using std::vector; +#ifndef WIN32 +using namespace stl_ext; +#endif + + +static int lemma_count = 0; +#define SHOW_LEMMA_COUNT -1 + +// One half of a resolution. We need this to distinguish +// between resolving as a clause and as a unit clause. +// if pivot == conclusion(proof) it is unit. + +struct Z3_resolvent { + iz3base::ast proof; + bool is_unit; + iz3base::ast pivot; + Z3_resolvent(const iz3base::ast &_proof, bool _is_unit, const iz3base::ast &_pivot){ + proof = _proof; + is_unit = _is_unit; + pivot = _pivot; + } +}; + +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const Z3_resolvent &p) const { + return (p.proof.hash() + p.pivot.hash()); + } + }; +} + +#ifdef WIN32 + +template <> inline +size_t stdext::hash_value(const Z3_resolvent& p) +{ + std::hash h; + return h(p); +} + + +namespace std { + template <> + class less { + public: + bool operator()(const Z3_resolvent &x, const Z3_resolvent &y) const { + size_t ixproof = (size_t) x.proof; + size_t iyproof = (size_t) y.proof; + if(ixproof < iyproof) return true; + if(ixproof > iyproof) return false; + return x.pivot < y.pivot; + } + }; +} + +#else + +bool operator==(const Z3_resolvent &x, const Z3_resolvent &y) { + return x.proof == y.proof && x.pivot == y.pivot; +} + + +#endif + +typedef std::vector ResolventAppSet; + +struct non_local_lits { + ResolventAppSet proofs; // the proof nodes being raised + non_local_lits(ResolventAppSet &_proofs){ + proofs.swap(_proofs); + } +}; + +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const non_local_lits &p) const { + size_t h = 0; + for(ResolventAppSet::const_iterator it = p.proofs.begin(), en = p.proofs.end(); it != en; ++it) + h += (size_t)*it; + return h; + } + }; +} + +#ifdef WIN32 + +template <> inline +size_t stdext::hash_value(const non_local_lits& p) +{ + std::hash h; + return h(p); +} + +namespace std { + template <> + class less { + public: + bool operator()(const non_local_lits &x, const non_local_lits &y) const { + ResolventAppSet::const_iterator itx = x.proofs.begin(); + ResolventAppSet::const_iterator ity = y.proofs.begin(); + while(true){ + if(ity == y.proofs.end()) return false; + if(itx == x.proofs.end()) return true; + size_t xi = (size_t) *itx; + size_t yi = (size_t) *ity; + if(xi < yi) return true; + if(xi > yi) return false; + ++itx; ++ity; + } + } + }; +} + +#else + +bool operator==(const non_local_lits &x, const non_local_lits &y) { + ResolventAppSet::const_iterator itx = x.proofs.begin(); + ResolventAppSet::const_iterator ity = y.proofs.begin(); + while(true){ + if(ity == y.proofs.end()) return itx == x.proofs.end(); + if(itx == x.proofs.end()) return ity == y.proofs.end(); + if(*itx != *ity) return false; + ++itx; ++ity; + } +} + + +#endif + +/* This translator goes directly from Z3 proofs to interpolatable + proofs without an intermediate representation as an iz3proof. */ + +class iz3translation_direct : public iz3translation { +public: + + typedef ast Zproof; // type of non-interpolating proofs + typedef iz3proof Iproof; // type of interpolating proofs + + /* 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 std::pair, hash_map > AstToIpf; + AstToIpf translation; // Zproof nodes to Iproof nodes + + AstHashSet antes_added; // Z3 proof terms whose antecedents have been added to the list + std::vector > antes; // list of antecedent/frame pairs + std::vector local_antes; // list of local antecedents + + Iproof *iproof; // the interpolating proof we are constructing + + 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 + + iz3secondary *secondary; // the secondary prover + + // Unique table for sets of non-local resolutions + hash_map non_local_lits_unique; + + // Unique table for resolvents + hash_map Z3_resolvent_unique; + + // Translation memo for case of non-local resolutions + hash_map non_local_translation; + + 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); + } + } + } + } + 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 as foci terms + 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 localise the arguments to + // the range of its function symbol + if(op(e) == Uninterpreted){ + symb f = sym(e); + range frng = sym_range(f); + int nargs = num_args(e); + if(nargs > 0 /* && (!is_local(e) || flo <= hi || fhi >= lo) */){ + if(ranges_intersect(frng,rng)) // localize to desired range if possible + {frng = range_glb(frng,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 = make(f,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)); + 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)); + 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; + } + + // add the premises of a proof term to the "antes" list + + void add_antes(ast proof){ + if(antes_added.find(proof) != antes_added.end()) return; + antes_added.insert(proof); + int frame = get_locality(proof); + if(frame != -1) + if(1){ + ast e = get_judgement(proof); + if(frame >= frames) frame = frames-1; // can happen if there are no symbols + antes.push_back(std::pair(e,frame)); + return; + } + pfrule dk = pr(proof); + if(dk == PR_ASSERTED){ + ast ass = conc(proof); + AstToInt::iterator it = frame_map.find(ass); + assert(it != frame_map.end()); + frame = it->second; + if(frame >= frames) frame = frames-1; // can happen if a theory fact + antes.push_back(std::pair(ass,frame)); + return; + } + if(dk == PR_TH_LEMMA && num_prems(proof) == 0){ + get_axiom_instance(conc(proof)); + } + if(dk == PR_QUANT_INST && num_prems(proof) == 0){ + get_quantifier_instance(conc(proof)); + } + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++){ + ast arg = prem(proof,i); + add_antes(arg); + } + } + + // 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)0; + 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)0); + 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; + } + + + struct invalid_lemma {}; + + + + + // prove a lemma (clause) using current antes list + // return proof of the lemma + // use the secondary prover + + int prove_lemma(std::vector &lits){ + + + // first try localization + if(antes.size() == 0){ + int local_frame = get_lits_locality(lits); + if(local_frame != -1) + return iproof->make_assumption(local_frame,lits); // no proof needed for purely local fact + } + + // group the assumptions by frame + std::vector preds(frames); + for(unsigned i = 0; i < preds.size(); i++) + preds[i] = mk_true(); + for(unsigned i = 0; i < antes.size(); i++){ + int frame = antes[i].second; + preds[frame] = mk_and(preds[frame],antes[i].first); // conjoin it to frame + } + + for(unsigned i = 0; i < lits.size(); i++){ + int frame; + if(!weak_mode()){ + frame = range_max(ast_scope(lits[i])); + if(frame >= frames) frame = frames-1; // could happen if contains no symbols + } + else { + frame = range_min(ast_scope(lits[i])); + if(frame < 0){ + frame = range_max(ast_scope(lits[i])); // could happen if contains no symbols + if(frame >= frames) frame = frames-1; + } + } + preds[frame] = mk_and(preds[frame],mk_not(lits[i])); + } + + + std::vector itps; // holds interpolants + + +#if 1 + // std::cout << "lemma: " << ++lemma_count << "\n"; + if(lemma_count == SHOW_LEMMA_COUNT){ + for(unsigned i = 0; i < lits.size(); i++) + show_lit(lits[i]); + std::cerr << "lemma written to file lemma.smt:\n"; + iz3base foo(*this,preds,std::vector(),std::vector()); + foo.print("lemma.smt"); + throw invalid_lemma(); + } +#endif + +#if 0 + std::cout << "\nLemma:\n"; + for(unsigned i = 0; i < lits.size(); i++) + show_lit(lits[i]); +#endif + + // interpolate using secondary prover + profiling::timer_start("foci"); + int sat = secondary->interpolate(preds,itps); + profiling::timer_stop("foci"); + + // if sat, lemma isn't valid, something is wrong + if(sat){ + std::cerr << "invalid lemma written to file invalid_lemma.smt:\n"; + iz3base foo(*this,preds,std::vector(),std::vector()); + foo.print("invalid_lemma.smt"); + throw invalid_lemma(); + } + assert(sat == 0); // if sat, lemma doesn't hold! + + // quantifiy the localization vars + for(unsigned i = 0; i < itps.size(); i++) + itps[i] = add_quants(itps[i],0,i); + + // Make a lemma, storing interpolants + Iproof::node res = iproof->make_lemma(lits,itps); + +#if 0 + std::cout << "Lemma interps\n"; + for(unsigned i = 0; i < itps.size(); i++) + show(itps[i]); +#endif + + // Reset state for the next lemma + antes.clear(); + antes_added.clear(); + clear_localization(); // use a fresh localization for each lemma + + return res; + } + + // sanity check: make sure that any non-local lit is really resolved + // with something in the non_local_lits set + + void check_non_local(ast lit, non_local_lits *nll){ + if(nll) + for(ResolventAppSet::iterator it = nll->proofs.begin(), en = nll->proofs.end(); it != en; ++it){ + ast con = (*it)->pivot; + if(con == mk_not(lit)) return; + } + assert(0 && "bug in non-local resolution handling"); + } + + + void get_local_conclusion_lits(ast proof, bool expect_clause, AstSet &lits){ + std::vector reslits; + if(expect_clause) + get_Z3_lits(conc(proof),reslits); + else reslits.push_back(conc(proof)); + for(unsigned i = 0; i < reslits.size(); i++) + if(is_local(reslits[i])) + lits.insert(reslits[i]); + AstSet &pfhyps = get_hyps(proof); + for(AstSet::iterator hit = pfhyps.begin(), hen = pfhyps.end(); hit != hen; ++hit) + if(is_local(*hit)) + lits.insert(mk_not(*hit)); + } + + + void collect_resolvent_lits(Z3_resolvent *res, const AstSet &hyps, std::vector &lits){ + if(!res->is_unit){ + std::vector reslits; + get_Z3_lits(conc(res->proof),reslits); + for(unsigned i = 0; i < reslits.size(); i++) + if(reslits[i] != res->pivot) + lits.push_back(reslits[i]); + } + AstSet &pfhyps = get_hyps(res->proof); + for(AstSet::iterator hit = pfhyps.begin(), hen = pfhyps.end(); hit != hen; ++hit) + if(hyps.find(*hit) == hyps.end()) + lits.push_back(mk_not(*hit)); + } + + void filter_resolvent_lits(non_local_lits *nll, std::vector &lits){ + std::vector orig_lits; orig_lits.swap(lits); + std::set pivs; + for(ResolventAppSet::iterator it = nll->proofs.begin(), en = nll->proofs.end(); it != en; ++it){ + Z3_resolvent *res = *it; + pivs.insert(res->pivot); + pivs.insert(mk_not(res->pivot)); + } + for(unsigned i = 0; i < orig_lits.size(); i++) + if(pivs.find(orig_lits[i]) == pivs.end()) + lits.push_back(orig_lits[i]); + } + + void collect_all_resolvent_lits(non_local_lits *nll, std::vector &lits){ + if(nll){ + std::vector orig_lits; orig_lits.swap(lits); + std::set pivs; + for(ResolventAppSet::iterator it = nll->proofs.begin(), en = nll->proofs.end(); it != en; ++it){ + Z3_resolvent *res = *it; + pivs.insert(res->pivot); + pivs.insert(mk_not(res->pivot)); + } + for(ResolventAppSet::iterator it = nll->proofs.begin(), en = nll->proofs.end(); it != en; ++it){ + Z3_resolvent *res = *it; + { + std::vector reslits; + if(!res->is_unit) get_Z3_lits(conc(res->proof),reslits); + else reslits.push_back(conc(res->proof)); + for(unsigned i = 0; i < reslits.size(); i++) +#if 0 + if(reslits[i] != res->pivot && pivs.find(reslits[i]) == pivs.end()) +#endif + if(is_local(reslits[i])) + lits.push_back(reslits[i]); + } + } + for(unsigned i = 0; i < orig_lits.size(); i++) + if(pivs.find(orig_lits[i]) == pivs.end()) + lits.push_back(orig_lits[i]); + } + } + + void collect_proof_clause(ast proof, bool expect_clause, std::vector &lits){ + if(expect_clause) + get_Z3_lits(conc(proof),lits); + else + lits.push_back(from_ast(conc(proof))); + AstSet &hyps = get_hyps(proof); + for(AstSet::iterator hit = hyps.begin(), hen = hyps.end(); hit != hen; ++hit) + lits.push_back(mk_not(*hit)); + } + + + // turn a bunch of literals into a lemma, replacing + // non-local lits with their local equivalents + // adds the accumulated antecedents (antes) as + // proof obligations of the lemma + + Iproof::node fix_lemma(std::vector &con_lits, AstSet &hyps, non_local_lits *nll){ + std::vector lits(con_lits); + for(AstSet::iterator it = hyps.begin(), en = hyps.end(); it != en; ++it) + lits.push_back(mk_not(*it)); + if(nll){ + for(ResolventAppSet::iterator it = nll->proofs.begin(), en = nll->proofs.end(); it != en; ++it){ + Z3_resolvent *res = *it; + collect_resolvent_lits(res,hyps,lits); + add_antes(res->proof); + } + filter_resolvent_lits(nll,lits); + } + for(unsigned int i = 0; i < lits.size(); i++){ + EquivTab::iterator it = equivs.find(lits[i]); + if(it != equivs.end()){ + lits[i] = it->second.first; // replace with local equivalent + add_antes(it->second.second); // collect the premises that prove this + } + else { + if(!is_local(lits[i])){ + check_non_local(lits[i],nll); + lits[i] = mk_false(); + } + } + } + // TODO: should check here that derivation is local? + Iproof::node res = prove_lemma(lits); + return res; + } + + 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; + } + + struct non_lit_local_ante {}; + + bool local_antes_simple; + + bool add_local_antes(ast proof, AstSet &hyps, bool expect_clause = false){ + if(antes_added.find(proof) != antes_added.end()) return true; + antes_added.insert(proof); + ast con = from_ast(conc(proof)); + pfrule dk = pr(proof); + if(is_local(con) || equivs.find(con) != equivs.end()){ + if(!expect_clause || num_lits(conc(proof)) == 1){ + AstSet &this_hyps = get_hyps(proof); + if(std::includes(hyps.begin(),hyps.end(),this_hyps.begin(),this_hyps.end())){ + // if(hyps.find(con) == hyps.end()) + if(/* lemma_count == SHOW_LEMMA_COUNT - 1 && */ !is_literal_or_lit_iff(conc(proof))){ + std::cout << "\nnon-lit local ante\n"; + show_step(proof); + show(conc(proof)); + throw non_lit_local_ante(); + } + local_antes.push_back(proof); + return true; + } + else + ; //std::cout << "bar!\n"; + } + } + if(dk == PR_ASSERTED + //|| dk == PR_HYPOTHESIS + //|| dk == PR_TH_LEMMA + || dk == PR_QUANT_INST + //|| dk == PR_UNIT_RESOLUTION + //|| dk == PR_LEMMA + ) + return false; + if(dk == PR_HYPOTHESIS && hyps.find(con) != hyps.end()) + ; //std::cout << "blif!\n"; + if(dk == PR_HYPOTHESIS + || dk == PR_LEMMA) + ; //std::cout << "foo!\n"; + if(dk == PR_TH_LEMMA && num_prems(proof) == 0){ + // Check if this is an axiom instance + get_axiom_instance(conc(proof)); + } + + // #define SIMPLE_PROOFS +#ifdef SIMPLE_PROOFS + if(!(dk == PR_TRANSITIVITY + || dk == PR_MONOTONICITY)) + local_antes_simple = false; +#endif + + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++){ + ast arg = prem(proof,i); + try { + if(!add_local_antes(arg, hyps, dk == PR_UNIT_RESOLUTION && i == 0)) + return false; + } + catch (non_lit_local_ante) { + std::cout << "\n"; + show_step(proof); + show(conc(proof)); + throw non_lit_local_ante(); + } + } + return true; + } + + std::vector lit_trace; + hash_set marked_proofs; + + bool proof_has_lit(ast proof, 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(ast lit, 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(ast lit, 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(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(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(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(ast lit){ + print_lit(lit); + std::cout << "\n"; + } + + void print_z3_lit(ast a){ + print_lit(from_ast(a)); + } + + void show_z3_lit(ast a){ + print_z3_lit(a); + std::cout << "\n"; + } + + + void show_con(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( 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( 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(ast proof){ + if(pfhist.size() == 0) + pfhist_pos = 0; + else pfhist_pos++; + pfhist.resize(pfhist_pos); + pfhist.push_back(proof); + show_step(proof); + } + + void show_nll(non_local_lits *nll){ + if(!nll)return; + for(ResolventAppSet::iterator it = nll->proofs.begin(), en = nll->proofs.end(); it != en; ++it){ + Z3_resolvent *res = *it; + show_step(res->proof); + std::cout << "Pivot: "; + show(res->pivot); + std::cout << std::endl; + } + } + + 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)); + } + } + + int extract_th_lemma_common(std::vector &lits, non_local_lits *nll, bool lemma_nll = true){ + std::vector la = local_antes; + local_antes.clear(); // clear antecedents for next lemma + antes_added.clear(); + // std::vector lits; + AstSet hyps; // no hyps + for(unsigned i = 0; i < la.size(); i++) + lits.push_back(mk_not(from_ast(conc(la[i])))); + // lits.push_back(from_ast(conc(proof))); + Iproof::node res =fix_lemma(lits,hyps, lemma_nll ? nll : 0); + for(unsigned i = 0; i < la.size(); i++){ + Iproof::node q = translate_main(la[i],nll,false); + ast pnode = from_ast(conc(la[i])); + assert(is_local(pnode) || equivs.find(pnode) != equivs.end()); + Iproof::node neg = res; + Iproof::node pos = q; + if(is_not(pnode)){ + pnode = mk_not(pnode); + std::swap(neg,pos); + } + try { + res = iproof->make_resolution(pnode,neg,pos); + } + catch (const iz3proof::proof_error){ + std::cout << "\nresolution error in theory lemma\n"; + std::cout << "lits:\n"; + for(unsigned j = 0; j < lits.size(); j++) + show_lit(lits[j]); + std::cout << "\nstep:\n"; + show_step(la[i]); + throw invalid_lemma(); + } + } + return res; + } + + Iproof::node extract_simple_proof(ast proof, hash_set &leaves){ + if(leaves.find(proof) != leaves.end()) + return iproof->make_hypothesis(conc(proof)); + ast con = from_ast(conc(proof)); + pfrule dk = pr(proof); + unsigned nprems = num_prems(proof); + std::vector args(nprems); + for(unsigned i = 0; i < nprems; i++){ + ast arg = prem(proof,i); + args[i] = extract_simple_proof(arg,leaves); + } + + switch(dk){ + case PR_TRANSITIVITY: + return iproof->make_transitivity(con,args[0],args[1]); + case PR_MONOTONICITY: + return iproof->make_congruence(con,args); + case PR_REFLEXIVITY: + return iproof->make_reflexivity(con); + case PR_SYMMETRY: + return iproof->make_symmetry(con,args[0]); + } + assert(0 && "extract_simple_proof: unknown op"); + return 0; + } + + int extract_th_lemma_simple(ast proof, std::vector &lits){ + std::vector la = local_antes; + local_antes.clear(); // clear antecedents for next lemma + antes_added.clear(); + + hash_set leaves; + for(unsigned i = 0; i < la.size(); i++) + leaves.insert(la[i]); + + Iproof::node ipf = extract_simple_proof(proof,leaves); + ast con = from_ast(conc(proof)); + Iproof::node hyp = iproof->make_hypothesis(mk_not(con)); + ipf = iproof->make_eqcontra(ipf,hyp); + + // std::vector lits; + AstSet hyps; // no hyps + for(unsigned i = 0; i < la.size(); i++) + lits.push_back(mk_not(from_ast(conc(la[i])))); + // lits.push_back(from_ast(conc(proof))); + + Iproof::node res = iproof->make_contra(ipf,lits); + + for(unsigned i = 0; i < la.size(); i++){ + Iproof::node q = translate_main(la[i],0,false); + ast pnode = from_ast(conc(la[i])); + assert(is_local(pnode) || equivs.find(pnode) != equivs.end()); + Iproof::node neg = res; + Iproof::node pos = q; + if(is_not(pnode)){ + pnode = mk_not(pnode); + std::swap(neg,pos); + } + try { + res = iproof->make_resolution(pnode,neg,pos); + } + catch (const iz3proof::proof_error){ + std::cout << "\nresolution error in theory lemma\n"; + std::cout << "lits:\n"; + for(unsigned j = 0; j < lits.size(); j++) + show_lit(lits[j]); + std::cout << "\nstep:\n"; + show_step(la[i]); + throw invalid_lemma(); + } + } + return res; + } + +// #define NEW_EXTRACT_TH_LEMMA + + void get_local_hyps(ast proof, std::set &res){ + std::set hyps = get_hyps(proof); + for(std::set::iterator it = hyps.begin(), en = hyps.end(); it != en; ++it){ + ast hyp = *it; + if(is_local(hyp)) + res.insert(hyp); + } + } + + int extract_th_lemma(ast proof, std::vector &lits, non_local_lits *nll){ + pfrule dk = pr(proof); + unsigned nprems = num_prems(proof); +#ifdef NEW_EXTRACT_TH_LEMMA + if(nprems == 0 && !nll) +#else + if(nprems == 0) +#endif + return 0; + if(nprems == 0 && dk == PR_TH_LEMMA) + // Check if this is an axiom instance + get_axiom_instance(conc(proof)); + + local_antes_simple = true; + for(unsigned i = 0; i < nprems; i++){ + ast arg = prem(proof,i); + if(!add_local_antes(arg,get_hyps(proof))){ + local_antes.clear(); // clear antecedents for next lemma + antes_added.clear(); + antes.clear(); + return 0; + } + } +#ifdef NEW_EXTRACT_TH_LEMMA + bool lemma_nll = nargs > 1; + if(nll && !lemma_nll){ + lemma_nll = false; + // std::cout << "lemma count = " << nll_lemma_count << "\n"; + for(ResolventAppSet::iterator it = nll->proofs.begin(), en = nll->proofs.end(); it != en; ++it){ + Z3_resolvent *res = *it; + ast arg = res->proof; + std::set loc_hyps; get_local_hyps(arg,loc_hyps); + if(!add_local_antes(arg,loc_hyps)){ + local_antes.clear(); // clear antecedents for next lemma + antes_added.clear(); + antes.clear(); + return 0; + } + } + collect_all_resolvent_lits(nll,lits); + } + int my_count = nll_lemma_count++; + int res; + try { + res = extract_th_lemma_common(lits,nll,lemma_nll); + } + catch (const invalid_lemma &) { + std::cout << "\n\nlemma: " << my_count; + std::cout << "\n\nproof node: \n"; + show_step(proof); + std::cout << "\n\nnon-local: \n"; + show_nll(nll); + pfgoto(nll->proofs[0]->proof); + show(conc(pfhist.back())); + pfprem(1); + show(conc(pfhist.back())); + pfprem(0); + show(conc(pfhist.back())); + pfprem(0); + show(conc(pfhist.back())); + pfprem(0); + show(conc(pfhist.back())); + std::cout << "\n\nliterals: \n"; + for(int i = 0; i < lits.size(); i++) + show_lit(lits[i]); + throw invalid_lemma(); + } + + return res; +#else +#ifdef SIMPLE_PROOFS + if(local_antes_simple && !nll) + return extract_th_lemma_simple(proof, lits); +#endif + return extract_th_lemma_common(lits,nll); +#endif + } + + int extract_th_lemma_ur(ast proof, int position, std::vector &lits, non_local_lits *nll){ + for(int i = 0; i <= position; i++){ + ast arg = prem(proof,i); + if(!add_local_antes(arg,get_hyps(proof),i==0)){ + local_antes.clear(); // clear antecedents for next lemma + antes_added.clear(); + antes.clear(); + return 0; + } + } + return extract_th_lemma_common(lits,nll); + } + + // see if any of the pushed resolvents are resolutions + // push the current proof into the latest such + int push_into_resolvent(ast proof, std::vector &lits, non_local_lits *nll, bool expect_clause){ + if(!nll) return 0; + if(num_args(proof) > 1) return 0; + ResolventAppSet resos = nll->proofs; + int pos = resos.size()-1; + for( ResolventAppSet::reverse_iterator it = resos.rbegin(), en = resos.rend(); it != en; ++it, --pos){ + Z3_resolvent *reso = *it; + ast ante = reso->proof; + ast pivot = reso->pivot; + bool is_unit = reso->is_unit; + pfrule dk = pr(ante); + bool pushable = dk == PR_UNIT_RESOLUTION || dk == PR_LEMMA; + if(!pushable && num_args(ante) > 1){ +#if 0 + if (!is_local(conc(ante))) + std::cout << "non-local "; + std::cout << "pushable!\n"; +#endif + pushable = true; + } + if(pushable){ + // remove the resolvent from list and add new clause as resolvent + resos.erase((++it).base()); + for(; pos < (int)resos.size(); pos++){ + Z3_resolvent *r = resos[pos]; + resos[pos] = find_resolvent(r->proof,r->is_unit,mk_not(pivot)); + } + resos.push_back(find_resolvent(proof,!expect_clause,mk_not(pivot))); + non_local_lits *new_nll = find_nll(resos); + try { + int res = translate_main(ante,new_nll,!is_unit); + return res; + } + catch (const invalid_lemma &) { + std::cout << "\n\npushing: \n"; + std::cout << "nproof node: \n"; + show_step(proof); + std::cout << "\n\nold non-local: \n"; + show_nll(nll); + std::cout << "\n\nnew non-local: \n"; + show_nll(new_nll); + throw invalid_lemma(); + } + } + } + return 0; // no pushed resolvents are resolution steps + } + + non_local_lits *find_nll(ResolventAppSet &proofs){ + if(proofs.empty()) + return (non_local_lits *)0; + std::pair foo(non_local_lits(proofs),(non_local_lits *)0); + std::pair::iterator,bool> bar = + non_local_lits_unique.insert(foo); + non_local_lits *&res = bar.first->second; + if(bar.second) + res = new non_local_lits(bar.first->first); + return res; + } + + Z3_resolvent *find_resolvent(ast proof, bool unit, ast pivot){ + std::pair foo(Z3_resolvent(proof,unit,pivot),(Z3_resolvent *)0); + std::pair::iterator,bool> bar = + Z3_resolvent_unique.insert(foo); + Z3_resolvent *&res = bar.first->second; + if(bar.second) + res = new Z3_resolvent(bar.first->first); + return res; + } + + // translate a unit resolution at position pos of given app + int translate_ur(ast proof, int position, non_local_lits *nll){ + ast ante = prem(proof,position); + if(position <= 0) + return translate_main(ante, nll); + ast pnode = conc(ante); + ast pnode_abs = !is_not(pnode) ? pnode : mk_not(pnode); + if(is_local(pnode) || equivs.find(pnode) != equivs.end()){ + Iproof::node neg = translate_ur(proof,position-1,nll); + Iproof::node pos = translate_main(ante, nll, false); + if(is_not(pnode)){ + pnode = mk_not(pnode); + std::swap(neg,pos); + } + try { + return iproof->make_resolution(pnode,neg,pos); + } + catch (const iz3proof::proof_error){ + std::cout << "resolution error in unit_resolution, position" << position << "\n"; + show_step(proof); + throw invalid_lemma(); + } + } + else { + // non-local pivot we have no local equivalent for + if(true){ + // try pushing the non-local resolution up + pfrule dk = pr(ante); + non_local_lits *old_nll = nll; + if(dk == PR_HYPOTHESIS) + ; //std::cout << "non-local hyp!\n"; // resolving with a hyp is a no-op + else { + ResolventAppSet new_proofs; + if(nll) new_proofs = nll->proofs; + Z3_resolvent *reso = find_resolvent(ante,true,pnode); + new_proofs.push_back(reso); + nll = find_nll(new_proofs); + } + try { + return translate_ur(proof,position-1,nll); + } + catch (const invalid_lemma &) { + if(old_nll != nll){ + std::cout << "\n\nadded_nll: \n"; + std::cout << "nproof node: \n"; + show_step(proof); + std::cout << "\n\new non-local step: \n"; + show_step(nll->proofs.back()->proof); + } + throw invalid_lemma(); + } + + } + else { + // just make a lemma + std::vector lits; + do_unit_resolution(proof,position,lits); + int res; + if(!(res = extract_th_lemma_ur(proof,position,lits,nll))){ + for(int i = 0; i <= position; i++){ + z3pf p = prem(proof,i); + add_antes(p); + } + res = fix_lemma(lits,get_hyps(proof),nll); + } + return res; + } + } + } + + non_local_lits *update_nll(ast proof, bool expect_clause, non_local_lits *nll){ + std::vector lits; + collect_proof_clause(proof,expect_clause,lits); + AstSet litset; + litset.insert(lits.begin(),lits.end()); + ResolventAppSet to_keep; + for(int i = nll->proofs.size()-1; i >= 0; --i){ + ast traced_lit = (nll->proofs[i])->pivot; + ast traced_lit_neg = mk_not(traced_lit); + if(litset.find(traced_lit) != litset.end() || litset.find(traced_lit_neg) != litset.end()){ + to_keep.push_back(nll->proofs[i]); + std::vector reslits; + AstSet dummy; + collect_resolvent_lits(nll->proofs[i],dummy,reslits); + litset.insert(reslits.begin(),reslits.end()); + } + } + if(to_keep.size() == nll->proofs.size()) return nll; + ResolventAppSet new_proofs; + for(int i = to_keep.size() - 1; i >= 0; --i) + new_proofs.push_back(to_keep[i]); + return find_nll(new_proofs); + } + + // translate a Z3 proof term into a foci proof term + + Iproof::node translate_main(ast proof, non_local_lits *nll, bool expect_clause = true){ + non_local_lits *old_nll = nll; + if(nll) nll = update_nll(proof,expect_clause,nll); + AstToIpf &tr = nll ? non_local_translation[nll] : translation; + hash_map &trc = expect_clause ? tr.first : tr.second; + std::pair foo(proof,INT_MAX); + std::pair bar = trc.insert(foo); + int &res = bar.first->second; + if(!bar.second) return res; + + + try { + 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; + } + + pfrule dk = pr(proof); + unsigned nprems = num_prems(proof); + if(dk == PR_UNIT_RESOLUTION){ + res = translate_ur(proof, nprems - 1, nll); + } + else if(dk == PR_LEMMA){ + ast contra = prem(proof,0); // this is a proof of false from some hyps + res = translate_main(contra, nll); + 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)); +#ifdef NEW_EXTRACT_TH_LEMMA + if(!(res = push_into_resolvent(proof,lits,nll,expect_clause))){ + if(!(res = extract_th_lemma(proof,lits,nll))){ +#else + if(!(res = extract_th_lemma(proof,lits,nll))){ + if(!(res = push_into_resolvent(proof,lits,nll,expect_clause))){ +#endif + std::cout << "extract theory lemma failed\n"; + add_antes(proof); + res = fix_lemma(lits,get_hyps(proof),nll); + } + } + } +#ifdef CHECK_PROOFS + + if(0){ + AstSet zpf_con_lits, ipf_con_lits; + get_local_conclusion_lits(proof, expect_clause, zpf_con_lits); + if(nll){ + for(unsigned i = 0; i < nll->proofs.size(); i++) + get_local_conclusion_lits(nll->proofs[i]->proof,!nll->proofs[i]->is_unit,zpf_con_lits); + } + std::vector ipf_con; + iproof->get_conclusion(res,ipf_con); + for(unsigned i = 0; i < ipf_con.size(); i++) + ipf_con_lits.insert(ipf_con[i]); + if(!(ipf_con_lits == zpf_con_lits)){ + std::cout << "proof error:\n"; + std::cout << "expected lits:\n"; + for(AstSet::iterator hit = zpf_con_lits.begin(), hen = zpf_con_lits.end(); hit != hen; ++hit) + show_lit(*hit); + std::cout << "got lits:\n"; + for(AstSet::iterator hit = ipf_con_lits.begin(), hen = ipf_con_lits.end(); hit != hen; ++hit) + show_lit(*hit); + std::cout << "\nproof step:"; + show_step(proof); + std::cout << "\n"; + throw invalid_lemma(); + } + } +#endif + + return res; + } + + catch (const invalid_lemma &) { + if(old_nll != nll){ + std::cout << "\n\nupdated nll: \n"; + std::cout << "nproof node: \n"; + show_step(proof); + std::cout << "\n\new non-local: \n"; + show_nll(nll); + } + throw invalid_lemma(); + } + + } + + // Proof translation is in two stages: + // 1) Translate ast proof term to Zproof + // 2) Translate Zproof to Iproof + + Iproof::node translate(ast proof, Iproof &dst){ + iproof = &dst; + Iproof::node Ipf = translate_main(proof,0); // builds result in dst + return Ipf; + } + + iz3translation_direct(iz3mgr &mgr, + iz3secondary *_secondary, + const std::vector &cnsts, + const std::vector &parents, + const std::vector &theory) + : iz3translation(mgr, cnsts, parents, theory) + { + secondary = _secondary; + 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 = 0; + } +}; + + + + +#ifdef IZ3_TRANSLATE_DIRECT + +iz3translation *iz3translation::create(iz3mgr &mgr, + iz3secondary *secondary, + const std::vector &cnsts, + const std::vector &parents, + const std::vector &theory){ + return new iz3translation_direct(mgr,secondary,cnsts,parents,theory); +} + + +#if 0 + +void iz3translation_direct_trace_lit(iz3translation_direct *p, ast lit, ast proof){ + p->trace_lit(lit, proof); +} + +void iz3translation_direct_show_step(iz3translation_direct *p, ast proof){ + p->show_step(proof); +} + +void iz3translation_direct_show_marked(iz3translation_direct *p, ast proof){ + p->show_marked(proof); +} + +void iz3translation_direct_show_lit(iz3translation_direct *p, ast lit){ + p->show_lit(lit); +} + +void iz3translation_direct_show_z3_lit(iz3translation_direct *p, ast a){ + p->show_z3_lit(a); +} + +void iz3translation_direct_pfgoto(iz3translation_direct *p, ast proof){ + p->pfgoto(proof); +} + +void iz3translation_direct_show_nll(iz3translation_direct *p, non_local_lits *nll){ + p->show_nll(nll); +} + +void iz3translation_direct_pfback(iz3translation_direct *p ){ + p->pfback(); +} + +void iz3translation_direct_pffwd(iz3translation_direct *p ){ + p->pffwd(); +} + +void iz3translation_direct_pfprem(iz3translation_direct *p, int i){ + p->pfprem(i); +} + + +struct stdio_fixer { + stdio_fixer(){ + std::cout.rdbuf()->pubsetbuf(0,0); + } + +} my_stdio_fixer; + +#endif + +#endif + +