diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 4bccdf6bb..b9641c869 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -55,7 +55,6 @@ def init_project_def(): add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv') add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') - add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic'], 'tactic/fpa') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') add_lib('qe', ['smt','sat'], 'qe') add_lib('duality', ['smt', 'interp', 'qe']) @@ -71,6 +70,7 @@ def init_project_def(): add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp') add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt') add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics') + add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') diff --git a/scripts/update_api.py b/scripts/update_api.py index 051e8fced..0d57a29ac 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -568,10 +568,12 @@ def mk_java(): java_native.write(' public static class ObjArrayPtr { public long[] value; }\n') java_native.write(' public static class UIntArrayPtr { public int[] value; }\n') java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') - if IS_WINDOWS or os.uname()[0]=="CYGWIN": - java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) - else: - java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name + + java_native.write(' static {\n') + java_native.write(' try { System.loadLibrary("z3java"); }\n') + java_native.write(' catch (UnsatisfiedLinkError ex) { System.loadLibrary("libz3java"); }\n') + java_native.write(' }\n') + java_native.write('\n') for name, result, params in _dotnet_decls: java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name))) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d2d2c6a3f..16b7cc1da 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2312,7 +2312,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * mk_ite(rm_nta, v1, result, result); } } - else { + else { + SASSERT(!m_arith_util.is_numeral(x)); bv_util & bu = m_bv_util; arith_util & au = m_arith_util; @@ -2330,12 +2331,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * expr_ref rme(rm, m); round(s, rme, sgn, sig, exp, result); - expr_ref c0(m); - mk_is_zero(x, c0); - mk_ite(c0, x, result, result); - expr * e = m.mk_eq(m_util.mk_to_real(result), x); - m_extra_assertions.push_back(e); + m_extra_assertions.push_back(e); } SASSERT(is_well_sorted(m, result)); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 738e8ec29..07a39bcae 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -143,9 +143,9 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) { if (m_hi_fp_unspecified) - result = m_util.au().mk_numeral(0, false); - else // The "hardware interpretation" is 0. + result = m_util.au().mk_numeral(rational(0), false); + else result = m_util.mk_internal_to_real_unspecified(); return BR_DONE; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 80aa10cde..9aa089096 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -528,6 +528,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "LRA" || s == "QF_FP" || s == "QF_FPBV" || + s == "QF_BVFP" || s == "HORN"; } @@ -547,6 +548,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const { s == "QF_AUFBV" || s == "QF_BVRE" || s == "QF_FPBV" || + s == "QF_BVFP" || s == "HORN"; } diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index d4c0e1efb..98ad5e51a 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -116,7 +116,7 @@ namespace smt { setup_LRA(); else if (m_logic == "QF_FP") setup_QF_FP(); - else if (m_logic == "QF_FPBV") + else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP") setup_QF_FPBV(); else setup_unknown(); diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 4854b3c07..3bee224b3 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -23,9 +23,47 @@ Notes: #include"fpa2bv_tactic.h" #include"smt_tactic.h" #include"propagate_values_tactic.h" +#include"probe_arith.h" +#include"qfnra_tactic.h" #include"qffp_tactic.h" + +struct has_fp_to_real_predicate { + struct found {}; + ast_manager & m; + bv_util bu; + fpa_util fu; + arith_util au; + + has_fp_to_real_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (au.is_real(s) && n->get_family_id() == fu.get_family_id() && + is_app(n) && to_app(n)->get_kind() == OP_FPA_TO_REAL) + throw found(); + } +}; + +class has_fp_to_real_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } + + virtual ~has_fp_to_real_probe() {} +}; + +probe * mk_has_fp_to_real_probe() { + return alloc(has_fp_to_real_probe); +} + + tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { params_ref simp_p = p; simp_p.set_bool("arith_lhs", true); @@ -40,10 +78,13 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { mk_propagate_values_tactic(m, p), using_params(mk_simplify_tactic(m, p), simp_p), mk_bit_blaster_tactic(m, p), - using_params(mk_simplify_tactic(m, p), simp_p), + using_params(mk_simplify_tactic(m, p), simp_p), cond(mk_is_propositional_probe(), mk_sat_tactic(m, p), - mk_smt_tactic(p)), + cond(mk_has_fp_to_real_probe(), + mk_qfnra_tactic(m, p), + mk_smt_tactic(p)) + ), mk_fail_if_undecided_tactic()))); st->updt_params(p); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index b28c8cf3d..687771a30 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -81,7 +81,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_ufbv_tactic(m, p); else if (logic=="QF_FP") return mk_qffp_tactic(m, p); - else if (logic == "QF_FPBV") + else if (logic == "QF_FPBV" || logic == "QF_BVFP") return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p);