mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable
This commit is contained in:
commit
137b8c8e04
|
@ -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')
|
||||
|
|
|
@ -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)))
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -529,6 +529,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";
|
||||
}
|
||||
|
||||
|
@ -548,6 +549,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";
|
||||
}
|
||||
|
||||
|
|
|
@ -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();
|
||||
|
|
|
@ -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<has_fp_to_real_predicate>(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);
|
||||
|
|
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue