From 13b61d894c0c352b2baa1e3c3cae7a939e97c160 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 9 Sep 2014 14:02:46 -0700 Subject: [PATCH 01/32] adding recursion bounds to duality --- src/duality/duality.h | 5 +++-- src/duality/duality_rpfp.cpp | 5 ++++- src/duality/duality_solver.cpp | 23 ++++++++++++++++------- src/muz/base/dl_context.cpp | 8 ++++++-- src/muz/base/dl_context.h | 5 +++-- src/muz/duality/duality_dl_interface.cpp | 17 ++++++++++++++--- src/muz/fp/dl_cmds.cpp | 20 ++++++++++++++------ 7 files changed, 60 insertions(+), 23 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index c1c9797f3..16576dd65 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -488,9 +488,10 @@ protected: std::vector Incoming; Term dual; Node *map; + unsigned recursion_bound; Node(const FuncDecl &_Name, const Transformer &_Annotation, const Transformer &_Bound, const Transformer &_Underapprox, const Term &_dual, RPFP *_owner, int _number) - : Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0;} + : Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0; recursion_bound = UINT_MAX;} }; /** Create a node in the graph. The input is a term R(v_1...v_n) @@ -829,7 +830,7 @@ protected: #ifdef _WINDOWS __declspec(dllexport) #endif - void FromClauses(const std::vector &clauses); + void FromClauses(const std::vector &clauses, const std::vector *bounds = 0); void FromFixpointContext(fixedpoint fp, std::vector &queries); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index ef37dd8a2..8c88dda72 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -3570,7 +3570,7 @@ namespace Duality { #define USE_QE_LITE - void RPFP::FromClauses(const std::vector &unskolemized_clauses){ + void RPFP::FromClauses(const std::vector &unskolemized_clauses, const std::vector *bounds){ hash_map pmap; func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort()); @@ -3663,6 +3663,7 @@ namespace Duality { pmap[R] = node; if (is_query) node->Bound = CreateRelation(std::vector(), ctx.bool_val(false)); + node->recursion_bound = bounds ? 0 : UINT_MAX; } } @@ -3728,6 +3729,8 @@ namespace Duality { Transformer T = CreateTransformer(Relparams,Indparams,body); Edge *edge = CreateEdge(Parent,T,Children); edge->labeled = labeled;; // remember for label extraction + if(bounds) + Parent->recursion_bound = std::max(Parent->recursion_bound,(*bounds)[i]); // edges.push_back(edge); } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 681582415..f54e00693 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -33,6 +33,7 @@ Revision History: #include #include #include +#include // TODO: make these official options or get rid of them @@ -304,7 +305,7 @@ namespace Duality { #ifdef BOUNDED struct Counter { - int val; + unsigned val; Counter(){val = 0;} }; typedef std::map NodeToCounter; @@ -321,6 +322,10 @@ namespace Duality { heuristic = !cex.get_tree() ? (Heuristic *)(new LocalHeuristic(rpfp)) : (Heuristic *)(new ReplayHeuristic(rpfp,cex)); #endif + // determine if we are recursion bounded + for(unsigned i = 0; i < rpfp->nodes.size(); i++) + if(rpfp->nodes[i]->recursion_bound < UINT_MAX) + RecursionBound = 0; cex.clear(); // in case we didn't use it for heuristic if(unwinding) delete unwinding; unwinding = new RPFP(rpfp->ls); @@ -461,7 +466,7 @@ namespace Duality { } return false; } - + /** Create an instance of a node in the unwinding. Set its annotation to true, and mark it unexpanded. */ Node* CreateNodeInstance(Node *node, int number = 0){ @@ -780,10 +785,8 @@ namespace Duality { std::vector &insts = insts_of_node[node]; for(unsigned j = 0; j < insts.size(); j++) if(indset->Contains(insts[j])) - if(NodePastRecursionBound(insts[j])){ + if(NodePastRecursionBound(insts[j],true)) recursionBounded = true; - return; - } } } @@ -801,12 +804,18 @@ namespace Duality { } #ifdef BOUNDED - bool NodePastRecursionBound(Node *node){ + bool NodePastRecursionBound(Node *node, bool report = false){ if(RecursionBound < 0) return false; NodeToCounter &backs = back_edges[node]; for(NodeToCounter::iterator it = backs.begin(), en = backs.end(); it != en; ++it){ - if(it->second.val > RecursionBound) + if(it->second.val > it->first->recursion_bound){ + if(report){ + std::ostringstream os; + os << "cut off " << it->first->Name.name() << " at depth " << it->second.val; + reporter->Message(os.str()); + } return true; + } } return false; } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index fbef46ae3..80af7eeb0 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -246,6 +246,7 @@ namespace datalog { m_rule_fmls_head = 0; m_rule_fmls.reset(); m_rule_names.reset(); + m_rule_bounds.reset(); m_argument_var_names.reset(); m_preds.reset(); m_preds_by_name.reset(); @@ -474,9 +475,10 @@ namespace datalog { return new_pred; } - void context::add_rule(expr* rl, symbol const& name) { + void context::add_rule(expr* rl, symbol const& name, unsigned bound) { m_rule_fmls.push_back(rl); m_rule_names.push_back(name); + m_rule_bounds.push_back(bound); } void context::flush_add_rules() { @@ -1102,12 +1104,13 @@ namespace datalog { } } - void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names){ + void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names, vector &bounds){ for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { expr_ref r = bind_variables(m_rule_fmls[i].get(), true); rules.push_back(r.get()); // rules.push_back(m_rule_fmls[i].get()); names.push_back(m_rule_names[i]); + bounds.push_back(m_rule_bounds[i]); } } @@ -1125,6 +1128,7 @@ namespace datalog { m_rule_names[i] = m_rule_names.back(); m_rule_fmls.pop_back(); m_rule_names.pop_back(); + m_rule_bounds.pop_back(); --i; } } diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 7349fa889..cf2c53913 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -194,6 +194,7 @@ namespace datalog { unsigned m_rule_fmls_head; expr_ref_vector m_rule_fmls; svector m_rule_names; + vector m_rule_bounds; expr_ref_vector m_background; model_converter_ref m_mc; proof_converter_ref m_pc; @@ -366,7 +367,7 @@ namespace datalog { rule_set & get_rules() { flush_add_rules(); return m_rule_set; } void get_rules_as_formulas(expr_ref_vector& fmls, svector& names); - void get_raw_rule_formulas(expr_ref_vector& fmls, svector& names); + void get_raw_rule_formulas(expr_ref_vector& fmls, svector& names, vector &bounds); void add_fact(app * head); void add_fact(func_decl * pred, const relation_fact & fact); @@ -383,7 +384,7 @@ namespace datalog { /** Method exposed from API for adding rules. */ - void add_rule(expr* rl, symbol const& name); + void add_rule(expr* rl, symbol const& name, unsigned bound = UINT_MAX); /** diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 849cf94ea..08c57b05e 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -155,8 +155,9 @@ lbool dl_interface::query(::expr * query) { expr_ref_vector rules(m_ctx.get_manager()); svector< ::symbol> names; + vector bounds; // m_ctx.get_rules_as_formulas(rules, names); - m_ctx.get_raw_rule_formulas(rules, names); + m_ctx.get_raw_rule_formulas(rules, names, bounds); // get all the rules as clauses std::vector &clauses = _d->clauses; @@ -200,6 +201,7 @@ lbool dl_interface::query(::expr * query) { expr qc = implies(q,_d->ctx.bool_val(false)); qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc); clauses.push_back(qc); + bounds.push_back(UINT_MAX); // get the background axioms unsigned num_asserts = m_ctx.get_num_assertions(); @@ -243,13 +245,21 @@ lbool dl_interface::query(::expr * query) { expr c = implies(_d->ctx.bool_val(false),f(args)); c = _d->ctx.make_quant(Forall,args,c); clauses.push_back(c); + bounds.push_back(UINT_MAX); } } } } + unsigned rb = m_ctx.get_params().recursion_bound(); + std::vector std_bounds; + for(unsigned i = 0; i < bounds.size(); i++){ + unsigned b = bounds[i]; + if (b == UINT_MAX) b = rb; + std_bounds.push_back(b); + } // creates 1-1 map between clauses and rpfp edges - _d->rpfp->FromClauses(clauses); + _d->rpfp->FromClauses(clauses,&std_bounds); // populate the edge-to-clause map for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i) @@ -271,11 +281,12 @@ lbool dl_interface::query(::expr * query) { rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0"); rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0"); rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file()); - unsigned rb = m_ctx.get_params().recursion_bound(); +#if 0 if(rb != UINT_MAX){ std::ostringstream os; os << rb; rs->SetOption("recursion_bound", os.str()); } +#endif // Solve! bool ans; diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index f9916808c..e2e3680cc 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -100,7 +100,7 @@ struct dl_context { dlctx().set_predicate_representation(pred, num_kinds, kinds); } - void add_rule(expr * rule, symbol const& name) { + void add_rule(expr * rule, symbol const& name, unsigned bound) { init(); if (m_collected_cmds) { expr_ref rl = m_context->bind_variables(rule, true); @@ -110,7 +110,7 @@ struct dl_context { m_trail.push(push_back_vector >(m_collected_cmds->m_names)); } else { - m_context->add_rule(rule, name); + m_context->add_rule(rule, name, bound); } } @@ -151,19 +151,22 @@ class dl_rule_cmd : public cmd { mutable unsigned m_arg_idx; expr* m_t; symbol m_name; + unsigned m_bound; public: dl_rule_cmd(dl_context * dl_ctx): cmd("rule"), m_dl_ctx(dl_ctx), m_arg_idx(0), - m_t(0) {} - virtual char const * get_usage() const { return "(forall (q) (=> (and body) head)) :optional-name"; } + m_t(0), + m_bound(UINT_MAX) {} + virtual char const * get_usage() const { return "(forall (q) (=> (and body) head)) :optional-name :optional-recursion-bound"; } virtual char const * get_descr(cmd_context & ctx) const { return "add a Horn rule."; } virtual unsigned get_arity() const { return VAR_ARITY; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { switch(m_arg_idx) { case 0: return CPK_EXPR; case 1: return CPK_SYMBOL; + case 2: return CPK_UINT; default: return CPK_SYMBOL; } } @@ -173,13 +176,18 @@ public: } virtual void set_next_arg(cmd_context & ctx, symbol const & s) { m_name = s; + m_arg_idx++; + } + virtual void set_next_arg(cmd_context & ctx, unsigned bound) { + m_bound = bound; + m_arg_idx++; } virtual void reset(cmd_context & ctx) { m_dl_ctx->reset(); prepare(ctx); } - virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; } + virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; m_bound = UINT_MAX; } virtual void finalize(cmd_context & ctx) { } virtual void execute(cmd_context & ctx) { - m_dl_ctx->add_rule(m_t, m_name); + m_dl_ctx->add_rule(m_t, m_name, m_bound); } }; From 4c71e9479d00048a9a6f8666499d7e1f4b616c73 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 30 Sep 2014 11:21:34 -0700 Subject: [PATCH 02/32] optimizing array final check --- src/smt/theory_array_base.cpp | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 3f96a1d62..6325a2a99 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -376,8 +376,10 @@ namespace smt { enode_vector::const_iterator end = r->end_parents(); for (; it != end; ++it) { enode * parent = *it; +#if 0 if (!ctx.is_relevant(parent)) continue; +#endif unsigned num_args = parent->get_num_args(); if (is_store(parent)) { SET_ARRAY(parent->get_arg(0)); @@ -399,6 +401,7 @@ namespace smt { return false; } +#if 0 void theory_array_base::collect_shared_vars(sbuffer & result) { TRACE("array_shared", tout << "collecting shared vars...\n";); context & ctx = get_context(); @@ -420,6 +423,29 @@ namespace smt { } unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); } +#else + void theory_array_base::collect_shared_vars(sbuffer & result) { + TRACE("array_shared", tout << "collecting shared vars...\n";); + context & ctx = get_context(); + ptr_buffer to_unmark; + unsigned num_vars = get_num_vars(); + for (unsigned i = 0; i < num_vars; i++) { + enode * n = get_enode(i); + if (ctx.is_relevant(n)) { + enode * r = n->get_root(); + if (!r->is_marked() && is_array_sort(r) && ctx.is_shared(r)) { + TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); + theory_var r_th_var = r->get_th_var(get_id()); + SASSERT(r_th_var != null_theory_var); + result.push_back(r_th_var); + } + r->set_mark(); + to_unmark.push_back(r); + } + } + unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); + } +#endif /** \brief Create interface variables for shared array variables. From 47635325014f2951d203897eae4d8120787a283d Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 30 Sep 2014 11:25:47 -0700 Subject: [PATCH 03/32] adding compile-time option to replace arrays with maps in smt (define SPARSE_MAP) --- src/smt/smt_context.h | 7 ++++++- src/smt/smt_enode.cpp | 6 +++--- src/smt/smt_enode.h | 29 ++++++++++++++++++++++++++--- src/util/map.h | 2 +- 4 files changed, 36 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7940b17be..5abdfa5f9 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -54,7 +54,11 @@ Revision History: // the case that each context only references a few expressions. // Using a map instead of a vector for the literals can compress space // consumption. +#ifdef SPARSE_MAP +#define USE_BOOL_VAR_VECTOR 0 +#else #define USE_BOOL_VAR_VECTOR 1 +#endif namespace smt { @@ -69,6 +73,7 @@ namespace smt { std::string last_failure_as_string() const; void set_progress_callback(progress_callback *callback); + protected: ast_manager & m_manager; smt_params & m_fparams; @@ -106,7 +111,7 @@ namespace smt { // ----------------------------------- enode * m_true_enode; enode * m_false_enode; - ptr_vector m_app2enode; // app -> enode + app2enode_t m_app2enode; // app -> enode ptr_vector m_enodes; plugin_manager m_theories; // mapping from theory_id -> theory ptr_vector m_theory_set; // set of theories for fast traversal diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 98b8eaf8b..451577357 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -24,7 +24,7 @@ namespace smt { /** \brief Initialize an enode in the given memory position. */ - enode * enode::init(ast_manager & m, void * mem, ptr_vector const & app2enode, app * owner, + enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); @@ -60,7 +60,7 @@ namespace smt { return n; } - enode * enode::mk(ast_manager & m, region & r, ptr_vector const & app2enode, app * owner, + enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); @@ -69,7 +69,7 @@ namespace smt { return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent); } - enode * enode::mk_dummy(ast_manager & m, ptr_vector const & app2enode, app * owner) { + enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) { unsigned sz = get_enode_size(owner->get_num_args()); void * mem = alloc_svect(char, sz); return init(m, mem, app2enode, owner, 0, false, false, 0, true, false); diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 505dea0ee..ca75028c3 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -38,6 +38,29 @@ namespace smt { } }; + /** \ brief Use sparse maps in SMT solver. + + Define this to use hash maps rather than vectors over ast + nodes. This is useful in the case there are many solvers, each + referencing few nodes from a large ast manager. There is some + unknown performance penalty for this. */ + + // #define SPARSE_MAP + +#ifndef SPARSE_MAP + typedef ptr_vector app2enode_t; // app -> enode +#else + class app2enode_t : public u_map { + public: + void setx(unsigned x, enode *val, enode *def){ + if(val == 0) + erase(x); + else + insert(x,val); + } + }; +#endif + class tmp_enode; /** @@ -115,7 +138,7 @@ namespace smt { friend class tmp_enode; - static enode * init(ast_manager & m, void * mem, ptr_vector const & app2enode, app * owner, + static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent); public: @@ -124,11 +147,11 @@ namespace smt { return sizeof(enode) + num_args * sizeof(enode*); } - static enode * mk(ast_manager & m, region & r, ptr_vector const & app2enode, app * owner, + static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent); - static enode * mk_dummy(ast_manager & m, ptr_vector const & app2enode, app * owner); + static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner); static void del_dummy(enode * n) { dealloc_svect(reinterpret_cast(n)); } diff --git a/src/util/map.h b/src/util/map.h index 3e8e10891..d659b89c0 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -131,7 +131,7 @@ public: value const& get(key const& k, value const& default_value) const { entry* e = find_core(k); if (e) { - return e->m_value; + return e->get_data().m_value; } else { return default_value; From 301cb51bbb81a3fd8db81e9baa8850dc2d6bc117 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 30 Sep 2014 12:42:30 -0700 Subject: [PATCH 04/32] added restarts options to duality (plus some other disabled features) --- src/duality/duality.h | 6 + src/duality/duality_rpfp.cpp | 67 ++++ src/duality/duality_solver.cpp | 391 +++++++++++++++++++++-- src/muz/base/fixedpoint_params.pyg | 1 + src/muz/duality/duality_dl_interface.cpp | 1 + 5 files changed, 446 insertions(+), 20 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 16576dd65..edd89d78f 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -104,6 +104,8 @@ namespace Duality { FuncDecl RenumberPred(const FuncDecl &f, int n); + FuncDecl NumberPred(const FuncDecl &f, int n); + Term ExtractStores(hash_map &memo, const Term &t, std::vector &cnstrs, hash_map &renaming); @@ -903,6 +905,10 @@ protected: int CumulativeDecisions(); + void GreedyReduceNodes(std::vector &nodes); + + check_result CheckWithConstrainedNodes(std::vector &posnodes,std::vector &negnodes); + solver &slvr(){ return *ls->slvr; } diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 8c88dda72..f2824c9b0 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2816,6 +2816,62 @@ namespace Duality { } } + void foobar(){ + } + + void RPFP::GreedyReduceNodes(std::vector &nodes){ + std::vector lits; + for(unsigned i = 0; i < nodes.size(); i++){ + Term b; std::vector v; + RedVars(nodes[i], b, v); + lits.push_back(!b); + expr bv = dualModel.eval(b); + if(eq(bv,ctx.bool_val(true))){ + check_result res = slvr_check(lits.size(),&lits[0]); + if(res == unsat) + lits.pop_back(); + else + foobar(); + } + } + } + + check_result RPFP::CheckWithConstrainedNodes(std::vector &posnodes,std::vector &negnodes){ + timer_start("Check"); + std::vector lits; + for(unsigned i = 0; i < posnodes.size(); i++){ + Term b; std::vector v; + RedVars(posnodes[i], b, v); + lits.push_back(b); + } + for(unsigned i = 0; i < negnodes.size(); i++){ + Term b; std::vector v; + RedVars(negnodes[i], b, v); + lits.push_back(!b); + } + check_result res = slvr_check(lits.size(),&lits[0]); + if(res == unsat && posnodes.size()){ + lits.resize(posnodes.size()); + res = slvr_check(lits.size(),&lits[0]); + } + dualModel = slvr().get_model(); +#if 0 + if(!dualModel.null()){ + std::cout << "posnodes called:\n"; + for(unsigned i = 0; i < posnodes.size(); i++) + if(!Empty(posnodes[i])) + std::cout << posnodes[i]->Name.name() << "\n"; + std::cout << "negnodes called:\n"; + for(unsigned i = 0; i < negnodes.size(); i++) + if(!Empty(negnodes[i])) + std::cout << negnodes[i]->Name.name() << "\n"; + } +#endif + timer_stop("Check"); + return res; + } + + 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())); @@ -3333,6 +3389,17 @@ namespace Duality { return ctx.function(name.c_str(), arity, &domain[0], f.range()); } + Z3User::FuncDecl Z3User::NumberPred(const FuncDecl &f, int n) + { + std::string name = f.name().str(); + name = name + "_" + 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, diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index f54e00693..49e591be2 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -255,6 +255,13 @@ namespace Duality { /** Called when done expanding a tree */ virtual void Done() {} + + /** Ask whether a node should be used/unused in the tree. Returns, + 1 if yes, -1 if no, and 0 if don't care. */ + + virtual int UseNode(Node *node){ + return 0; + } }; /** The Proposer class proposes conjectures eagerly. These can come @@ -302,6 +309,7 @@ namespace Duality { hash_set overapproxes; std::vector proposers; std::string ConjectureFile; + bool stratified_inlining_done; #ifdef BOUNDED struct Counter { @@ -314,6 +322,13 @@ namespace Duality { /** Solve the problem. */ virtual bool Solve(){ + PreSolve(); + bool res = SolveMain(); // does the actual work + PostSolve(); + return res; + } + + void PreSolve(){ reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp); conj_reporter = ConjectureFile.empty() ? 0 : CreateConjectureFileReporter(rpfp,ConjectureFile); #ifndef LOCALIZE_CONJECTURES @@ -342,9 +357,10 @@ namespace Duality { return false; #endif StratifiedLeafCount = -1; - timer_start("SolveMain"); - bool res = SolveMain(); // does the actual work - timer_stop("SolveMain"); + stratified_inlining_done = false; + } + + void PostSolve(){ // print_profile(std::cout); delete indset; delete heuristic; @@ -354,7 +370,16 @@ namespace Duality { delete conj_reporter; for(unsigned i = 0; i < proposers.size(); i++) delete proposers[i]; - return res; + } + + bool RecheckBounds(){ + for(unsigned i = 0; i < unwinding->nodes.size(); i++){ + Node *node = unwinding->nodes[i]; + node->Bound = node->map->Bound; + if(!SatisfyUpperBound(node)) + return false; + } + return true; } void CreateInitialUnwinding(){ @@ -417,6 +442,7 @@ namespace Duality { bool StratifiedInlining; // Do stratified inlining as preprocessing step int RecursionBound; // Recursion bound for bounded verification bool BatchExpand; + bool EnableRestarts; bool SetBoolOption(bool &opt, const std::string &value){ if(value == "0") { @@ -464,6 +490,9 @@ namespace Duality { if(option == "conjecture_file"){ ConjectureFile = value; } + if(option == "enable_restarts"){ + return SetBoolOption(EnableRestarts,value); + } return false; } @@ -901,6 +930,9 @@ namespace Duality { */ bool DoStratifiedInlining(){ + if(stratified_inlining_done) + return true; + stratified_inlining_done = true; DoTopoSort(); int depth = 1; // TODO: make this an option std::vector > unfolding_levels(depth+1); @@ -1043,10 +1075,17 @@ namespace Duality { h->SetOldNode(node); } + bool SolveMain(){ + timer_start("SolveMain"); + bool res = SolveMainInt(); // does the actual work + timer_stop("SolveMain"); + return res; + } + /** This does the actual solving work. We try to generate candidates for extension. If we succed, we extend the unwinding. If we fail, we have a solution. */ - bool SolveMain(){ + bool SolveMainInt(){ if(StratifiedInlining && !DoStratifiedInlining()) return false; #ifdef BOUNDED @@ -1776,6 +1815,7 @@ namespace Duality { } timer_stop("Propagate"); } + /** This class represents a derivation tree. */ class DerivationTree { @@ -2127,6 +2167,8 @@ namespace Duality { hash_map updates; + int restart_interval; + DerivationTreeSlow(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) : DerivationTree(_duality, rpfp, _reporter, _heuristic, _full_expand) { stack.push_back(stack_entry()); @@ -2135,6 +2177,7 @@ namespace Duality { struct DoRestart {}; virtual bool Build(){ + restart_interval = 3; while (true) { try { return BuildMain(); @@ -2145,15 +2188,47 @@ namespace Duality { while(stack.size() > 1) PopLevel(); reporter->Message("restarted"); + restart_interval += 1; } } } + + // When we check, try to use the same children that were used in the + // previous counterexample. + check_result Check(){ +#if 0 + std::vector posnodes, negnodes; + std::vector &expansions = stack.back().expansions; + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + std::vector &chs = node->Outgoing->Children; + for(unsigned j = 0; j < chs.size(); j++){ + Node *ch = chs[j]; + int use = heuristic->UseNode(ch); + if(use == 1) + posnodes.push_back(ch); + else if (use == -1) + negnodes.push_back(ch); + } + } + if(!(posnodes.empty() && negnodes.empty())){ + check_result res = tree->CheckWithConstrainedNodes(posnodes,negnodes); + if(res != unsat){ + reporter->Message("matched previous counterexample"); + return res; + } + } +#endif + return tree->Check(top); + } + bool BuildMain(){ stack.back().level = tree->slvr().get_scope_level(); bool was_sat = true; int update_failures = 0; + int total_updates = 0; while (true) { @@ -2165,7 +2240,7 @@ namespace Duality { reporter->Depth(stack.size()); // res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop - check_result foo = tree->Check(top); + check_result foo = Check(); res = foo == unsat ? l_false : l_true; if (res == l_false) { @@ -2193,11 +2268,18 @@ namespace Duality { throw DoRestart(); } #endif - if(RecordUpdate(node)) + if(RecordUpdate(node)){ update_count++; + total_updates++; + } else heuristic->Update(node->map); // make it less likely to expand this node in future } +#if 1 + if(duality->EnableRestarts) + if(total_updates >= restart_interval) + throw DoRestart(); +#endif if(update_count == 0){ if(was_sat){ update_failures++; @@ -2243,6 +2325,10 @@ namespace Duality { tree->Push(); std::vector &expansions = stack.back().expansions; #ifndef NO_DECISIONS +#if 0 + if(expansions.size() > 0) + tree->GreedyReduceNodes(expansions[0]->Outgoing->Children); // try to reduce number of children +#endif for(unsigned i = 0; i < expansions.size(); i++){ tree->FixCurrentState(expansions[i]->Outgoing); } @@ -2262,15 +2348,42 @@ namespace Duality { if(ExpandSomeNodes(false,expand_max)) continue; tree->Pop(1); + node_order.clear(); while(stack.size() > 1){ tree->Pop(1); + std::vector &expansions = stack.back().expansions; + for(unsigned i = 0; i < expansions.size(); i++) + node_order.push_back(expansions[i]); stack.pop_back(); } +#if 0 + Reduce(); +#endif return true; } } } + std::vector node_order; + + void Reduce(){ + tree->Push(); + // tree->AssertNode(top); // assert the negation of the top-level spec + for(int i = node_order.size()-1; i >= 0; --i){ + Edge *edge = node_order[i]->Outgoing; + if(edge){ + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *ch = edge->Children[j]; + if(!ch->Outgoing) + ch->Annotation.SetEmpty(); + } + tree->AssertEdge(edge,0,true); + } + } + tree->GreedyReduceNodes(node_order); // try to reduce the counterexample size + tree->Pop(1); + } + void PopLevel(){ std::vector &expansions = stack.back().expansions; tree->Pop(1); @@ -2869,17 +2982,7 @@ namespace Duality { return name; } - virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority, bool best_only){ - if(!high_priority || !old_cex.get_tree()){ - Heuristic::ChooseExpand(choices,best,false); - return; - } - // first, try to match the derivatino tree nodes to the old cex - std::set matched, unmatched; - for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it){ - Node *node = (*it); - if(cex_map.empty()) - cex_map[node] = old_cex.get_root(); // match the root nodes + Node *MatchNode(Node *node){ if(cex_map.find(node) == cex_map.end()){ // try to match an unmatched node Node *parent = node->Incoming[0]->Parent; // assumes we are a tree! if(cex_map.find(parent) == cex_map.end()) @@ -2902,7 +3005,30 @@ namespace Duality { cex_map[chs[i]] = 0; } matching_done: - Node *old_node = cex_map[node]; + return cex_map[node]; + } + + int UseNode(Node *node){ + if (!old_cex.get_tree()) + return 0; + Node *old_node = MatchNode(node); + if(!old_node) + return 0; + return old_cex.get_tree()->Empty(old_node) ? -1 : 1; + } + + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority, bool best_only){ + if(cex_map.empty()) + cex_map[*(choices.begin())] = old_cex.get_root(); // match the root nodes + if(!high_priority || !old_cex.get_tree()){ + Heuristic::ChooseExpand(choices,best,false); + return; + } + // first, try to match the derivatino tree nodes to the old cex + std::set matched, unmatched; + for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it){ + Node *node = (*it); + Node *old_node = MatchNode(node); if(!old_node) unmatched.insert(node); else if(old_cex.get_tree()->Empty(old_node)) @@ -3177,8 +3303,233 @@ namespace Duality { }; + + class DualityDepthBounded : public Solver { + + Duality *duality; + context &ctx; // Z3 context + solver &slvr; // Z3 solver + + public: + DualityDepthBounded(RPFP *_rpfp) : + ctx(_rpfp->ctx), + slvr(_rpfp->slvr()){ + rpfp = _rpfp; + DepthBoundRPFP(); + duality = alloc(Duality,drpfp); + } + + ~DualityDepthBounded(){ + dealloc(duality); + delete drpfp; + } + + bool Solve(){ + int depth_bound = 10; + bool res; + SetMaxDepthRPFP(depth_bound); + duality->PreSolve(); + while(true){ + res = duality->SolveMain(); + if(!res || GetSolution()) + break; + depth_bound++; + SetMaxDepthRPFP(depth_bound); + res = duality->RecheckBounds(); + if(!res) + break; + } + duality->PostSolve(); + if(!res) + ConvertCex(); + return res; + } + + Counterexample &GetCounterexample(){ + return cex; + } + + bool SetOption(const std::string &option, const std::string &value){ + return duality->SetOption(option,value); + } + + virtual void LearnFrom(Solver *old_solver){ + DualityDepthBounded *old = dynamic_cast(old_solver); + if(old){ + duality->LearnFrom(old->duality); + } + } + + bool IsResultRecursionBounded(){ + return duality->IsResultRecursionBounded(); + } + + void Cancel(){ + duality->Cancel(); + } + + typedef RPFP::Node Node; + typedef RPFP::Edge Edge; + RPFP *rpfp, *drpfp; + hash_map db_map, db_rev_map; + hash_map db_edge_rev_map; + std::vector db_saved_bounds; + Counterexample cex; + + expr AddParamToRels(hash_map &memo, hash_map &rmap, const expr &p, const expr &t) { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + expr &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(AddParamToRels(memo, rmap, p, t.arg(i))); + hash_map::iterator rit = rmap.find(f); + if(rit != rmap.end()){ + args.push_back(p); + res = (rit->second)(args); + res = ctx.make(And,res,ctx.make(Geq,p,ctx.int_val(0))); + } + else + res = f(args); + } + else if (t.is_quantifier()) + { + expr body = AddParamToRels(memo, rmap, p, t.body()); + res = clone_quantifier(t, body); + } + else res = t; + return res; + } + + + void DepthBoundRPFP(){ + drpfp = new RPFP(rpfp->ls); + expr dvar = ctx.int_const("@depth"); + expr dmax = ctx.int_const("@depth_max"); + for(unsigned i = 0; i < rpfp->nodes.size(); i++){ + Node *node = rpfp->nodes[i]; + std::vector arg_sorts; + const std::vector ¶ms = node->Annotation.IndParams; + for(unsigned j = 0; j < params.size(); j++) + arg_sorts.push_back(params[j].get_sort()); + arg_sorts.push_back(ctx.int_sort()); + std::string new_name = std::string("@db@") + node->Name.name().str(); + func_decl f = ctx.function(new_name.c_str(),arg_sorts.size(), &arg_sorts[0],ctx.bool_sort()); + std::vector args = params; + args.push_back(dvar); + expr pat = f(args); + Node *dnode = drpfp->CreateNode(pat); + db_map[node] = dnode; + db_rev_map[dnode] = node; + expr bound_fmla = node->Bound.Formula; + if(!eq(bound_fmla,ctx.bool_val(true))){ + bound_fmla = implies(dvar == dmax,bound_fmla); + dnode->Bound.Formula = bound_fmla; + } + db_saved_bounds.push_back(bound_fmla); + // dnode->Annotation.Formula = ctx.make(And,node->Annotation.Formula,ctx.make(Geq,dvar,ctx.int_val(0))); + } + for(unsigned i = 0; i < rpfp->edges.size(); i++){ + Edge *edge = rpfp->edges[i]; + std::vector new_children; + std::vector new_relparams; + hash_map rmap; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *ch = edge->Children[j]; + Node *nch = db_map[ch]; + func_decl f = nch->Name; + func_decl sf = drpfp->NumberPred(f,j); + new_children.push_back(nch); + new_relparams.push_back(sf); + rmap[edge->F.RelParams[j]] = sf; + } + std::vector new_indparams = edge->F.IndParams; + new_indparams.push_back(dvar); + hash_map memo; + expr new_fmla = AddParamToRels(memo,rmap,ctx.make(Sub,dvar,ctx.int_val(1)),edge->F.Formula); + RPFP::Transformer new_t = drpfp->CreateTransformer(new_relparams,new_indparams,new_fmla); + Node *new_parent = db_map[edge->Parent]; + db_edge_rev_map[drpfp->CreateEdge(new_parent,new_t,new_children)] = edge; + } + } + + void SetMaxDepthRPFP(int depth){ + hash_map subst; + expr dmax = ctx.int_const("@depth_max"); + subst[dmax] = ctx.int_val(depth); + for(unsigned i = 0; i < drpfp->nodes.size(); i++){ + Node *node = drpfp->nodes[i]; + expr fmla = db_saved_bounds[i]; + fmla = drpfp->SubstRec(subst,fmla); + node->Bound.Formula = fmla; + } + } + + void ConvertCex(){ + cex.clear(); + RPFP *tree = new RPFP(rpfp->ls); + Node *root; + Counterexample &dctx = duality->GetCounterexample(); + hash_map ctx_node_map; + for(unsigned i = 0; i < dctx.get_tree()->nodes.size(); i++){ + Node *dnode = dctx.get_tree()->nodes[i]; + Node *onode = db_rev_map[dnode->map->map]; + Node *node = tree->CloneNode(onode); + node->number = dnode->number; // numbers have to match for model to make sense + ctx_node_map[dnode] = node; + if(dnode == dctx.get_root()) + root = node; + } + for(unsigned i = 0; i < dctx.get_tree()->edges.size(); i++){ + Edge *dedge = dctx.get_tree()->edges[i]; + Edge *oedge = db_edge_rev_map[dedge->map]; + Node *parent = ctx_node_map[dedge->Parent]; + std::vector chs; + for(unsigned j = 0; j < dedge->Children.size(); j++) + chs.push_back(ctx_node_map[dedge->Children[j]]); + Edge *edge = tree->CreateEdge(parent,oedge->F,chs); + edge->number = dedge->number; // numbers have to match for model to make sense + edge->map = oedge; + } + tree->dualModel = dctx.get_tree()->dualModel; + cex.set(tree,root); + } + + bool GetSolution(){ + for(unsigned i = 0; i < rpfp->nodes.size(); i++) + if(!drpfp->nodes[i]->Annotation.SubsetEq(rpfp->nodes[i]->Bound)) + return false; + expr dvar = ctx.int_const("@depth"); + hash_map subst; + subst[dvar] = ctx.int_val(INT_MAX); + for(unsigned i = 0; i < rpfp->nodes.size(); i++){ + expr fmla = drpfp->nodes[i]->Annotation.Formula; + fmla = drpfp->SubstRec(subst,fmla); + fmla = fmla.simplify(); + rpfp->nodes[i]->Annotation.Formula = fmla; + } + return true; + } + + void UndoDepthBoundRPFP(){ +#if 0 + if(cex.get_tree()){ + // here, need to map the cex back... + } + // also need to map the proof back, but we don't... +#endif + } + }; + Solver *Solver::Create(const std::string &solver_class, RPFP *rpfp){ - Duality *s = alloc(Duality,rpfp); + // Solver *s = alloc(DualityDepthBounded,rpfp); + Solver *s = alloc(Duality,rpfp); return s; } diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 5bfbba6b2..832e3329e 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -78,6 +78,7 @@ def_module_params('fixedpoint', ('batch_expand', BOOL, False, 'DUALITY: use batch expansion'), ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), ('conjecture_file', STRING, '', 'DUALITY: save conjectures to file'), + ('enable_restarts', BOOL, False, 'DUALITY: enable restarts'), )) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 08c57b05e..55f6c3747 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -281,6 +281,7 @@ lbool dl_interface::query(::expr * query) { rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0"); rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0"); rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file()); + rs->SetOption("enable_restarts",m_ctx.get_params().enable_restarts() ? "1" : "0"); #if 0 if(rb != UINT_MAX){ std::ostringstream os; os << rb; From c5f17df310405b2f7718f1eaa93242cfa25e54de Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 1 Oct 2014 18:15:33 -0700 Subject: [PATCH 05/32] fixing an assert caused by previous change in theory_array_base.cpp --- src/smt/theory_array_base.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 6325a2a99..b2c17b4e0 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -433,14 +433,16 @@ namespace smt { enode * n = get_enode(i); if (ctx.is_relevant(n)) { enode * r = n->get_root(); - if (!r->is_marked() && is_array_sort(r) && ctx.is_shared(r)) { - TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); - theory_var r_th_var = r->get_th_var(get_id()); - SASSERT(r_th_var != null_theory_var); - result.push_back(r_th_var); + if (!r->is_marked()){ + if(is_array_sort(r) && ctx.is_shared(r)) { + TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); + theory_var r_th_var = r->get_th_var(get_id()); + SASSERT(r_th_var != null_theory_var); + result.push_back(r_th_var); + } + r->set_mark(); + to_unmark.push_back(r); } - r->set_mark(); - to_unmark.push_back(r); } } unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); From d54d758f45b745ec129db375364d5a00eef23ce5 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 1 Oct 2014 18:16:21 -0700 Subject: [PATCH 06/32] getting duality to recover from incompleteness-related failures by restarting --- src/duality/duality_profiling.cpp | 10 ++++++++++ src/duality/duality_solver.cpp | 25 ++++++++++++++++++------- 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp index d5dac0811..5bcda972a 100755 --- a/src/duality/duality_profiling.cpp +++ b/src/duality/duality_profiling.cpp @@ -125,8 +125,18 @@ namespace Duality { void timer_stop(const char *name){ if(current->name != name || !current->parent){ +#if 0 std::cerr << "imbalanced timer_start and timer_stop"; exit(1); +#endif + // in case we lost a timer stop due to an exception + while(current->name != name && current->parent) + current = current->parent; + if(current->parent){ + current->time += (current_time() - current->start_time); + current = current->parent; + } + return; } current->time += (current_time() - current->start_time); current = current->parent; diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 49e591be2..bbd1ebe0a 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -2252,22 +2252,27 @@ namespace Duality { int update_count = 0; for(unsigned i = 0; i < expansions.size(); i++){ Node *node = expansions[i]; - tree->SolveSingleNode(top,node); -#ifdef NO_GENERALIZE - node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); -#else try { + tree->SolveSingleNode(top,node); +#ifdef NO_GENERALIZE + node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); +#else if(expansions.size() == 1 && NodeTooComplicated(node)) SimplifyNode(node); else node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); Generalize(node); +#endif } catch(const RPFP::Bad &){ // bad interpolants can get us here throw DoRestart(); } -#endif + catch(char const *msg){ + // bad interpolants can get us here + reporter->Message(std::string("interpolation failure:") + msg); + throw DoRestart(); + } if(RecordUpdate(node)){ update_count++; total_updates++; @@ -2283,8 +2288,14 @@ namespace Duality { if(update_count == 0){ if(was_sat){ update_failures++; - if(update_failures > 10) - throw Incompleteness(); + if(update_failures > 10){ + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + node->map->Annotation.SetFull(); + reporter->Message("incompleteness: cleared annotation"); + } + throw DoRestart(); + } } reporter->Message("backtracked without learning"); } From 16445569f1a6cfd3fa04c7227d3d724dd16947c7 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sat, 4 Oct 2014 16:31:01 -0700 Subject: [PATCH 07/32] fix for quantifier abstraction --- src/muz/transforms/dl_transforms.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp index 2cf48d46b..9a4667f2c 100644 --- a/src/muz/transforms/dl_transforms.cpp +++ b/src/muz/transforms/dl_transforms.cpp @@ -71,7 +71,8 @@ namespace datalog { transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, ctx, 32000)); transf.register_plugin(alloc(datalog::mk_bit_blast, ctx, 35000)); - transf.register_plugin(alloc(datalog::mk_array_blast, ctx, 36000)); + if (!ctx.get_params().quantify_arrays()) + transf.register_plugin(alloc(datalog::mk_array_blast, ctx, 36000)); transf.register_plugin(alloc(datalog::mk_karr_invariants, ctx, 36010)); if (ctx.get_params().magic()) { transf.register_plugin(alloc(datalog::mk_magic_symbolic, ctx, 36020)); From e8985ff33dcb2d9d2705d632468443abb811ee99 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sat, 4 Oct 2014 17:17:33 -0700 Subject: [PATCH 08/32] working on transforms in duality --- src/muz/duality/duality_dl_interface.cpp | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 55f6c3747..c7fa0a08f 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -157,7 +157,27 @@ lbool dl_interface::query(::expr * query) { svector< ::symbol> names; vector bounds; // m_ctx.get_rules_as_formulas(rules, names); - m_ctx.get_raw_rule_formulas(rules, names, bounds); + + expr_ref query_ref(m_ctx.get_manager()); + if(****){ + m_ctx.flush_add_rules(); + datalog::rule_manager& rm = m_ctx.get_rule_manager(); + rm.mk_query(query, m_ctx.get_rules()); + apply_default_transformation(m_ctx); + rule_set &rs = m_ctx.get_rules(); + if(m_ctx.get_rules().get_output_predicates().empty()) + query_ref = m_ctx.get_manager().mk_true(); + else { + query_pred = m_ctx.get_rules().get_output_predicate(); + func_decl_ref query_pred(m_ctx.get_manager()); + query_pred = m_ctx.get_rules().get_output_predicate(); + ptr_vector sorts; + unsi + + } + } + else + m_ctx.get_raw_rule_formulas(rules, names, bounds); // get all the rules as clauses std::vector &clauses = _d->clauses; From ec48f6d129f856f216fc1885593e8d77ab6c89e8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sat, 4 Oct 2014 19:07:14 -0700 Subject: [PATCH 09/32] working on transforms for duality --- src/muz/base/dl_context.cpp | 3 +++ src/muz/duality/duality_dl_interface.cpp | 33 +++++++++++++++++------- 2 files changed, 26 insertions(+), 10 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 80af7eeb0..ca7277d07 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -985,6 +985,9 @@ namespace datalog { flush_add_rules(); break; case DUALITY_ENGINE: + // this lets us use duality with SAS 2013 abstraction + if(quantify_arrays()) + flush_add_rules(); break; default: UNREACHABLE(); diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index c7fa0a08f..7666b39cf 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -37,6 +37,7 @@ Revision History: #include "fixedpoint_params.hpp" #include "used_vars.h" #include "func_decl_dependencies.h" +#include "dl_transforms.h" // template class symbol_table; @@ -158,22 +159,34 @@ lbool dl_interface::query(::expr * query) { vector bounds; // m_ctx.get_rules_as_formulas(rules, names); + + // If using SAS 2013 abstractiion, we need to perform some transforms expr_ref query_ref(m_ctx.get_manager()); - if(****){ - m_ctx.flush_add_rules(); + if(m_ctx.quantify_arrays()){ datalog::rule_manager& rm = m_ctx.get_rule_manager(); rm.mk_query(query, m_ctx.get_rules()); apply_default_transformation(m_ctx); - rule_set &rs = m_ctx.get_rules(); + datalog::rule_set &rs = m_ctx.get_rules(); if(m_ctx.get_rules().get_output_predicates().empty()) - query_ref = m_ctx.get_manager().mk_true(); + query_ref = m_ctx.get_manager().mk_false(); else { - query_pred = m_ctx.get_rules().get_output_predicate(); - func_decl_ref query_pred(m_ctx.get_manager()); - query_pred = m_ctx.get_rules().get_output_predicate(); - ptr_vector sorts; - unsi - + func_decl_ref query_pred(m_ctx.get_manager()); + query_pred = m_ctx.get_rules().get_output_predicate(); + ptr_vector sorts; + unsigned nargs = query_pred.get()->get_arity(); + expr_ref_vector vars(m_ctx.get_manager()); + for(unsigned i = 0; i < nargs; i++){ + ::sort *s = query_pred.get()->get_domain(i); + vars.push_back(m_ctx.get_manager().mk_var(nargs-1-i,s)); + } + query_ref = m_ctx.get_manager().mk_app(query_pred.get(),nargs,vars.c_ptr()); + query = query_ref.get(); + } + unsigned nrules = rs.get_num_rules(); + for(unsigned i = 0; i < nrules; i++){ + expr_ref f(m_ctx.get_manager()); + rs.get_rule(i)->to_formula(f); + rules.push_back(f); } } else From bbdc8b33e0ab4153b2f3782f01025cf355a080df Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 8 Oct 2014 13:56:46 -0700 Subject: [PATCH 10/32] prevent creating some useless solvers in duality --- src/duality/duality_solver.cpp | 29 ++++++++++++++++-------- src/muz/duality/duality_dl_interface.cpp | 21 +---------------- 2 files changed, 21 insertions(+), 29 deletions(-) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index bbd1ebe0a..69759f9bb 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -802,6 +802,15 @@ namespace Duality { annot.Simplify(); } + bool NodeSolutionFromIndSetFull(Node *node){ + std::vector &insts = insts_of_node[node]; + for(unsigned j = 0; j < insts.size(); j++) + if(indset->Contains(insts[j])) + if(insts[j]->Annotation.IsFull()) + return true; + return false; + } + bool recursionBounded; /** See if the solution might be bounded. */ @@ -1453,16 +1462,18 @@ namespace Duality { slvr.pop(1); delete checker; #else - RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/); - 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); + if(!NodeSolutionFromIndSetFull(edge->Parent)){ + RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/); + 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); } - gen_cands_rpfp->Pop(1); #endif } updated_nodes.clear(); diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index c7fa0a08f..9a6d0c633 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -158,26 +158,7 @@ lbool dl_interface::query(::expr * query) { vector bounds; // m_ctx.get_rules_as_formulas(rules, names); - expr_ref query_ref(m_ctx.get_manager()); - if(****){ - m_ctx.flush_add_rules(); - datalog::rule_manager& rm = m_ctx.get_rule_manager(); - rm.mk_query(query, m_ctx.get_rules()); - apply_default_transformation(m_ctx); - rule_set &rs = m_ctx.get_rules(); - if(m_ctx.get_rules().get_output_predicates().empty()) - query_ref = m_ctx.get_manager().mk_true(); - else { - query_pred = m_ctx.get_rules().get_output_predicate(); - func_decl_ref query_pred(m_ctx.get_manager()); - query_pred = m_ctx.get_rules().get_output_predicate(); - ptr_vector sorts; - unsi - - } - } - else - m_ctx.get_raw_rule_formulas(rules, names, bounds); + m_ctx.get_raw_rule_formulas(rules, names, bounds); // get all the rules as clauses std::vector &clauses = _d->clauses; From 6e18f44d991344fc444b21c13e4c2233334ab6d8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 22 Oct 2014 10:42:23 -0700 Subject: [PATCH 11/32] fixed error check in read_interpolation_problem --- src/api/api_interp.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index dbf68da38..63ecc6c24 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -617,7 +617,7 @@ extern "C" { } for (unsigned j = 0; j < num - 1; j++) - if (read_parents[j] == SHRT_MIN){ + if (read_parents[j] == SHRT_MAX){ read_error << "formula " << j + 1 << ": unreferenced"; goto fail; } @@ -717,4 +717,4 @@ Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx, __in unsigned incremental, __in unsigned num_theory, __in_ecount(num_theory) Z3_ast *theory); -#endif \ No newline at end of file +#endif From 5454e389355f3a98e82ccd03815cf058458190fd Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 22 Oct 2014 10:43:04 -0700 Subject: [PATCH 12/32] replaced check_interpolants option with interp.check --- src/cmd_context/basic_cmds.cpp | 6 ------ src/cmd_context/cmd_context.cpp | 8 -------- src/cmd_context/cmd_context.h | 2 -- src/cmd_context/context_params.cpp | 5 ----- src/cmd_context/context_params.h | 1 - src/cmd_context/interpolant_cmds.cpp | 2 +- src/interp/iz3params.pyg | 1 + 7 files changed, 2 insertions(+), 23 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 836ade9ce..a80c5bc6c 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -241,7 +241,6 @@ protected: symbol m_produce_models; symbol m_produce_assignments; symbol m_produce_interpolants; - symbol m_check_interpolants; symbol m_regular_output_channel; symbol m_diagnostic_output_channel; symbol m_random_seed; @@ -256,7 +255,6 @@ protected: s == m_print_success || s == m_print_warning || s == m_expand_definitions || s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants || - s == m_check_interpolants || s == m_regular_output_channel || s == m_diagnostic_output_channel || s == m_random_seed || s == m_verbosity || s == m_global_decls; } @@ -275,7 +273,6 @@ public: m_produce_models(":produce-models"), m_produce_assignments(":produce-assignments"), m_produce_interpolants(":produce-interpolants"), - m_check_interpolants(":check-interpolants"), m_regular_output_channel(":regular-output-channel"), m_diagnostic_output_channel(":diagnostic-output-channel"), m_random_seed(":random-seed"), @@ -347,9 +344,6 @@ class set_option_cmd : public set_get_option_cmd { check_not_initialized(ctx, m_produce_interpolants); ctx.set_produce_interpolants(to_bool(value)); } - else if (m_option == m_check_interpolants) { - ctx.set_check_interpolants(to_bool(value)); - } else if (m_option == m_produce_unsat_cores) { check_not_initialized(ctx, m_produce_unsat_cores); ctx.set_produce_unsat_cores(to_bool(value)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index ce2838aba..731608524 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -397,10 +397,6 @@ void cmd_context::set_produce_interpolants(bool f) { // set_solver_factory(mk_smt_solver_factory()); } -void cmd_context::set_check_interpolants(bool f) { - m_params.m_check_interpolants = f; -} - bool cmd_context::produce_models() const { return m_params.m_model; } @@ -414,10 +410,6 @@ bool cmd_context::produce_interpolants() const { return m_params.m_proof; } -bool cmd_context::check_interpolants() const { - return m_params.m_check_interpolants; -} - bool cmd_context::produce_unsat_cores() const { return m_params.m_unsat_core; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index e34975183..8ad07e8cc 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -279,7 +279,6 @@ public: bool produce_models() const; bool produce_proofs() const; bool produce_interpolants() const; - bool check_interpolants() const; bool produce_unsat_cores() const; bool well_sorted_check_enabled() const; bool validate_model_enabled() const; @@ -287,7 +286,6 @@ public: void set_produce_unsat_cores(bool flag); void set_produce_proofs(bool flag); void set_produce_interpolants(bool flag); - void set_check_interpolants(bool flag); bool produce_assignments() const { return m_produce_assignments; } void set_produce_assignments(bool flag) { m_produce_assignments = flag; } void set_status(status st) { m_status = st; } diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 254a1d931..f87c8d264 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -61,9 +61,6 @@ void context_params::set(char const * param, char const * value) { else if (p == "proof") { set_bool(m_proof, param, value); } - else if (p == "check_interpolants") { - set_bool(m_check_interpolants, param, value); - } else if (p == "model") { set_bool(m_model, param, value); } @@ -105,7 +102,6 @@ void context_params::updt_params(params_ref const & p) { m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true)); m_auto_config = p.get_bool("auto_config", true); m_proof = p.get_bool("proof", false); - m_check_interpolants = p.get_bool("check_interpolants", false); m_model = p.get_bool("model", true); m_model_validate = p.get_bool("model_validate", false); m_trace = p.get_bool("trace", false); @@ -120,7 +116,6 @@ void context_params::collect_param_descrs(param_descrs & d) { d.insert("well_sorted_check", CPK_BOOL, "type checker", "true"); d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); - d.insert("check_interpolants", CPK_BOOL, "check correctness of interpolants", "false"); d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false"); d.insert("trace", CPK_BOOL, "trace generation for VCC", "false"); d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log"); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index e26fd3fe5..506e559db 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -30,7 +30,6 @@ public: bool m_auto_config; bool m_proof; bool m_interpolants; - bool m_check_interpolants; bool m_debug_ref_count; bool m_trace; std::string m_trace_file_name; diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index cb83b52f6..42646a99d 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -65,7 +65,7 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx, s.cleanup(); // verify, for the paranoid... - if(check || ctx.check_interpolants()){ + if(check || interp_params(m_params).check()){ std::ostringstream err; ast_manager &_m = ctx.m(); diff --git a/src/interp/iz3params.pyg b/src/interp/iz3params.pyg index 5b574c859..3116a18db 100644 --- a/src/interp/iz3params.pyg +++ b/src/interp/iz3params.pyg @@ -2,4 +2,5 @@ def_module_params('interp', description='interpolation parameters', export=True, params=(('profile', BOOL, False, '(INTERP) profile interpolation'), + ('check', BOOL, False, '(INTERP) check interpolants'), )) From 31a017e99e1569b3913bd260816a3b9a45d44b3f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 22 Oct 2014 19:47:50 +0100 Subject: [PATCH 13/32] FPA: standard function names consistency, improved error messages, bugfixes. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 308 +++++++++++++++------------- src/ast/float_decl_plugin.h | 45 ++-- src/ast/fpa/fpa2bv_converter.cpp | 88 ++++++-- src/ast/fpa/fpa2bv_converter.h | 9 +- src/ast/fpa/fpa2bv_rewriter.h | 18 +- src/ast/rewriter/float_rewriter.cpp | 41 ++-- src/ast/rewriter/float_rewriter.h | 9 +- 7 files changed, 303 insertions(+), 215 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 5466df069..f51101d79 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -40,11 +40,10 @@ void float_decl_plugin::set_manager(ast_manager * m, family_id id) { SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before float_decl_plugin. m_manager->inc_ref(m_int_sort); - if (m_manager->has_plugin(symbol("bv"))) { - // bv plugin is optional, so m_bv_plugin may be 0 + // BV is not optional anymore. + SASSERT(m_manager->has_plugin(symbol("bv"))); m_bv_fid = m_manager->mk_family_id("bv"); m_bv_plugin = static_cast(m_manager->get_plugin(m_bv_fid)); - } } float_decl_plugin::~float_decl_plugin() { @@ -103,6 +102,18 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) { m_fm.mk_nan(ebits, sbits, val); return true; } + else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_ZERO)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_pzero(ebits, sbits, val); + return true; + } + else if (is_app_of(n, m_family_id, OP_FLOAT_MINUS_ZERO)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_nzero(ebits, sbits, val); + return true; + } return false; } @@ -156,7 +167,7 @@ sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) { parameter ps[2] = { p1, p2 }; sort_size sz; sz = sort_size::mk_very_big(); // TODO: refine - return m_manager->mk_sort(symbol("FP"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps)); + return m_manager->mk_sort(symbol("FloatingPoint"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps)); } sort * float_decl_plugin::mk_rm_sort() { @@ -176,6 +187,14 @@ sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete return mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); case ROUNDING_MODE_SORT: return mk_rm_sort(); + case FLOAT16_SORT: + return mk_float_sort(5, 11); + case FLOAT32_SORT: + return mk_float_sort(8, 24); + case FLOAT64_SORT: + return mk_float_sort(11, 53); + case FLOAT128_SORT: + return mk_float_sort(15, 133); default: m_manager->raise_exception("unknown floating point theory sort"); return 0; @@ -229,17 +248,18 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par unsigned ebits = s->get_parameter(0).get_int(); unsigned sbits = s->get_parameter(1).get_int(); scoped_mpf val(m_fm); - if (k == OP_FLOAT_NAN) { - m_fm.mk_nan(ebits, sbits, val); + + switch (k) + { + case OP_FLOAT_NAN: m_fm.mk_nan(ebits, sbits, val); SASSERT(m_fm.is_nan(val)); + break; + case OP_FLOAT_MINUS_INF: m_fm.mk_ninf(ebits, sbits, val); break; + case OP_FLOAT_PLUS_INF: m_fm.mk_pinf(ebits, sbits, val); break; + case OP_FLOAT_MINUS_ZERO: m_fm.mk_nzero(ebits, sbits, val); break; + case OP_FLOAT_PLUS_ZERO: m_fm.mk_pzero(ebits, sbits, val); break; } - else if (k == OP_FLOAT_MINUS_INF) { - m_fm.mk_ninf(ebits, sbits, val); - } - else { - SASSERT(k == OP_FLOAT_PLUS_INF); - m_fm.mk_pinf(ebits, sbits, val); - } + return mk_value_decl(val); } @@ -248,14 +268,14 @@ func_decl * float_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_paramet if (arity != 2) m_manager->raise_exception("invalid number of arguments to floating point relation"); if (domain[0] != domain[1] || !is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments"); symbol name; switch (k) { - case OP_FLOAT_EQ: name = "=="; break; - case OP_FLOAT_LT: name = "<"; break; - case OP_FLOAT_GT: name = ">"; break; - case OP_FLOAT_LE: name = "<="; break; - case OP_FLOAT_GE: name = ">="; break; + case OP_FLOAT_EQ: name = "fp.eq"; break; + case OP_FLOAT_LT: name = "fp.lt"; break; + case OP_FLOAT_GT: name = "fp.gt"; break; + case OP_FLOAT_LE: name = "fp.lte"; break; + case OP_FLOAT_GE: name = "fp.gte"; break; default: UNREACHABLE(); break; @@ -270,17 +290,18 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param if (arity != 1) m_manager->raise_exception("invalid number of arguments to floating point relation"); if (!is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); symbol name; switch (k) { - case OP_FLOAT_IS_ZERO: name = "isZero"; break; - case OP_FLOAT_IS_NZERO: name = "isNZero"; break; - case OP_FLOAT_IS_PZERO: name = "isPZero"; break; - case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break; - case OP_FLOAT_IS_NAN: name = "isNaN"; break; - case OP_FLOAT_IS_INF: name = "isInfinite"; break; - case OP_FLOAT_IS_NORMAL: name = "isNormal"; break; - case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal"; break; + case OP_FLOAT_IS_ZERO: name = "fp.isZero"; break; + case OP_FLOAT_IS_NZERO: name = "fp.isNZero"; break; + case OP_FLOAT_IS_PZERO: name = "fp.isPZero"; break; + case OP_FLOAT_IS_NEGATIVE: name = "fp.isNegative"; break; + case OP_FLOAT_IS_POSITIVE: name = "fp.isPositive"; break; + case OP_FLOAT_IS_NAN: name = "fp.isNaN"; break; + case OP_FLOAT_IS_INF: name = "fp.isInfinite"; break; + case OP_FLOAT_IS_NORMAL: name = "fp.isNormal"; break; + case OP_FLOAT_IS_SUBNORMAL: name = "fp.isSubnormal"; break; default: UNREACHABLE(); break; @@ -293,11 +314,11 @@ func_decl * float_decl_plugin::mk_unary_decl(decl_kind k, unsigned num_parameter if (arity != 1) m_manager->raise_exception("invalid number of arguments to floating point operator"); if (!is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); symbol name; switch (k) { - case OP_FLOAT_ABS: name = "abs"; break; - case OP_FLOAT_UMINUS: name = "-"; break; + case OP_FLOAT_ABS: name = "fp.abs"; break; + case OP_FLOAT_NEG: name = "fp.neg"; break; default: UNREACHABLE(); break; @@ -310,12 +331,12 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete if (arity != 2) m_manager->raise_exception("invalid number of arguments to floating point operator"); if (domain[0] != domain[1] || !is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); symbol name; switch (k) { - case OP_FLOAT_REM: name = "remainder"; break; - case OP_FLOAT_MIN: name = "fp.min"; break; - case OP_FLOAT_MAX: name = "fp.max"; break; + case OP_FLOAT_REM: name = "fp.rem"; break; + case OP_FLOAT_MIN: name = "fp.min"; break; + case OP_FLOAT_MAX: name = "fp.max"; break; default: UNREACHABLE(); break; @@ -327,14 +348,16 @@ func_decl * float_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_param unsigned arity, sort * const * domain, sort * range) { if (arity != 3) m_manager->raise_exception("invalid number of arguments to floating point operator"); - if (!is_rm_sort(domain[0]) || domain[1] != domain[2] || !is_float_sort(domain[1])) - m_manager->raise_exception("sort mismatch"); + if (!is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort"); + if (domain[1] != domain[2] || !is_float_sort(domain[1])) + m_manager->raise_exception("sort mismatch, expected arguments 1 and 2 of equal FloatingPoint sorts"); symbol name; switch (k) { - case OP_FLOAT_ADD: name = "+"; break; - case OP_FLOAT_SUB: name = "-"; break; - case OP_FLOAT_MUL: name = "*"; break; - case OP_FLOAT_DIV: name = "/"; break; + case OP_FLOAT_ADD: name = "fp.add"; break; + case OP_FLOAT_SUB: name = "fp.sub"; break; + case OP_FLOAT_MUL: name = "fp.mul"; break; + case OP_FLOAT_DIV: name = "fp.div"; break; default: UNREACHABLE(); break; @@ -346,12 +369,14 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame unsigned arity, sort * const * domain, sort * range) { if (arity != 2) m_manager->raise_exception("invalid number of arguments to floating point operator"); - if (!is_rm_sort(domain[0]) || !is_float_sort(domain[1])) - m_manager->raise_exception("sort mismatch"); + if (!is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected RoundingMode as first argument"); + if (!is_float_sort(domain[1])) + m_manager->raise_exception("sort mismatch, expected FloatingPoint as second argument"); symbol name; switch (k) { - case OP_FLOAT_SQRT: name = "squareRoot"; break; - case OP_FLOAT_ROUND_TO_INTEGRAL: name = "roundToIntegral"; break; + case OP_FLOAT_SQRT: name = "fp.sqrt"; break; + case OP_FLOAT_ROUND_TO_INTEGRAL: name = "fp.roundToIntegral"; break; default: UNREACHABLE(); break; @@ -359,13 +384,15 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k)); } -func_decl * float_decl_plugin::mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * float_decl_plugin::mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 4) m_manager->raise_exception("invalid number of arguments to fused_ma operator"); - if (!is_rm_sort(domain[0]) || domain[1] != domain[2] || domain[1] != domain[3] || !is_float_sort(domain[1])) - m_manager->raise_exception("sort mismatch"); - symbol name("fusedMA"); + if (!is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected RoundingMode as first argument"); + if (domain[1] != domain[2] || domain[1] != domain[3] || !is_float_sort(domain[1])) + m_manager->raise_exception("sort mismatch, expected arguments 1,2,3 of equal FloatingPoint sort"); + symbol name("fp.fma"); return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k)); } @@ -375,12 +402,13 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, 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)) { - // When the bv_decl_plugin is installed, then we know how to convert 3 bit-vectors into a float! + // 3 BVs -> 1 FP sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); - symbol name("asFloat"); + symbol name("fp"); 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)) { + // 1 BV -> 1 FP if (num_parameters != 2) m_manager->raise_exception("invalid number of parameters to to_fp"); if (!parameters[0].is_int() || !parameters[1].is_int()) @@ -389,37 +417,67 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, int sbits = parameters[1].get_int(); sort * fp = mk_float_sort(ebits, sbits); - symbol name("asFloat"); + symbol name("to_fp"); + 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 == 2 && + is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) && + is_sort_of(domain[1], m_bv_fid, BV_SORT)) { + // Rounding + 1 BV -> 1 FP + 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("to_fp"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } + else if (arity == 2 && + is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) && + is_sort_of(domain[1], m_family_id, FLOAT_SORT)) { + // Rounding + 1 FP -> 1 FP + 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(); + if (!is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort"); + if (!is_sort_of(domain[1], m_family_id, FLOAT_SORT)) + m_manager->raise_exception("sort mismatch, expected second argument of FloatingPoint sort"); + + sort * fp = mk_float_sort(ebits, sbits); + symbol name("to_fp"); 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. + // 1 Real -> 1 FP if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) - m_manager->raise_exception("expecting two integer parameters to asFloat"); + m_manager->raise_exception("expecting two integer parameters to to_fp"); if (arity != 2 && arity != 3) - m_manager->raise_exception("invalid number of arguments to asFloat operator"); + m_manager->raise_exception("invalid number of arguments to to_fp operator"); if (arity == 3 && domain[2] != m_int_sort) - m_manager->raise_exception("sort mismatch"); - if (!is_rm_sort(domain[0]) || - !(domain[1] == m_real_sort || is_sort_of(domain[1], m_family_id, FLOAT_SORT))) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected second argument of Int sort"); + if (domain[1] != m_real_sort) + m_manager->raise_exception("sort mismatch, expected second argument of Real sort"); sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); - symbol name("asFloat"); + symbol name("to_fp"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); } } -func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * float_decl_plugin::mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { - if (!m_bv_plugin) - m_manager->raise_exception("asIEEEBV unsupported; use a logic with BV support"); if (arity != 1) m_manager->raise_exception("invalid number of arguments to asIEEEBV"); if (!is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); - - // When the bv_decl_plugin is installed, then we know how to convert a float to an IEEE bit-vector. + m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); + unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int(); parameter ps[] = { parameter(float_sz) }; sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps); @@ -429,41 +487,34 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter 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"); + m_manager->raise_exception("sort mismatch"); 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, +func_decl * float_decl_plugin::mk_to_ubv(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"); + m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort"); if (!is_sort_of(domain[1], m_bv_fid, BV_SORT)) - m_manager->raise_exception("sort mismtach"); + m_manager->raise_exception("sort mismatch, expected second argument of BV sort"); sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); - symbol name("to_fp_unsigned"); + symbol name("fp.t_ubv"); 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(); @@ -498,14 +549,15 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_FLOAT_IS_ZERO: case OP_FLOAT_IS_NZERO: case OP_FLOAT_IS_PZERO: - case OP_FLOAT_IS_SIGN_MINUS: + case OP_FLOAT_IS_NEGATIVE: + case OP_FLOAT_IS_POSITIVE: case OP_FLOAT_IS_NAN: case OP_FLOAT_IS_INF: case OP_FLOAT_IS_NORMAL: case OP_FLOAT_IS_SUBNORMAL: return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_ABS: - case OP_FLOAT_UMINUS: + case OP_FLOAT_NEG: return mk_unary_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_REM: case OP_FLOAT_MIN: @@ -517,20 +569,18 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_SUB: if (arity == 1) - return mk_unary_decl(OP_FLOAT_UMINUS, num_parameters, parameters, arity, domain, range); + return mk_unary_decl(OP_FLOAT_NEG, num_parameters, parameters, arity, domain, range); else return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_SQRT: case OP_FLOAT_ROUND_TO_INTEGRAL: return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_FUSED_MA: - 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_FMA: + return mk_fma(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_IEEE_BV: + return mk_float_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: @@ -544,8 +594,11 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters } void float_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - op_names.push_back(builtin_name("plusInfinity", OP_FLOAT_PLUS_INF)); - op_names.push_back(builtin_name("minusInfinity", OP_FLOAT_MINUS_INF)); + // These are the operators from the final draft of the SMT FloatingPoint 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("+zero", OP_FLOAT_PLUS_ZERO)); + op_names.push_back(builtin_name("-zero", OP_FLOAT_MINUS_ZERO)); op_names.push_back(builtin_name("NaN", OP_FLOAT_NAN)); op_names.push_back(builtin_name("roundNearestTiesToEven", OP_RM_NEAREST_TIES_TO_EVEN)); @@ -554,46 +607,6 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("roundTowardNegative", OP_RM_TOWARD_NEGATIVE)); op_names.push_back(builtin_name("roundTowardZero", OP_RM_TOWARD_ZERO)); - op_names.push_back(builtin_name("+", OP_FLOAT_ADD)); - op_names.push_back(builtin_name("-", OP_FLOAT_SUB)); - op_names.push_back(builtin_name("/", OP_FLOAT_DIV)); - op_names.push_back(builtin_name("*", OP_FLOAT_MUL)); - - op_names.push_back(builtin_name("abs", OP_FLOAT_ABS)); - op_names.push_back(builtin_name("remainder", OP_FLOAT_REM)); - op_names.push_back(builtin_name("fusedMA", OP_FLOAT_FUSED_MA)); - op_names.push_back(builtin_name("squareRoot", OP_FLOAT_SQRT)); - op_names.push_back(builtin_name("roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL)); - - op_names.push_back(builtin_name("==", OP_FLOAT_EQ)); - - op_names.push_back(builtin_name("<", OP_FLOAT_LT)); - op_names.push_back(builtin_name(">", OP_FLOAT_GT)); - op_names.push_back(builtin_name("<=", OP_FLOAT_LE)); - op_names.push_back(builtin_name(">=", OP_FLOAT_GE)); - - op_names.push_back(builtin_name("isNaN", OP_FLOAT_IS_NAN)); - op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF)); - op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO)); - op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO)); - op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO)); - op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL)); - op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL)); - op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS)); - - // Disabled min/max, clashes with user-defined min/max functions - // op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); - // op_names.push_back(builtin_name("max", OP_FLOAT_MAX)); - - op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT)); - - if (m_bv_plugin) - op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV)); - - // 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)); op_names.push_back(builtin_name("RTP", OP_RM_TOWARD_POSITIVE)); @@ -601,44 +614,47 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("RTZ", OP_RM_TOWARD_ZERO)); op_names.push_back(builtin_name("fp.abs", OP_FLOAT_ABS)); - op_names.push_back(builtin_name("fp.neg", OP_FLOAT_UMINUS)); + op_names.push_back(builtin_name("fp.neg", OP_FLOAT_NEG)); op_names.push_back(builtin_name("fp.add", OP_FLOAT_ADD)); op_names.push_back(builtin_name("fp.sub", OP_FLOAT_SUB)); op_names.push_back(builtin_name("fp.mul", OP_FLOAT_MUL)); op_names.push_back(builtin_name("fp.div", OP_FLOAT_DIV)); - op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FUSED_MA)); + op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FMA)); op_names.push_back(builtin_name("fp.sqrt", OP_FLOAT_SQRT)); op_names.push_back(builtin_name("fp.rem", OP_FLOAT_REM)); - op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ)); + op_names.push_back(builtin_name("fp.roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL)); + 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.leq", OP_FLOAT_LE)); op_names.push_back(builtin_name("fp.lt", OP_FLOAT_LT)); op_names.push_back(builtin_name("fp.geq", OP_FLOAT_GE)); op_names.push_back(builtin_name("fp.gt", OP_FLOAT_GT)); + op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ)); + op_names.push_back(builtin_name("fp.isNormal", OP_FLOAT_IS_NORMAL)); op_names.push_back(builtin_name("fp.isSubnormal", OP_FLOAT_IS_SUBNORMAL)); op_names.push_back(builtin_name("fp.isZero", OP_FLOAT_IS_ZERO)); op_names.push_back(builtin_name("fp.isInfinite", OP_FLOAT_IS_INF)); 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("to_fp", OP_TO_FLOAT)); + op_names.push_back(builtin_name("fp.isNegative", OP_FLOAT_IS_NEGATIVE)); + op_names.push_back(builtin_name("fp.isPositive", OP_FLOAT_IS_POSITIVE)); - if (m_bv_plugin) { - 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", OP_FLOAT_FP)); + 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.toReal", ?)); + op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT)); } 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("FloatingPoint", 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)); + // The final theory supports three common FloatingPoint sorts + sort_names.push_back(builtin_name("Float16", FLOAT16_SORT)); + sort_names.push_back(builtin_name("Float32", FLOAT32_SORT)); + sort_names.push_back(builtin_name("Float64", FLOAT64_SORT)); + sort_names.push_back(builtin_name("Float128", FLOAT128_SORT)); } expr * float_decl_plugin::get_some_value(sort * s) { @@ -662,6 +678,8 @@ bool float_decl_plugin::is_value(app * e) const { case OP_FLOAT_VALUE: case OP_FLOAT_PLUS_INF: case OP_FLOAT_MINUS_INF: + case OP_FLOAT_PLUS_ZERO: + case OP_FLOAT_MINUS_ZERO: case OP_FLOAT_NAN: return true; case OP_TO_FLOAT: diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 58c37080d..c7ec04932 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -27,7 +27,11 @@ Revision History: enum float_sort_kind { FLOAT_SORT, - ROUNDING_MODE_SORT + ROUNDING_MODE_SORT, + FLOAT16_SORT, + FLOAT32_SORT, + FLOAT64_SORT, + FLOAT128_SORT }; enum float_op_kind { @@ -37,22 +41,23 @@ enum float_op_kind { OP_RM_TOWARD_NEGATIVE, OP_RM_TOWARD_ZERO, - OP_FLOAT_VALUE, OP_FLOAT_PLUS_INF, OP_FLOAT_MINUS_INF, OP_FLOAT_NAN, + OP_FLOAT_PLUS_ZERO, + OP_FLOAT_MINUS_ZERO, OP_FLOAT_ADD, OP_FLOAT_SUB, - OP_FLOAT_UMINUS, + OP_FLOAT_NEG, OP_FLOAT_MUL, OP_FLOAT_DIV, OP_FLOAT_REM, OP_FLOAT_ABS, OP_FLOAT_MIN, OP_FLOAT_MAX, - OP_FLOAT_FUSED_MA, // x*y + z + OP_FLOAT_FMA, // x*y + z OP_FLOAT_SQRT, OP_FLOAT_ROUND_TO_INTEGRAL, @@ -68,13 +73,14 @@ enum float_op_kind { OP_FLOAT_IS_SUBNORMAL, OP_FLOAT_IS_PZERO, OP_FLOAT_IS_NZERO, - OP_FLOAT_IS_SIGN_MINUS, + OP_FLOAT_IS_NEGATIVE, + OP_FLOAT_IS_POSITIVE, OP_TO_FLOAT, - OP_TO_IEEE_BV, + OP_FLOAT_TO_IEEE_BV, OP_FLOAT_FP, - OP_FLOAT_TO_FP_UNSIGNED, + OP_FLOAT_TO_FP, OP_FLOAT_TO_UBV, OP_FLOAT_TO_SBV, OP_FLOAT_TO_REAL, @@ -125,16 +131,14 @@ class float_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_rm_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); + func_decl * mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); func_decl * mk_to_float(decl_kind k, unsigned num_parameters, parameter const * parameters, 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_float_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, @@ -195,6 +199,7 @@ public: family_id get_fid() const { return m_fid; } family_id get_family_id() const { return m_fid; } arith_util & au() { return m_a_util; } + float_decl_plugin & plugin() { return *m_plugin; } sort * mk_float_sort(unsigned ebits, unsigned sbits); sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); } @@ -242,16 +247,16 @@ public: app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); } app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); } app * mk_div(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_DIV, arg1, arg2, arg3); } - app * mk_uminus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_UMINUS, arg1); } + app * mk_neg(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_NEG, arg1); } app * mk_rem(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_REM, arg1, arg2); } app * mk_max(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MAX, arg1, arg2); } app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MIN, arg1, arg2); } app * mk_abs(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1); } app * mk_sqrt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_SQRT, arg1, arg2); } app * mk_round(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); } - app * mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) { + app * mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) { expr * args[4] = { arg1, arg2, arg3, arg4 }; - return m().mk_app(m_fid, OP_FLOAT_FUSED_MA, 4, args); + return m().mk_app(m_fid, OP_FLOAT_FMA, 4, args); } app * mk_float_eq(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_EQ, arg1, arg2); } @@ -267,11 +272,13 @@ public: app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); } app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); } app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); } - app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); } + app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); } + app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_POSITIVE, arg1); } + app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); } - bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_UMINUS); } + bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_NEG); } - app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_TO_IEEE_BV, arg1); } + app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_TO_IEEE_BV, arg1); } }; #endif diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d6f362902..5f92b4d94 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -136,12 +136,13 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { unsigned sbits = m_util.get_sbits(srt); expr_ref sgn(m), s(m), e(m); - sort_ref s_sgn(m), s_sig(m), s_exp(m); - s_sgn = m_bv_util.mk_sort(1); - s_sig = m_bv_util.mk_sort(sbits-1); - s_exp = m_bv_util.mk_sort(ebits); #ifdef Z3DEBUG + sort_ref s_sgn(m), s_sig(m), s_exp(m); + s_sgn = m_bv_util.mk_sort(1); + s_sig = m_bv_util.mk_sort(sbits - 1); + s_exp = m_bv_util.mk_sort(ebits); + std::string p("fpa2bv"); std::string name = f->get_name().str(); @@ -149,9 +150,17 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig); e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp); #else - sgn = m.mk_fresh_const(0, s_sgn); - s = m.mk_fresh_const(0, s_sig); - e = m.mk_fresh_const(0, s_exp); + expr_ref bv(m); + unsigned bv_sz = 1 + ebits + (sbits - 1); + bv = m.mk_fresh_const(0, m_bv_util.mk_sort(bv_sz)); + + sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv); + e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv); + s = m_bv_util.mk_extract(sbits - 2, 0, bv); + + SASSERT(m_bv_util.get_bv_size(sgn) == 1); + SASSERT(m_bv_util.get_bv_size(s) == sbits-1); + SASSERT(m_bv_util.get_bv_size(e) == ebits); #endif mk_triple(sgn, s, e, result); @@ -595,12 +604,12 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); expr_ref t(m); - mk_uminus(f, 1, &args[2], t); + mk_neg(f, 1, &args[2], t); expr * nargs[3] = { args[0], args[1], t }; mk_add(f, 3, nargs, result); } -void fpa2bv_converter::mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr * sgn, * s, * e; split(args[0], sgn, s, e); @@ -906,7 +915,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, TRACE("fpa2bv_div", tout << "DIV = " << mk_ismt2_pp(result, m) << std::endl; ); } -void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); // Remainder is always exact, so there is no rounding mode. @@ -1114,7 +1123,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, mk_triple(r_sgn, r_sig, r_exp, result); } -void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 4); // fusedma means (x * y) + z @@ -1835,9 +1844,18 @@ void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const mk_is_denormal(args[0], result); } -void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); mk_is_neg(args[0], result); + TRACE("fpa2bv_is_negative", tout << "result = " << mk_ismt2_pp(result, m) << std::endl;); +} + +void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + expr_ref t1(m), t2(m); + mk_is_nan(args[0], t1); + mk_is_pos(args[0], t2); + result = m.mk_and(m.mk_not(t1), t2); } void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -2123,7 +2141,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr * sgn, * s, * e; - split(args[0], sgn, s, e); + split(args[0], sgn, s, e); result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); } @@ -2132,19 +2150,55 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e 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) { + SASSERT(num == 2); + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_int()); + + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + int width = f->get_parameter(0).get_int(); + + expr * rm = args[0]; + expr * x = args[1]; + + expr * sgn, *s, *e; + split(x, sgn, s, e); + NOT_IMPLEMENTED_YET(); } void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_int()); + + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + int width = f->get_parameter(0).get_int(); + + expr * rm = args[0]; + expr * x = args[1]; + + expr * sgn, *s, *e; + split(x, sgn, s, e); + NOT_IMPLEMENTED_YET(); } void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + int width = f->get_parameter(0).get_int(); + + expr * rm = args[0]; + expr * x = args[1]; + + expr * sgn, *s, *e; + split(x, sgn, s, e); + NOT_IMPLEMENTED_YET(); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index dcb508ffd..eb539d8ae 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -94,14 +94,14 @@ public: void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -114,7 +114,8 @@ public: void mk_is_zero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 225aad668..7a245b71a 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -65,8 +65,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { bool max_steps_exceeded(unsigned num_steps) const { cooperate("fpa2bv"); - if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); return num_steps > m_max_steps; } @@ -117,17 +115,19 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE; case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE; case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE; + case OP_FLOAT_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; + case OP_FLOAT_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE; case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE; case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE; case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE; - case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE; + case OP_FLOAT_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE; case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE; case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE; - case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE; + case OP_FLOAT_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE; case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE; case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE; - case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE; + case OP_FLOAT_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE; @@ -142,18 +142,18 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; - case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_NEGATIVE: m_conv.mk_is_negative(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_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;); - throw tactic_exception("NYI"); + NOT_IMPLEMENTED_YET(); } } diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index a4212d579..7dc34dd11 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -36,17 +36,17 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c br_status st = BR_FAILED; SASSERT(f->get_family_id() == get_fid()); switch (f->get_decl_kind()) { - case OP_TO_FLOAT: st = mk_to_float(f, num_args, args, result); break; + case OP_TO_FLOAT: st = mk_to_fp(f, num_args, args, result); break; case OP_FLOAT_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break; case OP_FLOAT_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break; - case OP_FLOAT_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break; + case OP_FLOAT_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break; case OP_FLOAT_MUL: SASSERT(num_args == 3); st = mk_mul(args[0], args[1], args[2], result); break; case OP_FLOAT_DIV: SASSERT(num_args == 3); st = mk_div(args[0], args[1], args[2], result); break; case OP_FLOAT_REM: SASSERT(num_args == 2); st = mk_rem(args[0], args[1], result); break; case OP_FLOAT_ABS: SASSERT(num_args == 1); st = mk_abs(args[0], result); break; case OP_FLOAT_MIN: SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break; case OP_FLOAT_MAX: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break; - case OP_FLOAT_FUSED_MA: SASSERT(num_args == 4); st = mk_fused_ma(args[0], args[1], args[2], args[3], result); break; + case OP_FLOAT_FMA: SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break; case OP_FLOAT_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break; case OP_FLOAT_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break; @@ -62,10 +62,10 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break; case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break; 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_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break; + case OP_FLOAT_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break; + case OP_FLOAT_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; @@ -73,7 +73,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c return st; } -br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { +br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_parameter(0).is_int()); SASSERT(f->get_parameter(1).is_int()); @@ -154,7 +154,7 @@ br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { // a - b = a + (-b) - result = m_util.mk_add(arg1, arg2, m_util.mk_uminus(arg3)); + result = m_util.mk_add(arg1, arg2, m_util.mk_neg(arg3)); return BR_REWRITE2; } @@ -188,7 +188,7 @@ br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref return BR_FAILED; } -br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) { +br_status float_rewriter::mk_neg(expr * arg1, expr_ref & result) { if (m_util.is_nan(arg1)) { // -nan --> nan result = arg1; @@ -204,7 +204,7 @@ br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) { result = m_util.mk_plus_inf(m().get_sort(arg1)); return BR_DONE; } - if (m_util.is_uminus(arg1)) { + if (m_util.is_neg(arg1)) { // - - a --> a result = to_app(arg1)->get_arg(0); return BR_DONE; @@ -239,7 +239,7 @@ br_status float_rewriter::mk_abs(expr * arg1, expr_ref & result) { return BR_DONE; } result = m().mk_ite(m_util.mk_is_sign_minus(arg1), - m_util.mk_uminus(arg1), + m_util.mk_neg(arg1), arg1); return BR_REWRITE2; } @@ -284,7 +284,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { return BR_REWRITE_FULL; } -br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { +br_status float_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_value(arg1, rm)) { scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm()); @@ -480,7 +480,7 @@ br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) { +br_status float_rewriter::mk_is_negative(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { result = (m_util.fm().is_neg(v)) ? m().mk_true() : m().mk_false(); @@ -490,6 +490,17 @@ br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) { return BR_FAILED; } +br_status float_rewriter::mk_is_positive(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_neg(v) || m_util.fm().is_nan(v)) ? m().mk_false() : m().mk_true(); + return BR_DONE; + } + + return BR_FAILED; +} + + // This the SMT = br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_util.fm()), v2(m_util.fm()); @@ -532,10 +543,6 @@ br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref 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; } diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 0f44d227c..4d8cec856 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -45,17 +45,16 @@ public: br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result); - br_status mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); - br_status mk_uminus(expr * arg1, expr_ref & result); + br_status mk_neg(expr * arg1, expr_ref & result); br_status mk_rem(expr * arg1, expr * arg2, expr_ref & result); br_status mk_abs(expr * arg1, expr_ref & result); br_status mk_min(expr * arg1, expr * arg2, expr_ref & result); br_status mk_max(expr * arg1, expr * arg2, expr_ref & result); - br_status mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result); + br_status mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result); br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result); br_status mk_round(expr * arg1, expr * arg2, expr_ref & result); br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result); @@ -70,10 +69,12 @@ public: br_status mk_is_inf(expr * arg1, expr_ref & result); br_status mk_is_normal(expr * arg1, expr_ref & result); br_status mk_is_subnormal(expr * arg1, expr_ref & result); - br_status mk_is_sign_minus(expr * arg1, expr_ref & result); + br_status mk_is_negative(expr * arg1, expr_ref & result); + br_status mk_is_positive(expr * arg1, expr_ref & result); br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); + br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, 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); From 5adfbe885733f67b0d1f5f2a7d051d1a0c60b921 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 22 Oct 2014 21:57:57 +0100 Subject: [PATCH 14/32] Z3Py: Fix test output Signed-off-by: Nuno Lopes --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 470280630..f2318021f 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -38,7 +38,7 @@ Z3 exceptions: ... n = x + y ... except Z3Exception as ex: ... print("failed: %s" % ex) -failed: 'sort mismatch' +failed: sort mismatch """ from z3core import * from z3types import * From a6bee82ef8dd8ad49e90bdc80c796436e1ccaca0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 23 Oct 2014 17:10:31 +0100 Subject: [PATCH 15/32] Interpolation API: fixed some memory leaks Signed-off-by: Christoph M. Wintersteiger --- src/interp/iz3proof_itp.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index e89aa1d6d..52ddcd64f 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -3078,6 +3078,11 @@ public: m().dec_ref(add_pos); m().dec_ref(rewrite_A); m().dec_ref(rewrite_B); + m().dec_ref(normal_step); + m().dec_ref(normal_chain); + m().dec_ref(normal); + m().dec_ref(sforall); + m().dec_ref(sexists); } }; From 6a27d93776fce414f4c4a04fb8358361a2a07d70 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 23 Oct 2014 17:20:55 +0100 Subject: [PATCH 16/32] Fixed memory leaks in interpolation API Signed-off-by: Christoph M. Wintersteiger --- src/api/api_interp.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 63ecc6c24..dd689dcb0 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -273,6 +273,9 @@ extern "C" { 0 // ignore params for now ); + for (unsigned i = 0; i < cnsts.size(); i++) + _m.dec_ref(cnsts[i]); + Z3_lbool status = of_lbool(_status); Z3_ast_vector_ref *v = 0; From fd0920eb36c308f935b43a0bb4ee5cd910ffbd3f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 23 Oct 2014 19:15:26 +0100 Subject: [PATCH 17/32] Updated release notes Signed-off-by: Christoph M. Wintersteiger --- RELEASE_NOTES | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 643c9b26f..4be65b260 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -3,6 +3,15 @@ RELEASE NOTES Version 4.3.2 ============= +- Added preliminary support for the theory of floating point numbers (tactics qffpa, qffpabv, and logics QF_FPA, QF_FPABV). + +- Added the interpolation features of iZ3, which are now integrated into the Z3. + +- Fixed a multitude of bugs and inconsistencies that were reported to us either in person, by email, or on Codeplex. Of those that we do have records of, we would like to express our gratitude to: + Vladimir Klebanov, Konrad Jamrozik, Nuno Lopes, Carsten Ruetz, Esteban Pavese, Tomer Weiss, Ilya Mironov, Gabriele Paganelli, Levent Erkok, Fabian Emmes, David Cok, Etienne Kneuss, Arlen Cox, Matt Lewis, Carsten Otto, Paul Jackson, David Monniaux, Markus Rabe, Martin Pluecker, Jasmin Blanchette, Jules Villard, Andrew Gacek, George Karpenkov, Joerg Pfaehler, and Pablo Aledo + as well as the following Codeplex users that either reported bugs or took part in discussions: +xor88, parno, gario, Bauna, GManNickG, hanwentao, dinu09, fhowar, Cici, chinissai, barak_cohen, tvalentyn, krikunts, sukyoung, daramos, snedunuri, rajtendulkar, sonertari, nick8325, dvitek, amdragon, Beatgodes, dmonniaux, nickolai, DameNingen, mangpo, ttsiodras, blurium, sbrickey, pcodemod, indranilsaha, apanda, hougaardj, yoff, EfForEffort, Ansotegui, scottgw, viorelpreoteasa, idudka, c2855337, gario, jnfoster, omarmrivas, switicus, vosandi, foens, yzwwf, Heizmann, znajem, ilyagri, hougaardj, cliguda, rgrig, 92c849c1ccc707173, edmcman, cipher1024, MichaelvW, hellok, n00b42, ic3guy, Adorf, tvcsantos, zilongwang, Elarnon, immspw, jbridge99, danliew, zverlov, petross, jmh93, dradorf, fniksic, Heyji, cxcfan, henningg, wxlfrank, rvprasad, MovGP0, jackie1015, cowang, ffaghih, sanpra1989, gzchenyin, baitman, xjtulixiangyang, andreis, trucnguyenlam, erizzi, hanhchi, qsp, windypan, vadave, gradanne, SamWot, gsingh93, manjeetdahiya, zverlov, and RaLa + - New parameter setting infrastructure. Now, it is possible to set parameter for Z3 internal modules. Several parameter names changed. Execute `z3 -p` for the new parameter list. - Added get_version() and get_version_string() to Z3Py From 7d196201dc00db41693d53abb63104462001792b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Oct 2014 12:33:20 +0100 Subject: [PATCH 18/32] fixed warnings Signed-off-by: Christoph M. Wintersteiger --- .gitignore | 1 + src/util/mpz.cpp | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.gitignore b/.gitignore index 647529b4f..7757275f3 100644 --- a/.gitignore +++ b/.gitignore @@ -64,3 +64,4 @@ src/util/version.h src/api/java/Native.cpp src/api/java/Native.java src/api/java/enumerations/*.java +*.bak diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index bd7f30a76..94df9f78d 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -1535,7 +1535,7 @@ bool mpz_manager::is_power_of_two(mpz const & a, unsigned & shift) { return false; if (is_small(a)) { if (::is_power_of_two(a.m_val)) { - shift = ::log2(a.m_val); + shift = ::log2((unsigned)a.m_val); return true; } else { @@ -1838,7 +1838,7 @@ unsigned mpz_manager::log2(mpz const & a) { if (is_nonpos(a)) return 0; if (is_small(a)) - return ::log2(a.m_val); + return ::log2((unsigned)a.m_val); #ifndef _MP_GMP COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4); mpz_cell * c = a.m_ptr; @@ -1860,7 +1860,7 @@ unsigned mpz_manager::mlog2(mpz const & a) { if (is_nonneg(a)) return 0; if (is_small(a)) - return ::log2(-a.m_val); + return ::log2((unsigned)-a.m_val); #ifndef _MP_GMP COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4); mpz_cell * c = a.m_ptr; From e0c42f589225883c03438f6c5f9ad1fe9368708a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Oct 2014 14:43:01 +0100 Subject: [PATCH 19/32] Java API bugfix Signed-off-by: Christoph M. Wintersteiger --- scripts/update_api.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index e08adf111..2fbf42cca 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -297,11 +297,13 @@ def param2javaw(p): k = param_kind(p) if k == OUT: return "jobject" - if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: + elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: if param_type(p) == INT or param_type(p) == UINT: return "jintArray" else: return "jlongArray" + elif k == OUT_MANAGED_ARRAY: + return "jlong"; else: return type2javaw(param_type(p)) From 4d62ff6b9fe241e76ae64e8fe4322df1980a8aaf Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Oct 2014 15:53:52 +0100 Subject: [PATCH 20/32] Spelling. Thanks to codeplex user regehr for reporting this. Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index f2318021f..e58e47640 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1398,7 +1398,7 @@ def BoolVector(prefix, sz, ctx=None): return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ] def FreshBool(prefix='b', ctx=None): - """Return a fresh Bolean constant in the given context using the given prefix. + """Return a fresh Boolean constant in the given context using the given prefix. If `ctx=None`, then the global context is used. From 6e159bd442a8c338ebd9d94d489cef51eb18f25a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Oct 2014 15:54:49 +0100 Subject: [PATCH 21/32] updated release notes Signed-off-by: Christoph M. Wintersteiger --- RELEASE_NOTES | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 4be65b260..fa4857e32 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -10,7 +10,7 @@ Version 4.3.2 - Fixed a multitude of bugs and inconsistencies that were reported to us either in person, by email, or on Codeplex. Of those that we do have records of, we would like to express our gratitude to: Vladimir Klebanov, Konrad Jamrozik, Nuno Lopes, Carsten Ruetz, Esteban Pavese, Tomer Weiss, Ilya Mironov, Gabriele Paganelli, Levent Erkok, Fabian Emmes, David Cok, Etienne Kneuss, Arlen Cox, Matt Lewis, Carsten Otto, Paul Jackson, David Monniaux, Markus Rabe, Martin Pluecker, Jasmin Blanchette, Jules Villard, Andrew Gacek, George Karpenkov, Joerg Pfaehler, and Pablo Aledo as well as the following Codeplex users that either reported bugs or took part in discussions: -xor88, parno, gario, Bauna, GManNickG, hanwentao, dinu09, fhowar, Cici, chinissai, barak_cohen, tvalentyn, krikunts, sukyoung, daramos, snedunuri, rajtendulkar, sonertari, nick8325, dvitek, amdragon, Beatgodes, dmonniaux, nickolai, DameNingen, mangpo, ttsiodras, blurium, sbrickey, pcodemod, indranilsaha, apanda, hougaardj, yoff, EfForEffort, Ansotegui, scottgw, viorelpreoteasa, idudka, c2855337, gario, jnfoster, omarmrivas, switicus, vosandi, foens, yzwwf, Heizmann, znajem, ilyagri, hougaardj, cliguda, rgrig, 92c849c1ccc707173, edmcman, cipher1024, MichaelvW, hellok, n00b42, ic3guy, Adorf, tvcsantos, zilongwang, Elarnon, immspw, jbridge99, danliew, zverlov, petross, jmh93, dradorf, fniksic, Heyji, cxcfan, henningg, wxlfrank, rvprasad, MovGP0, jackie1015, cowang, ffaghih, sanpra1989, gzchenyin, baitman, xjtulixiangyang, andreis, trucnguyenlam, erizzi, hanhchi, qsp, windypan, vadave, gradanne, SamWot, gsingh93, manjeetdahiya, zverlov, and RaLa +xor88, parno, gario, Bauna, GManNickG, hanwentao, dinu09, fhowar, Cici, chinissai, barak_cohen, tvalentyn, krikunts, sukyoung, daramos, snedunuri, rajtendulkar, sonertari, nick8325, dvitek, amdragon, Beatgodes, dmonniaux, nickolai, DameNingen, mangpo, ttsiodras, blurium, sbrickey, pcodemod, indranilsaha, apanda, hougaardj, yoff, EfForEffort, Ansotegui, scottgw, viorelpreoteasa, idudka, c2855337, gario, jnfoster, omarmrivas, switicus, vosandi, foens, yzwwf, Heizmann, znajem, ilyagri, hougaardj, cliguda, rgrig, 92c849c1ccc707173, edmcman, cipher1024, MichaelvW, hellok, n00b42, ic3guy, Adorf, tvcsantos, zilongwang, Elarnon, immspw, jbridge99, danliew, zverlov, petross, jmh93, dradorf, fniksic, Heyji, cxcfan, henningg, wxlfrank, rvprasad, MovGP0, jackie1015, cowang, ffaghih, sanpra1989, gzchenyin, baitman, xjtulixiangyang, andreis, trucnguyenlam, erizzi, hanhchi, qsp, windypan, vadave, gradanne, SamWot, gsingh93, manjeetdahiya, zverlov, RaLa, and regehr. - New parameter setting infrastructure. Now, it is possible to set parameter for Z3 internal modules. Several parameter names changed. Execute `z3 -p` for the new parameter list. From cc99e967866de3b975ce9facf08e02cec0df1db7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Oct 2014 18:00:36 +0100 Subject: [PATCH 22/32] Java API Cleanup Signed-off-by: Christoph M. Wintersteiger --- examples/java/README | 10 ++++------ src/api/java/README | 3 +++ src/api/java/manifest | 2 +- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/examples/java/README b/examples/java/README index fa1f20a63..6da4958e4 100644 --- a/examples/java/README +++ b/examples/java/README @@ -1,7 +1,5 @@ -### This is work-in-progress and does not work yet. - -Small example using the Z3 Java bindings. -To build the example execute +A small example using the Z3 Java bindings. +To build the example, configure Z3 with the --java option to scripts/mk_make.py, build via make examples in the build directory. @@ -11,5 +9,5 @@ which can be run on Windows via On Linux and FreeBSD, we must use LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample - - \ No newline at end of file +On OSX, the corresponding option is DYLD_LIBRARY_PATH: + DYLD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample diff --git a/src/api/java/README b/src/api/java/README index 7afe098fb..c9dbcf8f7 100644 --- a/src/api/java/README +++ b/src/api/java/README @@ -1,3 +1,6 @@ Java bindings ------------- +The Java bindings will be included in the Z3 build if it is configured with +the option --java to python scripts/mk_make.py. This will produce the +com.microsoft.z3.jar package in the build directory. diff --git a/src/api/java/manifest b/src/api/java/manifest index b54445cf2..88eac9a3a 100644 --- a/src/api/java/manifest +++ b/src/api/java/manifest @@ -1,2 +1,2 @@ Manifest-Version: 1.0 -Created-By: 4.3.0 (Microsoft Research LTD.) +Created-By: 4.3.2 (Microsoft Research LTD.) From 60cf1d5a4f24802a283f3b427d70b578b1b2989c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Oct 2014 18:02:58 +0100 Subject: [PATCH 23/32] Update copyright notices Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Properties/AssemblyInfo | 2 +- src/api/ml/z3_theory_stubs.c | 2 +- src/shell/main.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/dotnet/Properties/AssemblyInfo b/src/api/dotnet/Properties/AssemblyInfo index ee0e3f354..001264e79 100644 --- a/src/api/dotnet/Properties/AssemblyInfo +++ b/src/api/dotnet/Properties/AssemblyInfo @@ -12,7 +12,7 @@ using System.Security.Permissions; [assembly: AssemblyConfiguration("")] [assembly: AssemblyCompany("Microsoft Corporation")] [assembly: AssemblyProduct("Z3")] -[assembly: AssemblyCopyright("Copyright © Microsoft Corporation 2006")] +[assembly: AssemblyCopyright("Copyright (C) 2006-2014 Microsoft Corporation")] [assembly: AssemblyTrademark("")] [assembly: AssemblyCulture("")] diff --git a/src/api/ml/z3_theory_stubs.c b/src/api/ml/z3_theory_stubs.c index d17a1790d..a48b94553 100644 --- a/src/api/ml/z3_theory_stubs.c +++ b/src/api/ml/z3_theory_stubs.c @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2010 Microsoft Corporation +Copyright (c) Microsoft Corporation Module Name: diff --git a/src/shell/main.cpp b/src/shell/main.cpp index f23bc470c..0eb612f35 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -65,7 +65,7 @@ void display_usage() { #ifdef Z3GITHASH std::cout << " - build hashcode " << STRINGIZE_VALUE_OF(Z3GITHASH); #endif - std::cout << "]. (C) Copyright 2006-2013 Microsoft Corp.\n"; + std::cout << "]. (C) Copyright 2006-2014 Microsoft Corp.\n"; std::cout << "Usage: z3 [options] [-file:]file\n"; std::cout << "\nInput format:\n"; std::cout << " -smt use parser for SMT input format.\n"; From 2f9b3c42eb0e629fdb9c88a2a41863e73e8ffb09 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Oct 2014 19:43:36 +0100 Subject: [PATCH 24/32] Java API cleanup Signed-off-by: Christoph M. Wintersteiger --- examples/java/README | 1 + src/api/java/mk_java.py | 463 ---------------------------------------- 2 files changed, 1 insertion(+), 463 deletions(-) delete mode 100644 src/api/java/mk_java.py diff --git a/examples/java/README b/examples/java/README index 6da4958e4..1939afc49 100644 --- a/examples/java/README +++ b/examples/java/README @@ -1,4 +1,5 @@ A small example using the Z3 Java bindings. + To build the example, configure Z3 with the --java option to scripts/mk_make.py, build via make examples in the build directory. diff --git a/src/api/java/mk_java.py b/src/api/java/mk_java.py deleted file mode 100644 index 87f3e274a..000000000 --- a/src/api/java/mk_java.py +++ /dev/null @@ -1,463 +0,0 @@ -###################################################### -# Copyright (c) 2012 Microsoft Corporation -# -# Auxiliary scripts for generating Java bindings -# from the managed API. -# -# Author: Christoph M. Wintersteiger (cwinter) -###################################################### - - -### -# DO NOT USE THIS SCRIPT! -# This script creates a rough draft of a Java API from -# the managed API, but does not automated the process. -### - -CS="../dotnet/" -EXT=".cs" -EXCLUDE=["Enumerations.cs", "Native.cs", "AssemblyInfo.cs"] -OUTDIR="com/Microsoft/Z3/" -ENUMS_FILE = "Enumerations.cs" - -import os -import fileinput -import string -import re - -EXCLUDE_METHODS = [ [ "Context.cs", "public Expr MkNumeral(ulong" ], - [ "Context.cs", "public Expr MkNumeral(uint" ], - [ "Context.cs", "public RatNum MkReal(ulong" ], - [ "Context.cs", "public RatNum MkReal(uint" ], - [ "Context.cs", "public IntNum MkInt(ulong" ], - [ "Context.cs", "public IntNum MkInt(uint" ], - [ "Context.cs", "public BitVecNum MkBV(ulong" ], - [ "Context.cs", "public BitVecNum MkBV(uint" ], - ] - -ENUMS = [] - -def mk_java_bindings(): - print "Generating Java bindings (from C# bindings in " + CS + ")..." - print "Finding enumerations in " + ENUMS_FILE + "..." - find_enums(ENUMS_FILE) - for root, dirs, files in os.walk(CS): - for fn in files: - if not fn in EXCLUDE and fn.endswith(EXT): - translate(fn) - -def subst_getters(s, getters): - for g in getters: - s = s.replace(g, g + "()") - -def type_replace(s): - s = s.replace(" bool", " boolean") - s = s.replace("(bool", "(boolean") - s = s.replace("uint", "int") - s = s.replace("ulong", "long") - s = s.replace("string", "String") - s = s.replace("IntPtr", "long") - s = s.replace("Dictionary<", "Map<") - s = s.replace("UInt64", "long") - s = s.replace("Int64", "long") - s = s.replace("List", "LinkedList") - s = s.replace("System.Exception", "Exception") - return s - -def rename_native(s): - while s.find("Native.Z3") != -1: - i0 = s.find("Native.Z3") - i1 = s.find("(", i0) - c0 = s[:i0] - c1 = s[i0:i1] - c1 = c1.replace("Native.Z3_", "Native.") - c2 = s[i1:] - lc_callback = lambda pat: pat.group("id").upper() - c1 = re.sub("_(?P\w)", lc_callback, c1) - s = c0 + c1 + c2 - return s - -def find_enums(fn): - for line in fileinput.input(os.path.join(CS, fn)): - s = string.rstrip(string.lstrip(line)) - if s.startswith("public enum"): - ENUMS.append(s.split(" ")[2]) - - -def enum_replace(line): - for e in ENUMS: - if line.find("case") != -1: - line = line.replace(e + ".", "") - elif line.find("== (int)") != -1 or line.find("!= (int)") != -1: - line = re.sub("\(int\)" + e + "\.(?P[A-Z0-9_]*)", e + ".\g.toInt()", line) - elif line.find("==") != -1 or line.find("!=") != -1: - line = re.sub(e + "\.(?P[A-Z0-9_]*)", e + ".\g", line) - else: - # line = re.sub("\(\(" + e + "\)(?P.*\(.*)\)", "(" + e + ".values()[\g])", line) - line = re.sub("\(" + e + "\)(?P.*\(.*\))", e + ".fromInt(\g)", line) - return line - -def replace_generals(a): - a = re.sub(" NativeObject", " NativeObject()", a) - a = re.sub("\.NativeObject", ".NativeObject()", a) - a = re.sub("(?P[\.\(])Id", "\gId()", a) - a = a.replace("(Context ==", "(Context() ==") - a = a.replace("(Context,", "(Context(),") - a = a.replace("Context.", "Context().") - a = a.replace(".nCtx", ".nCtx()") - a = a.replace("(nCtx", "(nCtx()") - a = re.sub("Context\(\).(?P[^_]*)_DRQ", "Context().\g_DRQ()", a) - a = re.sub("ASTKind", "ASTKind()", a) - a = re.sub("IsExpr(?P[ ;])", "IsExpr()\g", a) - a = re.sub("IsNumeral(?P[ ;])", "IsNumeral()\g", a) - a = re.sub("IsInt(?P[ ;])", "IsInt()\g", a) - a = re.sub("IsReal(?P[ ;])", "IsReal()\g", a) - a = re.sub("IsVar(?P[ ;\)])", "IsVar()\g", a) - a = re.sub("FuncDecl.DeclKind", "FuncDecl().DeclKind()", a) - a = re.sub("FuncDecl.DomainSize", "FuncDecl().DomainSize()", a) - a = re.sub("(?P[=&]) Num(?P[a-zA-Z]*)", "\g Num\g()", a) - a = re.sub("= Denominator", "= Denominator()", a) - a = re.sub(", BoolSort(?P[\)\.])", ", BoolSort()\g", a) - a = re.sub(", RealSort(?P[\)\.])", ", RealSort()\g", a) - a = re.sub(", IntSort(?P[\)\.])", ", IntSort()\g", a) - a = a.replace("? 1 : 0", "? true : false") - if a.find("Native.") != -1 and a.find("!= 0") != -1: - a = a.replace("!= 0", "") - if a.find("Native.") != -1 and a.find("== 0") != -1: - a = a.replace("== 0", "^ true") - return a - -def translate(filename): - tgtfn = OUTDIR + filename.replace(EXT, ".java") - print "Translating " + filename + " to " + tgtfn - tgt = open(tgtfn, "w") - in_header = 0 - in_class = 0 - in_static_class = 0 - in_javadoc = 0 - lastindent = 0 - skip_brace = 0 - in_getter = "" - in_getter_type = "" - in_unsupported = 0 - getters = [] - in_bracket_op = 0 - in_getter_get = 0 - in_getter_set = 0 - had_ulong_res = 0 - in_enum = 0 - missing_foreach_brace = 0 - foreach_opened_brace = 0 - for line in fileinput.input(os.path.join(CS, filename)): - s = string.rstrip(string.lstrip(line)) - if in_javadoc: - if s.startswith("///"): - lastindent = line.find(s); - if s.startswith("/// "): - pass - else: - a = line - a = a.replace("", "") - a = a.replace("", "") - a = a.replace("///"," *") - a = a.replace("","@return ") - a = a.replace("","") - tgt.write(a) - else: - t = "" - for i in range(0, lastindent): - t += " " - tgt.write(t + " **/\n") - in_javadoc = 0 - - # for i in range(0, len(EXCLUDE_METHODS)): - # if filename == EXCLUDE_METHODS[i][0] and s.startswith(EXCLUDE_METHODS[i][1]): - # tgt.write(t + "/* Not translated because it would translate to a function with clashing types. */\n") - # in_unsupported = 1 - # break - - - if in_unsupported: - if s == "}": - in_unsupported = 0 - elif not in_javadoc: - if not in_header and s.find("/*++") != -1: - in_header = 1 - tgt.write("/**\n") - elif in_header and s.startswith("--*/"): - in_header = 0 - tgt.write(" * This file was automatically generated from " + filename + " \n") - tgt.write(" **/\n") - tgt.write("\npackage com.Microsoft.Z3;\n\n") - tgt.write("import java.math.BigInteger;\n") - tgt.write("import java.util.*;\n") - tgt.write("import java.lang.Exception;\n") - tgt.write("import com.Microsoft.Z3.Enumerations.*;\n") - elif in_header == 1: - # tgt.write(" * " + line.replace(filename, tgtfn)) - pass - elif s.startswith("using"): - if s.find("System.Diagnostics.Contracts") == -1: - tgt.write("/* " + s + " */\n") - elif s.startswith("namespace"): - pass - elif s.startswith("public") and s.find("operator") != -1 and (s.find("==") != -1 or s.find("!=") != -1): - t = "" - for i in range(0, line.find(s)+1): - t += " " - tgt.write(t + "/* Overloaded operators are not translated. */\n") - in_unsupported = 1 - elif s.startswith("public enum"): - tgt.write(line.replace("enum", "class")) - in_enum = 1 - elif in_enum == 1: - if s == "}": - tgt.write(line) - in_enum = 0 - else: - line = re.sub("(?P.*)\W*=\W*(?P[^\n,])", "public static final int \g = \g;", line) - tgt.write(line.replace(",","")) - elif s.startswith("public class") or s.startswith("internal class") or s.startswith("internal abstract class"): - a = line.replace(":", "extends").replace("internal ", "") - a = a.replace(", IComparable", "") - a = type_replace(a) - tgt.write(a) - in_class = 1 - in_static_class = 0 - elif s.startswith("public static class") or s.startswith("abstract class"): - tgt.write(line.replace(":", "extends").replace("static", "final")) - in_class = 1 - in_static_class = 1 - elif s.startswith("/// "): - tgt.write(line.replace("/// ", "/**")) - in_javadoc = 1 - elif skip_brace and s == "{": - skip_brace = 0 - elif ((s.find("public") != -1 or s.find("protected") != -1) and s.find("class") == -1 and s.find("event") == -1 and s.find("(") == -1) or s.startswith("internal virtual IntPtr NativeObject") or s.startswith("internal Context Context"): - if (s.startswith("new")): - s = s[3:] - s = s.replace("internal virtual", "") - s = s.replace("internal", "") - tokens = s.split(" ") - # print "TOKENS: " + str(len(tokens)) - if len(tokens) == 3: - in_getter = tokens[2] - in_getter_type = type_replace((tokens[0] + " " + tokens[1])) - if in_static_class: - in_getter_type = in_getter_type.replace("static", "") - lastindent = line.find(s) - skip_brace = 1 - getters.append(in_getter) - elif len(tokens) == 4: - if tokens[2].startswith("this["): - in_bracket_op = 1 - in_getter = type_replace(tokens[2]).replace("this[", "get(") - in_getter += " " + tokens[3].replace("]", ")") - in_getter_type = type_replace(tokens[0] + " " + tokens[1]) - else: - in_getter = tokens[3] - in_getter_type = type_replace(tokens[0] + " " + tokens[1] + " " + tokens[2]) - if in_static_class: - in_getter_type = in_getter_type.replace("static", "") - lastindent = line.find(s) - skip_brace = 1 - getters.append(in_getter) - else: - in_getter = tokens[2] - in_getter_type = type_replace(tokens[0] + " " + tokens[1]) - if tokens[2].startswith("this["): - lastindent = line.find(s) - t = "" - for i in range(0, lastindent): t += " " - tgt.write(t + "/* operator this[] not translated */\n ") - in_unsupported = 1 - else: - if in_static_class: - in_getter_type = in_getter_type.replace("static", "") - rest = s[s.find("get ") + 4:-1] - subst_getters(rest, getters) - rest = type_replace(rest) - rest = rename_native(rest) - rest = replace_generals(rest) - rest = enum_replace(rest) - t = "" - for i in range(0, lastindent): - t += " " - tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n") - if rest.find("}") == -1: - in_getter_get = 1 - else: - getters.append(in_getter) - in_getter = "" - in_getter_type = "" - print "ACC: " + s + " --> " + in_getter - elif s.find("{ get {") != -1: - line = type_replace(line) - line = line.replace("internal ", "") - d = line[0:line.find("{ get")] - rest = line[line.find("{ get")+5:] - rest = rest.replace("} }", "}") - rest = re.sub("Contract.\w+\([\s\S]*\);", "", rest) - subst_getters(rest, getters) - rest = rename_native(rest) - rest = replace_generals(rest) - rest = enum_replace(rest) - if in_bracket_op: - tgt.write(d + rest) - else: - tgt.write(d + "()" + rest) - print "ACC: " + s + " --> " + in_getter - elif in_getter != "" and s.startswith("get"): - t = "" - for i in range(0, lastindent): - t += " " - if len(s) > 3: rest = s[3:] - else: rest = "" - subst_getters(rest, getters) - rest = type_replace(rest) - rest = rename_native(rest) - rest = replace_generals(rest) - rest = enum_replace(rest) - if in_bracket_op: - tgt.write(t + in_getter_type + " " + in_getter + " " + rest + "\n") - else: - tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n") - if rest.find("}") == -1: - in_getter_get = 1 - elif in_getter != "" and s.startswith("set"): - t = "" - for i in range(0, lastindent): - t += " " - if len(s) > 3: rest = type_replace(s[3:]) - else: rest = "" - subst_getters(rest, getters) - rest = rest.replace("(Integer)value", "Integer(value)") - rest = type_replace(rest) - rest = rename_native(rest) - rest = replace_generals(rest) - rest = enum_replace(rest) - ac_acc = in_getter_type[:in_getter_type.find(' ')] - ac_type = in_getter_type[in_getter_type.find(' ')+1:] - if in_bracket_op: - in_getter = in_getter.replace("get", "set").replace(")", "") - tgt.write(t + ac_acc + " void " + in_getter + ", " + ac_type + " value) " + rest + "\n") - else: - tgt.write(t + ac_acc + " void set" + in_getter + "(" + ac_type + " value) " + rest + "\n") - if rest.find("}") == -1: - in_getter_set = 1 - elif in_getter != "" and in_getter_get == 1 and s == "}": - tgt.write(line) - in_getter_get = 0 - elif in_getter != "" and in_getter_set == 1 and s == "}": - tgt.write(line) - in_getter_set = 0 - elif in_getter != "" and in_getter_get == 0 and in_getter_set == 0 and s == "}": - in_getter = "" - in_getter_type == "" - in_bracket_op = 0 - skip_brace = 0 - elif s.startswith("uint ") and s.find("=") == -1: - line = line.replace("uint", "Integer", line) - line = re.sub("(?P\w+)(?P[,;])", "\g\g", line) - tgt.write(line); - elif (not in_class and (s.startswith("{") or s.startswith("}"))) or s.startswith("[") or s.startswith("#"): - # tgt.write("// Skipping: " + s) - pass - elif line == "}\n": - pass - else: - # indent = line.find(s) - # tgt.write("// LINE: " + line) - if line.find(": base") != -1: - line = re.sub(": base\((?P

[^\{]*)\)", "{ super(\g

);", line) - line = line[4:] - obraces = line.count("{") - cbraces = line.count("}") - mbraces = obraces - cbraces - # tgt.write("// obraces = " + str(obraces) + "\n") - if obraces == 1: - skip_brace = 1 - else: - for i in range(0, mbraces): - line = line.replace("\n", "}\n") - if (s.find("public") != -1 or s.find("protected") != -1 or s.find("internal") != -1) and s.find("(") != -1: - line = re.sub(" = [\w.]+(?P[,;\)])", "\g", line) - a = type_replace(line) - a = enum_replace(a) - a = re.sub("(?P[\(, ])params ", "\g", a) - a = a.replace("base.", "super.") - a = re.sub("Contract.\w+\([\s\S]*\);", "", a) - a = rename_native(a) - a = re.sub("~\w+\(\)", "protected void finalize()", a) - - if missing_foreach_brace == 1: - # a = a.replace("\n", " // checked " + str(foreach_opened_brace) + "\n") - if foreach_opened_brace == 0 and a.find("{") != -1: - foreach_opened_brace = 1 - elif foreach_opened_brace == 0 and a.find("}") == -1: - a = a.replace("\n", "}}\n") - foreach_opened_brace = 0 - missing_foreach_brace = 0 - elif foreach_opened_brace == 1 and a.find("}") != -1: - a = a.replace("\n", "}}\n") - foreach_opened_brace = 0 - missing_foreach_brace = 0 - -# if a.find("foreach") != -1: -# missing_foreach_brace = 1 -# a = re.sub("foreach\s*\((?P[\w <>,]+)\s+(?P\w+)\s+in\s+(?P\w+)\)", - # "{ Iterator fe_i = \g.iterator(); while (fe_i.hasNext()) { \g \g = (long)fe_i.next(); ", -# a) - a = re.sub("foreach\s*\((?P[\w <>,]+)\s+(?P\w+)\s+in\s+(?P\w+)\)", - "for (\g \g: \g)", - a) - if a.find("long o: m_queue") != -1: - a = a.replace("long", "Long") - a = a.replace("readonly ", "") - a = a.replace("const ", "final ") - a = a.replace("String ToString", "String toString") - a = a.replace(".ToString", ".toString") - a = a.replace("internal ", "") - a = a.replace("new static", "static") - a = a.replace("new public", "public") - a = a.replace("override ", "") - a = a.replace("virtual ", "") - a = a.replace("o as AST", "(AST) o") - a = a.replace("o as Sort", "(Sort) o") - a = a.replace("other as AST", "(AST) other") - a = a.replace("o as FuncDecl", "(FuncDecl) o") - a = a.replace("IntPtr obj", "long obj") - a = a.replace("IntPtr o", "long o") - a = a.replace("new long()", "0") - a = a.replace("long.Zero", "0") - a = a.replace("object o", "Object o") - a = a.replace("object other", "Object other") - a = a.replace("IntPtr res = IntPtr.Zero;", "Native.IntPtr res = new Native.IntPtr();") - a = a.replace("out res", "res") - a = a.replace("GC.ReRegisterForFinalize(m_ctx);", "") - a = a.replace("GC.SuppressFinalize(this);", "") - a = a.replace(".Length", ".length") - a = a.replace("m_queue.Count", "m_queue.size()") - a = a.replace("m_queue.Add", "m_queue.add") - a = a.replace("m_queue.Clear", "m_queue.clear") - a = a.replace("for (long ", "for (int ") - a = a.replace("ReferenceEquals(Context, ctx)", "Context() == ctx") - a = a.replace("BigInteger.Parse", "new BigInteger") - if had_ulong_res == 0 and a.find("ulong res = 0") != -1: - a = a.replace("ulong res = 0;", "LongPtr res = new LongPtr();") - elif had_ulong_res == 1: - a = a.replace("ref res)", "res)") - if a.find("return res;") != -1: - a = a.replace("return res;", "return res.value;") - had_ulong_res = 0 - a = a.replace("lock (", "synchronized (") - if in_static_class: - a = a.replace("static", "") - a = re.sub("ref (?P\w+)", "\g", a) - subst_getters(a, getters) - a = re.sub("NativeObject = (?P.*);", "setNativeObject(\g);", a) - a = replace_generals(a) - tgt.write(a) - tgt.close() - -mk_java_bindings() From ddebb4a69d8c6105187063e3647136d720e3c41c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Oct 2014 19:45:21 +0100 Subject: [PATCH 25/32] Documentation fixes Signed-off-by: Christoph M. Wintersteiger --- doc/mk_api_doc.py | 8 ++++++++ doc/z3api.dox | 14 +++++++++----- src/api/java/AST.java | 20 ++------------------ src/api/java/Expr.java | 2 +- src/api/java/Global.java | 5 ++--- src/api/java/Sort.java | 19 +------------------ src/api/z3_algebraic.h | 16 +++++++++++++++- src/api/z3_api.h | 7 ++----- src/api/z3_interp.h | 18 +++++++++++++++++- src/api/z3_polynomial.h | 16 ++++++++++++++++ src/api/z3_rcf.h | 15 +++++++++++++++ 11 files changed, 88 insertions(+), 52 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 6e530243a..633f96c6b 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -27,6 +27,10 @@ try: shutil.copyfile('website.dox', 'tmp/website.dox') shutil.copyfile('../src/api/python/z3.py', 'tmp/z3py.py') cleanup_API('../src/api/z3_api.h', 'tmp/z3_api.h') + cleanup_API('../src/api/z3_algebraic.h', 'tmp/z3_algebraic.h') + cleanup_API('../src/api/z3_polynomial.h', 'tmp/z3_polynomial.h') + cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h') + cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h') print "Removed annotations from z3_api.h." try: @@ -38,6 +42,10 @@ try: exit(1) print "Generated C and .NET API documentation." os.remove('tmp/z3_api.h') + os.remove('tmp/z3_algebraic.h') + os.remove('tmp/z3_polynomial.h') + os.remove('tmp/z3_rcf.h') + os.remove('tmp/z3_interp.h') print "Removed temporary file z3_api.h." os.remove('tmp/website.dox') print "Removed temporary file website.dox" diff --git a/doc/z3api.dox b/doc/z3api.dox index 0233e6d83..dbaa3c8b8 100644 --- a/doc/z3api.dox +++ b/doc/z3api.dox @@ -363,7 +363,7 @@ TYPEDEF_HIDES_STRUCT = NO # 2^(16+SYMBOL_CACHE_SIZE). The valid range is 0..9, the default is 0, # corresponding to a cache size of 2^16 = 65536 symbols. -SYMBOL_CACHE_SIZE = 0 +# SYMBOL_CACHE_SIZE = 0 # Similar to the SYMBOL_CACHE_SIZE the size of the symbol lookup cache can be # set using LOOKUP_CACHE_SIZE. This cache is used to resolve symbols given @@ -708,7 +708,11 @@ INPUT_ENCODING = UTF-8 # *.f90 *.f *.for *.vhd *.vhdl FILE_PATTERNS = website.dox \ - z3_api.h \ + z3_api.h \ + z3_algebraic.h \ + z3_polynomial.h \ + z3_rcf.h \ + z3_interp.h \ z3++.h \ z3py.py \ ApplyResult.cs \ @@ -1477,13 +1481,13 @@ XML_OUTPUT = xml # which can be used by a validating XML parser to check the # syntax of the XML files. -XML_SCHEMA = +# XML_SCHEMA = # The XML_DTD tag can be used to specify an XML DTD, # which can be used by a validating XML parser to check the # syntax of the XML files. -XML_DTD = +# XML_DTD = # If the XML_PROGRAMLISTING tag is set to YES Doxygen will # dump the program listings (including syntax highlighting @@ -1699,7 +1703,7 @@ DOT_NUM_THREADS = 0 # the DOTFONTPATH environment variable or by setting DOT_FONTPATH to the # directory containing the font. -DOT_FONTNAME = FreeSans +# DOT_FONTNAME = FreeSans # The DOT_FONTSIZE tag can be used to set the size of the font of dot graphs. # The default size is 10pt. diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 1f5463ec7..a201d5697 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -24,28 +24,12 @@ import com.microsoft.z3.enumerations.Z3_ast_kind; **/ public class AST extends Z3Object { - /** - * Comparison operator. An AST An - * AST - * - * @return True if and are from - * the same context and represent the same sort; false otherwise. - **/ - /* Overloaded operators are not translated. */ - - /** - * Comparison operator. An AST An - * AST - * - * @return True if and are not - * from the same context or represent different sorts; false - * otherwise. - **/ /* Overloaded operators are not translated. */ /** * Object comparison. - **/ + * another AST + **/ public boolean equals(Object o) { AST casted = null; diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 3773e749d..a4c669dad 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -40,7 +40,7 @@ public class Expr extends AST /** * Returns a simplified version of the expression * A set of - * parameters to configure the simplifier + * parameters a Params object to configure the simplifier * **/ public Expr simplify(Params p) throws Z3Exception diff --git a/src/api/java/Global.java b/src/api/java/Global.java index b97e48721..c93f46c88 100644 --- a/src/api/java/Global.java +++ b/src/api/java/Global.java @@ -50,8 +50,7 @@ public final class Global /** * Get a global (or module) parameter. * - * Returns null if the parameter does not exist. - * The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value. + * Returns null if the parameter parameter id does not exist. * This function cannot be invoked simultaneously from different threads without synchronization. * The result string stored in param_value is stored in a shared location. * @@ -70,7 +69,7 @@ public final class Global * * This command will not affect already created objects (such as tactics and solvers) * - * @seealso SetParameter + * **/ public static void resetParameters() { diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 7bcc7ce7e..7d89428c6 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -25,27 +25,10 @@ import com.microsoft.z3.enumerations.Z3_sort_kind; **/ public class Sort extends AST { - /** - * Comparison operator. A Sort A - * Sort - * - * @return True if and are from - * the same context and represent the same sort; false otherwise. - **/ /* Overloaded operators are not translated. */ /** - * Comparison operator. A Sort A - * Sort - * - * @return True if and are not - * from the same context or represent different sorts; false - * otherwise. - **/ - /* Overloaded operators are not translated. */ - - /** - * Equality operator for objects of type Sort. + * Equality operator for objects of type Sort. * * @return **/ diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h index eef791170..8b6d97aa8 100644 --- a/src/api/z3_algebraic.h +++ b/src/api/z3_algebraic.h @@ -23,7 +23,19 @@ Notes: #ifdef __cplusplus extern "C" { -#endif // __cplusplus +#endif // __cplusplus + + /** + \defgroup capi C API + + */ + + /*@{*/ + + /** + @name Algebraic Numbers API + */ + /*@{*/ /** \brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic @@ -218,6 +230,8 @@ extern "C" { */ int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]); + /*@}*/ + /*@}*/ #ifdef __cplusplus }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 2e3ddf4b4..248d2161e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -771,7 +771,6 @@ typedef enum The premises of the rules is a sequence of clauses. The first clause argument is the main clause of the rule. - One literal from the second, third, .. clause is resolved with a literal from the first (main) clause. Premises of the rules are of the form @@ -1143,8 +1142,8 @@ typedef enum { - Z3_FILE_ACCESS_ERRROR: A file could not be accessed. - Z3_INVALID_USAGE: API call is invalid in the current state. - Z3_INTERNAL_FATAL: An error internal to Z3 occurred. - - Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized\mlonly.\endmlonly\conly with #Z3_inc_ref. - - Z3_EXCEPTION: Internal Z3 exception. Additional details can be retrieved using \mlonly #Z3_get_error_msg. \endmlonly \conly #Z3_get_error_msg_ex. + - Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized \mlonly.\endmlonly \conly with #Z3_inc_ref. + - Z3_EXCEPTION: Internal Z3 exception. Additional details can be retrieved using #Z3_get_error_msg. */ typedef enum { @@ -1287,8 +1286,6 @@ extern "C" { \sa Z3_global_param_set - The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value. - \remark This function cannot be invoked simultaneously from different threads without synchronization. The result string stored in param_value is stored in shared location. diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h index 729851988..6ae26c0ed 100644 --- a/src/api/z3_interp.h +++ b/src/api/z3_interp.h @@ -24,7 +24,14 @@ extern "C" { #endif // __cplusplus /** - @name Interpolation + \defgroup capi C API + + */ + + /*@{*/ + + /** + @name Interpolation API */ /*@{*/ @@ -184,6 +191,8 @@ extern "C" { \param cnsts Returns sequence of formulas (do not free) \param parents Returns the parents vector (or NULL for sequence) \param error Returns an error message in case of failure (do not free the string) + \param num_theory Number of theory terms + \param theory Theory terms Returns true on success. @@ -232,6 +241,8 @@ extern "C" { \param parents The parents vector (or NULL for sequence) \param interps The interpolant to check \param error Returns an error message if interpolant incorrect (do not free the string) + \param num_theory Number of theory terms + \param theory Theory terms Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if incorrect, and Z3_L_UNDEF if unknown. @@ -258,6 +269,8 @@ extern "C" { \param cnsts Array of constraints \param parents The parents vector (or NULL for sequence) \param filename The file name to write + \param num_theory Number of theory terms + \param theory Theory terms def_API('Z3_write_interpolation_problem', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(STRING), _in(UINT), _in_array(5, AST))) */ @@ -270,6 +283,9 @@ extern "C" { __in unsigned num_theory, __in_ecount(num_theory) Z3_ast theory[]); + /*@}*/ + /*@}*/ + #ifdef __cplusplus }; #endif // __cplusplus diff --git a/src/api/z3_polynomial.h b/src/api/z3_polynomial.h index 614e654f9..f55a63dd4 100644 --- a/src/api/z3_polynomial.h +++ b/src/api/z3_polynomial.h @@ -24,6 +24,19 @@ Notes: extern "C" { #endif // __cplusplus + /** + \defgroup capi C API + + */ + + /*@{*/ + + + /** + @name Polynomials API + */ + /*@{*/ + /** \brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x. @@ -38,6 +51,9 @@ extern "C" { Z3_ast_vector Z3_API Z3_polynomial_subresultants(__in Z3_context c, __in Z3_ast p, __in Z3_ast q, __in Z3_ast x); + /*@}*/ + /*@}*/ + #ifdef __cplusplus }; #endif // __cplusplus diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h index e2b4b7e05..04fe40253 100644 --- a/src/api/z3_rcf.h +++ b/src/api/z3_rcf.h @@ -25,6 +25,18 @@ Notes: #ifdef __cplusplus extern "C" { #endif // __cplusplus + + /** + \defgroup capi C API + + */ + + /*@{*/ + + /** + @name Real Closed Fields API + */ + /*@{*/ /** \brief Delete a RCF numeral created using the RCF API. @@ -192,6 +204,9 @@ extern "C" { */ void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num * n, __out Z3_rcf_num * d); + /*@}*/ + /*@}*/ + #ifdef __cplusplus }; #endif // __cplusplus From da71d5ee0157b2c5d521e13b90139d4c3e7c68d8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 24 Oct 2014 11:53:03 -0700 Subject: [PATCH 26/32] unlimit stack on linux/mac --- src/interp/iz3interp.cpp | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 0d394090f..7a0090981 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -513,3 +513,26 @@ void interpolation_options_struct::apply(iz3base &b){ b.set_option((*it).first,(*it).second); } +// On linux and mac, unlimit stack space so we get recursion + +#if defined(_WINDOWS) || defined(_CYGWIN) + +#else + +#include +#include + +class iz3stack_unlimiter { +public: + iz3stack_unlimiter() { + struct rlimit rl = {RLIM_INFINITY, RLIM_INFINITY}; + setrlimit(RLIMIT_STACK, &rl); + // nothing to be done if above fails + } +}; + +// initializing this will unlimit stack + +iz3stack_unlimiter the_iz3stack_unlimiter; + +#endif From 0713535fa6a3a5fb510d5e05f7bf7bff44b3b6d9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Oct 2014 21:00:23 +0100 Subject: [PATCH 27/32] Documentation website fixes. Signed-off-by: Christoph M. Wintersteiger --- .gitignore | 2 ++ doc/website.dox | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 7757275f3..65a69bf51 100644 --- a/.gitignore +++ b/.gitignore @@ -65,3 +65,5 @@ src/api/java/Native.cpp src/api/java/Native.java src/api/java/enumerations/*.java *.bak +doc/api +doc/code diff --git a/doc/website.dox b/doc/website.dox index 6936b4f77..d048dab0c 100644 --- a/doc/website.dox +++ b/doc/website.dox @@ -15,5 +15,5 @@ - .NET API - Java API - Python API (also available in pydoc format). - - Try Z3 online at RiSE4Fun using Python or SMT 2.0. + - Try Z3 online at RiSE4Fun. */ From cb3e9c96441406a7dd64a7cd2eec45b676d98b9e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 25 Oct 2014 16:58:16 +0100 Subject: [PATCH 28/32] Bugfix for FPA models --- src/tactic/fpa/fpa2bv_model_converter.cpp | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 9b4b5a70f..53fa2405b 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -111,14 +111,25 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { unsigned ebits = fu.get_ebits(var->get_range()); unsigned sbits = fu.get_sbits(var->get_range()); - expr_ref sgn(m), sig(m), exp(m); - sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl()); - sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl()); - exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl()); + expr_ref sgn(m), sig(m), exp(m); + bv_mdl->eval(a->get_arg(0), sgn, true); + bv_mdl->eval(a->get_arg(1), sig, true); + bv_mdl->eval(a->get_arg(2), exp, true); + SASSERT(a->is_app_of(fu.get_family_id(), OP_TO_FLOAT)); + +#ifdef Z3DEBUG + SASSERT(to_app(a->get_arg(0))->get_decl()->get_arity() == 0); + SASSERT(to_app(a->get_arg(1))->get_decl()->get_arity() == 0); + SASSERT(to_app(a->get_arg(1))->get_decl()->get_arity() == 0); seen.insert(to_app(a->get_arg(0))->get_decl()); seen.insert(to_app(a->get_arg(1))->get_decl()); seen.insert(to_app(a->get_arg(2))->get_decl()); +#else + SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT); + SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT); + seen.insert(to_app(to_app(a->get_arg(0))->get_arg(0))->get_decl()); +#endif if (!sgn && !sig && !exp) continue; From 6b51f7a6104c23b855ccf1e89bb5d7f10991471e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 25 Oct 2014 16:59:24 +0100 Subject: [PATCH 29/32] Added item to release notes Signed-off-by: Christoph M. Wintersteiger --- RELEASE_NOTES | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index fa4857e32..ad2dcaf00 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,5 +1,10 @@ RELEASE NOTES +Version 4.3.3 +============= + +- Fixed bug in floating point models + Version 4.3.2 ============= From f50a8b0a59ff5c98f509dddb46da33033384bf5d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 25 Oct 2014 17:05:02 +0100 Subject: [PATCH 30/32] Bumped version number. Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_project.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 170124bd8..b30bba609 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -9,7 +9,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): - set_version(4, 3, 2, 0) + set_version(4, 3, 3, 0) add_lib('util', []) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) From b4600ffda00b0ba2ba874effb1cb6e3139e6a6cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Oct 2014 14:24:21 +0100 Subject: [PATCH 31/32] add print to SMT-LIB format from solver Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 1 + src/api/c++/z3++.h | 20 ++++++++++++++++++++ 2 files changed, 21 insertions(+) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index b348e7d36..0d8a3ceb3 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -21,6 +21,7 @@ void demorgan() { // adding the negation of the conjecture as a constraint. s.add(!conjecture); std::cout << s << "\n"; + std::cout << s.to_smt2() << "\n"; switch (s.check()) { case unsat: std::cout << "de-Morgan is valid\n"; break; case sat: std::cout << "de-Morgan is not valid\n"; break; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index c35208d86..7380e52f1 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1314,6 +1314,26 @@ namespace z3 { expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; } + + std::string to_smt2(char const* status = "unknown") { + array es(assertions()); + Z3_ast const* fmls = es.ptr(); + Z3_ast fml = 0; + unsigned sz = es.size(); + if (sz > 0) { + --sz; + fml = fmls[sz]; + } + else { + fml = ctx().bool_val(true); + } + return std::string(Z3_benchmark_to_smtlib_string( + ctx(), + "", "", status, "", + sz, + fmls, + fml)); + } }; class goal : public object { From 591f6d096f437445c56b51292e75fe757cd48dd1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 3 Nov 2014 14:26:57 +0000 Subject: [PATCH 32/32] .NET API project directories fixed. Thanks to Marc Brockschmidt for reporting this. --- src/api/dotnet/Microsoft.Z3.csproj | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj index cc7d3c0c5..36bd6ad02 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -19,12 +19,12 @@ true full false - ..\..\..\..\..\cwinter\bugs\z3bugs\Debug\ + ..\Debug\ DEBUG;TRACE prompt 4 true - C:\cwinter\bugs\z3bugs\Debug\Microsoft.Z3.XML + ..\Debug\Microsoft.Z3.XML False False True @@ -254,7 +254,7 @@ true - ..\..\..\..\..\cwinter\bugs\z3bugs\Debug\ + ..\x86\Debug\ DEBUG;TRACE true full @@ -266,7 +266,7 @@ MinimumRecommendedRules.ruleset ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - C:\cwinter\bugs\z3bugs\Debug\Microsoft.Z3.XML + ..\x86\Debug\Microsoft.Z3.XML bin\x86\Release\