diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9295c949f..2fff61778 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -638,7 +638,13 @@ def is_compiler(given, expected): def is_CXX_gpp(): return is_compiler(CXX, 'g++') +def is_clang_in_gpp_form(cc): + version_string = subprocess.check_output([cc, '--version']) + return version_string.find('clang') != -1 + def is_CXX_clangpp(): + if is_compiler(CXX, 'g++'): + return is_clang_in_gpp_form(CXX) return is_compiler(CXX, 'clang++') def get_cpp_files(path): diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 560ee5885..98722022c 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include #include +#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index b000201b7..68f7596ee 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1850,6 +1850,7 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const { ast_manager& m = const_cast(*this); + if (decl->is_associative()) { sort * expected = decl->get_domain(0); for (unsigned i = 0; i < num_args; i++) { @@ -1894,7 +1895,18 @@ void ast_manager::check_sorts_core(ast const * n) const { if (n->get_kind() != AST_APP) return; // nothing else to check... app const * a = to_app(n); - check_sort(a->get_decl(), a->get_num_args(), a->get_args()); + func_decl* d = a->get_decl(); + check_sort(d, a->get_num_args(), a->get_args()); + if (a->get_num_args() == 2 && + !d->is_flat_associative() && + d->is_right_associative()) { + check_sorts_core(a->get_arg(1)); + } + if (a->get_num_args() == 2 && + !d->is_flat_associative() && + d->is_left_associative()) { + check_sorts_core(a->get_arg(0)); + } } bool ast_manager::check_sorts(ast const * n) const { diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index eb8aba9ae..1adedb2d7 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -213,6 +213,9 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) { s = to_sort(parameters[0].get_ast()); } + else if (num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()) { + s = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + } else if (range != 0 && is_float_sort(range)) { s = range; } @@ -376,7 +379,19 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); symbol name("asFloat"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + } + else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) { + if (num_parameters != 2) + m_manager->raise_exception("invalid number of parameters to to_fp"); + if (!parameters[0].is_int() || !parameters[1].is_int()) + m_manager->raise_exception("invalid parameter type to to_fp"); + int ebits = parameters[0].get_int(); + int sbits = parameters[1].get_int(); + + sort * fp = mk_float_sort(ebits, sbits); + symbol name("asFloat"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } else { // .. Otherwise we only know how to convert rationals/reals. if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) @@ -412,6 +427,53 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } +func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("fp unsupported; use a logic with BV support"); + if (arity != 3) + m_manager->raise_exception("invalid number of arguments to fp"); + if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) || + !is_sort_of(domain[1], m_bv_fid, BV_SORT) || + !is_sort_of(domain[2], m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismtach"); + + sort * fp = mk_float_sort(domain[1]->get_parameter(0).get_int(), domain[2]->get_parameter(0).get_int() + 1); + symbol name("fp"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k)); +} + +func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("to_fp_unsigned unsupported; use a logic with BV support"); + if (arity != 2) + m_manager->raise_exception("invalid number of arguments to to_fp_unsigned"); + if (is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismtach"); + if (!is_sort_of(domain[1], m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismtach"); + + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + symbol name("to_fp_unsigned"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k)); +} + +func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + +func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + +func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (k) { @@ -465,6 +527,16 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_fused_ma(k, num_parameters, parameters, arity, domain, range); case OP_TO_IEEE_BV: return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_FP: + return mk_from3bv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_FP_UNSIGNED: + return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_UBV: + return mk_to_ubv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_SBV: + return mk_to_sbv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_REAL: + return mk_to_real(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -517,8 +589,9 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co if (m_bv_plugin) op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV)); - // We also support draft version 3 - op_names.push_back(builtin_name("fp", OP_TO_FLOAT)); + // These are the operators from the final draft of the SMT FloatingPoints standard + op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF)); + op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF)); op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN)); op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY)); @@ -547,23 +620,24 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN)); op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN)); op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX)); - op_names.push_back(builtin_name("fp.convert", OP_TO_FLOAT)); + op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT)); if (m_bv_plugin) { - // op_names.push_back(builtin_name("fp.fromBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.fromUBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.fromSBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.toUBv", OP_TO_IEEE_BV)); - // op_names.push_back(builtin_name("fp.toSBv", OP_TO_IEEE_BV)); + op_names.push_back(builtin_name("fp", OP_FLOAT_FP)); + op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED)); + op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV)); + op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV)); } - - op_names.push_back(builtin_name("fp.fromReal", OP_TO_FLOAT)); + // op_names.push_back(builtin_name("fp.toReal", ?)); } void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { sort_names.push_back(builtin_name("FP", FLOAT_SORT)); sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT)); + + // In the SMT FPA final draft, FP is called FloatingPoint + sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT)); } expr * float_decl_plugin::get_some_value(sort * s) { diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index f1b60a91b..3786b76ee 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -72,6 +72,12 @@ enum float_op_kind { OP_TO_FLOAT, OP_TO_IEEE_BV, + + OP_FLOAT_FP, + OP_FLOAT_TO_FP_UNSIGNED, + OP_FLOAT_TO_UBV, + OP_FLOAT_TO_SBV, + OP_FLOAT_TO_REAL, LAST_FLOAT_OP }; @@ -125,7 +131,17 @@ class float_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - + func_decl * mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); void recycled_id(unsigned id); diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 6ef147f1c..ecd06ff38 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -64,6 +64,11 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break; case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; + case OP_FLOAT_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; + case OP_FLOAT_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(args[0], args[1], result); break; + case OP_FLOAT_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break; + case OP_FLOAT_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break; + case OP_FLOAT_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; } return st; } @@ -504,3 +509,42 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) { return BR_FAILED; } + +br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { + bv_util bu(m()); + rational r1, r2, r3; + unsigned bvs1, bvs2, bvs3; + + if (bu.is_numeral(arg1, r1, bvs1) && bu.is_numeral(arg2, r2, bvs2) && bu.is_numeral(arg3, r3, bvs3)) { + SASSERT(m_util.fm().mpz_manager().is_one(r2.to_mpq().denominator())); + SASSERT(m_util.fm().mpz_manager().is_one(r3.to_mpq().denominator())); + SASSERT(m_util.fm().mpz_manager().is_int64(r3.to_mpq().numerator())); + scoped_mpf v(m_util.fm()); + mpf_exp_t biased_exp = m_util.fm().mpz_manager().get_int64(r2.to_mpq().numerator()); + m_util.fm().set(v, bvs2, bvs3 + 1, + r1.is_one(), + r3.to_mpq().numerator(), + m_util.fm().unbias_exp(bvs2, biased_exp)); + TRACE("fp_rewriter", tout << "v = " << m_util.fm().to_string(v) << std::endl;); + result = m_util.mk_value(v); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_real(expr * arg1, expr_ref & result) { + return BR_FAILED; +} \ No newline at end of file diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 4a0879d4b..0f44d227c 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -73,6 +73,12 @@ public: br_status mk_is_sign_minus(expr * arg1, expr_ref & result); br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); + + br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); + br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_real(expr * arg1, expr_ref & result); }; #endif diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index 2a7de3176..7fd44c088 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -114,7 +114,7 @@ static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); - ptr_vector cnsts(end - it); + ptr_vector cnsts((unsigned)(end - it)); for (int i = 0; it != end; ++it, ++i) cnsts[i] = *it; @@ -139,10 +139,11 @@ static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) { get_interpolant_and_maybe_check(ctx,t,m_params,false); } +#if 0 static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) { get_interpolant_and_maybe_check(ctx,t,m_params,true); } - +#endif static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){ diff --git a/src/duality/duality.h b/src/duality/duality.h index 979071639..8c469b9e4 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -36,12 +36,11 @@ namespace Duality { struct Z3User { context &ctx; - solver &slvr; typedef func_decl FuncDecl; typedef expr Term; - Z3User(context &_ctx, solver &_slvr) : ctx(_ctx), slvr(_slvr){} + Z3User(context &_ctx) : ctx(_ctx){} const char *string_of_int(int n); @@ -53,6 +52,8 @@ namespace Duality { Term SubstRec(hash_map &memo, const Term &t); + Term SubstRec(hash_map &memo, hash_map &map, const Term &t); + void Strengthen(Term &x, const Term &y); // return the func_del of an app if it is uninterpreted @@ -77,14 +78,14 @@ namespace Duality { void Summarize(const Term &t); - int CumulativeDecisions(); - int CountOperators(const Term &t); Term SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val); Term RemoveRedundancy(const Term &t); + Term IneqToEq(const Term &t); + bool IsLiteral(const expr &lit, expr &atom, expr &val); expr Negate(const expr &f); @@ -98,7 +99,10 @@ namespace Duality { bool IsClosedFormula(const Term &t); Term AdjustQuantifiers(const Term &t); -private: + + FuncDecl RenumberPred(const FuncDecl &f, int n); + +protected: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); int CountOperatorsRec(hash_set &memo, const Term &t); @@ -108,6 +112,7 @@ private: expr ReduceAndOr(const std::vector &args, bool is_and, std::vector &res); expr FinishAndOr(const std::vector &args, bool is_and); expr PullCommonFactors(std::vector &args, bool is_and); + Term IneqToEqRec(hash_map &memo, const Term &t); }; @@ -256,9 +261,9 @@ private: } #endif - iZ3LogicSolver(context &c) : LogicSolver(c) { + iZ3LogicSolver(context &c, bool models = true) : LogicSolver(c) { ctx = ictx = &c; - slvr = islvr = new interpolating_solver(*ictx); + slvr = islvr = new interpolating_solver(*ictx, models); need_goals = false; islvr->SetWeakInterpolants(true); } @@ -308,8 +313,8 @@ private: } LogicSolver *ls; - - private: + + protected: int nodeCount; int edgeCount; @@ -324,7 +329,7 @@ private: public: model dualModel; - private: + protected: literals dualLabels; std::list stack; std::vector axioms; // only saved here for printing purposes @@ -340,7 +345,7 @@ private: inherit the axioms. */ - RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) + RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) { ls = _ls; nodeCount = 0; @@ -350,7 +355,7 @@ private: proof_core = 0; } - ~RPFP(); + virtual ~RPFP(); /** Symbolic representation of a relational transformer */ class Transformer @@ -574,7 +579,7 @@ private: * you must pop the context accordingly. The second argument is * the number of pushes we are inside. */ - void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); + virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); /* Constrain an edge by the annotation of one of its children. */ @@ -808,9 +813,31 @@ private: /** Edges of the graph. */ std::vector edges; + /** Fuse a vector of transformers. If the total number of inputs of the transformers + is N, then the result is an N-ary transfomer whose output is the union of + the outputs of the given transformers. The is, suppose we have a vetor of transfoermers + {T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer + + F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) = + T_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M)) + */ + + Transformer Fuse(const std::vector &trs); + + /** Fuse edges so that each node is the output of at most one edge. This + transformation is solution-preserving, but changes the numbering of edges in + counterexamples. + */ + void FuseEdges(); + + void RemoveDeadNodes(); + Term SubstParams(const std::vector &from, const std::vector &to, const Term &t); + Term SubstParamsNoCapture(const std::vector &from, + const std::vector &to, const Term &t); + Term Localize(Edge *e, const Term &t); void EvalNodeAsConstraint(Node *p, Transformer &res); @@ -829,7 +856,13 @@ private: */ void ComputeProofCore(); - private: + int CumulativeDecisions(); + + solver &slvr(){ + return *ls->slvr; + } + + protected: void ClearProofCore(){ if(proof_core) @@ -947,6 +980,8 @@ private: expr SimplifyOr(std::vector &lits); + expr SimplifyAnd(std::vector &lits); + void SetAnnotation(Node *root, const expr &t); void AddEdgeToSolver(Edge *edge); @@ -959,9 +994,58 @@ private: expr NegateLit(const expr &f); + expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox); + + bool IsVar(const expr &t); + + void GetVarsRec(hash_set &memo, const expr &cnst, std::vector &vars); + + expr UnhoistPullRec(hash_map & memo, const expr &w, hash_map & init_defs, hash_map & const_params, hash_map &const_params_inv, std::vector &new_params); + + void AddParamsToTransformer(Transformer &trans, const std::vector ¶ms); + + expr AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector ¶ms); + + expr GetRelRec(hash_set &memo, const expr &t, const func_decl &rel); + + expr GetRel(Edge *edge, int child_idx); + + void GetDefs(const expr &cnst, hash_map &defs); + + void GetDefsRec(const expr &cnst, hash_map &defs); + + void AddParamsToNode(Node *node, const std::vector ¶ms); + + void UnhoistLoop(Edge *loop_edge, Edge *init_edge); + + void Unhoist(); + + Term ElimIteRec(hash_map &memo, const Term &t, std::vector &cnsts); + + Term ElimIte(const Term &t); + + void MarkLiveNodes(hash_map > &outgoing, hash_set &live_nodes, Node *node); + + virtual void slvr_add(const expr &e); + + virtual void slvr_pop(int i); + + virtual void slvr_push(); + + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); + + virtual lbool ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); + }; - /** RPFP solver base class. */ + + /** RPFP solver base class. */ class Solver { @@ -1005,6 +1089,8 @@ private: /** Object thrown on cancellation */ struct Canceled {}; + /** Object thrown on incompleteness */ + struct Incompleteness {}; }; } @@ -1042,3 +1128,130 @@ namespace std { } }; } + +// #define LIMIT_STACK_WEIGHT 5 + + +namespace Duality { + /** Caching version of RPFP. Instead of asserting constraints, returns assumption literals */ + + class RPFP_caching : public RPFP { + public: + + /** appends assumption literals for edge to lits. if with_children is true, + includes that annotation of the edge's children. + */ + void AssertEdgeCache(Edge *e, std::vector &lits, bool with_children = false); + + /** appends assumption literals for node to lits */ + void AssertNodeCache(Node *, std::vector lits); + + /** check assumption lits, and return core */ + check_result CheckCore(const std::vector &assumps, std::vector &core); + + /** Clone another RPFP into this one, keeping a map */ + void Clone(RPFP *other); + + /** Get the clone of a node */ + Node *GetNodeClone(Node *other_node); + + /** Get the clone of an edge */ + Edge *GetEdgeClone(Edge *other_edge); + + /** Try to strengthen the parent of an edge */ + void GeneralizeCache(Edge *edge); + + /** Try to propagate some facts from children to parents of edge. + Return true if success. */ + bool PropagateCache(Edge *edge); + + /** Construct a caching RPFP using a LogicSolver */ + RPFP_caching(LogicSolver *_ls) : RPFP(_ls) {} + + /** Constraint an edge by its child's annotation. Return + assumption lits. */ + void ConstrainParentCache(Edge *parent, Node *child, std::vector &lits); + +#ifdef LIMIT_STACK_WEIGHT + virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); +#endif + + virtual ~RPFP_caching(){} + + protected: + hash_map AssumptionLits; + hash_map NodeCloneMap; + hash_map EdgeCloneMap; + std::vector alit_stack; + std::vector alit_stack_sizes; + hash_map > edge_solvers; + +#ifdef LIMIT_STACK_WEIGHT + struct weight_counter { + int val; + weight_counter(){val = 0;} + void swap(weight_counter &other){ + std::swap(val,other.val); + } + }; + + struct big_stack_entry { + weight_counter weight_added; + std::vector new_alits; + std::vector alit_stack; + std::vector alit_stack_sizes; + }; + + std::vector new_alits; + weight_counter weight_added; + std::vector big_stack; +#endif + + + + void GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map = 0); + + void GreedyReduceCache(std::vector &assumps, std::vector &core); + + void FilterCore(std::vector &core, std::vector &full_core); + void ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector &lits); + + virtual void slvr_add(const expr &e); + + virtual void slvr_pop(int i); + + virtual void slvr_push(); + + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); + + virtual lbool ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); + + void GetTermTreeAssertionLiterals(TermTree *assumptions); + + void GetTermTreeAssertionLiteralsRec(TermTree *assumptions); + + LogicSolver *SolverForEdge(Edge *edge, bool models); + + public: + struct scoped_solver_for_edge { + LogicSolver *orig_ls; + RPFP_caching *rpfp; + scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){ + rpfp = _rpfp; + orig_ls = rpfp->ls; + rpfp->ls = rpfp->SolverForEdge(edge,models); + } + ~scoped_solver_for_edge(){ + rpfp->ls = orig_ls; + } + }; + + }; + +} diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp index bec32c51a..a4e9e0240 100755 --- a/src/duality/duality_profiling.cpp +++ b/src/duality/duality_profiling.cpp @@ -25,7 +25,14 @@ Revision History: #include #include +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#endif + #include "duality_wrapper.h" +#include "iz3profiling.h" namespace Duality { @@ -103,6 +110,7 @@ namespace Duality { output_time(*pfs, it->second.t); (*pfs) << std::endl; } + profiling::print(os); // print the interpolation stats } void timer_start(const char *name){ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index a5e2b9167..2d52ab283 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -21,13 +21,21 @@ Revision History: -#include "duality.h" -#include "duality_profiling.h" +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#endif + #include #include #include #include + +#include "duality.h" +#include "duality_profiling.h" + #ifndef WIN32 // #define Z3OPS #endif @@ -104,7 +112,7 @@ namespace Duality { lits.push_back(t); } - int Z3User::CumulativeDecisions(){ + int RPFP::CumulativeDecisions(){ #if 0 std::string stats = Z3_statistics_to_string(ctx); int pos = stats.find("decisions:"); @@ -113,7 +121,7 @@ namespace Duality { std::string val = stats.substr(pos,end-pos); return atoi(val.c_str()); #endif - return slvr.get_num_decisions(); + return slvr().get_num_decisions(); } @@ -370,6 +378,38 @@ namespace Duality { return res; } + Z3User::Term Z3User::SubstRec(hash_map &memo, hash_map &map, const Term &t) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(SubstRec(memo, map, t.arg(i))); + hash_map::iterator it = map.find(f); + if(it != map.end()) + f = it->second; + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + { + std::vector pats; + t.get_patterns(pats); + for(unsigned i = 0; i < pats.size(); i++) + pats[i] = SubstRec(memo, map, pats[i]); + Term body = SubstRec(memo, map, t.body()); + res = clone_quantifier(t, body, pats); + } + // res = CloneQuantifier(t,SubstRec(memo, t.body())); + else res = t; + return res; + } + bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){ if(!(lit.is_quantifier() && IsClosedFormula(lit))){ if(!lit.is_app()) @@ -519,6 +559,20 @@ namespace Duality { const expr &lit = args[i]; expr atom, val; if(IsLiteral(lit,atom,val)){ + if(atom.is_app() && atom.decl().get_decl_kind() == Equal) + if(pol ? eq(val,ctx.bool_val(true)) : eq(val,ctx.bool_val(false))){ + expr lhs = atom.arg(0), rhs = atom.arg(1); + if(lhs.is_numeral()) + std::swap(lhs,rhs); + if(rhs.is_numeral() && lhs.is_app()){ + for(unsigned j = 0; j < args.size(); j++) + if(j != i){ + smemo.clear(); + smemo[lhs] = rhs; + args[j] = SubstRec(smemo,args[j]); + } + } + } for(unsigned j = 0; j < args.size(); j++) if(j != i){ smemo.clear(); @@ -580,6 +634,50 @@ namespace Duality { return t; } + Z3User::Term Z3User::IneqToEqRec(hash_map &memo, const Term &t) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(IneqToEqRec(memo, t.arg(i))); + + decl_kind k = f.get_decl_kind(); + if(k == And){ + for(int i = 0; i < nargs-1; i++){ + if((args[i].is_app() && args[i].decl().get_decl_kind() == Geq && + args[i+1].is_app() && args[i+1].decl().get_decl_kind() == Leq) + || + (args[i].is_app() && args[i].decl().get_decl_kind() == Leq && + args[i+1].is_app() && args[i+1].decl().get_decl_kind() == Geq)) + if(eq(args[i].arg(0),args[i+1].arg(0)) && eq(args[i].arg(1),args[i+1].arg(1))){ + args[i] = ctx.make(Equal,args[i].arg(0),args[i].arg(1)); + args[i+1] = ctx.bool_val(true); + } + } + } + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + { + Term body = IneqToEqRec(memo,t.body()); + res = clone_quantifier(t, body); + } + else res = t; + return res; + } + + Z3User::Term Z3User::IneqToEq(const Term &t){ + hash_map memo; + return IneqToEqRec(memo,t); + } + Z3User::Term Z3User::SubstRecHide(hash_map &memo, const Term &t, int number) { std::pair foo(t,expr(ctx)); @@ -618,6 +716,51 @@ namespace Duality { return some_diff ? SubstRec(memo,t) : t; } + RPFP::Term RPFP::SubstParamsNoCapture(const std::vector &from, + const std::vector &to, const Term &t){ + hash_map memo; + bool some_diff = false; + for(unsigned i = 0; i < from.size(); i++) + if(i < to.size() && !eq(from[i],to[i])){ + memo[from[i]] = to[i]; + // if the new param is not being mapped to anything else, we need to rename it to prevent capture + // note, if the new param *is* mapped later in the list, it will override this substitution + const expr &w = to[i]; + if(memo.find(w) == memo.end()){ + std::string old_name = w.decl().name().str(); + func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), w.get_sort()); + expr y = fresh(); + memo[w] = y; + } + some_diff = true; + } + return some_diff ? SubstRec(memo,t) : t; + } + + + + RPFP::Transformer RPFP::Fuse(const std::vector &trs){ + assert(!trs.empty()); + const std::vector ¶ms = trs[0]->IndParams; + std::vector fmlas(trs.size()); + fmlas[0] = trs[0]->Formula; + for(unsigned i = 1; i < trs.size(); i++) + fmlas[i] = SubstParamsNoCapture(trs[i]->IndParams,params,trs[i]->Formula); + std::vector rel_params = trs[0]->RelParams; + for(unsigned i = 1; i < trs.size(); i++){ + const std::vector ¶ms2 = trs[i]->RelParams; + hash_map map; + for(unsigned j = 0; j < params2.size(); j++){ + func_decl rel = RenumberPred(params2[j],rel_params.size()); + rel_params.push_back(rel); + map[params2[j]] = rel; + } + hash_map memo; + fmlas[i] = SubstRec(memo,map,fmlas[i]); + } + return Transformer(rel_params,params,ctx.make(Or,fmlas),trs[0]->owner); + } + void Z3User::Strengthen(Term &x, const Term &y) { @@ -711,6 +854,33 @@ namespace Duality { #endif + expr RPFP::GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox) + { + if (e->dual.null()) { + timer_start("ReducedDualEdge"); + e->dual = ReducedDualEdge(e); + timer_stop("ReducedDualEdge"); + timer_start("getting children"); + if(underapprox){ + std::vector cus(e->Children.size()); + for(unsigned i = 0; i < e->Children.size(); i++) + cus[i] = !UnderapproxFlag(e->Children[i]) || GetUnderapprox(e->Children[i]); + expr cnst = conjoin(cus); + e->dual = e->dual && cnst; + } + timer_stop("getting children"); + timer_start("Persisting"); + std::list::reverse_iterator it = stack.rbegin(); + for(int i = 0; i < persist && it != stack.rend(); i++) + it++; + if(it != stack.rend()) + it->edges.push_back(e); + timer_stop("Persisting"); + //Console.WriteLine("{0}", cnst); + } + return e->dual; + } + /** For incremental solving, asserts the constraint associated * with this edge in the SMT context. If this edge is removed, * you must pop the context accordingly. The second argument is @@ -732,45 +902,240 @@ namespace Duality { { if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) return; - if (e->dual.null()) - { - timer_start("ReducedDualEdge"); - e->dual = ReducedDualEdge(e); - timer_stop("ReducedDualEdge"); - timer_start("getting children"); - if(with_children) - for(unsigned i = 0; i < e->Children.size(); i++) - e->dual = e->dual && GetAnnotation(e->Children[i]); - if(underapprox){ - std::vector cus(e->Children.size()); - for(unsigned i = 0; i < e->Children.size(); i++) - cus[i] = !UnderapproxFlag(e->Children[i]) || GetUnderapprox(e->Children[i]); - expr cnst = conjoin(cus); - e->dual = e->dual && cnst; - } - timer_stop("getting children"); - timer_start("Persisting"); - std::list::reverse_iterator it = stack.rbegin(); - for(int i = 0; i < persist && it != stack.rend(); i++) - it++; - if(it != stack.rend()) - it->edges.push_back(e); -#if 0 - if(persist != 0) - Z3_persist_ast(ctx,e->dual,persist); -#endif - timer_stop("Persisting"); - //Console.WriteLine("{0}", cnst); - } + expr fmla = GetEdgeFormula(e, persist, with_children, underapprox); timer_start("solver add"); - slvr.add(e->dual); + slvr_add(e->dual); timer_stop("solver add"); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParent(e,e->Children[i]); + } + + +#ifdef LIMIT_STACK_WEIGHT + void RPFP_caching::AssertEdge(Edge *e, int persist, bool with_children, bool underapprox) + { + unsigned old_new_alits = new_alits.size(); + if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) + return; + expr fmla = GetEdgeFormula(e, persist, with_children, underapprox); + timer_start("solver add"); + slvr_add(e->dual); + timer_stop("solver add"); + if(old_new_alits < new_alits.size()) + weight_added.val++; + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParent(e,e->Children[i]); + } +#endif + + // caching verion of above + void RPFP_caching::AssertEdgeCache(Edge *e, std::vector &lits, bool with_children){ + if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) + return; + expr fmla = GetEdgeFormula(e, 0, with_children, false); + GetAssumptionLits(fmla,lits); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParentCache(e,e->Children[i],lits); + } + + void RPFP::slvr_add(const expr &e){ + slvr().add(e); + } + + void RPFP_caching::slvr_add(const expr &e){ + GetAssumptionLits(e,alit_stack); + } + + void RPFP::slvr_pop(int i){ + slvr().pop(i); + } + + void RPFP::slvr_push(){ + slvr().push(); + } + + void RPFP_caching::slvr_pop(int i){ + for(int j = 0; j < i; j++){ +#ifdef LIMIT_STACK_WEIGHT + if(alit_stack_sizes.empty()){ + if(big_stack.empty()) + throw "stack underflow"; + for(unsigned k = 0; k < new_alits.size(); k++){ + if(AssumptionLits.find(new_alits[k]) == AssumptionLits.end()) + throw "foo!"; + AssumptionLits.erase(new_alits[k]); + } + big_stack_entry &bsb = big_stack.back(); + bsb.alit_stack_sizes.swap(alit_stack_sizes); + bsb.alit_stack.swap(alit_stack); + bsb.new_alits.swap(new_alits); + bsb.weight_added.swap(weight_added); + big_stack.pop_back(); + slvr().pop(1); + continue; + } +#endif + alit_stack.resize(alit_stack_sizes.back()); + alit_stack_sizes.pop_back(); + } + } + + void RPFP_caching::slvr_push(){ +#ifdef LIMIT_STACK_WEIGHT + if(weight_added.val > LIMIT_STACK_WEIGHT){ + big_stack.resize(big_stack.size()+1); + big_stack_entry &bsb = big_stack.back(); + bsb.alit_stack_sizes.swap(alit_stack_sizes); + bsb.alit_stack.swap(alit_stack); + bsb.new_alits.swap(new_alits); + bsb.weight_added.swap(weight_added); + slvr().push(); + for(unsigned i = 0; i < bsb.alit_stack.size(); i++) + slvr().add(bsb.alit_stack[i]); + return; + } +#endif + alit_stack_sizes.push_back(alit_stack.size()); + } + + check_result RPFP::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ + return slvr().check(n, assumptions, core_size, core); + } + + check_result RPFP_caching::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ + unsigned oldsiz = alit_stack.size(); + if(n && assumptions) + std::copy(assumptions,assumptions+n,std::inserter(alit_stack,alit_stack.end())); + check_result res; + if(core_size && core){ + std::vector full_core(alit_stack.size()), core1(n); + std::copy(assumptions,assumptions+n,core1.begin()); + res = slvr().check(alit_stack.size(), &alit_stack[0], core_size, &full_core[0]); + full_core.resize(*core_size); + if(res == unsat){ + FilterCore(core1,full_core); + *core_size = core1.size(); + std::copy(core1.begin(),core1.end(),core); + } + } + else + res = slvr().check(alit_stack.size(), &alit_stack[0]); + alit_stack.resize(oldsiz); + return res; + } + + lbool RPFP::ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals, + bool weak){ + return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak); + } + + lbool RPFP_caching::ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals, + bool weak){ + GetTermTreeAssertionLiterals(assumptions); + return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak); + } + + void RPFP_caching::GetTermTreeAssertionLiteralsRec(TermTree *assumptions){ + std::vector alits; + hash_map map; + GetAssumptionLits(assumptions->getTerm(),alits,&map); + std::vector &ts = assumptions->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + GetAssumptionLits(ts[i],alits,&map); + assumptions->setTerm(ctx.bool_val(true)); + ts = alits; + for(unsigned i = 0; i < alits.size(); i++) + ts.push_back(ctx.make(Implies,alits[i],map[alits[i]])); + for(unsigned i = 0; i < assumptions->getChildren().size(); i++) + GetTermTreeAssertionLiterals(assumptions->getChildren()[i]); + return; + } + + void RPFP_caching::GetTermTreeAssertionLiterals(TermTree *assumptions){ + // optimize binary case + if(assumptions->getChildren().size() == 1 + && assumptions->getChildren()[0]->getChildren().size() == 0){ + hash_map map; + TermTree *child = assumptions->getChildren()[0]; + std::vector dummy; + GetAssumptionLits(child->getTerm(),dummy,&map); + std::vector &ts = child->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + GetAssumptionLits(ts[i],dummy,&map); + std::vector assumps; + slvr().get_proof().get_assumptions(assumps); + if(!proof_core){ // save the proof core for later use + proof_core = new hash_set; + for(unsigned i = 0; i < assumps.size(); i++) + proof_core->insert(assumps[i]); + } + std::vector *cnsts[2] = {&child->getTerms(),&assumptions->getTerms()}; + for(unsigned i = 0; i < assumps.size(); i++){ + expr &ass = assumps[i]; + expr alit = (ass.is_app() && ass.decl().get_decl_kind() == Implies) ? ass.arg(0) : ass; + bool isA = map.find(alit) != map.end(); + cnsts[isA ? 0 : 1]->push_back(ass); + } + } + else + GetTermTreeAssertionLiteralsRec(assumptions); + } + + void RPFP::AddToProofCore(hash_set &core){ + std::vector assumps; + slvr().get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++) + core.insert(assumps[i]); + } + + void RPFP::ComputeProofCore(){ + if(!proof_core){ + proof_core = new hash_set; + AddToProofCore(*proof_core); + } + } + + + void RPFP_caching::GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map){ + std::vector conjs; + CollectConjuncts(fmla,conjs); + for(unsigned i = 0; i < conjs.size(); i++){ + const expr &conj = conjs[i]; + std::pair foo(conj,expr(ctx)); + std::pair::iterator, bool> bar = AssumptionLits.insert(foo); + Term &res = bar.first->second; + if(bar.second){ + func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort()); + res = pred(); +#ifdef LIMIT_STACK_WEIGHT + new_alits.push_back(conj); +#endif + slvr().add(ctx.make(Implies,res,conj)); + // std::cout << res << ": " << conj << "\n"; + } + if(opt_map) + (*opt_map)[res] = conj; + lits.push_back(res); + } } void RPFP::ConstrainParent(Edge *parent, Node *child){ ConstrainEdgeLocalized(parent,GetAnnotation(child)); } + void RPFP_caching::ConstrainParentCache(Edge *parent, Node *child, std::vector &lits){ + ConstrainEdgeLocalizedCache(parent,GetAnnotation(child),lits); + } + /** For incremental solving, asserts the negation of the upper bound associated * with a node. @@ -782,10 +1147,60 @@ namespace Duality { { n->dual = GetUpperBound(n); stack.back().nodes.push_back(n); - slvr.add(n->dual); + slvr_add(n->dual); } } + // caching version of above + void RPFP_caching::AssertNodeCache(Node *n, std::vector lits){ + if (n->dual.null()) + { + n->dual = GetUpperBound(n); + stack.back().nodes.push_back(n); + GetAssumptionLits(n->dual,lits); + } + } + + /** Clone another RPFP into this one, keeping a map */ + void RPFP_caching::Clone(RPFP *other){ +#if 0 + for(unsigned i = 0; i < other->nodes.size(); i++) + NodeCloneMap[other->nodes[i]] = CloneNode(other->nodes[i]); +#endif + for(unsigned i = 0; i < other->edges.size(); i++){ + Edge *edge = other->edges[i]; + Node *parent = CloneNode(edge->Parent); + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++) + // cs.push_back(NodeCloneMap[edge->Children[j]]); + cs.push_back(CloneNode(edge->Children[j])); + EdgeCloneMap[edge] = CreateEdge(parent,edge->F,cs); + } + } + + /** Get the clone of a node */ + RPFP::Node *RPFP_caching::GetNodeClone(Node *other_node){ + return NodeCloneMap[other_node]; + } + + /** Get the clone of an edge */ + RPFP::Edge *RPFP_caching::GetEdgeClone(Edge *other_edge){ + return EdgeCloneMap[other_edge]; + } + + /** check assumption lits, and return core */ + check_result RPFP_caching::CheckCore(const std::vector &assumps, std::vector &core){ + core.resize(assumps.size()); + unsigned core_size; + check_result res = slvr().check(assumps.size(),(expr *)&assumps[0],&core_size,&core[0]); + if(res == unsat) + core.resize(core_size); + else + core.clear(); + return res; + } + + /** Assert a constraint on an edge in the SMT context. */ @@ -799,9 +1214,15 @@ namespace Duality { { e->constraints.push_back(tl); stack.back().constraints.push_back(std::pair(e,tl)); - slvr.add(tl); + slvr_add(tl); } + void RPFP_caching::ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector &lits) + { + e->constraints.push_back(tl); + stack.back().constraints.push_back(std::pair(e,tl)); + GetAssumptionLits(tl,lits); + } /** Declare a constant in the background theory. */ @@ -829,7 +1250,7 @@ namespace Duality { void RPFP::RemoveAxiom(const Term &t) { - slvr.RemoveInterpolationAxiom(t); + slvr().RemoveInterpolationAxiom(t); } #endif @@ -878,7 +1299,7 @@ namespace Duality { // if (dualLabels != null) dualLabels.Dispose(); timer_start("interpolate_tree"); - lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals,true); + lbool res = ls_interpolate_tree(tree, interpolant, dualModel,goals,true); timer_stop("interpolate_tree"); if (res == l_false) { @@ -924,7 +1345,7 @@ namespace Duality { ClearProofCore(); timer_start("interpolate_tree"); - lbool res = ls->interpolate_tree(tree, interpolant, dualModel,0,true); + lbool res = ls_interpolate_tree(tree, interpolant, dualModel,0,true); timer_stop("interpolate_tree"); if (res == l_false) { @@ -970,26 +1391,27 @@ namespace Duality { check_result RPFP::Check(Node *root, std::vector underapproxes, std::vector *underapprox_core ) { + timer_start("Check"); ClearProofCore(); // if (dualModel != null) dualModel.Dispose(); check_result res; if(!underapproxes.size()) - res = slvr.check(); + res = slvr_check(); else { std::vector us(underapproxes.size()); for(unsigned i = 0; i < underapproxes.size(); i++) us[i] = UnderapproxFlag(underapproxes[i]); - slvr.check(); // TODO: no idea why I need to do this + slvr_check(); // TODO: no idea why I need to do this if(underapprox_core){ std::vector unsat_core(us.size()); unsigned core_size = 0; - res = slvr.check(us.size(),&us[0],&core_size,&unsat_core[0]); + res = slvr_check(us.size(),&us[0],&core_size,&unsat_core[0]); underapprox_core->resize(core_size); for(unsigned i = 0; i < core_size; i++) (*underapprox_core)[i] = UnderapproxFlagRev(unsat_core[i]); } else { - res = slvr.check(us.size(),&us[0]); + res = slvr_check(us.size(),&us[0]); bool dump = false; if(dump){ std::vector cnsts; @@ -999,17 +1421,20 @@ namespace Duality { ls->write_interpolation_problem("temp.smt",cnsts,std::vector()); } } - // check_result temp = slvr.check(); + // check_result temp = slvr_check(); } - dualModel = slvr.get_model(); + dualModel = slvr().get_model(); + timer_stop("Check"); return res; } check_result RPFP::CheckUpdateModel(Node *root, std::vector assumps){ - // check_result temp1 = slvr.check(); // no idea why I need to do this + // check_result temp1 = slvr_check(); // no idea why I need to do this ClearProofCore(); - check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]); - dualModel = slvr.get_model(); + check_result res = slvr_check(assumps.size(),&assumps[0]); + model mod = slvr().get_model(); + if(!mod.null()) + dualModel = mod;; return res; } @@ -1022,8 +1447,6 @@ namespace Duality { return dualModel.eval(tl); } - - /** Returns true if the given node is empty in the primal solution. For proecudure summaries, this means that the procedure is not called in the current counter-model. */ @@ -1301,7 +1724,7 @@ namespace Duality { } } /* Unreachable! */ - throw "error in RPFP::GetLabelsRec"; + // throw "error in RPFP::GetLabelsRec"; goto done; } else if(k == Not) { @@ -1470,6 +1893,57 @@ namespace Duality { return res; } + RPFP::Term RPFP::ElimIteRec(hash_map &memo, const Term &t, std::vector &cnsts){ + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(bar.second){ + if(t.is_app()){ + int nargs = t.num_args(); + std::vector args; + if(t.decl().get_decl_kind() == Equal){ + expr lhs = t.arg(0); + expr rhs = t.arg(1); + if(rhs.decl().get_decl_kind() == Ite){ + expr rhs_args[3]; + lhs = ElimIteRec(memo,lhs,cnsts); + for(int i = 0; i < 3; i++) + rhs_args[i] = ElimIteRec(memo,rhs.arg(i),cnsts); + res = (rhs_args[0] && (lhs == rhs_args[1])) || ((!rhs_args[0]) && (lhs == rhs_args[2])); + goto done; + } + } + if(t.decl().get_decl_kind() == Ite){ + func_decl sym = ctx.fresh_func_decl("@ite", t.get_sort()); + res = sym(); + cnsts.push_back(ElimIteRec(memo,ctx.make(Equal,res,t),cnsts)); + } + else { + for(int i = 0; i < nargs; i++) + args.push_back(ElimIteRec(memo,t.arg(i),cnsts)); + res = t.decl()(args.size(),&args[0]); + } + } + else if(t.is_quantifier()) + res = clone_quantifier(t,ElimIteRec(memo,t.body(),cnsts)); + else + res = t; + } + done: + return res; + } + + RPFP::Term RPFP::ElimIte(const Term &t){ + hash_map memo; + std::vector cnsts; + expr res = ElimIteRec(memo,t,cnsts); + if(!cnsts.empty()){ + cnsts.push_back(res); + res = ctx.make(And,cnsts); + } + return res; + } + void RPFP::Implicant(hash_map &memo, const Term &f, std::vector &lits, hash_set &dont_cares){ hash_set done[2]; ImplicantRed(memo,f,lits,done,true, dont_cares); @@ -1927,10 +2401,14 @@ namespace Duality { for(int i = 0; i < num_args; i++) CollectConjuncts(f.arg(i),lits,false); } - else if(pos) - lits.push_back(f); - else - lits.push_back(!f); + else if(pos){ + if(!eq(f,ctx.bool_val(true))) + lits.push_back(f); + } + else { + if(!eq(f,ctx.bool_val(false))) + lits.push_back(!f); + } } struct TermLt { @@ -2253,6 +2731,45 @@ namespace Duality { } } + void RPFP_caching::FilterCore(std::vector &core, std::vector &full_core){ + hash_set core_set; + std::copy(full_core.begin(),full_core.end(),std::inserter(core_set,core_set.begin())); + std::vector new_core; + for(unsigned i = 0; i < core.size(); i++) + if(core_set.find(core[i]) != core_set.end()) + new_core.push_back(core[i]); + core.swap(new_core); + } + + void RPFP_caching::GreedyReduceCache(std::vector &assumps, std::vector &core){ + std::vector lits = assumps, full_core; + std::copy(core.begin(),core.end(),std::inserter(lits,lits.end())); + + // verify + check_result res = CheckCore(lits,full_core); + if(res != unsat) + throw "should be unsat"; + FilterCore(core,full_core); + + std::vector dummy; + if(CheckCore(full_core,dummy) != unsat) + throw "should be unsat"; + + for(unsigned i = 0; i < core.size(); ){ + expr temp = core[i]; + std::swap(core[i],core.back()); + core.pop_back(); + lits.resize(assumps.size()); + std::copy(core.begin(),core.end(),std::inserter(lits,lits.end())); + res = CheckCore(lits,full_core); + if(res != unsat){ + core.push_back(temp); + std::swap(core[i],core.back()); + i++; + } + } + } + expr RPFP::NegateLit(const expr &f){ if(f.is_app() && f.decl().get_decl_kind() == Not) return f.arg(0); @@ -2278,6 +2795,14 @@ namespace Duality { return ctx.make(Or,lits); } + expr RPFP::SimplifyAnd(std::vector &lits){ + if(lits.size() == 0) + return ctx.bool_val(true); + if(lits.size() == 1) + return lits[0]; + return ctx.make(And,lits); + } + // set up edge constraint in aux solver void RPFP::AddEdgeToSolver(Edge *edge){ if(!edge->dual.null()) @@ -2289,6 +2814,7 @@ namespace Duality { } void RPFP::InterpolateByCases(Node *root, Node *node){ + bool axioms_added = false; aux_solver.push(); AddEdgeToSolver(node->Outgoing); node->Annotation.SetEmpty(); @@ -2320,15 +2846,25 @@ namespace Duality { std::vector case_lits; itp = StrengthenFormulaByCaseSplitting(itp, case_lits); SetAnnotation(node,itp); + node->Annotation.Formula = node->Annotation.Formula.simplify(); } if(node->Annotation.IsEmpty()){ - std::cout << "bad in InterpolateByCase -- core:\n"; - std::vector assumps; - slvr.get_proof().get_assumptions(assumps); - for(unsigned i = 0; i < assumps.size(); i++) - assumps[i].show(); - throw "ack!"; + if(!axioms_added){ + // add the axioms in the off chance they are useful + const std::vector &theory = ls->get_axioms(); + for(unsigned i = 0; i < theory.size(); i++) + aux_solver.add(theory[i]); + axioms_added = true; + } + else { + std::cout << "bad in InterpolateByCase -- core:\n"; + std::vector assumps; + slvr().get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++) + assumps[i].show(); + throw "ack!"; + } } Pop(1); node->Annotation.UnionWith(old_annot); @@ -2340,6 +2876,7 @@ namespace Duality { } void RPFP::Generalize(Node *root, Node *node){ + timer_start("Generalize"); aux_solver.push(); AddEdgeToSolver(node->Outgoing); expr fmla = GetAnnotation(node); @@ -2349,21 +2886,135 @@ namespace Duality { aux_solver.pop(1); NegateLits(conjuncts); SetAnnotation(node,SimplifyOr(conjuncts)); + timer_stop("Generalize"); } + RPFP::LogicSolver *RPFP_caching::SolverForEdge(Edge *edge, bool models){ + uptr &p = edge_solvers[edge]; + if(!p.get()){ + scoped_no_proof no_proofs_please(ctx.m()); // no proofs + p.set(new iZ3LogicSolver(ctx,models)); // no models + } + return p.get(); + } + + + // caching version of above + void RPFP_caching::GeneralizeCache(Edge *edge){ + timer_start("Generalize"); + scoped_solver_for_edge ssfe(this,edge); + Node *node = edge->Parent; + std::vector assumps, core, conjuncts; + AssertEdgeCache(edge,assumps); + for(unsigned i = 0; i < edge->Children.size(); i++){ + expr ass = GetAnnotation(edge->Children[i]); + std::vector clauses; + if(!ass.is_true()){ + CollectConjuncts(ass.arg(1),clauses); + for(unsigned j = 0; j < clauses.size(); j++) + GetAssumptionLits(ass.arg(0) || clauses[j],assumps); + } + } + expr fmla = GetAnnotation(node); + std::vector lits; + if(fmla.is_true()){ + timer_stop("Generalize"); + return; + } + assumps.push_back(fmla.arg(0).arg(0)); + CollectConjuncts(!fmla.arg(1),lits); +#if 0 + for(unsigned i = 0; i < lits.size(); i++){ + const expr &lit = lits[i]; + if(lit.is_app() && lit.decl().get_decl_kind() == Equal){ + lits[i] = ctx.make(Leq,lit.arg(0),lit.arg(1)); + lits.push_back(ctx.make(Leq,lit.arg(1),lit.arg(0))); + } + } +#endif + hash_map lit_map; + for(unsigned i = 0; i < lits.size(); i++) + GetAssumptionLits(lits[i],core,&lit_map); + GreedyReduceCache(assumps,core); + for(unsigned i = 0; i < core.size(); i++) + conjuncts.push_back(lit_map[core[i]]); + NegateLits(conjuncts); + SetAnnotation(node,SimplifyOr(conjuncts)); + timer_stop("Generalize"); + } + + // caching version of above + bool RPFP_caching::PropagateCache(Edge *edge){ + timer_start("PropagateCache"); + scoped_solver_for_edge ssfe(this,edge); + bool some = false; + { + std::vector candidates, skip; + Node *node = edge->Parent; + CollectConjuncts(node->Annotation.Formula,skip); + for(unsigned i = 0; i < edge->Children.size(); i++){ + Node *child = edge->Children[i]; + if(child->map == node->map){ + CollectConjuncts(child->Annotation.Formula,candidates); + break; + } + } + if(candidates.empty()) goto done; + hash_set skip_set; + std::copy(skip.begin(),skip.end(),std::inserter(skip_set,skip_set.begin())); + std::vector new_candidates; + for(unsigned i = 0; i < candidates.size(); i++) + if(skip_set.find(candidates[i]) == skip_set.end()) + new_candidates.push_back(candidates[i]); + candidates.swap(new_candidates); + if(candidates.empty()) goto done; + std::vector assumps, core, conjuncts; + AssertEdgeCache(edge,assumps); + for(unsigned i = 0; i < edge->Children.size(); i++){ + expr ass = GetAnnotation(edge->Children[i]); + if(eq(ass,ctx.bool_val(true))) + continue; + std::vector clauses; + CollectConjuncts(ass.arg(1),clauses); + for(unsigned j = 0; j < clauses.size(); j++) + GetAssumptionLits(ass.arg(0) || clauses[j],assumps); + } + for(unsigned i = 0; i < candidates.size(); i++){ + unsigned old_size = assumps.size(); + node->Annotation.Formula = candidates[i]; + expr fmla = GetAnnotation(node); + assumps.push_back(fmla.arg(0).arg(0)); + GetAssumptionLits(!fmla.arg(1),assumps); + std::vector full_core; + check_result res = CheckCore(assumps,full_core); + if(res == unsat) + conjuncts.push_back(candidates[i]); + assumps.resize(old_size); + } + if(conjuncts.empty()) + goto done; + SetAnnotation(node,SimplifyAnd(conjuncts)); + some = true; + } + done: + timer_stop("PropagateCache"); + return some; + } + + /** Push a scope. Assertions made after Push can be undone by Pop. */ void RPFP::Push() { stack.push_back(stack_entry()); - slvr.push(); + slvr_push(); } /** Pop a scope (see Push). Note, you cannot pop axioms. */ void RPFP::Pop(int num_scopes) { - slvr.pop(num_scopes); + slvr_pop(num_scopes); for (int i = 0; i < num_scopes; i++) { stack_entry &back = stack.back(); @@ -2381,15 +3032,15 @@ namespace Duality { all the popped constraints */ void RPFP::PopPush(){ - slvr.pop(1); - slvr.push(); + slvr_pop(1); + slvr_push(); stack_entry &back = stack.back(); for(std::list::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it) - slvr.add((*it)->dual); + slvr_add((*it)->dual); for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) - slvr.add((*it)->dual); + slvr_add((*it)->dual); for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) - slvr.add((*it).second); + slvr_add((*it).second); } @@ -2407,6 +3058,17 @@ namespace Duality { return ctx.function(name.c_str(), nargs, &sorts[0], t.get_sort()); } + Z3User::FuncDecl Z3User::RenumberPred(const FuncDecl &f, int n) + { + std::string name = f.name().str(); + name = name.substr(0,name.rfind('_')) + "_" + string_of_int(n); + int arity = f.arity(); + std::vector domain; + for(int i = 0; i < arity; i++) + domain.push_back(f.domain(i)); + return ctx.function(name.c_str(), arity, &domain[0], f.range()); + } + // Scan the clause body for occurrences of the predicate unknowns RPFP::Term RPFP::ScanBody(hash_map &memo, @@ -2453,7 +3115,7 @@ namespace Duality { bool Z3User::is_variable(const Term &t){ if(!t.is_app()) - return false; + return t.is_var(); return t.decl().get_decl_kind() == Uninterpreted && t.num_args() == 0; } @@ -2602,6 +3264,8 @@ namespace Duality { arg.decl().get_decl_kind() == Uninterpreted); } +#define USE_QE_LITE + void RPFP::FromClauses(const std::vector &unskolemized_clauses){ hash_map pmap; func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort()); @@ -2609,6 +3273,7 @@ namespace Duality { std::vector clauses(unskolemized_clauses); // first, skolemize the clauses +#ifndef USE_QE_LITE for(unsigned i = 0; i < clauses.size(); i++){ expr &t = clauses[i]; if (t.is_quantifier() && t.is_quantifier_forall()) { @@ -2625,11 +3290,32 @@ namespace Duality { t = SubstBound(subst,t.body()); } } +#else + std::vector > substs(clauses.size()); +#endif // create the nodes from the heads of the clauses for(unsigned i = 0; i < clauses.size(); i++){ Term &clause = clauses[i]; + +#ifdef USE_QE_LITE + Term &t = clause; + if (t.is_quantifier() && t.is_quantifier_forall()) { + int bound = t.get_quantifier_num_bound(); + std::vector sorts; + std::vector names; + for(int j = 0; j < bound; j++){ + sort the_sort = t.get_quantifier_bound_sort(j); + symbol name = t.get_quantifier_bound_name(j); + expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort)); + substs[i][bound-1-j] = skolem; + } + clause = t.body(); + } + +#endif + if(clause.is_app() && clause.decl().get_decl_kind() == Uninterpreted) clause = implies(ctx.bool_val(true),clause); if(!canonical_clause(clause)) @@ -2661,6 +3347,13 @@ namespace Duality { seen.insert(arg); Indparams.push_back(arg); } +#ifdef USE_QE_LITE + { + hash_map > sb_memo; + for(unsigned j = 0; j < Indparams.size(); j++) + Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]); + } +#endif Node *node = CreateNode(R(Indparams.size(),&Indparams[0])); //nodes.push_back(node); pmap[R] = node; @@ -2704,17 +3397,346 @@ namespace Duality { Term labeled = body; std::vector lbls; // TODO: throw this away for now body = RemoveLabels(body,lbls); + // body = IneqToEq(body); // UFO converts x=y to (x<=y & x >= y). Undo this. body = body.simplify(); +#ifdef USE_QE_LITE + std::set idxs; + for(unsigned j = 0; j < Indparams.size(); j++) + if(Indparams[j].is_var()) + idxs.insert(Indparams[j].get_index_value()); + body = body.qe_lite(idxs,false); + hash_map > sb_memo; + body = SubstBoundRec(sb_memo,substs[i],0,body); + for(unsigned j = 0; j < Indparams.size(); j++) + Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]); +#endif + // Create the edge Transformer T = CreateTransformer(Relparams,Indparams,body); Edge *edge = CreateEdge(Parent,T,Children); edge->labeled = labeled;; // remember for label extraction // edges.push_back(edge); } + + // undo hoisting of expressions out of loops + RemoveDeadNodes(); + Unhoist(); + // FuseEdges(); } + // The following mess is used to undo hoisting of expressions outside loops by compilers + + expr RPFP::UnhoistPullRec(hash_map & memo, const expr &w, hash_map & init_defs, hash_map & const_params, hash_map &const_params_inv, std::vector &new_params){ + if(memo.find(w) != memo.end()) + return memo[w]; + expr res; + if(init_defs.find(w) != init_defs.end()){ + expr d = init_defs[w]; + std::vector vars; + hash_set get_vars_memo; + GetVarsRec(get_vars_memo,d,vars); + hash_map map; + for(unsigned j = 0; j < vars.size(); j++){ + expr x = vars[j]; + map[x] = UnhoistPullRec(memo,x,init_defs,const_params,const_params_inv,new_params); + } + expr defn = SubstRec(map,d); + res = defn; + } + else if(const_params_inv.find(w) == const_params_inv.end()){ + std::string old_name = w.decl().name().str(); + func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), w.get_sort()); + expr y = fresh(); + const_params[y] = w; + const_params_inv[w] = y; + new_params.push_back(y); + res = y; + } + else + res = const_params_inv[w]; + memo[w] = res; + return res; + } + + void RPFP::AddParamsToTransformer(Transformer &trans, const std::vector ¶ms){ + std::copy(params.begin(),params.end(),std::inserter(trans.IndParams,trans.IndParams.end())); + } + + expr RPFP::AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector ¶ms){ + int n = app.num_args(); + std::vector args(n); + for (int i = 0; i < n; i++) + args[i] = app.arg(i); + std::copy(params.begin(),params.end(),std::inserter(args,args.end())); + return new_decl(args); + } + + expr RPFP::GetRelRec(hash_set &memo, const expr &t, const func_decl &rel){ + if(memo.find(t) != memo.end()) + return expr(); + memo.insert(t); + if (t.is_app()) + { + func_decl f = t.decl(); + if(f == rel) + return t; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++){ + expr res = GetRelRec(memo,t.arg(i),rel); + if(!res.null()) + return res; + } + } + else if (t.is_quantifier()) + return GetRelRec(memo,t.body(),rel); + return expr(); + } + + expr RPFP::GetRel(Edge *edge, int child_idx){ + func_decl &rel = edge->F.RelParams[child_idx]; + hash_set memo; + return GetRelRec(memo,edge->F.Formula,rel); + } + + void RPFP::GetDefsRec(const expr &cnst, hash_map &defs){ + if(cnst.is_app()){ + switch(cnst.decl().get_decl_kind()){ + case And: { + int n = cnst.num_args(); + for(int i = 0; i < n; i++) + GetDefsRec(cnst.arg(i),defs); + break; + } + case Equal: { + expr lhs = cnst.arg(0); + expr rhs = cnst.arg(1); + if(IsVar(lhs)) + defs[lhs] = rhs; + break; + } + default: + break; + } + } + } + + void RPFP::GetDefs(const expr &cnst, hash_map &defs){ + // GetDefsRec(IneqToEq(cnst),defs); + GetDefsRec(cnst,defs); + } + + bool RPFP::IsVar(const expr &t){ + return t.is_app() && t.num_args() == 0 && t.decl().get_decl_kind() == Uninterpreted; + } + + void RPFP::GetVarsRec(hash_set &memo, const expr &t, std::vector &vars){ + if(memo.find(t) != memo.end()) + return; + memo.insert(t); + if (t.is_app()) + { + if(IsVar(t)){ + vars.push_back(t); + return; + } + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++){ + GetVarsRec(memo,t.arg(i),vars); + } + } + else if (t.is_quantifier()) + GetVarsRec(memo,t.body(),vars); + } + + void RPFP::AddParamsToNode(Node *node, const std::vector ¶ms){ + int arity = node->Annotation.IndParams.size(); + std::vector domain; + for(int i = 0; i < arity; i++) + domain.push_back(node->Annotation.IndParams[i].get_sort()); + for(unsigned i = 0; i < params.size(); i++) + domain.push_back(params[i].get_sort()); + std::string old_name = node->Name.name().str(); + func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), domain, ctx.bool_sort()); + node->Name = fresh; + AddParamsToTransformer(node->Annotation,params); + AddParamsToTransformer(node->Bound,params); + AddParamsToTransformer(node->Underapprox,params); + } + + void RPFP::UnhoistLoop(Edge *loop_edge, Edge *init_edge){ + loop_edge->F.Formula = IneqToEq(loop_edge->F.Formula); + init_edge->F.Formula = IneqToEq(init_edge->F.Formula); + expr pre = GetRel(loop_edge,0); + if(pre.null()) + return; // this means the loop got simplified away + int nparams = loop_edge->F.IndParams.size(); + hash_map const_params, const_params_inv; + std::vector work_list; + // find the parameters that are constant in the loop + for(int i = 0; i < nparams; i++){ + if(eq(pre.arg(i),loop_edge->F.IndParams[i])){ + const_params[pre.arg(i)] = init_edge->F.IndParams[i]; + const_params_inv[init_edge->F.IndParams[i]] = pre.arg(i); + work_list.push_back(pre.arg(i)); + } + } + // get the definitions in the initialization + hash_map defs,memo,subst; + GetDefs(init_edge->F.Formula,defs); + // try to pull them inside the loop + std::vector new_params; + for(unsigned i = 0; i < work_list.size(); i++){ + expr v = work_list[i]; + expr w = const_params[v]; + expr def = UnhoistPullRec(memo,w,defs,const_params,const_params_inv,new_params); + if(!eq(def,v)) + subst[v] = def; + } + // do the substitutions + if(subst.empty()) + return; + subst[pre] = pre; // don't substitute inside the precondition itself + loop_edge->F.Formula = SubstRec(subst,loop_edge->F.Formula); + loop_edge->F.Formula = ElimIte(loop_edge->F.Formula); + init_edge->F.Formula = ElimIte(init_edge->F.Formula); + // add the new parameters + if(new_params.empty()) + return; + Node *parent = loop_edge->Parent; + AddParamsToNode(parent,new_params); + AddParamsToTransformer(loop_edge->F,new_params); + AddParamsToTransformer(init_edge->F,new_params); + std::vector &incoming = parent->Incoming; + for(unsigned i = 0; i < incoming.size(); i++){ + Edge *in_edge = incoming[i]; + std::vector &chs = in_edge->Children; + for(unsigned j = 0; j < chs.size(); j++) + if(chs[j] == parent){ + expr lit = GetRel(in_edge,j); + expr new_lit = AddParamsToApp(lit,parent->Name,new_params); + func_decl fd = SuffixFuncDecl(new_lit,j); + int nargs = new_lit.num_args(); + std::vector args; + for(int k = 0; k < nargs; k++) + args.push_back(new_lit.arg(k)); + new_lit = fd(nargs,&args[0]); + in_edge->F.RelParams[j] = fd; + hash_map map; + map[lit] = new_lit; + in_edge->F.Formula = SubstRec(map,in_edge->F.Formula); + } + } + } + + void RPFP::Unhoist(){ + hash_map > outgoing; + for(unsigned i = 0; i < edges.size(); i++) + outgoing[edges[i]->Parent].push_back(edges[i]); + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + std::vector &outs = outgoing[node]; + // if we're not a simple loop with one entry, give up + if(outs.size() == 2){ + for(int j = 0; j < 2; j++){ + Edge *loop_edge = outs[j]; + Edge *init_edge = outs[1-j]; + if(loop_edge->Children.size() == 1 && loop_edge->Children[0] == loop_edge->Parent){ + UnhoistLoop(loop_edge,init_edge); + break; + } + } + } + } + } + + void RPFP::FuseEdges(){ + hash_map > outgoing; + for(unsigned i = 0; i < edges.size(); i++){ + outgoing[edges[i]->Parent].push_back(edges[i]); + } + hash_set edges_to_delete; + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + std::vector &outs = outgoing[node]; + if(outs.size() > 1 && outs.size() <= 16){ + std::vector trs(outs.size()); + for(unsigned j = 0; j < outs.size(); j++) + trs[j] = &outs[j]->F; + Transformer tr = Fuse(trs); + std::vector chs; + for(unsigned j = 0; j < outs.size(); j++) + for(unsigned k = 0; k < outs[j]->Children.size(); k++) + chs.push_back(outs[j]->Children[k]); + CreateEdge(node,tr,chs); + for(unsigned j = 0; j < outs.size(); j++) + edges_to_delete.insert(outs[j]); + } + } + std::vector new_edges; + hash_set all_nodes; + for(unsigned j = 0; j < edges.size(); j++){ + if(edges_to_delete.find(edges[j]) == edges_to_delete.end()){ +#if 0 + if(all_nodes.find(edges[j]->Parent) != all_nodes.end()) + throw "help!"; + all_nodes.insert(edges[j]->Parent); +#endif + new_edges.push_back(edges[j]); + } + else + delete edges[j]; + } + edges.swap(new_edges); + } + + void RPFP::MarkLiveNodes(hash_map > &outgoing, hash_set &live_nodes, Node *node){ + if(live_nodes.find(node) != live_nodes.end()) + return; + live_nodes.insert(node); + std::vector &outs = outgoing[node]; + for(unsigned i = 0; i < outs.size(); i++) + for(unsigned j = 0; j < outs[i]->Children.size(); j++) + MarkLiveNodes(outgoing, live_nodes,outs[i]->Children[j]); + } + + void RPFP::RemoveDeadNodes(){ + hash_map > outgoing; + for(unsigned i = 0; i < edges.size(); i++) + outgoing[edges[i]->Parent].push_back(edges[i]); + hash_set live_nodes; + for(unsigned i = 0; i < nodes.size(); i++) + if(!nodes[i]->Bound.IsFull()) + MarkLiveNodes(outgoing,live_nodes,nodes[i]); + std::vector new_edges; + for(unsigned j = 0; j < edges.size(); j++){ + if(live_nodes.find(edges[j]->Parent) != live_nodes.end()) + new_edges.push_back(edges[j]); + else { + Edge *edge = edges[j]; + for(unsigned int i = 0; i < edge->Children.size(); i++){ + std::vector &ic = edge->Children[i]->Incoming; + for(std::vector::iterator it = ic.begin(), en = ic.end(); it != en; ++it){ + if(*it == edge){ + ic.erase(it); + break; + } + } + } + delete edge; + } + } + edges.swap(new_edges); + std::vector new_nodes; + for(unsigned j = 0; j < nodes.size(); j++){ + if(live_nodes.find(nodes[j]) != live_nodes.end()) + new_nodes.push_back(nodes[j]); + else + delete nodes[j]; + } + nodes.swap(new_nodes); + } void RPFP::WriteSolution(std::ostream &s){ for(unsigned i = 0; i < nodes.size(); i++){ @@ -2854,26 +3876,26 @@ namespace Duality { } - void RPFP::AddToProofCore(hash_set &core){ - std::vector assumps; - slvr.get_proof().get_assumptions(assumps); - for(unsigned i = 0; i < assumps.size(); i++) - core.insert(assumps[i]); + + bool RPFP::proof_core_contains(const expr &e){ + return proof_core->find(e) != proof_core->end(); } - - void RPFP::ComputeProofCore(){ - if(!proof_core){ - proof_core = new hash_set; - AddToProofCore(*proof_core); - } + + bool RPFP_caching::proof_core_contains(const expr &e){ + std::vector foo; + GetAssumptionLits(e,foo); + for(unsigned i = 0; i < foo.size(); i++) + if(proof_core->find(foo[i]) != proof_core->end()) + return true; + return false; } bool RPFP::EdgeUsedInProof(Edge *edge){ ComputeProofCore(); - if(!edge->dual.null() && proof_core->find(edge->dual) != proof_core->end()) + if(!edge->dual.null() && proof_core_contains(edge->dual)) return true; for(unsigned i = 0; i < edge->constraints.size(); i++) - if(proof_core->find(edge->constraints[i]) != proof_core->end()) + if(proof_core_contains(edge->constraints[i])) return true; return false; } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 13c839186..973ad769c 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -19,6 +19,12 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#endif + #include "duality.h" #include "duality_profiling.h" @@ -26,6 +32,7 @@ Revision History: #include #include #include +#include // TODO: make these official options or get rid of them @@ -37,14 +44,18 @@ Revision History: #define MINIMIZE_CANDIDATES // #define MINIMIZE_CANDIDATES_HARDER #define BOUNDED -#define CHECK_CANDS_FROM_IND_SET +// #define CHECK_CANDS_FROM_IND_SET #define UNDERAPPROX_NODES #define NEW_EXPAND #define EARLY_EXPAND // #define TOP_DOWN // #define EFFORT_BOUNDED_STRAT #define SKIP_UNDERAPPROX_NODES - +#define USE_RPFP_CLONE +// #define KEEP_EXPANSIONS +// #define USE_CACHING_RPFP +// #define PROPAGATE_BEFORE_CHECK +#define USE_NEW_GEN_CANDS namespace Duality { @@ -101,7 +112,7 @@ namespace Duality { public: Duality(RPFP *_rpfp) : ctx(_rpfp->ctx), - slvr(_rpfp->slvr), + slvr(_rpfp->slvr()), nodes(_rpfp->nodes), edges(_rpfp->edges) { @@ -115,8 +126,42 @@ namespace Duality { Report = false; StratifiedInlining = false; RecursionBound = -1; + { + scoped_no_proof no_proofs_please(ctx.m()); +#ifdef USE_RPFP_CLONE + clone_ls = new RPFP::iZ3LogicSolver(ctx, false); // no models needed for this one + clone_rpfp = new RPFP_caching(clone_ls); + clone_rpfp->Clone(rpfp); +#endif +#ifdef USE_NEW_GEN_CANDS + gen_cands_ls = new RPFP::iZ3LogicSolver(ctx); + gen_cands_rpfp = new RPFP_caching(gen_cands_ls); + gen_cands_rpfp->Clone(rpfp); +#endif + } } + ~Duality(){ +#ifdef USE_RPFP_CLONE + delete clone_rpfp; + delete clone_ls; +#endif +#ifdef USE_NEW_GEN_CANDS + delete gen_cands_rpfp; + delete gen_cands_ls; +#endif + } + +#ifdef USE_RPFP_CLONE + RPFP::LogicSolver *clone_ls; + RPFP_caching *clone_rpfp; +#endif +#ifdef USE_NEW_GEN_CANDS + RPFP::LogicSolver *gen_cands_ls; + RPFP_caching *gen_cands_rpfp; +#endif + + typedef RPFP::Node Node; typedef RPFP::Edge Edge; @@ -804,8 +849,10 @@ namespace Duality { Node *child = chs[i]; if(TopoSort[child] < TopoSort[node->map]){ Node *leaf = LeafMap[child]; - if(!indset->Contains(leaf)) + if(!indset->Contains(leaf)){ + node->Outgoing->F.Formula = ctx.bool_val(false); // make this a proper leaf, else bogus cex return node->Outgoing; + } } } @@ -1085,7 +1132,8 @@ namespace Duality { void ExtractCandidateFromCex(Edge *edge, RPFP *checker, Node *root, Candidate &candidate){ candidate.edge = edge; for(unsigned j = 0; j < edge->Children.size(); j++){ - Edge *lb = root->Outgoing->Children[j]->Outgoing; + Node *node = root->Outgoing->Children[j]; + Edge *lb = node->Outgoing; std::vector &insts = insts_of_node[edge->Children[j]]; #ifndef MINIMIZE_CANDIDATES for(int k = insts.size()-1; k >= 0; k--) @@ -1095,8 +1143,8 @@ namespace Duality { { Node *inst = insts[k]; if(indset->Contains(inst)){ - if(checker->Empty(lb->Parent) || - eq(checker->Eval(lb,NodeMarker(inst)),ctx.bool_val(true))){ + if(checker->Empty(node) || + eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){ candidate.Children.push_back(inst); goto next_child; } @@ -1166,6 +1214,25 @@ namespace Duality { #endif + Node *CheckerForEdgeClone(Edge *edge, RPFP_caching *checker){ + Edge *gen_cands_edge = checker->GetEdgeClone(edge); + Node *root = gen_cands_edge->Parent; + root->Outgoing = gen_cands_edge; + GenNodeSolutionFromIndSet(edge->Parent, root->Bound); +#if 0 + if(root->Bound.IsFull()) + return = 0; +#endif + checker->AssertNode(root); + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = gen_cands_edge->Children[j]; + GenNodeSolutionWithMarkers(oc,nc->Annotation,true); + } + checker->AssertEdge(gen_cands_edge,1,true); + return root; + } + /** If the current proposed solution is not inductive, use the induction failure to generate candidates for extension. */ void GenCandidatesFromInductionFailure(bool full_scan = false){ @@ -1175,6 +1242,7 @@ namespace Duality { Edge *edge = edges[i]; if(!full_scan && updated_nodes.find(edge->Parent) == updated_nodes.end()) continue; +#ifndef USE_NEW_GEN_CANDS slvr.push(); RPFP *checker = new RPFP(rpfp->ls); Node *root = CheckerForEdge(edge,checker); @@ -1186,6 +1254,18 @@ namespace Duality { } slvr.pop(1); delete checker; +#else + RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */); + gen_cands_rpfp->Push(); + Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp); + if(gen_cands_rpfp->Check(root) != unsat){ + Candidate candidate; + ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate); + reporter->InductionFailure(edge,candidate.Children); + candidates.push_back(candidate); + } + gen_cands_rpfp->Pop(1); +#endif } updated_nodes.clear(); timer_stop("GenCandIndFail"); @@ -1309,6 +1389,9 @@ namespace Duality { node. */ bool SatisfyUpperBound(Node *node){ if(node->Bound.IsFull()) return true; +#ifdef PROPAGATE_BEFORE_CHECK + Propagate(); +#endif reporter->Bound(node); int start_decs = rpfp->CumulativeDecisions(); DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand); @@ -1412,13 +1495,77 @@ namespace Duality { } } + // Propagate conjuncts up the unwinding + void Propagate(){ + reporter->Message("beginning propagation"); + timer_start("Propagate"); + std::vector sorted_nodes = unwinding->nodes; + std::sort(sorted_nodes.begin(),sorted_nodes.end(),std::less()); // sorts by sequence number + hash_map > facts; + for(unsigned i = 0; i < sorted_nodes.size(); i++){ + Node *node = sorted_nodes[i]; + std::set &node_facts = facts[node->map]; + if(!(node->Outgoing && indset->Contains(node))) + continue; + std::vector conj_vec; + unwinding->CollectConjuncts(node->Annotation.Formula,conj_vec); + std::set conjs; + std::copy(conj_vec.begin(),conj_vec.end(),std::inserter(conjs,conjs.begin())); + if(!node_facts.empty()){ + RPFP *checker = new RPFP(rpfp->ls); + slvr.push(); + Node *root = checker->CloneNode(node); + Edge *edge = node->Outgoing; + // checker->AssertNode(root); + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = checker->CloneNode(oc); + nc->Annotation = oc->Annotation; // is this needed? + cs.push_back(nc); + } + Edge *checker_edge = checker->CreateEdge(root,edge->F,cs); + checker->AssertEdge(checker_edge, 0, true, false); + std::vector propagated; + for(std::set ::iterator it = node_facts.begin(), en = node_facts.end(); it != en;){ + const expr &fact = *it; + if(conjs.find(fact) == conjs.end()){ + root->Bound.Formula = fact; + slvr.push(); + checker->AssertNode(root); + check_result res = checker->Check(root); + slvr.pop(); + if(res != unsat){ + std::set ::iterator victim = it; + ++it; + node_facts.erase(victim); // if it ain't true, nix it + continue; + } + propagated.push_back(fact); + } + ++it; + } + slvr.pop(); + for(unsigned i = 0; i < propagated.size(); i++){ + root->Annotation.Formula = propagated[i]; + UpdateNodeToNode(node,root); + } + delete checker; + } + for(std::set ::iterator it = conjs.begin(), en = conjs.end(); it != en; ++it){ + expr foo = *it; + node_facts.insert(foo); + } + } + timer_stop("Propagate"); + } /** This class represents a derivation tree. */ class DerivationTree { public: DerivationTree(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) - : slvr(rpfp->slvr), + : slvr(rpfp->slvr()), ctx(rpfp->ctx) { duality = _duality; @@ -1462,7 +1609,13 @@ namespace Duality { constrained = _constrained; false_approx = true; timer_start("Derive"); +#ifndef USE_CACHING_RPFP tree = _tree ? _tree : new RPFP(rpfp->ls); +#else + RPFP::LogicSolver *cache_ls = new RPFP::iZ3LogicSolver(ctx); + cache_ls->slvr->push(); + tree = _tree ? _tree : new RPFP_caching(cache_ls); +#endif tree->HornClauses = rpfp->HornClauses; tree->Push(); // so we can clear out the solver later when finished top = CreateApproximatedInstance(root); @@ -1474,19 +1627,28 @@ namespace Duality { timer_start("Pop"); tree->Pop(1); timer_stop("Pop"); +#ifdef USE_CACHING_RPFP + cache_ls->slvr->pop(1); + delete cache_ls; + tree->ls = rpfp->ls; +#endif timer_stop("Derive"); return res; } #define WITH_CHILDREN - Node *CreateApproximatedInstance(RPFP::Node *from){ - Node *to = tree->CloneNode(from); - to->Annotation = from->Annotation; + void InitializeApproximatedInstance(RPFP::Node *to){ + to->Annotation = to->map->Annotation; #ifndef WITH_CHILDREN tree->CreateLowerBoundEdge(to); #endif leaves.push_back(to); + } + + Node *CreateApproximatedInstance(RPFP::Node *from){ + Node *to = tree->CloneNode(from); + InitializeApproximatedInstance(to); return to; } @@ -1555,13 +1717,23 @@ namespace Duality { virtual void ExpandNode(RPFP::Node *p){ // tree->RemoveEdge(p->Outgoing); - Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); - std::vector &cs = edge->Children; - std::vector children(cs.size()); - for(unsigned i = 0; i < cs.size(); i++) - children[i] = CreateApproximatedInstance(cs[i]); - Edge *ne = tree->CreateEdge(p, p->map->Outgoing->F, children); - ne->map = p->map->Outgoing->map; + Edge *ne = p->Outgoing; + if(ne) { + // reporter->Message("Recycling edge..."); + std::vector &cs = ne->Children; + for(unsigned i = 0; i < cs.size(); i++) + InitializeApproximatedInstance(cs[i]); + // ne->dual = expr(); + } + else { + Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); + std::vector &cs = edge->Children; + std::vector children(cs.size()); + for(unsigned i = 0; i < cs.size(); i++) + children[i] = CreateApproximatedInstance(cs[i]); + ne = tree->CreateEdge(p, p->map->Outgoing->F, children); + ne->map = p->map->Outgoing->map; + } #ifndef WITH_CHILDREN tree->AssertEdge(ne); // assert the edge in the solver #else @@ -1703,12 +1875,25 @@ namespace Duality { void RemoveExpansion(RPFP::Node *p){ Edge *edge = p->Outgoing; Node *parent = edge->Parent; +#ifndef KEEP_EXPANSIONS std::vector cs = edge->Children; tree->DeleteEdge(edge); for(unsigned i = 0; i < cs.size(); i++) tree->DeleteNode(cs[i]); +#endif leaves.push_back(parent); } + + // remove all the descendants of tree root (but not root itself) + void RemoveTree(RPFP *tree, RPFP::Node *root){ + Edge *edge = root->Outgoing; + std::vector cs = edge->Children; + tree->DeleteEdge(edge); + for(unsigned i = 0; i < cs.size(); i++){ + RemoveTree(tree,cs[i]); + tree->DeleteNode(cs[i]); + } + } }; class DerivationTreeSlow : public DerivationTree { @@ -1730,13 +1915,14 @@ namespace Duality { virtual bool Build(){ - stack.back().level = tree->slvr.get_scope_level(); + stack.back().level = tree->slvr().get_scope_level(); + bool was_sat = true; while (true) { lbool res; - unsigned slvr_level = tree->slvr.get_scope_level(); + unsigned slvr_level = tree->slvr().get_scope_level(); if(slvr_level != stack.back().level) throw "stacks out of sync!"; @@ -1756,14 +1942,22 @@ namespace Duality { tree->SolveSingleNode(top,node); if(expansions.size() == 1 && NodeTooComplicated(node)) SimplifyNode(node); - tree->Generalize(top,node); + else + node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); + Generalize(node); if(RecordUpdate(node)) update_count++; + else + heuristic->Update(node->map); // make it less likely to expand this node in future } - if(update_count == 0) + if(update_count == 0){ + if(was_sat) + throw Incompleteness(); reporter->Message("backtracked without learning"); + } } tree->ComputeProofCore(); // need to compute the proof core before popping solver + bool propagated = false; while(1) { std::vector &expansions = stack.back().expansions; bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop @@ -1787,28 +1981,42 @@ namespace Duality { RemoveExpansion(node); } stack.pop_back(); - if(prev_level_used || stack.size() == 1) break; + if(stack.size() == 1)break; + if(prev_level_used){ + Node *node = stack.back().expansions[0]; + if(!Propagate(node)) break; + if(!RecordUpdate(node)) break; // shouldn't happen! + RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list + propagated = true; + continue; + } + if(propagated) break; // propagation invalidates the proof core, so disable non-chron backtrack RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list std::vector &unused_ex = stack.back().expansions; for(unsigned i = 0; i < unused_ex.size(); i++) heuristic->Update(unused_ex[i]->map); // make it less likely to expand this node in future } HandleUpdatedNodes(); - if(stack.size() == 1) + if(stack.size() == 1){ + if(top->Outgoing) + tree->DeleteEdge(top->Outgoing); // in case we kept the tree return false; + } + was_sat = false; } else { + was_sat = true; tree->Push(); std::vector &expansions = stack.back().expansions; for(unsigned i = 0; i < expansions.size(); i++){ tree->FixCurrentState(expansions[i]->Outgoing); } #if 0 - if(tree->slvr.check() == unsat) + if(tree->slvr().check() == unsat) throw "help!"; #endif stack.push_back(stack_entry()); - stack.back().level = tree->slvr.get_scope_level(); + stack.back().level = tree->slvr().get_scope_level(); if(ExpandSomeNodes(false,1)){ continue; } @@ -1822,13 +2030,18 @@ namespace Duality { } bool NodeTooComplicated(Node *node){ + int ops = tree->CountOperators(node->Annotation.Formula); + if(ops > 10) return true; + node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); return tree->CountOperators(node->Annotation.Formula) > 3; } void SimplifyNode(Node *node){ // have to destroy the old proof to get a new interpolant + timer_start("SimplifyNode"); tree->PopPush(); tree->InterpolateByCases(top,node); + timer_stop("SimplifyNode"); } bool LevelUsedInProof(unsigned level){ @@ -1927,6 +2140,39 @@ namespace Duality { throw "can't unmap node"; } + void Generalize(Node *node){ +#ifndef USE_RPFP_CLONE + tree->Generalize(top,node); +#else + RPFP_caching *clone_rpfp = duality->clone_rpfp; + if(!node->Outgoing->map) return; + Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map); + Node *clone_node = clone_edge->Parent; + clone_node->Annotation = node->Annotation; + for(unsigned i = 0; i < clone_edge->Children.size(); i++) + clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation; + clone_rpfp->GeneralizeCache(clone_edge); + node->Annotation = clone_node->Annotation; +#endif + } + + bool Propagate(Node *node){ +#ifdef USE_RPFP_CLONE + RPFP_caching *clone_rpfp = duality->clone_rpfp; + Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map); + Node *clone_node = clone_edge->Parent; + clone_node->Annotation = node->map->Annotation; + for(unsigned i = 0; i < clone_edge->Children.size(); i++) + clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation; + bool res = clone_rpfp->PropagateCache(clone_edge); + if(res) + node->Annotation = clone_node->Annotation; + return res; +#else + return false; +#endif + } + }; @@ -1948,6 +2194,11 @@ namespace Duality { Duality *parent; bool some_updates; +#define NO_CONJ_ON_SIMPLE_LOOPS +#ifdef NO_CONJ_ON_SIMPLE_LOOPS + hash_set simple_loops; +#endif + Node *&covered_by(Node *node){ return cm[node].covered_by; } @@ -1982,6 +2233,24 @@ namespace Duality { Covering(Duality *_parent){ parent = _parent; some_updates = false; + +#ifdef NO_CONJ_ON_SIMPLE_LOOPS + hash_map > outgoing; + for(unsigned i = 0; i < parent->rpfp->edges.size(); i++) + outgoing[parent->rpfp->edges[i]->Parent].push_back(parent->rpfp->edges[i]); + for(unsigned i = 0; i < parent->rpfp->nodes.size(); i++){ + Node * node = parent->rpfp->nodes[i]; + std::vector &outs = outgoing[node]; + if(outs.size() == 2){ + for(int j = 0; j < 2; j++){ + Edge *loop_edge = outs[j]; + if(loop_edge->Children.size() == 1 && loop_edge->Children[0] == loop_edge->Parent) + simple_loops.insert(node); + } + } + } +#endif + } bool IsCoveredRec(hash_set &memo, Node *node){ @@ -2144,6 +2413,11 @@ namespace Duality { } bool CouldCover(Node *covered, Node *covering){ +#ifdef NO_CONJ_ON_SIMPLE_LOOPS + // Forsimple loops, we rely on propagation, not covering + if(simple_loops.find(covered->map) != simple_loops.end()) + return false; +#endif #ifdef UNDERAPPROX_NODES // if(parent->underapprox_map.find(covering) != parent->underapprox_map.end()) // return parent->underapprox_map[covering] == covered; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 55883202f..cf2c803cb 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -18,6 +18,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "duality_wrapper.h" #include #include "smt_solver.h" @@ -30,10 +37,11 @@ Revision History: namespace Duality { - solver::solver(Duality::context& c, bool extensional) : object(c), the_model(c) { + solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) { params_ref p; p.set_bool("proof", true); // this is currently useless - p.set_bool("model", true); + if(models) + p.set_bool("model", true); p.set_bool("unsat_core", true); p.set_bool("mbqi",true); p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants @@ -44,6 +52,7 @@ namespace Duality { m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); m_solver->updt_params(p); // why do we have to do this? canceled = false; + m_mode = m().proof_mode(); } expr context::constant(const std::string &name, const sort &ty){ @@ -338,6 +347,17 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return ctx().cook(result); } + expr expr::qe_lite(const std::set &idxs, bool index_of_bound) const { + ::qe_lite qe(m()); + expr_ref result(to_expr(raw()),m()); + proof_ref pf(m()); + uint_set uis; + for(std::set::const_iterator it=idxs.begin(), en = idxs.end(); it != en; ++it) + uis.insert(*it); + qe(uis,index_of_bound,result); + return ctx().cook(result); + } + expr clone_quantifier(const expr &q, const expr &b){ return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw()))); } @@ -362,6 +382,18 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st } + unsigned func_decl::arity() const { + return (to_func_decl(raw())->get_arity()); + } + + sort func_decl::domain(unsigned i) const { + return sort(ctx(),(to_func_decl(raw())->get_domain(i))); + } + + sort func_decl::range() const { + return sort(ctx(),(to_func_decl(raw())->get_range())); + } + func_decl context::fresh_func_decl(char const * prefix, const std::vector &domain, sort const & range){ std::vector < ::sort * > _domain(domain.size()); for(unsigned i = 0; i < domain.size(); i++) @@ -504,7 +536,10 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st add(linear_assumptions[i][j]); } - check_result res = check(); + check_result res = unsat; + + if(!m_solver->get_proof()) + res = check(); if(res == unsat){ diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 3515194c0..891c4ca6f 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -26,6 +26,7 @@ Revision History: #include #include #include +#include #include"version.h" #include @@ -50,6 +51,7 @@ Revision History: #include"scoped_ctrl_c.h" #include"cancel_eh.h" #include"scoped_timer.h" +#include"scoped_proof.h" namespace Duality { @@ -449,6 +451,7 @@ namespace Duality { bool is_datatype() const { return get_sort().is_datatype(); } bool is_relation() const { return get_sort().is_relation(); } bool is_finite_domain() const { return get_sort().is_finite_domain(); } + bool is_true() const {return is_app() && decl().get_decl_kind() == True; } bool is_numeral() const { return is_app() && decl().get_decl_kind() == OtherArith && m().is_unique_value(to_expr(raw())); @@ -560,6 +563,8 @@ namespace Duality { expr qe_lite() const; + expr qe_lite(const std::set &idxs, bool index_of_bound) const; + friend expr clone_quantifier(const expr &, const expr &); friend expr clone_quantifier(const expr &q, const expr &b, const std::vector &patterns); @@ -718,6 +723,7 @@ namespace Duality { m_model = s; return *this; } + bool null() const {return !m_model;} expr eval(expr const & n, bool model_completion=true) const { ::model * _m = m_model.get(); @@ -811,8 +817,9 @@ namespace Duality { ::solver *m_solver; model the_model; bool canceled; + proof_gen_mode m_mode; public: - solver(context & c, bool extensional = false); + solver(context & c, bool extensional = false, bool models = true); solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;} ~solver() { @@ -824,6 +831,7 @@ namespace Duality { m_ctx = s.m_ctx; m_solver = s.m_solver; the_model = s.the_model; + m_mode = s.m_mode; return *this; } struct cancel_exception {}; @@ -832,11 +840,12 @@ namespace Duality { throw(cancel_exception()); } // void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); } - void push() { m_solver->push(); } - void pop(unsigned n = 1) { m_solver->pop(n); } + void push() { scoped_proof_mode spm(m(),m_mode); m_solver->push(); } + void pop(unsigned n = 1) { scoped_proof_mode spm(m(),m_mode); m_solver->pop(n); } // void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } - void add(expr const & e) { m_solver->assert_expr(e); } + void add(expr const & e) { scoped_proof_mode spm(m(),m_mode); m_solver->assert_expr(e); } check_result check() { + scoped_proof_mode spm(m(),m_mode); checkpoint(); lbool r = m_solver->check_sat(0,0); model_ref m; @@ -845,6 +854,7 @@ namespace Duality { return to_check_result(r); } check_result check_keep_model(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + scoped_proof_mode spm(m(),m_mode); model old_model(the_model); check_result res = check(n,assumptions,core_size,core); if(the_model == 0) @@ -852,6 +862,7 @@ namespace Duality { return res; } check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + scoped_proof_mode spm(m(),m_mode); checkpoint(); std::vector< ::expr *> _assumptions(n); for (unsigned i = 0; i < n; i++) { @@ -876,6 +887,7 @@ namespace Duality { } #if 0 check_result check(expr_vector assumptions) { + scoped_proof_mode spm(m(),m_mode); unsigned n = assumptions.size(); z3array _assumptions(n); for (unsigned i = 0; i < n; i++) { @@ -900,17 +912,19 @@ namespace Duality { int get_num_decisions(); void cancel(){ + scoped_proof_mode spm(m(),m_mode); canceled = true; if(m_solver) m_solver->cancel(); } - unsigned get_scope_level(){return m_solver->get_scope_level();} + unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();} void show(); void show_assertion_ids(); proof get_proof(){ + scoped_proof_mode spm(m(),m_mode); return proof(ctx(),m_solver->get_proof()); } @@ -1294,8 +1308,8 @@ namespace Duality { class interpolating_solver : public solver { public: - interpolating_solver(context &ctx) - : solver(ctx) + interpolating_solver(context &ctx, bool models = true) + : solver(ctx, true, models) { weak_mode = false; } @@ -1359,6 +1373,21 @@ namespace Duality { typedef double clock_t; clock_t current_time(); inline void output_time(std::ostream &os, clock_t time){os << time;} + + template class uptr { + public: + X *ptr; + uptr(){ptr = 0;} + void set(X *_ptr){ + if(ptr) delete ptr; + ptr = _ptr; + } + X *get(){ return ptr;} + ~uptr(){ + if(ptr) delete ptr; + } + }; + }; // to make Duality::ast hashable @@ -1393,6 +1422,18 @@ namespace std { }; } +// to make Duality::ast usable in ordered collections +namespace std { + template <> + class less { + public: + bool operator()(const Duality::expr &s, const Duality::expr &t) const { + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + // to make Duality::func_decl hashable namespace hash_space { template <> @@ -1425,6 +1466,5 @@ namespace std { }; } - #endif diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index f316c22cf..26146bfa3 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -18,6 +18,12 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif #include "iz3base.h" #include diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp index b4e55af20..d423ba48f 100755 --- a/src/interp/iz3checker.cpp +++ b/src/interp/iz3checker.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3base.h" #include "iz3checker.h" diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index 75d9aa604..94f282265 100755 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -66,7 +66,7 @@ Revision History: namespace stl_ext { template <> class hash { - stl_ext::hash H; + stl_ext::hash H; public: size_t operator()(const std::string &s) const { return H(s.c_str()); diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 56dc1ccec..c204cc35d 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -18,6 +18,14 @@ Revision History: --*/ /* Copyright 2011 Microsoft Research. */ + +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include #include #include diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index f35dae93f..6664cd2fe 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -18,6 +18,15 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#pragma warning(disable:4805) +#pragma warning(disable:4800) +#endif + #include "iz3mgr.h" #include @@ -172,7 +181,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ std::vector names; - std::vector types; + std::vector types; std::vector bound_asts; unsigned num_bound = bvs.size(); @@ -485,7 +494,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& coeffs){ get_farkas_coeffs(proof,rats); coeffs.resize(rats.size()); for(unsigned i = 0; i < rats.size(); i++){ - sort *is = m().mk_sort(m_arith_fid, INT_SORT); + class sort *is = m().mk_sort(m_arith_fid, INT_SORT); ast coeff = cook(m_arith_util.mk_numeral(rats[i],is)); coeffs[i] = coeff; } @@ -640,9 +649,9 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector &coeffs, const std::vector &ineqs){ +iz3mgr::ast iz3mgr::sum_inequalities(const std::vector &coeffs, const std::vector &ineqs, bool round_off){ ast zero = make_int("0"); ast thing = make(Leq,zero,zero); for(unsigned i = 0; i < ineqs.size(); i++){ - linear_comb(thing,coeffs[i],ineqs[i]); + linear_comb(thing,coeffs[i],ineqs[i], round_off); } thing = simplify_ineq(thing); return thing; diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 645c72ccb..e974a199b 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -22,6 +22,7 @@ Revision History: #include +#include #include "iz3hash.h" #include"well_sorted.h" @@ -262,6 +263,7 @@ class iz3mgr { default:; } assert(0); + return 0; } ast arg(const ast &t, int i){ @@ -606,9 +608,9 @@ class iz3mgr { return d; } - void linear_comb(ast &P, const ast &c, const ast &Q); + void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false); - ast sum_inequalities(const std::vector &coeffs, const std::vector &ineqs); + ast sum_inequalities(const std::vector &coeffs, const std::vector &ineqs, bool round_off = false); ast simplify_ineq(const ast &ineq){ ast res = make(op(ineq),arg(ineq,0),z3_simplify(arg(ineq,1))); diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp index df6fcaf53..31b375c0f 100644 --- a/src/interp/iz3pp.cpp +++ b/src/interp/iz3pp.cpp @@ -58,20 +58,20 @@ namespace stl_ext { class free_func_visitor { ast_manager& m; func_decl_set m_funcs; - obj_hashtable m_sorts; + obj_hashtable m_sorts; public: free_func_visitor(ast_manager& m): m(m) {} void operator()(var * n) { } void operator()(app * n) { m_funcs.insert(n->get_decl()); - sort* s = m.get_sort(n); + class sort* s = m.get_sort(n); if (s->get_family_id() == null_family_id) { m_sorts.insert(s); } } void operator()(quantifier * n) { } func_decl_set& funcs() { return m_funcs; } - obj_hashtable& sorts() { return m_sorts; } + obj_hashtable& sorts() { return m_sorts; } }; class iz3pp_helper : public iz3mgr { @@ -146,8 +146,8 @@ void iz3pp(ast_manager &m, func_decl_set &funcs = visitor.funcs(); func_decl_set::iterator it = funcs.begin(), end = funcs.end(); - obj_hashtable& sorts = visitor.sorts(); - obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); + obj_hashtable& sorts = visitor.sorts(); + obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); diff --git a/src/interp/iz3profiling.cpp b/src/interp/iz3profiling.cpp index 262254271..2c4a31d58 100755 --- a/src/interp/iz3profiling.cpp +++ b/src/interp/iz3profiling.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3profiling.h" #include diff --git a/src/interp/iz3proof.cpp b/src/interp/iz3proof.cpp index 968a4b25a..3fefea73f 100755 --- a/src/interp/iz3proof.cpp +++ b/src/interp/iz3proof.cpp @@ -18,6 +18,12 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif #include "iz3proof.h" #include "iz3profiling.h" diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 75d14bca1..61ed78463 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3proof_itp.h" #ifndef WIN32 @@ -2170,7 +2177,8 @@ class iz3proof_itp_impl : public iz3proof_itp { for(unsigned i = 0; i < prem_cons.size(); i++){ const ast &lit = prem_cons[i]; if(get_term_type(lit) == LitA) - linear_comb(thing,coeffs[i],lit); + // Farkas rule seems to assume strict integer inequalities are rounded + linear_comb(thing,coeffs[i],lit,true /*round_off*/); } thing = simplify_ineq(thing); for(unsigned i = 0; i < prem_cons.size(); i++){ @@ -2195,9 +2203,9 @@ class iz3proof_itp_impl : public iz3proof_itp { /** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */ - void linear_comb(ast &P, const ast &c, const ast &Q){ + void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false){ ast Qrhs; - bool strict = op(P) == Lt; + bool qstrict = false; if(is_not(Q)){ ast nQ = arg(Q,0); switch(op(nQ)){ @@ -2209,11 +2217,11 @@ class iz3proof_itp_impl : public iz3proof_itp { break; case Geq: Qrhs = make(Sub,arg(nQ,1),arg(nQ,0)); - strict = true; + qstrict = true; break; case Leq: Qrhs = make(Sub,arg(nQ,0),arg(nQ,1)); - strict = true; + qstrict = true; break; default: throw proof_error(); @@ -2229,17 +2237,20 @@ class iz3proof_itp_impl : public iz3proof_itp { break; case Lt: Qrhs = make(Sub,arg(Q,1),arg(Q,0)); - strict = true; + qstrict = true; break; case Gt: Qrhs = make(Sub,arg(Q,0),arg(Q,1)); - strict = true; + qstrict = true; break; default: throw proof_error(); } } Qrhs = make(Times,c,Qrhs); + bool pstrict = op(P) == Lt, strict = pstrict || qstrict; + if(pstrict && qstrict && round_off) + Qrhs = make(Sub,Qrhs,make_int(rational(1))); if(strict) P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs)); else diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index fae914292..6a1b665cf 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3translate.h" #include "iz3proof.h" #include "iz3profiling.h" @@ -1079,7 +1086,7 @@ public: my_cons.push_back(mk_not(arg(con,i))); my_coeffs.push_back(farkas_coeffs[i]); } - ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons)); + ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */)); my_cons.push_back(mk_not(farkas_con)); my_coeffs.push_back(make_int("1")); std::vector my_hyps; @@ -1103,7 +1110,7 @@ public: my_cons.push_back(conc(prem(proof,i-1))); my_coeffs.push_back(farkas_coeffs[i]); } - ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons)); + ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */)); std::vector my_hyps; for(int i = 1; i < nargs; i++) my_hyps.push_back(prems[i-1]); @@ -1642,6 +1649,10 @@ public: res = iproof->make_axiom(lits); break; } + case PR_IFF_TRUE: { // turns p into p <-> true, noop for us + res = args[0]; + break; + } default: assert(0 && "translate_main: unsupported proof rule"); throw unsupported(); diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 4b7d47e0f..a85c9a1c5 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -20,6 +20,14 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#pragma warning(disable:4390) +#endif + #include "iz3translate.h" #include "iz3proof.h" #include "iz3profiling.h" @@ -58,7 +66,9 @@ namespace stl_ext { static int lemma_count = 0; +#if 0 static int nll_lemma_count = 0; +#endif #define SHOW_LEMMA_COUNT -1 // One half of a resolution. We need this to distinguish diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 12dd4ff3e..248aca163 100644 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -35,10 +35,15 @@ Revision History: #include "model_smt2_pp.h" #include "model_v2_pp.h" #include "fixedpoint_params.hpp" -#include "scoped_proof.h" // template class symbol_table; +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif #include "duality.h" #include "duality_profiling.h" @@ -213,6 +218,9 @@ lbool dl_interface::query(::expr * query) { catch (Duality::solver::cancel_exception &exn){ throw default_exception("duality canceled"); } + catch (Duality::Solver::Incompleteness &exn){ + throw default_exception("incompleteness"); + } // profile! diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index d34aa2ec8..ec62efa1c 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -759,7 +759,8 @@ namespace smt { app * fact = to_app(m_manager.get_fact(pr)); app * n1_owner = n1->get_owner(); app * n2_owner = n2->get_owner(); - if (fact->get_num_args() != 2 || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) { + bool is_eq = m_manager.is_eq(fact) || m_manager.is_iff(fact); + if (!is_eq || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) { CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2), tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n"; if (fact->get_num_args() == 2) { diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index ebccf4d52..144925164 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1836,6 +1836,21 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a // Just keep it here, as there will be something else that uses it. mk_triple(args[0], args[1], args[2], result); } + else if (num == 1 && m_bv_util.is_bv(args[0])) { + sort * s = f->get_range(); + unsigned to_sbits = m_util.get_sbits(s); + unsigned to_ebits = m_util.get_ebits(s); + + expr * bv = args[0]; + int sz = m_bv_util.get_bv_size(bv); + SASSERT((unsigned)sz == to_sbits + to_ebits); + + m_bv_util.mk_extract(sz - 1, sz - 1, bv); + mk_triple(m_bv_util.mk_extract(sz - 1, sz - 1, bv), + m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv), + m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv), + result); + } else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) { // We also support float to float conversion sort * s = f->get_range(); @@ -2043,6 +2058,27 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); } +void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 3); + mk_triple(args[0], args[2], args[1], result); +} + +void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(to_app(e)->get_num_args() == 3); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 821618bae..79c8039ef 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -122,7 +122,13 @@ public: void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + + void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); obj_map const & const2bv() const { return m_const2bv; } obj_map const & rm_const2bv() const { return m_rm_const2bv; } diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index d737683a8..b2e3da939 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -139,6 +139,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE; case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index f3c913ccc..90cfc8c92 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -36,3 +36,77 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) { mk_sat_tactic(m, p), mk_fail_if_undecided_tactic()); } + +struct is_non_qffpa_predicate { + struct found {}; + ast_manager & m; + float_util u; + + is_non_qffpa_predicate(ast_manager & _m) :m(_m), u(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s))) + throw found(); + family_id fid = s->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == u.get_family_id()) + return; + + throw found(); + } +}; + +struct is_non_qffpabv_predicate { + struct found {}; + ast_manager & m; + bv_util bu; + float_util fu; + + is_non_qffpabv_predicate(ast_manager & _m) :m(_m), bu(m), fu(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !(fu.is_float(s) || fu.is_rm(s) || bu.is_bv_sort(s))) + throw found(); + family_id fid = s->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == fu.get_family_id() || fid == bu.get_family_id()) + return; + + throw found(); + } +}; + +class is_qffpa_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +class is_qffpabv_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +probe * mk_is_qffpa_probe() { + return alloc(is_qffpa_probe); +} + +probe * mk_is_qffpabv_probe() { + return alloc(is_qffpabv_probe); +} + \ No newline at end of file diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h index 8ca2183c1..cd16c5817 100644 --- a/src/tactic/fpa/qffpa_tactic.h +++ b/src/tactic/fpa/qffpa_tactic.h @@ -30,4 +30,11 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref()); ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)") */ +probe * mk_is_qffpa_probe(); +probe * mk_is_qffpabv_probe(); +/* + ADD_PROBE("is-qffpa", "true if the goal is in QF_FPA (FloatingPoints).", "mk_is_qffpa_probe()") + ADD_PROBE("is-qffpabv", "true if the goal is in QF_FPABV (FloatingPoints+Bitvectors).", "mk_is_qffpabv_probe()") +*/ + #endif diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index d65ba8d35..9ecc16ecf 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -27,6 +27,7 @@ Notes: #include"nra_tactic.h" #include"probe_arith.h" #include"quant_tactics.h" +#include"qffpa_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), @@ -37,7 +38,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m), cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), - mk_smt_tactic())))))))), + cond(mk_is_qffpabv_probe(), mk_qffpa_tactic(m, p), + mk_smt_tactic()))))))))), p); return st; } diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 8585e7eda..40d20b644 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -49,8 +49,11 @@ Revision History: // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects // the x87 FPU, even when /arch:SSE2 is on. // Luckily, these are kind of standardized, at least for Windows/Linux/OSX. +#ifdef __clang__ +#undef USE_INTRINSICS +#else #include - +#endif hwf_manager::hwf_manager() : m_mpz_manager(m_mpq_manager) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 5910f55c9..8cb6ed4fc 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1400,6 +1400,10 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) { return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false)); } +mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) { + return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false)); +} + void mpf_manager::mk_nzero(unsigned ebits, unsigned sbits, mpf & o) { o.sbits = sbits; o.ebits = ebits; diff --git a/src/util/mpf.h b/src/util/mpf.h index 284b0ba7f..83646f9f3 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -182,6 +182,8 @@ public: mpf_exp_t mk_max_exp(unsigned ebits); mpf_exp_t mk_min_exp(unsigned ebits); + mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent); + /** \brief Return the biggest k s.t. 2^k <= a.