diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6ea794040..e4c788cea 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -59,8 +59,9 @@ def init_project_def(): add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') + add_lib('interp', ['solver']) API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h'] - add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'], + add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure', 'interp'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False) diff --git a/src/interp/foci2.h b/src/interp/foci2.h new file mode 100755 index 000000000..3f32b8118 --- /dev/null +++ b/src/interp/foci2.h @@ -0,0 +1,56 @@ +#ifndef FOCI2_H +#define FOCI2_H + +#include +#include + +#ifdef WIN32 +#define FOCI2_EXPORT __declspec(dllexport) +#else +#define FOCI2_EXPORT __attribute__ ((visibility ("default"))) +#endif + +class foci2 { + public: + virtual ~foci2(){} + + typedef int ast; + typedef int symb; + + /** Built-in operators */ + enum ops { + And = 0, Or, Not, Iff, Ite, Equal, Plus, Times, Floor, Leq, Div, Bool, Int, Array, Tsym, Fsym, Forall, Exists, Distinct, LastOp + }; + + virtual symb mk_func(const std::string &s) = 0; + virtual symb mk_pred(const std::string &s) = 0; + virtual ast mk_op(ops op, const std::vector args) = 0; + virtual ast mk_op(ops op, ast) = 0; + virtual ast mk_op(ops op, ast, ast) = 0; + virtual ast mk_op(ops op, ast, ast, ast) = 0; + virtual ast mk_int(const std::string &) = 0; + virtual ast mk_rat(const std::string &) = 0; + virtual ast mk_true() = 0; + virtual ast mk_false() = 0; + virtual ast mk_app(symb,const std::vector args) = 0; + + virtual bool get_func(ast, symb &) = 0; + virtual bool get_pred(ast, symb &) = 0; + virtual bool get_op(ast, ops &) = 0; + virtual bool get_true(ast id) = 0; + virtual bool get_false(ast id) = 0; + virtual bool get_int(ast id, std::string &res) = 0; + virtual bool get_rat(ast id, std::string &res) = 0; + virtual const std::string &get_symb(symb) = 0; + + virtual int get_num_args(ast) = 0; + virtual ast get_arg(ast, int) = 0; + + virtual void show_ast(ast) = 0; + + virtual bool interpolate(const std::vector &frames, std::vector &itps, std::vector parents) = 0; + + FOCI2_EXPORT static foci2 *create(const std::string &); +}; + +#endif diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp new file mode 100755 index 000000000..44006f7f2 --- /dev/null +++ b/src/interp/iz3base.cpp @@ -0,0 +1,228 @@ +/* Copyright 2011 Microsoft Research. */ + +#include "iz3base.h" +#include +#include +#include +#include + + +#ifndef WIN32 +using namespace stl_ext; +#endif + + +iz3base::range &iz3base::ast_range(ast t){ + return ast_ranges_hash[t].rng; +} + +iz3base::range &iz3base::sym_range(symb d){ + return sym_range_hash[d]; +} + +void iz3base::add_frame_range(int frame, ast t){ + range &rng = ast_range(t); + if(!in_range(frame,rng)){ + range_add(frame,rng); + for(int i = 0, n = num_args(t); i < n; ++i) + add_frame_range(frame,arg(t,i)); + if(op(t) == Uninterpreted) + range_add(frame,sym_range(sym(t))); + } +} + +#if 1 +iz3base::range &iz3base::ast_scope(ast t){ + ranges &rngs = ast_ranges_hash[t]; + range &rng = rngs.scp; + if(!rngs.scope_computed){ // not computed yet + rng = range_full(); + for(int i = 0, n = num_args(t); i < n; ++i) + rng = range_glb(rng,ast_scope(arg(t,i))); + if(op(t) == Uninterpreted) + if(parents.empty() || num_args(t) == 0) // in tree mode, all function syms are global + rng = range_glb(rng,sym_range(sym(t))); + rngs.scope_computed = true; + } + return rng; +} +#else +iz3base::range &iz3base::ast_scope(ast t){ + ranges &rngs = ast_ranges_hash[t]; + if(rngs.scope_computed) return rngs.scp; + range rng = range_full(); + for(int i = 0, n = num_args(t); i < n; ++i) + rng = range_glb(rng,ast_scope(arg(t,i))); + if(op(t) == Uninterpreted) + if(parents.empty() || num_args(t) == 0) // in tree mode, all function syms are global + rng = range_glb(rng,sym_range(sym(t))); + rngs = ast_ranges_hash[t]; + rngs.scope_computed = true; + rngs.scp = rng; + return rngs.scp; +} +#endif + +void iz3base::print(const std::string &filename){ + ast t = make(And,cnsts); + assert(0 && "not implemented"); + // Z3_string smt = Z3_benchmark_to_smtlib_string(ctx,"iZ3","QFLIA","unsat","",0,0,t); + // std::ofstream f(filename.c_str()); + // f << smt; +} + + +void iz3base::gather_conjuncts_rec(ast n, std::vector &conjuncts, stl_ext::hash_set &memo){ + if(memo.find(n) == memo.end()){ + memo.insert(n); + if(op(n) == And){ + int nargs = num_args(n); + for(int i = 0; i < nargs; i++) + gather_conjuncts_rec(arg(n,i),conjuncts,memo); + } + else + conjuncts.push_back(n); + } +} + +void iz3base::gather_conjuncts(ast n, std::vector &conjuncts){ + hash_set memo; + gather_conjuncts_rec(n,conjuncts,memo); +} + +bool iz3base::is_literal(ast n){ + if(is_not(n))n = arg(n,0); + if(is_true(n) || is_false(n)) return false; + if(op(n) == And) return false; + return true; +} + +iz3base::ast iz3base::simplify_and(std::vector &conjuncts){ + hash_set memo; + for(unsigned i = 0; i < conjuncts.size(); i++){ + if(is_false(conjuncts[i])) + return conjuncts[i]; + if(is_true(conjuncts[i]) || memo.find(conjuncts[i]) != memo.end()){ + std::swap(conjuncts[i],conjuncts.back()); + conjuncts.pop_back(); + } + else if(memo.find(mk_not(conjuncts[i])) != memo.end()) + return mk_false(); // contradiction! + else + memo.insert(conjuncts[i]); + } + if(conjuncts.empty())return mk_true(); + return make(And,conjuncts); +} + +iz3base::ast iz3base::simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map &memo, int depth){ + if(is_not(n))return mk_not(simplify_with_lit_rec(mk_not(n),lit,memo,depth)); + if(n == lit) return mk_true(); + ast not_lit = mk_not(lit); + if(n == not_lit) return mk_false(); + if(op(n) != And || depth <= 0) return n; + std::pair foo(n,(ast)0); + std::pair::iterator,bool> bar = memo.insert(foo); + ast &res = bar.first->second; + if(!bar.second) return res; + int nargs = num_args(n); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = simplify_with_lit_rec(arg(n,i),lit,memo,depth-1); + res = simplify_and(args); + return res; +} + +iz3base::ast iz3base::simplify_with_lit(ast n, ast lit){ + hash_map memo; + return simplify_with_lit_rec(n,lit,memo,1); +} + +iz3base::ast iz3base::simplify(ast n){ + if(is_not(n)) return mk_not(simplify(mk_not(n))); + std::pair memo_obj(n,(ast)0); + std::pair::iterator,bool> memo = simplify_memo.insert(memo_obj); + ast &res = memo.first->second; + if(!memo.second) return res; + switch(op(n)){ + case And: { + std::vector conjuncts; + gather_conjuncts(n,conjuncts); + for(unsigned i = 0; i < conjuncts.size(); i++) + conjuncts[i] = simplify(conjuncts[i]); +#if 0 + for(unsigned i = 0; i < conjuncts.size(); i++) + if(is_literal(conjuncts[i])) + for(unsigned j = 0; j < conjuncts.size(); j++) + if(j != i) + conjuncts[j] = simplify_with_lit(conjuncts[j],conjuncts[i]); +#endif + res = simplify_and(conjuncts); + } + break; + case Equal: { + ast x = arg(n,0); + ast y = arg(n,1); + if(ast_id(x) > ast_id(y)) + std::swap(x,y); + res = make(Equal,x,y); + break; + } + default: + res = n; + } + return res; +} + +void iz3base::initialize(const std::vector &_parts, const std::vector &_parents, const std::vector &theory){ + cnsts = _parts; + 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]); + } +} + +void iz3base::check_interp(const std::vector &itps, std::vector &theory){ +#if 0 + Z3_config config = Z3_mk_config(); + Z3_context vctx = Z3_mk_context(config); + int frames = cnsts.size(); + std::vector foocnsts(cnsts); + for(unsigned i = 0; i < frames; i++) + foocnsts[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),cnsts[i]); + Z3_write_interpolation_problem(ctx,frames,&foocnsts[0],0, "temp_lemma.smt", theory.size(), &theory[0]); + int vframes,*vparents; + Z3_ast *vcnsts; + const char *verror; + bool ok = Z3_read_interpolation_problem(vctx,&vframes,&vcnsts,0,"temp_lemma.smt",&verror); + assert(ok); + std::vector vvcnsts(vframes); + std::copy(vcnsts,vcnsts+vframes,vvcnsts.begin()); + std::vector vitps(itps.size()); + for(unsigned i = 0; i < itps.size(); i++) + vitps[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),itps[i]); + Z3_write_interpolation_problem(ctx,itps.size(),&vitps[0],0,"temp_interp.smt"); + int iframes,*iparents; + Z3_ast *icnsts; + const char *ierror; + ok = Z3_read_interpolation_problem(vctx,&iframes,&icnsts,0,"temp_interp.smt",&ierror); + assert(ok); + const char *error = 0; + bool iok = Z3_check_interpolant(vctx, frames, &vvcnsts[0], parents.size() ? &parents[0] : 0, icnsts, &error); + assert(iok); +#endif +} + +bool iz3base::is_sat(ast f){ + assert(0 && "iz3base::is_sat() not implemented"); +#if 0 + Z3_push(ctx); + Z3_assert_cnstr(ctx,f); + Z3_lbool res = Z3_check(ctx); + Z3_pop(ctx,1); + return res != Z3_L_FALSE; +#endif +} + diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h new file mode 100755 index 000000000..383a89ea4 --- /dev/null +++ b/src/interp/iz3base.h @@ -0,0 +1,107 @@ +/* Copyright 2011 Microsoft Research. */ + +#ifndef IZ3BASE_H +#define IZ3BASE_H + +#include "iz3mgr.h" +#include "iz3scopes.h" + +/* Base class for interpolators. Includes an AST manager and a scoping + object as bases. */ + +class iz3base : public iz3mgr, public scopes { + + public: + + /** Get the range in which an expression occurs. This is the + smallest subtree containing all occurrences of the + expression. */ + range &ast_range(ast); + + /** Get the scope of an expression. This is the set of tree nodes in + which all of the expression's symbols are in scope. */ + range &ast_scope(ast); + + /** Get the range of a symbol. This is the smallest subtree containing + all occurrences of the symbol. */ + range &sym_range(symb); + + /** Is an expression local (in scope in some frame)? */ + + bool is_local(ast node){ + return !range_is_empty(ast_scope(node)); + } + + /** Simplify an expression */ + + ast simplify(ast); + + /** Constructor */ + + iz3base(scoped_ptr &_m_manager, + const std::vector &_cnsts, + const std::vector &_parents, + const std::vector &_theory) + : iz3mgr(_m_manager), 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; + } + + /* Are we doing weak interpolants? */ + bool weak_mode(){return weak;} + + /** Print interpolation problem to an SMTLIB format file */ + void print(const std::string &filename); + + /** Check correctness of a solutino to this problem. */ + void check_interp(const std::vector &itps, std::vector &theory); + + /** For convenience -- is this formula SAT? */ + bool is_sat(ast); + + /** Interpolator for clauses, to be implemented */ + virtual void interpolate_clause(std::vector &lits, std::vector &itps){ + throw "no interpolator"; + } + + private: + + struct ranges { + range rng; + range scp; + bool scope_computed; + ranges(){scope_computed = false;} + }; + + stl_ext::hash_map sym_range_hash; + stl_ext::hash_map ast_ranges_hash; + stl_ext::hash_map simplify_memo; + + + void add_frame_range(int frame, ast t); + + void initialize(const std::vector &_parts, const std::vector &_parents, const std::vector &_theory); + + std::vector cnsts; + + bool is_literal(ast n); + void gather_conjuncts_rec(ast n, std::vector &conjuncts, stl_ext::hash_set &memo); + void gather_conjuncts(ast n, std::vector &conjuncts); + ast simplify_and(std::vector &conjuncts); + ast simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map &memo, int depth); + ast simplify_with_lit(ast n, ast lit); + + bool weak; + +}; + + + + + +#endif diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp new file mode 100755 index 000000000..741391a8d --- /dev/null +++ b/src/interp/iz3foci.cpp @@ -0,0 +1,327 @@ +/* Copyright 2011 Microsoft Research. */ + +#include +#include +#include + +#include "iz3hash.h" +#include "foci2.h" +#include "iz3foci.h" + +#ifndef WIN32 +using namespace stl_ext; +#endif + +class iz3foci_impl : public iz3secondary { + + int frames; + int *parents; + foci2 *foci; + foci2::symb select_op; + foci2::symb store_op; + foci2::symb mod_op; + +public: + iz3foci_impl(iz3mgr *mgr, int _frames, int *_parents) : iz3secondary(*mgr) { + frames = _frames; + parents = _parents; + foci = 0; + } + + typedef hash_map AstToNode; + AstToNode ast_to_node; // maps Z3 ast's to foci expressions + + typedef hash_map NodeToAst; + NodeToAst node_to_ast; // maps Z3 ast's to foci expressions + + typedef hash_map FuncDeclToSymbol; + FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols + + typedef hash_map SymbolToFuncDecl; + SymbolToFuncDecl symbol_to_func_decl; // maps symbols to Z3 func decls + + int from_symb(symb func){ + std::string name = string_of_symbol(func); + bool is_bool = is_bool_type(get_range_type(func)); + foci2::symb f; + if(is_bool) + f = foci->mk_pred(name); + else + f = foci->mk_func(name); + symbol_to_func_decl[f] = func; + func_decl_to_symbol[func] = f; + return f; + } + + // create a symbol corresponding to a DeBruijn index of a particular type + // the type has to be encoded into the name because the same index can + // occur with different types + foci2::symb make_deBruijn_symbol(int index, int type){ + std::ostringstream s; + s << "#" << index << "#" << type; + return foci->mk_func(s.str()); + } + + int from_Z3_ast(ast t){ + std::pair foo(t,0); + std::pair bar = ast_to_node.insert(foo); + int &res = bar.first->second; + if(!bar.second) return res; + int nargs = num_args(t); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = from_Z3_ast(arg(t,i)); + + switch(op(t)){ + case True: + res = foci->mk_true(); break; + case False: + res = foci->mk_false(); break; + case And: + res = foci->mk_op(foci2::And,args); break; + case Or: + res = foci->mk_op(foci2::Or,args); break; + case Not: + res = foci->mk_op(foci2::Not,args[0]); break; + case Iff: + res = foci->mk_op(foci2::Iff,args); break; + case OP_OEQ: // bit of a mystery, this one... + if(args[0] == args[1]) res = foci->mk_true(); + else res = foci->mk_op(foci2::Iff,args); + break; + case Ite: + if(is_bool_type(get_type(t))) + res = foci->mk_op(foci2::And,foci->mk_op(foci2::Or,foci->mk_op(foci2::Not,args[0]),args[1]),foci->mk_op(foci2::Or,args[0],args[2])); + else + res = foci->mk_op(foci2::Ite,args); + break; + case Equal: + res = foci->mk_op(foci2::Equal,args); break; + case Implies: + args[0] = foci->mk_op(foci2::Not,args[0]); res = foci->mk_op(foci2::Or,args); break; + case Xor: + res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Iff,args)); break; + case Leq: + res = foci->mk_op(foci2::Leq,args); break; + case Geq: + std::swap(args[0],args[1]); res = foci->mk_op(foci2::Leq,args); break; + case Gt: + res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break; + case Lt: + std::swap(args[0],args[1]); res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break; + case Plus: + res = foci->mk_op(foci2::Plus,args); break; + case Sub: + args[1] = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[1]); res = foci->mk_op(foci2::Plus,args); break; + case Uminus: + res = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[0]); break; + case Times: + res = foci->mk_op(foci2::Times,args); break; + case Idiv: + res = foci->mk_op(foci2::Div,args); break; + case Mod: + res = foci->mk_app(mod_op,args); break; + case Select: + res = foci->mk_app(select_op,args); break; + case Store: + res = foci->mk_app(store_op,args); break; + case Distinct: + res = foci->mk_op(foci2::Distinct,args); break; + case Uninterpreted: { + symb func = sym(t); + FuncDeclToSymbol::iterator it = func_decl_to_symbol.find(func); + foci2::symb f = (it == func_decl_to_symbol.end()) ? from_symb(func) : it->second; + if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==1) // HACK to handle Z3 labels + res = args[0]; + else if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==0) // HACK to handle Z3 labels + res = foci->mk_true(); + else res = foci->mk_app(f,args); + break; + } + case Numeral: { + std::string s = string_of_numeral(t); + res = foci->mk_int(s); + } + case Forall: + case Exists: { + bool is_forall = op(t) == Forall; + foci2::ops qop = is_forall ? foci2::Forall : foci2::Exists; + int bvs = get_quantifier_num_bound(t); + std::vector foci_bvs(bvs); + for(int i = 0; i < bvs; i++){ + std::string name = get_quantifier_bound_name(t,i); + //Z3_string name = Z3_get_symbol_string(ctx,sym); + // type ty = get_quantifier_bound_type(t,i); + foci2::symb f = foci->mk_func(name); + foci2::ast v = foci->mk_app(f,std::vector()); + foci_bvs[i] = v; + } + foci2::ast body = from_Z3_ast(get_quantifier_body(t)); + foci_bvs.push_back(body); + res = foci->mk_op(qop,foci_bvs); + node_to_ast[res] = t; // desperate + } + case Variable: { // a deBruijn index + int index = get_variable_index_value(t); + type ty = get_type(t); + foci2::symb symbol = make_deBruijn_symbol(index,(int)(ty)); + res = foci->mk_app(symbol,std::vector()); + } + default: + { + std::cerr << "iZ3: unsupported Z3 operator in expression\n "; + print_expr(std::cerr,t); + std::cerr << "\n"; + assert(0 && "iZ3: unsupported Z3 operator"); + } + } + return res; + } + + // convert an expr to Z3 ast + ast to_Z3_ast(foci2::ast i){ + std::pair foo(i,(ast)0); + std::pair bar = node_to_ast.insert(foo); + if(!bar.second) return bar.first->second; + ast &res = bar.first->second; + + if(i < 0){ + res = mk_not(to_Z3_ast(-i)); + return res; + } + + // get the arguments + unsigned n = foci->get_num_args(i); + std::vector args(n); + for(unsigned j = 0; j < n; j++) + args[j] = to_Z3_ast(foci->get_arg(i,j)); + + // handle operators + foci2::ops o; + foci2::symb f; + std::string nval; + if(foci->get_true(i)) + res = mk_true(); + else if(foci->get_false(i)) + res = mk_false(); + else if(foci->get_op(i,o)){ + switch(o){ + case foci2::And: + res = make(And,args); break; + case foci2::Or: + res = make(Or,args); break; + case foci2::Not: + res = mk_not(args[0]); break; + case foci2::Iff: + res = make(Iff,args[0],args[1]); break; + case foci2::Ite: + res = make(Ite,args[0],args[1],args[2]); break; + case foci2::Equal: + res = make(Equal,args[0],args[1]); break; + case foci2::Plus: + res = make(Plus,args); break; + case foci2::Times: + res = make(Times,args); break; + case foci2::Div: + res = make(Div,args[0],args[1]); break; + case foci2::Leq: + res = make(Leq,args[0],args[1]); break; + case foci2::Distinct: + res = make(Distinct,args); + break; + case foci2::Tsym: + res = mk_true(); + break; + case foci2::Fsym: + res = mk_false(); + break; + case foci2::Forall: + case foci2::Exists: + { + int nargs = n; + std::vector bounds(nargs-1); + for(int i = 0; i < nargs-1; i++) + bounds[i] = args[i]; + opr oz = o == foci2::Forall ? Forall : Exists; + res = make_quant(oz,bounds,args[nargs-1]); + } + break; + default: + assert("unknown built-in op"); + } + } + else if(foci->get_int(i,nval)){ + res = make_int(nval); + } + else if(foci->get_func(i,f)){ + if(f == select_op){ + assert(n == 2); + res = make(Select,args[0],args[1]); + } + else if(f == store_op){ + assert(n == 3); + res = make(Store,args[0],args[1],args[2]); + } + else if(f == mod_op){ + assert(n == 2); + res = make(Mod,args[0],args[1]); + } + else { + std::pair foo(f,(symb)0); + std::pair bar = symbol_to_func_decl.insert(foo); + symb &func_decl = bar.first->second; + if(bar.second){ + std::cout << "unknown function symbol:\n"; + foci->show_ast(i); + assert(0); + } + res = make(func_decl,args); + } + } + else { + std::cerr << "iZ3: unknown FOCI expression kind\n"; + assert(0 && "iZ3: unknown FOCI expression kind"); + } + return res; + } + + int interpolate(const std::vector &cnsts, std::vector &itps){ + assert((int)cnsts.size() == frames); + foci = foci2::create("lia"); + if(!foci){ + std::cerr << "iZ3: cannot find foci lia solver.\n"; + assert(0); + } + select_op = foci->mk_func("select"); + store_op = foci->mk_func("store"); + mod_op = foci->mk_func("mod"); + std::vector foci_cnsts(frames), foci_itps(frames-1), foci_parents; + if(parents) + foci_parents.resize(frames); + for(int i = 0; i < frames; i++){ + foci_cnsts[i] = from_Z3_ast(cnsts[i]); + if(parents) + foci_parents[i] = parents[i]; + } + int res = foci->interpolate(foci_cnsts, foci_itps, foci_parents); + if(res == 0){ + assert((int)foci_itps.size() == frames-1); + itps.resize(frames-1); + for(int i = 0; i < frames-1; i++){ + // foci->show_ast(foci_itps[i]); + itps[i] = to_Z3_ast(foci_itps[i]); + } + } + ast_to_node.clear(); + node_to_ast.clear(); + func_decl_to_symbol.clear(); + symbol_to_func_decl.clear(); + delete foci; + return res; + } + +}; + +iz3secondary *iz3foci::create(iz3mgr *mgr, int num, int *parents){ + return new iz3foci_impl(mgr,num,parents); +} diff --git a/src/interp/iz3foci.h b/src/interp/iz3foci.h new file mode 100755 index 000000000..4b7040b98 --- /dev/null +++ b/src/interp/iz3foci.h @@ -0,0 +1,15 @@ +/* Copyright 2011 Microsoft Research. */ + +#ifndef IZ3FOCI_H +#define IZ3FOCI_H + +#include "iz3secondary.h" + +/** Secondary prover based on Cadence FOCI. */ + +class iz3foci { + public: + static iz3secondary *create(iz3mgr *mgr, int num, int *parents); +}; + +#endif diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h new file mode 100755 index 000000000..abbe5b5fb --- /dev/null +++ b/src/interp/iz3hash.h @@ -0,0 +1,151 @@ + +// pull in the headers for has_map and hash_set +// these live in non-standard places + +#ifndef IZ3_HASH_H +#define IZ3_HASH_H + +//#define USE_UNORDERED_MAP +#ifdef USE_UNORDERED_MAP + +#define stl_ext std +#define hash_space std +#include +#include +#define hash_map unordered_map +#define hash_set unordered_set + +#else + +#if __GNUC__ >= 3 +#undef __DEPRECATED +#define stl_ext __gnu_cxx +#define hash_space stl_ext +#include +#include +#else +#ifdef WIN32 +#define stl_ext stdext +#define hash_space std +#include +#include +#else +#define stl_ext std +#define hash_space std +#include +#include +#endif +#endif + +#endif + +#include + +// stupid STL doesn't include hash function for class string + +#ifndef WIN32 + +namespace stl_ext { + template <> + class hash { + stl_ext::hash H; + public: + size_t operator()(const std::string &s) const { + return H(s.c_str()); + } + }; +} + +#endif + +namespace hash_space { + template <> + class hash > { + public: + size_t operator()(const std::pair &p) const { + return p.first + p.second; + } + }; +} + +#ifdef WIN32 +template <> inline +size_t stdext::hash_value >(const std::pair& p) +{ // hash _Keyval to size_t value one-to-one + return p.first + p.second; +} +#endif + +namespace hash_space { + template + class hash > { + public: + size_t operator()(const std::pair &p) const { + return (size_t)p.first + (size_t)p.second; + } + }; +} + +#if 0 +template inline +size_t stdext::hash_value >(const std::pair& p) +{ // hash _Keyval to size_t value one-to-one + return (size_t)p.first + (size_t)p.second; +} +#endif + +#ifdef WIN32 + +namespace std { + template <> + class less > { + public: + bool operator()(const pair &x, const pair &y) const { + return x.first < y.first || x.first == y.first && x.second < y.second; + } + }; + +} + +namespace std { + template + class less > { + public: + bool operator()(const pair &x, const pair &y) const { + return (size_t)x.first < (size_t)y.first || (size_t)x.first == (size_t)y.first && (size_t)x.second < (size_t)y.second; + } + }; + +} + +#endif + + +#ifndef WIN32 + +namespace stl_ext { + template + class hash { + public: + size_t operator()(const T *p) const { + return (size_t) p; + } + }; +} + +#endif + +#ifdef WIN32 + + + + +template +class hash_map : public stl_ext::hash_map > > {}; + +template +class hash_set : public stl_ext::hash_set > > {}; + +#endif + +#endif diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp new file mode 100644 index 000000000..b79fa0f6b --- /dev/null +++ b/src/interp/iz3mgr.cpp @@ -0,0 +1,352 @@ +/* Copyright 2011 Microsoft Research. */ + + +#include "iz3mgr.h" + +#include +#include +#include +#include + +#include "expr_abstract.h" + + +#ifndef WIN32 +using namespace stl_ext; +#endif + + +std::ostream &operator <<(std::ostream &s, const iz3mgr::ast &a){ + return s; +} + + +iz3mgr::ast iz3mgr::make_var(const std::string &name, type ty){ + symbol s = symbol(name.c_str()); + return m().mk_const(m().mk_const_decl(s, ty)); +} + +iz3mgr::ast iz3mgr::make(opr op, int n, raw_ast **args){ + return m().mk_app(m().get_basic_family_id(), op, 0, 0, n, (expr **)args); +} + +iz3mgr::ast iz3mgr::make(opr op, const std::vector &args){ + static std::vector a(10); + if(a.size() < args.size()) + a.resize(args.size()); + for(unsigned i = 0; i < args.size(); i++) + a[i] = args[i].raw(); + return make(op,args.size(), args.size() ? &a[0] : 0); +} + +iz3mgr::ast iz3mgr::make(opr op){ + return make(op,0,0); +} + +iz3mgr::ast iz3mgr::make(opr op, ast &arg0){ + raw_ast *a = arg0.raw(); + return make(op,1,&a); +} + +iz3mgr::ast iz3mgr::make(opr op, ast &arg0, ast &arg1){ + raw_ast *args[2]; + args[0] = arg0.raw(); + args[1] = arg1.raw(); + return make(op,2,args); +} + +iz3mgr::ast iz3mgr::make(opr op, ast &arg0, ast &arg1, ast &arg2){ + raw_ast *args[3]; + args[0] = arg0.raw(); + args[1] = arg1.raw(); + args[2] = arg2.raw(); + return make(op,3,args); +} + +iz3mgr::ast iz3mgr::make(symb sym, int n, raw_ast **args){ + return m().mk_app(sym, n, (expr **) args); +} + +iz3mgr::ast iz3mgr::make(symb sym, const std::vector &args){ + static std::vector a(10); + if(a.size() < args.size()) + a.resize(args.size()); + for(unsigned i = 0; i < args.size(); i++) + a[i] = args[i].raw(); + return make(sym,args.size(), args.size() ? &a[0] : 0); +} + +iz3mgr::ast iz3mgr::make(symb sym){ + return make(sym,0,0); +} + +iz3mgr::ast iz3mgr::make(symb sym, ast &arg0){ + raw_ast *a = arg0.raw(); + return make(sym,1,&a); +} + +iz3mgr::ast iz3mgr::make(symb sym, ast &arg0, 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){ + raw_ast *args[3]; + args[0] = arg0.raw(); + args[1] = arg1.raw(); + args[2] = arg2.raw(); + return make(sym,3,args); +} + +iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ + if(bvs.size() == 0) return body; + std::vector foo(bvs.size()); + + + std::vector names; + std::vector types; + std::vector bound_asts; + unsigned num_bound = bvs.size(); + + for (unsigned i = 0; i < num_bound; ++i) { + app* a = to_app(bvs[i].raw()); + symbol s(to_app(a)->get_decl()->get_name()); + names.push_back(s); + types.push_back(m().get_sort(a)); + bound_asts.push_back(a); + } + expr_ref abs_body(m()); + expr_abstract(m(), 0, num_bound, &bound_asts[0], to_expr(body.raw()), abs_body); + expr_ref result(m()); + result = m().mk_quantifier( + op == Forall, + names.size(), &types[0], &names[0], abs_body.get(), + 0, + symbol(), + symbol(), + 0, 0, + 0, 0 + ); + return result.get(); +} + +iz3mgr::ast iz3mgr::clone(ast &t, const std::vector &_args){ + if(_args.size() == 0) + return t; + + ast_manager& m = *m_manager.get(); + expr* a = to_expr(t.raw()); + static std::vector rargs(10); + if(rargs.size() < _args.size()) + rargs.resize(_args.size()); + for(unsigned i = 0; i < _args.size(); i++) + rargs[i] = _args[i].raw(); + expr* const* args = (expr **)&rargs[0]; + switch(a->get_kind()) { + case AST_APP: { + app* e = to_app(a); + if (e->get_num_args() != _args.size()) { + assert(0); + } + else { + a = m.mk_app(e->get_decl(), _args.size(), args); + } + break; + } + case AST_QUANTIFIER: { + if (_args.size() != 1) { + assert(0); + } + else { + a = m.update_quantifier(to_quantifier(a), args[0]); + } + break; + } + default: + break; + } + return a; +} + + +void iz3mgr::show(ast t){ + std::cout << mk_pp(t.raw(), m()) << std::endl; +} + +void iz3mgr::print_expr(std::ostream &s, const ast &e){ + s << mk_pp(e.raw(), m()); +} + + +void iz3mgr::print_clause(std::ostream &s, std::vector &cls){ + s << "("; + for(unsigned i = 0; i < cls.size(); i++){ + if(i > 0) s << ","; + print_expr(s,cls[i]); + } + s << ")"; +} + +void iz3mgr::show_clause(std::vector &cls){ + print_clause(std::cout,cls); + std::cout << std::endl; +} + +void iz3mgr::print_lit(ast lit){ + ast abslit = is_not(lit) ? arg(lit,0) : lit; + int f = op(abslit); + if(f == And || f == Or || f == Iff){ + if(is_not(lit)) std::cout << "~"; + std::cout << "[" << abslit << "]"; + } + else + std::cout << lit; +} + + +static int pretty_cols = 79; +static int pretty_indent_chars = 2; + +static int pretty_find_delim(const std::string &s, int pos){ + int level = 0; + int end = s.size(); + for(; pos < end; pos++){ + int ch = s[pos]; + if(ch == '(')level++; + if(ch == ')')level--; + if(level < 0 || (level == 0 && ch == ','))break; + } + return pos; +} + +static void pretty_newline(std::ostream &f, int indent){ + f << std::endl; + for(int i = 0; i < indent; i++) + f << " "; +} + +void iz3mgr::pretty_print(std::ostream &f, const std::string &s){ + int cur_indent = 0; + int indent = 0; + int col = 0; + int pos = 0; + while(pos < (int)s.size()){ + int delim = pretty_find_delim(s,pos); + if(s[pos] != ')' && s[pos] != ',' && cur_indent > indent){ + pretty_newline(f,indent); + cur_indent = indent; + col = indent; + continue; + } + if (col + delim - pos > pretty_cols) { + if (col > indent) { + pretty_newline(f,indent); + cur_indent = indent; + col = indent; + continue; + } + unsigned paren = s.find('(',pos); + if(paren != std::string::npos){ + int chars = paren - pos + 1; + f << s.substr(pos,chars); + indent += pretty_indent_chars; + if(col) pretty_newline(f,indent); + cur_indent = indent; + pos += chars; + col = indent; + continue; + } + } + int chars = delim - pos + 1; + f << s.substr(pos,chars); + pos += chars; + col += chars; + if(s[delim] == ')') + indent -= pretty_indent_chars; + } +} + + +iz3mgr::opr iz3mgr::op(ast &t){ + ast_kind dk = t.raw()->get_kind(); + switch(dk){ + case AST_APP: { + expr * e = to_expr(t.raw()); + if (m().is_unique_value(e)) + return Numeral; + func_decl *d = to_app(t.raw())->get_decl(); + if (null_family_id == d->get_family_id()) + return Uninterpreted; + // return (opr)d->get_decl_kind(); + if (m_basic_fid == d->get_family_id()) { + switch(d->get_decl_kind()) { + case OP_TRUE: return True; + case OP_FALSE: return False; + case OP_EQ: return Equal; + case OP_DISTINCT: return Distinct; + case OP_ITE: return Ite; + case OP_AND: return And; + case OP_OR: return Or; + case OP_IFF: return Iff; + case OP_XOR: return Xor; + case OP_NOT: return Not; + case OP_IMPLIES: return Implies; + case OP_OEQ: return Oeq; + default: + return Other; + } + } + if (m_arith_fid == d->get_family_id()) { + switch(d->get_decl_kind()) { + case OP_LE: return Leq; + case OP_GE: return Geq; + case OP_LT: return Lt; + case OP_GT: return Gt; + case OP_ADD: return Plus; + case OP_SUB: return Sub; + case OP_UMINUS: return Uminus; + case OP_MUL: return Times; + case OP_DIV: return Div; + case OP_IDIV: return Idiv; + case OP_REM: return Rem; + case OP_MOD: return Mod; + case OP_POWER: return Power; + case OP_TO_REAL: return ToReal; + case OP_TO_INT: return ToInt; + case OP_IS_INT: return IsInt; + default: + return Other; + } + } + if (m_array_fid == d->get_family_id()) { + switch(d->get_decl_kind()) { + case OP_STORE: return Store; + case OP_SELECT: return Select; + case OP_CONST_ARRAY: return ConstArray; + case OP_ARRAY_DEFAULT: return ArrayDefault; + case OP_ARRAY_MAP: return ArrayMap; + case OP_SET_UNION: return SetUnion; + case OP_SET_INTERSECT: return SetIntersect; + case OP_SET_DIFFERENCE: return SetDifference; + case OP_SET_COMPLEMENT: return SetComplement; + case OP_SET_SUBSET: return SetSubSet; + case OP_AS_ARRAY: return AsArray; + default: + return Other; + } + } + + return Other; + } + + + case AST_QUANTIFIER: + return to_quantifier(t.raw())->is_forall() ? Forall : Exists; + case AST_VAR: + return Variable; + default:; + } + return Other; +} diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h new file mode 100644 index 000000000..211b9a45a --- /dev/null +++ b/src/interp/iz3mgr.h @@ -0,0 +1,397 @@ +/* Copyright 2011 Microsoft Research. */ + +#ifndef IZ3MGR_H +#define IZ3MGR_H + + +#include +#include "iz3hash.h" + +#include"well_sorted.h" +#include"arith_decl_plugin.h" +#include"bv_decl_plugin.h" +#include"datatype_decl_plugin.h" +#include"array_decl_plugin.h" +#include"ast_translation.h" +#include"ast_pp.h" +#include"ast_ll_pp.h" +#include"ast_smt_pp.h" +#include"ast_smt2_pp.h" +#include"th_rewriter.h" +#include"var_subst.h" +#include"expr_substitution.h" +#include"pp.h" +#include"scoped_ctrl_c.h" +#include"cancel_eh.h" +#include"scoped_timer.h" +//# include"pp_params.hpp" + +/* A wrapper around an ast manager, providing convenience methods. */ + +/** Shorthands for some built-in operators. */ + + + +// rename this to keep it accessible, as we use ast for something else +typedef ast raw_ast; + +/** Wrapper around an ast pointer */ +class ast_r { + raw_ast *_ast; + public: + raw_ast * const &raw() const {return _ast;} + ast_r(raw_ast *a){_ast = a;} + + ast_r(){_ast = 0;} + bool eq(const ast_r &other) const { + return _ast == other._ast; + } + friend bool operator==(const ast_r &x, const ast_r&y){ + return x.eq(y); + } +}; + + +// to make ast_r hashable +namespace stl_ext { + template <> + class hash { + public: + size_t operator()(const ast_r &s) const { + return s.raw()->get_id(); + } + }; +} + +// to make ast_r usable in ordered collections +namespace std { + template <> + class less { + public: + size_t operator()(const ast_r &s, const ast_r &t) const { + return s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + + +/** Wrapper around an AST manager, providing convenience methods. */ + +class iz3mgr { + + public: + typedef ast_r ast; + // typedef decl_kind opr; + typedef func_decl *symb; + typedef sort *type; + + enum opr { + True, + False, + And, + Or, + Not, + Iff, + Ite, + Equal, + Implies, + Distinct, + Xor, + Oeq, + Leq, + Geq, + Lt, + Gt, + Plus, + Sub, + Uminus, + Times, + Div, + Idiv, + Rem, + Mod, + Power, + ToReal, + ToInt, + IsInt, + Select, + Store, + ConstArray, + ArrayDefault, + ArrayMap, + SetUnion, + SetIntersect, + SetDifference, + SetComplement, + SetSubSet, + AsArray, + Numeral, + Forall, + Exists, + Variable, + Uninterpreted, + Other + }; + + opr op(ast &t); + + unsigned ast_id(const ast &x) + { + return to_expr(x.raw())->get_id(); + } + + /** Overloads for constructing ast. */ + + ast make_var(const std::string &name, type ty); + 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, ast &arg0, ast &arg1, 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_quant(opr op, const std::vector &bvs, ast &body); + ast clone(ast &t, const std::vector &args); + + ast_manager &m() {return *m_manager.get();} + + + /** Methods for destructing ast. */ + + + int num_args(ast t){ + ast_kind dk = t.raw()->get_kind(); + switch(dk){ + case AST_APP: + return to_app(t.raw())->get_num_args(); + case AST_QUANTIFIER: + return 1; + case AST_VAR: + return 0; + default:; + } + assert(0); + } + + ast arg(ast t, int i){ + ast_kind dk = t.raw()->get_kind(); + switch(dk){ + case AST_APP: + return to_app(t.raw())->get_arg(i); + case AST_QUANTIFIER: + return to_quantifier(t.raw())->get_expr(); + default:; + } + assert(0); + return ast((raw_ast *)0); + } + + symb sym(ast t){ + return to_app(t.raw())->get_decl(); + } + + std::string string_of_symbol(symb s){ + symbol _s = s->get_name(); + if (_s.is_numerical()) { + std::ostringstream buffer; + buffer << _s.get_num(); + return buffer.str(); + } + else { + return _s.bare_str(); + } + } + + type get_type(ast t){ + return m().get_sort(to_expr(t.raw())); + } + + std::string string_of_numeral(const ast& t){ + rational r; + expr* e = to_expr(t.raw()); + assert(e); + if (m_arith_util.is_numeral(e, r)) + return r.to_string(); + assert(0); + return "NaN"; + } + + int get_quantifier_num_bound(const ast &t) { + return to_quantifier(t.raw())->get_num_decls(); + } + + std::string get_quantifier_bound_name(const ast &t, unsigned i) { + return to_quantifier(t.raw())->get_decl_names()[i].bare_str(); + } + + type get_quantifier_bound_type(const ast &t, unsigned i) { + return to_quantifier(t.raw())->get_decl_sort(i); + } + + ast get_quantifier_body(const ast &t) { + return to_quantifier(t.raw())->get_expr(); + } + + unsigned get_variable_index_value(const ast &t) { + var* va = to_var(t.raw()); + return va->get_idx(); + } + + bool is_bool_type(type t){ + family_id fid = to_sort(t)->get_family_id(); + decl_kind k = to_sort(t)->get_decl_kind(); + return fid == m().get_basic_family_id() && k == BOOL_SORT; + } + + type get_range_type(symb s){ + return to_func_decl(s)->get_range(); + } + + bool is_true(ast t){ + return op(t) == True; + } + + bool is_false(ast t){ + return op(t) == False; + } + + bool is_iff(ast t){ + return op(t) == Iff; + } + + bool is_or(ast t){ + return op(t) == Or; + } + + bool is_not(ast t){ + return op(t) == Not; + } + + // Some constructors that simplify things + + ast mk_not(ast x){ + opr o = op(x); + if(o == True) return make(False); + if(o == False) return make(True); + if(o == Not) return arg(x,0); + return make(Not,x); + } + + ast mk_and(ast x, ast y){ + opr ox = op(x); + opr oy = op(y); + if(ox == True) return y; + if(oy == True) return x; + if(ox == False) return x; + if(oy == False) return y; + if(x == y) return x; + return make(And,x,y); + } + + ast mk_or(ast x, ast y){ + opr ox = op(x); + opr oy = op(y); + if(ox == False) return y; + if(oy == False) return x; + if(ox == True) return x; + if(oy == True) return y; + if(x == y) return x; + return make(Or,x,y); + } + + ast mk_equal(ast x, ast y){ + if(x == y) return make(True); + opr ox = op(x); + opr oy = op(y); + if(ox == True) return y; + if(oy == True) return x; + if(ox == False) return mk_not(y); + if(oy == False) return mk_not(x); + if(ox == False && oy == True) return make(False); + if(oy == False && ox == True) return make(False); + return make(Equal,x,y); + } + + ast z3_ite(ast x, ast y, ast z){ + opr ox = op(x); + opr oy = op(y); + opr oz = op(z); + if(ox == True) return y; + if(ox == False) return z; + if(y == z) return y; + if(oy == True && oz == False) return x; + if(oz == True && oy == False) return mk_not(x); + return make(Ite,x,y,z); + } + + ast make_int(const std::string &s) { + sort *r = m().mk_sort(m_arith_fid, INT_SORT); + return m_arith_util.mk_numeral(rational(s.c_str()),r); + } + + + ast mk_false() { return make(False); } + + ast mk_true() { return make(True); } + + /** For debugging */ + void show(ast); + + /** Constructor */ + + void print_lit(ast lit); + + void print_expr(std::ostream &s, const ast &e); + + void print_clause(std::ostream &s, std::vector &cls); + + void show_clause(std::vector &cls); + + static void pretty_print(std::ostream &f, const std::string &s); + + iz3mgr(scoped_ptr &_m_manager) + : m_manager(_m_manager), + m_arith_util(*_m_manager) + { + m_basic_fid = m().get_basic_family_id(); + m_arith_fid = m().mk_family_id("arith"); + m_bv_fid = m().mk_family_id("bv"); + m_array_fid = m().mk_family_id("array"); + m_dt_fid = m().mk_family_id("datatype"); + m_datalog_fid = m().mk_family_id("datalog_relation"); + } + + iz3mgr(const iz3mgr& other) + : m_manager(other.m_manager), + m_arith_util((const arith_util&)*other.m_manager) + { + m_basic_fid = m().get_basic_family_id(); + m_arith_fid = m().mk_family_id("arith"); + m_bv_fid = m().mk_family_id("bv"); + m_array_fid = m().mk_family_id("array"); + m_dt_fid = m().mk_family_id("datatype"); + m_datalog_fid = m().mk_family_id("datalog_relation"); + } + + protected: + scoped_ptr m_manager; + + private: + ast make(opr op, int n, raw_ast **args); + + ast make(symb sym, int n, raw_ast **args); + + family_id m_basic_fid; + family_id m_array_fid; + family_id m_arith_fid; + family_id m_bv_fid; + family_id m_dt_fid; + family_id m_datalog_fid; + arith_util m_arith_util; +}; + +#endif + diff --git a/src/interp/iz3profiling.h b/src/interp/iz3profiling.h new file mode 100755 index 000000000..fd518b1d9 --- /dev/null +++ b/src/interp/iz3profiling.h @@ -0,0 +1,20 @@ +/* Copyright 2011 Microsoft Research. */ + +#ifndef IZ3PROFILING_H +#define IZ3PROFILING_H + +#include + +namespace profiling { + /** Start a timer with given name */ + void timer_start(const char *); + /** Stop a timer with given name */ + void timer_stop(const char *); + /** Print out timings */ + void print(std::ostream &s); + /** Show the current time. */ + void show_time(); +} + +#endif + diff --git a/src/interp/iz3proof.cpp b/src/interp/iz3proof.cpp new file mode 100755 index 000000000..4c79a4ae6 --- /dev/null +++ b/src/interp/iz3proof.cpp @@ -0,0 +1,604 @@ +/* Copyright 2011 Microsoft Research. */ + + +#include "iz3proof.h" +#include "iz3profiling.h" + +#include +#include +#include +#include + +// #define FACTOR_INTERPS +// #define CHECK_PROOFS + + +void iz3proof::resolve(ast pivot, std::vector &cls1, const std::vector &cls2){ +#ifdef CHECK_PROOFS + std::vector orig_cls1 = cls1; +#endif + ast neg_pivot = pv->mk_not(pivot); + bool found_pivot1 = false, found_pivot2 = false; + for(unsigned i = 0; i < cls1.size(); i++){ + if(cls1[i] == neg_pivot){ + cls1[i] = cls1.back(); + cls1.pop_back(); + found_pivot1 = true; + break; + } + } + { + std::set memo; + memo.insert(cls1.begin(),cls1.end()); + for(unsigned j = 0; j < cls2.size(); j++){ + if(cls2[j] == pivot) + found_pivot2 = true; + else + if(memo.find(cls2[j]) == memo.end()) + cls1.push_back(cls2[j]); + } + } + if(found_pivot1 && found_pivot2) + return; + +#ifdef CHECK_PROOFS + std::cerr << "resolution anomaly: " << nodes.size()-1 << "\n"; +#if 0 + std::cerr << "pivot: "; {pv->print_lit(pivot); std::cout << "\n";} + std::cerr << "left clause:\n"; + for(unsigned i = 0; i < orig_cls1.size(); i++) + {pv->print_lit(orig_cls1[i]); std::cout << "\n";} + std::cerr << "right clause:\n"; + for(unsigned i = 0; i < cls2.size(); i++) + {pv->print_lit(cls2[i]); std::cout << "\n";} + throw proof_error(); +#endif +#endif +} + +iz3proof::node iz3proof::make_resolution(ast pivot, node premise1, node premise2) +{ + if(nodes[premise1].rl == Hypothesis) return premise2; // resolve with hyp is noop + if(nodes[premise2].rl == Hypothesis) return premise1; + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Resolution; + n.aux = pivot; + n.premises.resize(2); + n.premises[0] = (premise1); + n.premises[1] = (premise2); +#ifdef CHECK_PROOFS + n.conclusion = nodes[premise1].conclusion; + resolve(pivot,n.conclusion,nodes[premise2].conclusion); + n.frame = 1; +#else + n.frame = 0; // compute conclusion lazily +#endif + return res; +} + +iz3proof::node iz3proof::resolve_lemmas(ast pivot, node premise1, node premise2) +{ + std::vector lits(nodes[premise1].conclusion), itp; // no interpolant + resolve(pivot,lits,nodes[premise2].conclusion); + return make_lemma(lits,itp); +} + + +iz3proof::node iz3proof::make_assumption(int frame, const std::vector &assumption){ +#if 0 + std::cout << "assumption: \n"; + for(unsigned i = 0; i < assumption.size(); i++) + pv->show(assumption[i]); + std::cout << "\n"; +#endif + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Assumption; + n.conclusion.resize(1); + n.conclusion = assumption; + n.frame = frame; + return res; +} + +iz3proof::node iz3proof::make_hypothesis(ast hypothesis){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Hypothesis; + n.conclusion.resize(2); + n.conclusion[0] = hypothesis; + n.conclusion[1] = pv->mk_not(hypothesis); + return res; +} + +iz3proof::node iz3proof::make_theory(const std::vector &conclusion, std::vector premises){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Theory; + n.conclusion = conclusion; + n.premises = premises; + return res; +} + +iz3proof::node iz3proof::make_axiom(const std::vector &conclusion){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Axiom; + n.conclusion = conclusion; + return res; +} + +iz3proof::node iz3proof::make_contra(node prem, const std::vector &conclusion){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Contra; + n.conclusion = conclusion; +#ifdef CHECK_PROOFS + //if(!(conclusion == nodes[prem].conclusion)){ + //std::cerr << "internal error: proof error\n"; + //assert(0 && "proof error"); + //} +#endif + n.premises.push_back(prem); + return res; +} + + +iz3proof::node iz3proof::make_lemma(const std::vector &conclusion, const std::vector &interpolation){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Lemma; + n.conclusion = conclusion; + n.frame = interps.size(); + interps.push_back(interpolation); + return res; +} + +/** Make a Reflexivity node. This rule produces |- x = x */ + +iz3proof::node iz3proof::make_reflexivity(ast con){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Reflexivity; + n.conclusion.push_back(con); + return res; +} + +/** Make a Symmetry node. This takes a derivation of |- x = y and + produces | y = x */ + +iz3proof::node iz3proof::make_symmetry(ast con, node prem){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Reflexivity; + n.conclusion.push_back(con); + n.premises.push_back(prem); + return res; +} + +/** Make a transitivity node. This takes derivations of |- x = y + and |- y = z produces | x = z */ + +iz3proof::node iz3proof::make_transitivity(ast con, node prem1, node prem2){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Transitivity; + n.conclusion.push_back(con); + n.premises.push_back(prem1); + n.premises.push_back(prem2); + return res; +} + + +/** Make a congruence node. This takes derivations of |- x_i = y_i + and produces |- f(x_1,...,x_n) = f(y_1,...,y_n) */ + +iz3proof::node iz3proof::make_congruence(ast con, const std::vector &prems){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = Congruence; + n.conclusion.push_back(con); + n.premises = prems; + return res; +} + + +/** Make an equality contradicition node. This takes |- x = y + and |- !(x = y) and produces false. */ + +iz3proof::node iz3proof::make_eqcontra(node prem1, node prem2){ + node res = make_node(); + node_struct &n = nodes[res]; + n.rl = EqContra; + n.premises.push_back(prem1); + n.premises.push_back(prem2); + return res; +} + +iz3proof::node iz3proof::copy_rec(stl_ext::hash_map &memo, iz3proof &src, node n){ + stl_ext::hash_map::iterator it = memo.find(n); + if(it != memo.end()) return (*it).second; + node_struct &ns = src.nodes[n]; + std::vector prems(ns.premises.size()); + for(unsigned i = 0; i < prems.size(); i++) + prems[i] = copy_rec(memo,src,ns.premises[i]); + nodes.push_back(ns); + nodes.back().premises.swap(prems); + if(ns.rl == Lemma){ + nodes.back().frame = interps.size(); + interps.push_back(src.interps[ns.frame]); + } + int res = nodes.size()-1; + memo[n] = res; + return res; +} + +iz3proof::node iz3proof::copy(iz3proof &src, node n){ + stl_ext::hash_map memo; + return copy_rec(memo, src, n); +} + +bool iz3proof::pred_in_A(ast id){ + return weak + ? pv->ranges_intersect(pv->ast_range(id),rng) : + pv->range_contained(pv->ast_range(id),rng); +} + +bool iz3proof::term_in_B(ast id){ + prover::range r = pv->ast_scope(id); + if(weak) { + if(pv->range_min(r) == SHRT_MIN) + return !pv->range_contained(r,rng); + else + return !pv->ranges_intersect(r,rng); + } + else + return !pv->range_contained(r,rng); +} + +bool iz3proof::frame_in_A(int frame){ + return pv->in_range(frame,rng); +} + +bool iz3proof::lit_in_B(ast lit){ + return + b_lits.find(lit) != b_lits.end() + || b_lits.find(pv->mk_not(lit)) != b_lits.end(); +} + +iz3proof::ast iz3proof::my_or(ast x, ast y){ + return pv->mk_not(pv->mk_and(pv->mk_not(x),pv->mk_not(y))); +} + +iz3proof::ast iz3proof::get_A_lits(std::vector &cls){ + ast foo = pv->mk_false(); + for(unsigned i = 0; i < cls.size(); i++){ + ast lit = cls[i]; + if(b_lits.find(pv->mk_not(lit)) == b_lits.end()){ + if(pv->range_max(pv->ast_scope(lit)) == pv->range_min(pv->ast_scope(lit))){ + std::cout << "bad lit: " << pv->range_max(rng) << " : " << pv->range_max(pv->ast_scope(lit)) << " : " << (pv->ast_id(lit)) << " : "; + pv->show(lit); + } + foo = my_or(foo,lit); + } + } + return foo; +} + +iz3proof::ast iz3proof::get_B_lits(std::vector &cls){ + ast foo = pv->mk_false(); + for(unsigned i = 0; i < cls.size(); i++){ + ast lit = cls[i]; + if(b_lits.find(pv->mk_not(lit)) != b_lits.end()) + foo = my_or(foo,lit); + } + return foo; +} + +void iz3proof::set_of_B_lits(std::vector &cls, std::set &res){ + for(unsigned i = 0; i < cls.size(); i++){ + ast lit = cls[i]; + if(b_lits.find(pv->mk_not(lit)) != b_lits.end()) + res.insert(lit); + } +} + +void iz3proof::set_of_A_lits(std::vector &cls, std::set &res){ + for(unsigned i = 0; i < cls.size(); i++){ + ast lit = cls[i]; + if(b_lits.find(pv->mk_not(lit)) == b_lits.end()) + res.insert(lit); + } +} + +void iz3proof::find_B_lits(){ + b_lits.clear(); + for(unsigned i = 0; i < nodes.size(); i++){ + node_struct &n = nodes[i]; + std::vector &cls = n.conclusion; + if(n.rl == Assumption){ + if(weak) goto lemma; + if(!frame_in_A(n.frame)) + for(unsigned j = 0; j < cls.size(); j++) + b_lits.insert(cls[j]); + } + else if(n.rl == Lemma) { + lemma: + for(unsigned j = 0; j < cls.size(); j++) + if(term_in_B(cls[j])) + b_lits.insert(cls[j]); + } + } +} + +iz3proof::ast iz3proof::disj_of_set(std::set &s){ + ast res = pv->mk_false(); + for(std::set::iterator it = s.begin(), en = s.end(); it != en; ++it) + res = my_or(*it,res); + return res; +} + +void iz3proof::mk_and_factor(int p1, int p2, int i, std::vector &itps, std::vector > &disjs){ +#ifdef FACTOR_INTERPS + std::set &d1 = disjs[p1]; + std::set &d2 = disjs[p2]; + if(!weak){ + if(pv->is_true(itps[p1])){ + itps[i] = itps[p2]; + disjs[i] = disjs[p2]; + } + else if(pv->is_true(itps[p2])){ + itps[i] = itps[p1]; + disjs[i] = disjs[p1]; + } + else { + std::set p1only,p2only; + std::insert_iterator > p1o(p1only,p1only.begin()); + std::insert_iterator > p2o(p2only,p2only.begin()); + std::insert_iterator > dio(disjs[i],disjs[i].begin()); + std::set_difference(d1.begin(),d1.end(),d2.begin(),d2.end(),p1o); + std::set_difference(d2.begin(),d2.end(),d1.begin(),d1.end(),p2o); + std::set_intersection(d1.begin(),d1.end(),d2.begin(),d2.end(),dio); + ast p1i = my_or(itps[p1],disj_of_set(p1only)); + ast p2i = my_or(itps[p2],disj_of_set(p2only)); + itps[i] = pv->mk_and(p1i,p2i); + } + } + else { + itps[i] = pv->mk_and(itps[p1],itps[p2]); + std::insert_iterator > dio(disjs[i],disjs[i].begin()); + std::set_union(d1.begin(),d1.end(),d2.begin(),d2.end(),dio); + } +#endif +} + +void iz3proof::mk_or_factor(int p1, int p2, int i, std::vector &itps, std::vector > &disjs){ +#ifdef FACTOR_INTERPS + std::set &d1 = disjs[p1]; + std::set &d2 = disjs[p2]; + if(weak){ + if(pv->is_false(itps[p1])){ + itps[i] = itps[p2]; + disjs[i] = disjs[p2]; + } + else if(pv->is_false(itps[p2])){ + itps[i] = itps[p1]; + disjs[i] = disjs[p1]; + } + else { + std::set p1only,p2only; + std::insert_iterator > p1o(p1only,p1only.begin()); + std::insert_iterator > p2o(p2only,p2only.begin()); + std::insert_iterator > dio(disjs[i],disjs[i].begin()); + std::set_difference(d1.begin(),d1.end(),d2.begin(),d2.end(),p1o); + std::set_difference(d2.begin(),d2.end(),d1.begin(),d1.end(),p2o); + std::set_intersection(d1.begin(),d1.end(),d2.begin(),d2.end(),dio); + ast p1i = pv->mk_and(itps[p1],pv->mk_not(disj_of_set(p1only))); + ast p2i = pv->mk_and(itps[p2],pv->mk_not(disj_of_set(p2only))); + itps[i] = my_or(p1i,p2i); + } + } + else { + itps[i] = my_or(itps[p1],itps[p2]); + std::insert_iterator > dio(disjs[i],disjs[i].begin()); + std::set_union(d1.begin(),d1.end(),d2.begin(),d2.end(),dio); + } +#endif +} + +void iz3proof::interpolate_lemma(node_struct &n){ + if(interps[n.frame].size()) + return; // already computed + pv->interpolate_clause(n.conclusion,interps[n.frame]); +} + + iz3proof::ast iz3proof::interpolate(const prover::range &_rng, bool _weak +#ifdef CHECK_PROOFS + , ast assump + , std::vector *parents +#endif +){ + // std::cout << "proof size: " << nodes.size() << "\n"; + rng = _rng; + weak = _weak; +#ifdef CHECK_PROOFS + if(nodes[nodes.size()-1].conclusion.size() != 0) + std::cerr << "internal error: proof conclusion is not empty clause\n"; + if(!child_interps.size()){ + child_interps.resize(nodes.size()); + for(unsigned j = 0; j < nodes.size(); j++) + child_interps[j] = pv->mk_true(); + } +#endif + std::vector itps(nodes.size()); +#ifdef FACTOR_INTERPS + std::vector > disjs(nodes.size()); +#endif + profiling::timer_start("Blits"); + find_B_lits(); + profiling::timer_stop("Blits"); + profiling::timer_start("interp_proof"); + // strengthen(); + for(unsigned i = 0; i < nodes.size(); i++){ + node_struct &n = nodes[i]; + ast &q = itps[i]; + switch(n.rl){ + case Assumption: { + + if(frame_in_A(n.frame)){ + /* HypC-A */ + if(!weak) +#ifdef FACTOR_INTERPS + { + q = pv->mk_false(); + set_of_B_lits(n.conclusion,disjs[i]); + } +#else + q = get_B_lits(n.conclusion); +#endif + else + q = pv->mk_false(); + } + else { + /* HypEq-B */ + if(!weak) + q = pv->mk_true(); + else +#ifdef FACTOR_INTERPS + { + q = pv->mk_true(); + set_of_A_lits(n.conclusion,disjs[i]); + } +#else + q = pv->mk_not(get_A_lits(n.conclusion)); +#endif + } + break; + } + case Resolution: { + ast p = n.aux; + p = pv->is_not(p) ? pv->mk_not(p) : p; // should be positive, but just in case + if(lit_in_B(p)) +#ifdef FACTOR_INTERPS + mk_and_factor(n.premises[0],n.premises[1],i,itps,disjs); +#else + q = pv->mk_and(itps[n.premises[0]],itps[n.premises[1]]); +#endif + else +#ifdef FACTOR_INTERPS + mk_or_factor(n.premises[0],n.premises[1],i,itps,disjs); +#else + q = my_or(itps[n.premises[0]],itps[n.premises[1]]); +#endif + break; + } + case Lemma: { + interpolate_lemma(n); // make sure lemma interpolants have been computed + q = interps[n.frame][pv->range_max(rng)]; + break; + } + case Contra: { + q = itps[n.premises[0]]; +#ifdef FACTOR_INTERPS + disjs[i] = disjs[n.premises[0]]; +#endif + break; + } + default: + assert(0 && "rule not allowed in interpolated proof"); + } +#ifdef CHECK_PROOFS + int this_frame = pv->range_max(rng); + if(0 && this_frame == 39) { + std::vector alits; + ast s = pv->mk_true(); + for(unsigned j = 0; j < n.conclusion.size(); j++) + if(pred_in_A(n.conclusion[j])){ + int scpmax = pv->range_max(pv->ast_scope(n.conclusion[j])); + if(scpmax == this_frame) + s = pv->mk_and(s,pv->mk_not(n.conclusion[j])); + } + ast ci = child_interps[i]; + s = pv->mk_and(pv->mk_and(s,pv->mk_and(assump,pv->mk_not(q))),ci); + if(pv->is_sat(s)){ + std::cout << "interpolation invariant violated at step " << i << "\n"; + assert(0 && "interpolation invariant violated"); + } + } + if((*parents)[this_frame] == 39) + child_interps[i] = pv->mk_and(child_interps[i],q); +#endif + } + ast &bar = itps[nodes.size()-1]; +#ifdef FACTOR_INTERPS + if(!weak) + bar = my_or(bar,disj_of_set(disjs[nodes.size()-1])); + else + bar = pv->mk_and(bar,pv->mk_not(disj_of_set(disjs[nodes.size()-1]))); +#endif + profiling::timer_stop("interp_proof"); + profiling::timer_start("simplifying"); + bar = pv->simplify(bar); + profiling::timer_stop("simplifying"); + return bar; +} + + +void iz3proof::print(std::ostream &s, int id){ + node_struct &n = nodes[id]; + switch(n.rl){ + case Assumption: + s << "Assumption("; + pv->print_clause(s,n.conclusion); + s << ")"; + break; + case Hypothesis: + s << "Hyp("; pv->print_expr(s,n.conclusion[0]); s << ")"; break; + case Reflexivity: + s << "Refl("; pv->print_expr(s,n.conclusion[0]); s << ")"; break; + case Symmetry: + s << "Symm("; print(s,n.premises[0]); s << ")"; break; + case Transitivity: + s << "Trans("; print(s,n.premises[0]); s << ","; print(s,n.premises[1]); s << ")"; break; + case Congruence: + s << "Cong("; pv->print_expr(s,n.conclusion[0]); + for(unsigned i = 0; i < n.premises.size(); i++){ + s << ","; + print(s,n.premises[i]); + } + s << ")"; break; + case EqContra: + s << "EqContra("; print(s,n.premises[0]); s << ","; print(s,n.premises[1]); s << ")"; break; + case Resolution: + s << "Res("; + pv->print_expr(s,n.aux); s << ","; + print(s,n.premises[0]); s << ","; print(s,n.premises[1]); s << ")"; + break; + case Lemma: + s << "Lemma("; + pv->print_clause(s,n.conclusion); + for(unsigned i = 0; i < n.premises.size(); i++){ + s << ","; + print(s,n.premises[i]); + } + s << ")"; + break; + case Contra: + s << "Contra("; + print(s,n.premises[0]); + s << ")"; + break; + default:; + } +} + + +void iz3proof::show(int id){ + std::ostringstream ss; + print(ss,id); + iz3base::pretty_print(std::cout,ss.str()); + // std::cout << ss.str(); + std::cout << "\n"; +} + + diff --git a/src/interp/iz3proof.h b/src/interp/iz3proof.h new file mode 100755 index 000000000..ea1973f63 --- /dev/null +++ b/src/interp/iz3proof.h @@ -0,0 +1,255 @@ +/* Copyright 2011 Microsoft Research. */ + +#ifndef IZ3PROOF_H +#define IZ3PROOF_H + +#include + +#include "iz3base.h" +#include "iz3secondary.h" + +// #define CHECK_PROOFS + +/** This class defines a simple proof system. + + A proof is a dag consisting of "nodes". The children of each node + are its "premises". Each node has a "conclusion" that is a clause, + represented as a vector of literals. + + The literals are represented by abstract syntax trees. Operations + on these, including computation of scopes are provided by iz3base. + + A proof can be interpolated, provided it is restricted to the + rules Resolution, Assumption, Contra and Lemma, and that all + clauses are strict (i.e., each literal in each clause is local). + + */ + +class iz3proof { + public: + /** The type of proof nodes (nodes in the derivation tree). */ + typedef int node; + + /** 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; + + /** Object thrown in case of a proof error. */ + struct proof_error {}; + + /* Null proof node */ + static const node null = -1; + + /** Make a resolution node with given pivot liter and premises. + The conclusion of premise1 should contain the negation of the + pivot literal, while the conclusion of premise2 should containe the + pivot literal. + */ + node make_resolution(ast pivot, node premise1, node premise2); + + /** Make an assumption node. The given clause is assumed in the given frame. */ + node make_assumption(int frame, const std::vector &assumption); + + /** Make a hypothesis node. If phi is the hypothesis, this is + effectively phi |- phi. */ + node make_hypothesis(ast hypothesis); + + /** Make a theory node. This can be any inference valid in the theory. */ + node make_theory(const std::vector &conclusion, std::vector premises); + + /** Make an axiom node. The conclusion must be an instance of an axiom. */ + node make_axiom(const std::vector &conclusion); + + /** Make a Contra node. This rule takes a derivation of the form + Gamma |- False and produces |- \/~Gamma. */ + + node make_contra(node prem, const std::vector &conclusion); + + /** Make a lemma node. A lemma node must have an interpolation. */ + node make_lemma(const std::vector &conclusion, const std::vector &interpolation); + + /** Make a Reflexivity node. This rule produces |- x = x */ + + node make_reflexivity(ast con); + + /** Make a Symmetry node. This takes a derivation of |- x = y and + produces | y = x */ + + node make_symmetry(ast con, node prem); + + /** Make a transitivity node. This takes derivations of |- x = y + and |- y = z produces | x = z */ + + node make_transitivity(ast con, node prem1, node prem2); + + /** Make a congruence node. This takes derivations of |- x_i = y_i + and produces |- f(x_1,...,x_n) = f(y_1,...,y_n) */ + + node make_congruence(ast con, const std::vector &prems); + + /** Make an equality contradicition node. This takes |- x = y + and |- !(x = y) and produces false. */ + + node make_eqcontra(node prem1, node prem2); + + /** Get the rule of a node in a proof. */ + rule get_rule(node n){ + return nodes[n].rl; + } + + /** Get the pivot of a resolution node. */ + ast get_pivot(node n){ + return nodes[n].aux; + } + + /** Get the frame of an assumption node. */ + int get_frame(node n){ + return nodes[n].frame; + } + + /** Get the number of literals of the conclusion of a node. */ + int get_num_conclusion_lits(node n){ + return get_conclusion(n).size(); + } + + /** Get the nth literal of the conclusion of a node. */ + ast get_nth_conclusion_lit(node n, int i){ + return get_conclusion(n)[i]; + } + + /** Get the conclusion of a node. */ + void get_conclusion(node n, std::vector &result){ + result = get_conclusion(n); + } + + /** Get the number of premises of a node. */ + int get_num_premises(node n){ + return nodes[n].premises.size(); + } + + /** Get the nth premise of a node. */ + int get_nth_premise(node n, int i){ + return nodes[n].premises[i]; + } + + /** Get all the premises of a node. */ + void get_premises(node n, std::vector &result){ + result = nodes[n].premises; + } + + /** Create a new proof node, replacing the premises of an old + one. */ + + node clone(node n, std::vector &premises){ + if(premises == nodes[n].premises) + return n; + nodes.push_back(nodes[n]); + nodes.back().premises = premises; + return nodes.size()-1; + } + + /** Copy a proof node from src */ + node copy(iz3proof &src, node n); + + /** Resolve two lemmas on a given literal. */ + + node resolve_lemmas(ast pivot, node left, node right); + + /** Swap two proofs. */ + void swap(iz3proof &other){ + std::swap(pv,other.pv); + nodes.swap(other.nodes); + interps.swap(other.interps); + } + + /** Compute an interpolant for a proof, where the "A" side is defined by + the given range of frames. Parameter "weak", when true, uses different + interpolation system that resutls in generally weaker interpolants. + */ + ast interpolate(const prover::range &_rng, bool weak = false +#ifdef CHECK_PROOFS + , Z3_ast assump = (Z3_ast)0, std::vector *parents = 0 + +#endif + ); + + /** print proof node to a stream */ + + void print(std::ostream &s, node n); + + /** show proof node on stdout */ + void show(node n); + + /** Construct a proof, with a given prover. */ + iz3proof(prover *p){ + pv = p; + } + + /** Default constructor */ + iz3proof(){pv = 0;} + + + protected: + + struct node_struct { + rule rl; + ast aux; + int frame; + std::vector conclusion; + std::vector premises; + }; + + std::vector nodes; + std::vector > interps; // interpolations of lemmas + prover *pv; + + node make_node(){ + nodes.push_back(node_struct()); + return nodes.size()-1; + } + + void resolve(ast pivot, std::vector &cls1, const std::vector &cls2); + + node copy_rec(stl_ext::hash_map &memo, iz3proof &src, node n); + + void interpolate_lemma(node_struct &n); + + // lazily compute the result of resolution + // the node member "frame" indicates result is computed + const std::vector &get_conclusion(node x){ + node_struct &n = nodes[x]; + if(n.rl == Resolution && !n.frame){ + n.conclusion = get_conclusion(n.premises[0]); + resolve(n.aux,n.conclusion,get_conclusion(n.premises[1])); + n.frame = 1; + } + return n.conclusion; + } + + prover::range rng; + bool weak; + stl_ext::hash_set b_lits; + ast my_or(ast x, ast y); +#ifdef CHECK_PROOFS + std::vector child_interps; +#endif + bool pred_in_A(ast id); + bool term_in_B(ast id); + bool frame_in_A(int frame); + bool lit_in_B(ast lit); + ast get_A_lits(std::vector &cls); + ast get_B_lits(std::vector &cls); + void find_B_lits(); + ast disj_of_set(std::set &s); + void mk_or_factor(int p1, int p2, int i, std::vector &itps, std::vector > &disjs); + void mk_and_factor(int p1, int p2, int i, std::vector &itps, std::vector > &disjs); + void set_of_B_lits(std::vector &cls, std::set &res); + void set_of_A_lits(std::vector &cls, std::set &res); +}; + +#endif diff --git a/src/interp/iz3scopes.cpp b/src/interp/iz3scopes.cpp new file mode 100755 index 000000000..65c6f6d88 --- /dev/null +++ b/src/interp/iz3scopes.cpp @@ -0,0 +1,302 @@ +/* Copyright 2011 Microsoft Research. */ + +#include + +#include "iz3scopes.h" + + +/** computes the least common ancestor of two nodes in the tree, or SHRT_MAX if none */ +int scopes::tree_lca(int n1, int n2){ + if(!tree_mode()) + return std::max(n1,n2); + if(n1 == SHRT_MIN) return n2; + if(n2 == SHRT_MIN) return n1; + 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()); + if(n1 < n2) n1 = parents[n1]; + else n2 = parents[n2]; + } + return n1; +} + +/** computes the greatest common descendant two nodes in the tree, or SHRT_MIN if none */ +int scopes::tree_gcd(int n1, int n2){ + if(!tree_mode()) + return std::min(n1,n2); + int foo = tree_lca(n1,n2); + if(foo == n1) return n2; + if(foo == n2) return n1; + return SHRT_MIN; +} + +#ifndef FULL_TREE + +/** test whether a tree node is contained in a range */ +bool scopes::in_range(int n, const range &rng){ + return tree_lca(rng.lo,n) == n && tree_gcd(rng.hi,n) == n; +} + +/** test whether two ranges of tree nodes intersect */ +bool scopes::ranges_intersect(const range &rng1, const range &rng2){ + return tree_lca(rng1.lo,rng2.hi) == rng2.hi && tree_lca(rng1.hi,rng2.lo) == rng1.hi; +} + + +bool scopes::range_contained(const range &rng1, const range &rng2){ + return tree_lca(rng2.lo,rng1.lo) == rng1.lo + && tree_lca(rng1.hi,rng2.hi) == rng2.hi; +} + +scopes::range scopes::range_lub(const range &rng1, const range &rng2){ + range res; + res.lo = tree_gcd(rng1.lo,rng2.lo); + res.hi = tree_lca(rng1.hi,rng2.hi); + return res; +} + +scopes::range scopes::range_glb(const range &rng1, const range &rng2){ + range res; + res.lo = tree_lca(rng1.lo,rng2.lo); + res.hi = tree_gcd(rng1.hi,rng2.hi); + return res; +} + +#else + + + namespace std { + template <> + class hash { + public: + size_t operator()(const scopes::range_lo &p) const { + return p.lo + (size_t)p.next; + } + }; + } + + template <> inline + size_t stdext::hash_value(const scopes::range_lo& p) + { + std::hash h; + return h(p); + } + + namespace std { + template <> + class less { + public: + bool operator()(const scopes::range_lo &x, const scopes::range_lo &y) const { + return x.lo < y.lo || x.lo == y.lo && (size_t)x.next < (size_t)y.next; + } + }; + } + + + struct range_op { + scopes::range_lo *x, *y; + int hi; + range_op(scopes::range_lo *_x, scopes::range_lo *_y, int _hi){ + x = _x; y = _y; hi = _hi; + } + }; + + namespace std { + template <> + class hash { + public: + size_t operator()(const range_op &p) const { + return (size_t) p.x + (size_t)p.y + p.hi; + } + }; + } + + template <> inline + size_t stdext::hash_value(const range_op& p) + { + std::hash h; + return h(p); + } + + namespace std { + template <> + class less { + public: + bool operator()(const range_op &x, const range_op &y) const { + return (size_t)x.x < (size_t)y.x || x.x == y.x && + ((size_t)x.y < (size_t)y.y || x.y == y.y && x.hi < y.hi); + } + }; + } + + struct range_tables { + hash_map unique; + hash_map lub; + hash_map glb; + }; + + + scopes::range_lo *scopes::find_range_lo(int lo, range_lo *next){ + range_lo foo(lo,next); + std::pair baz(foo,(range_lo *)0); + std::pair::iterator,bool> bar = rt->unique.insert(baz); + if(bar.second) + bar.first->second = new range_lo(lo,next); + return bar.first->second; + //std::pair::iterator,bool> bar = rt->unique.insert(foo); + // const range_lo *baz = &*(bar.first); + // return (range_lo *)baz; // exit const hell + } + + scopes::range_lo *scopes::range_lub_lo(range_lo *rng1, range_lo *rng2){ + if(!rng1) return rng2; + if(!rng2) return rng1; + if(rng1->lo > rng2->lo) + std::swap(rng1,rng2); + std::pair foo(range_op(rng1,rng2,0),(range_lo *)0); + std::pair::iterator,bool> bar = rt->lub.insert(foo); + range_lo *&res = bar.first->second; + if(!bar.second) return res; + if(!(rng1->next && rng1->next->lo <= rng2->lo)){ + for(int lo = rng1->lo; lo <= rng2->lo; lo = parents[lo]) + if(lo == rng2->lo) + {rng2 = rng2->next; break;} + } + range_lo *baz = range_lub_lo(rng1->next,rng2); + res = find_range_lo(rng1->lo,baz); + return res; + } + + + scopes::range_lo *scopes::range_glb_lo(range_lo *rng1, range_lo *rng2, int hi){ + if(!rng1) return rng1; + if(!rng2) return rng2; + if(rng1->lo > rng2->lo) + std::swap(rng1,rng2); + std::pair cand(range_op(rng1,rng2,hi),(range_lo *)0); + std::pair::iterator,bool> bar = rt->glb.insert(cand); + range_lo *&res = bar.first->second; + if(!bar.second) return res; + range_lo *foo; + if(!(rng1->next && rng1->next->lo <= rng2->lo)){ + int lim = hi; + if(rng1->next) lim = std::min(lim,rng1->next->lo); + int a = rng1->lo, b = rng2->lo; + while(a != b && b <= lim){ + a = parents[a]; + if(a > b)std::swap(a,b); + } + if(a == b && b <= lim){ + foo = range_glb_lo(rng1->next,rng2->next,hi); + foo = find_range_lo(b,foo); + } + else + foo = range_glb_lo(rng2,rng1->next,hi); + } + else foo = range_glb_lo(rng1->next,rng2,hi); + res = foo; + return res; + } + + /** computes the lub (smallest containing subtree) of two ranges */ + scopes::range scopes::range_lub(const range &rng1, const range &rng2){ + int hi = tree_lca(rng1.hi,rng2.hi); + if(hi == SHRT_MAX) return range_full(); + range_lo *lo = range_lub_lo(rng1.lo,rng2.lo); + return range(hi,lo); + } + + /** computes the glb (intersection) of two ranges */ + scopes::range scopes::range_glb(const range &rng1, const range &rng2){ + if(rng1.hi == SHRT_MAX) return rng2; + if(rng2.hi == SHRT_MAX) return rng1; + int hi = tree_gcd(rng1.hi,rng2.hi); + range_lo *lo = hi == SHRT_MIN ? 0 : range_glb_lo(rng1.lo,rng2.lo,hi); + if(!lo) hi = SHRT_MIN; + return range(hi,lo); + } + + /** is this range empty? */ + bool scopes::range_is_empty(const range &rng){ + return rng.hi == SHRT_MIN; + } + + /** return an empty range */ + scopes::range scopes::range_empty(){ + return range(SHRT_MIN,0); + } + + /** return a full range */ + scopes::range scopes::range_full(){ + return range(SHRT_MAX,0); + } + + /** return the maximal element of a range */ + int scopes::range_max(const range &rng){ + return rng.hi; + } + + /** return a minimal (not necessarily unique) element of a range */ + int scopes::range_min(const range &rng){ + if(rng.hi == SHRT_MAX) return SHRT_MIN; + return rng.lo ? rng.lo->lo : SHRT_MAX; + } + + + /** return range consisting of downward closure of a point */ + scopes::range scopes::range_downward(int _hi){ + std::vector descendants(parents.size()); + for(int i = descendants.size() - 1; i >= 0 ; i--) + descendants[i] = i == _hi || parents[i] < parents.size() && descendants[parents[i]]; + for(unsigned i = 0; i < descendants.size() - 1; i++) + if(parents[i] < parents.size()) + descendants[parents[i]] = false; + range_lo *foo = 0; + for(int i = descendants.size() - 1; i >= 0; --i) + if(descendants[i]) foo = find_range_lo(i,foo); + return range(_hi,foo); + } + + /** add an element to a range */ + void scopes::range_add(int i, range &n){ + range foo = range(i, find_range_lo(i,0)); + n = range_lub(foo,n); + } + + /** Choose an element of rng1 that is near to rng2 */ + int scopes::range_near(const range &rng1, const range &rng2){ + + int frame; + int thing = tree_lca(rng1.hi,rng2.hi); + if(thing != rng1.hi) return rng1.hi; + range line = range(rng1.hi,find_range_lo(rng2.hi,(range_lo *)0)); + line = range_glb(line,rng1); + return range_min(line); + } + + + /** test whether a tree node is contained in a range */ + bool scopes::in_range(int n, const range &rng){ + range r = range_empty(); + range_add(n,r); + r = range_glb(rng,r); + return !range_is_empty(r); + } + + /** test whether two ranges of tree nodes intersect */ + bool scopes::ranges_intersect(const range &rng1, const range &rng2){ + range r = range_glb(rng1,rng2); + return !range_is_empty(r); + } + + + bool scopes::range_contained(const range &rng1, const range &rng2){ + range r = range_glb(rng1,rng2); + return r.hi == rng1.hi && r.lo == rng1.lo; + } + + +#endif + + diff --git a/src/interp/iz3scopes.h b/src/interp/iz3scopes.h new file mode 100755 index 000000000..e7ca387d5 --- /dev/null +++ b/src/interp/iz3scopes.h @@ -0,0 +1,167 @@ +/* Copyright 2011 Microsoft Research. */ + +#ifndef IZ3SOPES_H +#define IZ3SOPES_H + +#include +#include + +class scopes { + + public: + /** Construct from parents vector. */ + scopes(const std::vector &_parents){ + parents = _parents; + } + + /** The parents vector defining the tree structure */ + std::vector parents; + + // #define FULL_TREE +#ifndef FULL_TREE + struct range { + range(){ + lo = SHRT_MAX; + hi = SHRT_MIN; + } + short lo, hi; + }; + + /** computes the lub (smallest containing subtree) of two ranges */ + range range_lub(const range &rng1, const range &rng2); + + /** computes the glb (intersection) of two ranges */ + range range_glb(const range &rng1, const range &rng2); + + /** is this range empty? */ + bool range_is_empty(const range &rng){ + return rng.hi < rng.lo; + } + + /** return an empty range */ + range range_empty(){ + range res; + res.lo = SHRT_MAX; + res.hi = SHRT_MIN; + return res; + } + + /** return an empty range */ + range range_full(){ + range res; + res.lo = SHRT_MIN; + res.hi = SHRT_MAX; + return res; + } + + /** return the maximal element of a range */ + int range_max(const range &rng){ + return rng.hi; + } + + /** return a minimal (not necessarily unique) element of a range */ + int range_min(const range &rng){ + return rng.lo; + } + + /** return range consisting of downward closure of a point */ + range range_downward(int _hi){ + range foo; + foo.lo = SHRT_MIN; + foo.hi = _hi; + return foo; + } + + void range_add(int i, range &n){ + if(i < n.lo) n.lo = i; + if(i > n.hi) n.hi = i; + } + + /** Choose an element of rng1 that is near to rng2 */ + int range_near(const range &rng1, const range &rng2){ + int frame; + int thing = tree_lca(rng1.lo,rng2.hi); + if(thing == rng1.lo) frame = rng1.lo; + else frame = tree_gcd(thing,rng1.hi); + return frame; + } +#else + + struct range_lo { + int lo; + range_lo *next; + range_lo(int _lo, range_lo *_next){ + lo = _lo; + next = _next; + } + }; + + struct range { + int hi; + range_lo *lo; + range(int _hi, range_lo *_lo){ + hi = _hi; + lo = _lo; + } + range(){ + hi = SHRT_MIN; + lo = 0; + } + }; + + range_tables *rt; + + /** computes the lub (smallest containing subtree) of two ranges */ + range range_lub(const range &rng1, const range &rng2); + + /** computes the glb (intersection) of two ranges */ + range range_glb(const range &rng1, const range &rng2); + + /** is this range empty? */ + bool range_is_empty(const range &rng); + + /** return an empty range */ + range range_empty(); + + /** return a full range */ + range range_full(); + + /** return the maximal element of a range */ + int range_max(const range &rng); + + /** return a minimal (not necessarily unique) element of a range */ + int range_min(const range &rng); + + /** return range consisting of downward closure of a point */ + range range_downward(int _hi); + + /** add an element to a range */ + void range_add(int i, range &n); + + /** Choose an element of rng1 that is near to rng2 */ + int range_near(const range &rng1, const range &rng2); + + range_lo *find_range_lo(int lo, range_lo *next); + range_lo *range_lub_lo(range_lo *rng1, range_lo *rng2); + range_lo *range_glb_lo(range_lo *rng1, range_lo *rng2, int lim); + +#endif + + /** test whether a tree node is contained in a range */ + bool in_range(int n, const range &rng); + + /** test whether two ranges of tree nodes intersect */ + bool ranges_intersect(const range &rng1, const range &rng2); + + /** test whether range rng1 contained in range rng2 */ + bool range_contained(const range &rng1, const range &rng2); + + private: + int tree_lca(int n1, int n2); + int tree_gcd(int n1, int n2); + bool tree_mode(){return parents.size() != 0;} + + + +}; +#endif diff --git a/src/interp/iz3secondary.h b/src/interp/iz3secondary.h new file mode 100755 index 000000000..749feaacc --- /dev/null +++ b/src/interp/iz3secondary.h @@ -0,0 +1,22 @@ +/* Copyright 2011 Microsoft Research. */ + +#ifndef IZ3SECONDARY_H +#define IZ3SECONDARY_H + +/** Interface class for secondary provers. */ + +#include "iz3base.h" +#include + +class iz3secondary : public iz3mgr { + public: + virtual int interpolate(const std::vector &frames, std::vector &interpolants) = 0; + virtual ~iz3secondary(){} + + protected: + iz3secondary(const iz3mgr &mgr) : iz3mgr(mgr) {} +}; + + + +#endif