From 0b3e50d6e67bace32f8d9e3a8a6c11af144371be Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 17 Dec 2013 13:53:10 +0000 Subject: [PATCH 01/10] Added #include because VS2013 needs that for std::max/std::min Signed-off-by: Christoph M. Wintersteiger --- src/interp/iz3scopes.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/interp/iz3scopes.cpp b/src/interp/iz3scopes.cpp index 382779be0..198ecffe3 100755 --- a/src/interp/iz3scopes.cpp +++ b/src/interp/iz3scopes.cpp @@ -19,6 +19,8 @@ Revision History: #include +#include + #include "iz3scopes.h" From 0d6220f383c4e171ee5f19a840a172653cf1eb60 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Dec 2013 21:53:04 +0200 Subject: [PATCH 02/10] revert is_all_int bugfix Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 7593e9a52..21b892e57 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -476,10 +476,10 @@ namespace smt { typename vector::const_iterator it = r.begin_entries(); typename vector::const_iterator end = r.end_entries(); for (; it != end; ++it) { - if (!it->is_dead() && !it->m_coeff.is_int()) { + if (!it->is_dead() && !it->m_coeff.is_int()) TRACE("gomory_cut", display_row(tout, r, true);); return false; - } + } return true; } From 81f1f7690df331065f775aa15b9abea6441fa5be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Dec 2013 15:59:56 -0800 Subject: [PATCH 03/10] fix bug in rational.is_int32, it recognized rationals; fix bug reported by Anvesh for integer arithmetic Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/lia2pb_tactic.cpp | 1 + src/util/rational.h | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 6fee55e4b..9ee8f6728 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -71,6 +71,7 @@ class lia2pb_tactic : public tactic { if (m_bm.has_lower(n, l, s) && m_bm.has_upper(n, u, s) && l.is_zero() && + !u.is_neg() && u.get_num_bits() <= m_max_bits) { return true; diff --git a/src/util/rational.h b/src/util/rational.h index fc03228bf..c02a5a2c3 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -104,7 +104,7 @@ public: } bool is_int32() const { - if (is_small()) return true; + if (is_small() && is_int()) return true; // we don't assume that if it is small, then it is int32. if (!is_int64()) return false; int64 v = get_int64(); From 084a6f35eb2f1ad7db7b6c89bf580e36f4052a75 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Jan 2014 17:37:35 -0800 Subject: [PATCH 04/10] fix bug reported by Nuno Lopes: inlining is unsound for negated predicates Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_rule_inliner.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 3e933b099..d9dad5c56 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -527,6 +527,9 @@ namespace datalog { bool mk_rule_inliner::do_eager_inlining(rule * r, rule_set const& rules, rule_ref& res) { + if (r->has_negation()) { + return false; + } SASSERT(rules.is_closed()); const rule_stratifier& strat = rules.get_stratifier(); From da4793de76a5e0a34bb00c333f8c2902d1c96ec3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Jan 2014 21:14:30 -0800 Subject: [PATCH 05/10] fix type checking bug reported by Nate Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index b000201b7..68f7596ee 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1850,6 +1850,7 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const { ast_manager& m = const_cast(*this); + if (decl->is_associative()) { sort * expected = decl->get_domain(0); for (unsigned i = 0; i < num_args; i++) { @@ -1894,7 +1895,18 @@ void ast_manager::check_sorts_core(ast const * n) const { if (n->get_kind() != AST_APP) return; // nothing else to check... app const * a = to_app(n); - check_sort(a->get_decl(), a->get_num_args(), a->get_args()); + func_decl* d = a->get_decl(); + check_sort(d, a->get_num_args(), a->get_args()); + if (a->get_num_args() == 2 && + !d->is_flat_associative() && + d->is_right_associative()) { + check_sorts_core(a->get_arg(1)); + } + if (a->get_num_args() == 2 && + !d->is_flat_associative() && + d->is_left_associative()) { + check_sorts_core(a->get_arg(0)); + } } bool ast_manager::check_sorts(ast const * n) const { From b80302cfb0a49efd42eeb45436c934d3c6ff0835 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jan 2014 13:41:47 -0800 Subject: [PATCH 06/10] generalize guard in conflict resolution to handle non-equality binary predicates Signed-off-by: Nikolaj Bjorner --- src/smt/smt_conflict_resolution.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index d34aa2ec8..ec62efa1c 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -759,7 +759,8 @@ namespace smt { app * fact = to_app(m_manager.get_fact(pr)); app * n1_owner = n1->get_owner(); app * n2_owner = n2->get_owner(); - if (fact->get_num_args() != 2 || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) { + bool is_eq = m_manager.is_eq(fact) || m_manager.is_iff(fact); + if (!is_eq || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) { CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2), tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n"; if (fact->get_num_args() == 2) { From 73a1dddc45c5d75a0a428800fddbf799a9e31f9b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 21 Jan 2014 17:06:13 +0000 Subject: [PATCH 07/10] Bugfixes for the build on new OSX machines (XCode 5.0 on). --- scripts/mk_util.py | 12 ++++++++++++ src/util/hwf.cpp | 5 ++++- 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9295c949f..0b1dd47a2 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -638,7 +638,19 @@ def is_compiler(given, expected): def is_CXX_gpp(): return is_compiler(CXX, 'g++') +def is_clang_in_gpp_form(cc): + outf = open('clang_version', 'rw') + subprocess.call([cc, '--version'], stdout=outf, stderr=outf) + outf.seek(0) + version_string = outf.read() + contains_clang = version_string.find('clang') != -1 + outf.close() + os.remove('clang_version') + return contains_clang + def is_CXX_clangpp(): + if is_compiler(CXX, 'g++'): + return is_clang_in_gpp_form(CXX) return is_compiler(CXX, 'clang++') def get_cpp_files(path): diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 8585e7eda..40d20b644 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -49,8 +49,11 @@ Revision History: // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects // the x87 FPU, even when /arch:SSE2 is on. // Luckily, these are kind of standardized, at least for Windows/Linux/OSX. +#ifdef __clang__ +#undef USE_INTRINSICS +#else #include - +#endif hwf_manager::hwf_manager() : m_mpz_manager(m_mpq_manager) From b2be81fd4d3d6399f15bb1ae70f88978c6b82700 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 22 Jan 2014 13:41:48 +0000 Subject: [PATCH 08/10] bugfix for OSX build configuration --- scripts/mk_util.py | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0b1dd47a2..2fff61778 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -639,14 +639,8 @@ def is_CXX_gpp(): return is_compiler(CXX, 'g++') def is_clang_in_gpp_form(cc): - outf = open('clang_version', 'rw') - subprocess.call([cc, '--version'], stdout=outf, stderr=outf) - outf.seek(0) - version_string = outf.read() - contains_clang = version_string.find('clang') != -1 - outf.close() - os.remove('clang_version') - return contains_clang + version_string = subprocess.check_output([cc, '--version']) + return version_string.find('clang') != -1 def is_CXX_clangpp(): if is_compiler(CXX, 'g++'): From 0e74362ecbde4c137d393ded081d30604df9d4a1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Jan 2014 15:36:23 +0000 Subject: [PATCH 09/10] Added support for the final draft of the FPA standard (and fpa2bv conversion). Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 96 ++++++++++++++++++++++--- src/ast/float_decl_plugin.h | 18 ++++- src/ast/rewriter/float_rewriter.cpp | 44 ++++++++++++ src/ast/rewriter/float_rewriter.h | 6 ++ src/tactic/fpa/fpa2bv_converter.cpp | 36 ++++++++++ src/tactic/fpa/fpa2bv_converter.h | 8 ++- src/tactic/fpa/fpa2bv_rewriter.h | 5 ++ src/tactic/fpa/qffpa_tactic.cpp | 74 +++++++++++++++++++ src/tactic/fpa/qffpa_tactic.h | 7 ++ src/tactic/portfolio/default_tactic.cpp | 4 +- src/util/mpf.cpp | 4 ++ src/util/mpf.h | 2 + 12 files changed, 290 insertions(+), 14 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index eb8aba9ae..1adedb2d7 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -213,6 +213,9 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) { s = to_sort(parameters[0].get_ast()); } + else if (num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()) { + s = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + } else if (range != 0 && is_float_sort(range)) { s = range; } @@ -376,7 +379,19 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); symbol name("asFloat"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + } + else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) { + if (num_parameters != 2) + m_manager->raise_exception("invalid number of parameters to to_fp"); + if (!parameters[0].is_int() || !parameters[1].is_int()) + m_manager->raise_exception("invalid parameter type to to_fp"); + int ebits = parameters[0].get_int(); + int sbits = parameters[1].get_int(); + + sort * fp = mk_float_sort(ebits, sbits); + symbol name("asFloat"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } else { // .. Otherwise we only know how to convert rationals/reals. if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) @@ -412,6 +427,53 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } +func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("fp unsupported; use a logic with BV support"); + if (arity != 3) + m_manager->raise_exception("invalid number of arguments to fp"); + if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) || + !is_sort_of(domain[1], m_bv_fid, BV_SORT) || + !is_sort_of(domain[2], m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismtach"); + + sort * fp = mk_float_sort(domain[1]->get_parameter(0).get_int(), domain[2]->get_parameter(0).get_int() + 1); + symbol name("fp"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k)); +} + +func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("to_fp_unsigned unsupported; use a logic with BV support"); + if (arity != 2) + m_manager->raise_exception("invalid number of arguments to to_fp_unsigned"); + if (is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismtach"); + if (!is_sort_of(domain[1], m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismtach"); + + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + symbol name("to_fp_unsigned"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k)); +} + +func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + +func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + +func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (k) { @@ -465,6 +527,16 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_fused_ma(k, num_parameters, parameters, arity, domain, range); case OP_TO_IEEE_BV: return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_FP: + return mk_from3bv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_FP_UNSIGNED: + return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_UBV: + return mk_to_ubv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_SBV: + return mk_to_sbv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_REAL: + return mk_to_real(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -517,8 +589,9 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co if (m_bv_plugin) op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV)); - // We also support draft version 3 - op_names.push_back(builtin_name("fp", OP_TO_FLOAT)); + // These are the operators from the final draft of the SMT FloatingPoints standard + op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF)); + op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF)); op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN)); op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY)); @@ -547,23 +620,24 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN)); op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN)); op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX)); - op_names.push_back(builtin_name("fp.convert", OP_TO_FLOAT)); + op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT)); if (m_bv_plugin) { - // op_names.push_back(builtin_name("fp.fromBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.fromUBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.fromSBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.toUBv", OP_TO_IEEE_BV)); - // op_names.push_back(builtin_name("fp.toSBv", OP_TO_IEEE_BV)); + op_names.push_back(builtin_name("fp", OP_FLOAT_FP)); + op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED)); + op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV)); + op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV)); } - - op_names.push_back(builtin_name("fp.fromReal", OP_TO_FLOAT)); + // op_names.push_back(builtin_name("fp.toReal", ?)); } void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { sort_names.push_back(builtin_name("FP", FLOAT_SORT)); sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT)); + + // In the SMT FPA final draft, FP is called FloatingPoint + sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT)); } expr * float_decl_plugin::get_some_value(sort * s) { diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index f1b60a91b..3786b76ee 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -72,6 +72,12 @@ enum float_op_kind { OP_TO_FLOAT, OP_TO_IEEE_BV, + + OP_FLOAT_FP, + OP_FLOAT_TO_FP_UNSIGNED, + OP_FLOAT_TO_UBV, + OP_FLOAT_TO_SBV, + OP_FLOAT_TO_REAL, LAST_FLOAT_OP }; @@ -125,7 +131,17 @@ class float_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - + func_decl * mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); void recycled_id(unsigned id); diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 6ef147f1c..ecd06ff38 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -64,6 +64,11 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break; case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; + case OP_FLOAT_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; + case OP_FLOAT_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(args[0], args[1], result); break; + case OP_FLOAT_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break; + case OP_FLOAT_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break; + case OP_FLOAT_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; } return st; } @@ -504,3 +509,42 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) { return BR_FAILED; } + +br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { + bv_util bu(m()); + rational r1, r2, r3; + unsigned bvs1, bvs2, bvs3; + + if (bu.is_numeral(arg1, r1, bvs1) && bu.is_numeral(arg2, r2, bvs2) && bu.is_numeral(arg3, r3, bvs3)) { + SASSERT(m_util.fm().mpz_manager().is_one(r2.to_mpq().denominator())); + SASSERT(m_util.fm().mpz_manager().is_one(r3.to_mpq().denominator())); + SASSERT(m_util.fm().mpz_manager().is_int64(r3.to_mpq().numerator())); + scoped_mpf v(m_util.fm()); + mpf_exp_t biased_exp = m_util.fm().mpz_manager().get_int64(r2.to_mpq().numerator()); + m_util.fm().set(v, bvs2, bvs3 + 1, + r1.is_one(), + r3.to_mpq().numerator(), + m_util.fm().unbias_exp(bvs2, biased_exp)); + TRACE("fp_rewriter", tout << "v = " << m_util.fm().to_string(v) << std::endl;); + result = m_util.mk_value(v); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_real(expr * arg1, expr_ref & result) { + return BR_FAILED; +} \ No newline at end of file diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 4a0879d4b..0f44d227c 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -73,6 +73,12 @@ public: br_status mk_is_sign_minus(expr * arg1, expr_ref & result); br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); + + br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); + br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_real(expr * arg1, expr_ref & result); }; #endif diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index ebccf4d52..144925164 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1836,6 +1836,21 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a // Just keep it here, as there will be something else that uses it. mk_triple(args[0], args[1], args[2], result); } + else if (num == 1 && m_bv_util.is_bv(args[0])) { + sort * s = f->get_range(); + unsigned to_sbits = m_util.get_sbits(s); + unsigned to_ebits = m_util.get_ebits(s); + + expr * bv = args[0]; + int sz = m_bv_util.get_bv_size(bv); + SASSERT((unsigned)sz == to_sbits + to_ebits); + + m_bv_util.mk_extract(sz - 1, sz - 1, bv); + mk_triple(m_bv_util.mk_extract(sz - 1, sz - 1, bv), + m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv), + m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv), + result); + } else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) { // We also support float to float conversion sort * s = f->get_range(); @@ -2043,6 +2058,27 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); } +void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 3); + mk_triple(args[0], args[2], args[1], result); +} + +void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(to_app(e)->get_num_args() == 3); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 821618bae..79c8039ef 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -122,7 +122,13 @@ public: void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + + void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); obj_map const & const2bv() const { return m_const2bv; } obj_map const & rm_const2bv() const { return m_rm_const2bv; } diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index d737683a8..b2e3da939 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -139,6 +139,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE; case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index f3c913ccc..90cfc8c92 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -36,3 +36,77 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) { mk_sat_tactic(m, p), mk_fail_if_undecided_tactic()); } + +struct is_non_qffpa_predicate { + struct found {}; + ast_manager & m; + float_util u; + + is_non_qffpa_predicate(ast_manager & _m) :m(_m), u(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s))) + throw found(); + family_id fid = s->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == u.get_family_id()) + return; + + throw found(); + } +}; + +struct is_non_qffpabv_predicate { + struct found {}; + ast_manager & m; + bv_util bu; + float_util fu; + + is_non_qffpabv_predicate(ast_manager & _m) :m(_m), bu(m), fu(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !(fu.is_float(s) || fu.is_rm(s) || bu.is_bv_sort(s))) + throw found(); + family_id fid = s->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == fu.get_family_id() || fid == bu.get_family_id()) + return; + + throw found(); + } +}; + +class is_qffpa_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +class is_qffpabv_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +probe * mk_is_qffpa_probe() { + return alloc(is_qffpa_probe); +} + +probe * mk_is_qffpabv_probe() { + return alloc(is_qffpabv_probe); +} + \ No newline at end of file diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h index 8ca2183c1..cd16c5817 100644 --- a/src/tactic/fpa/qffpa_tactic.h +++ b/src/tactic/fpa/qffpa_tactic.h @@ -30,4 +30,11 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref()); ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)") */ +probe * mk_is_qffpa_probe(); +probe * mk_is_qffpabv_probe(); +/* + ADD_PROBE("is-qffpa", "true if the goal is in QF_FPA (FloatingPoints).", "mk_is_qffpa_probe()") + ADD_PROBE("is-qffpabv", "true if the goal is in QF_FPABV (FloatingPoints+Bitvectors).", "mk_is_qffpabv_probe()") +*/ + #endif diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index d65ba8d35..9ecc16ecf 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -27,6 +27,7 @@ Notes: #include"nra_tactic.h" #include"probe_arith.h" #include"quant_tactics.h" +#include"qffpa_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), @@ -37,7 +38,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m), cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), - mk_smt_tactic())))))))), + cond(mk_is_qffpabv_probe(), mk_qffpa_tactic(m, p), + mk_smt_tactic()))))))))), p); return st; } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 5910f55c9..8cb6ed4fc 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1400,6 +1400,10 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) { return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false)); } +mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) { + return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false)); +} + void mpf_manager::mk_nzero(unsigned ebits, unsigned sbits, mpf & o) { o.sbits = sbits; o.ebits = ebits; diff --git a/src/util/mpf.h b/src/util/mpf.h index 284b0ba7f..83646f9f3 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -182,6 +182,8 @@ public: mpf_exp_t mk_max_exp(unsigned ebits); mpf_exp_t mk_min_exp(unsigned ebits); + mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent); + /** \brief Return the biggest k s.t. 2^k <= a. From f111dd4e612ba2b0edfc9476f94aec2a5c093b94 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 28 Jan 2014 14:00:42 +0000 Subject: [PATCH 10/10] Fixes for the build on OS X 10.9 --- src/api/api_interp.cpp | 1 + src/interp/iz3hash.h | 2 +- src/interp/iz3mgr.cpp | 4 ++-- src/interp/iz3mgr.h | 1 + src/interp/iz3pp.cpp | 10 +++++----- 5 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 560ee5885..98722022c 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include #include +#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index 75d9aa604..94f282265 100755 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -66,7 +66,7 @@ Revision History: namespace stl_ext { template <> class hash { - stl_ext::hash H; + stl_ext::hash H; public: size_t operator()(const std::string &s) const { return H(s.c_str()); diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index f35dae93f..b85df81be 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -172,7 +172,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ std::vector names; - std::vector types; + std::vector types; std::vector bound_asts; unsigned num_bound = bvs.size(); @@ -485,7 +485,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& coeffs){ get_farkas_coeffs(proof,rats); coeffs.resize(rats.size()); for(unsigned i = 0; i < rats.size(); i++){ - sort *is = m().mk_sort(m_arith_fid, INT_SORT); + class sort *is = m().mk_sort(m_arith_fid, INT_SORT); ast coeff = cook(m_arith_util.mk_numeral(rats[i],is)); coeffs[i] = coeff; } diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 645c72ccb..7da247287 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -22,6 +22,7 @@ Revision History: #include +#include #include "iz3hash.h" #include"well_sorted.h" diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp index df6fcaf53..31b375c0f 100644 --- a/src/interp/iz3pp.cpp +++ b/src/interp/iz3pp.cpp @@ -58,20 +58,20 @@ namespace stl_ext { class free_func_visitor { ast_manager& m; func_decl_set m_funcs; - obj_hashtable m_sorts; + obj_hashtable m_sorts; public: free_func_visitor(ast_manager& m): m(m) {} void operator()(var * n) { } void operator()(app * n) { m_funcs.insert(n->get_decl()); - sort* s = m.get_sort(n); + class sort* s = m.get_sort(n); if (s->get_family_id() == null_family_id) { m_sorts.insert(s); } } void operator()(quantifier * n) { } func_decl_set& funcs() { return m_funcs; } - obj_hashtable& sorts() { return m_sorts; } + obj_hashtable& sorts() { return m_sorts; } }; class iz3pp_helper : public iz3mgr { @@ -146,8 +146,8 @@ void iz3pp(ast_manager &m, func_decl_set &funcs = visitor.funcs(); func_decl_set::iterator it = funcs.begin(), end = funcs.end(); - obj_hashtable& sorts = visitor.sorts(); - obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); + obj_hashtable& sorts = visitor.sorts(); + obj_hashtable::iterator sit = sorts.begin(), send = sorts.end();