mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix #6746, fix type errors in java bindings

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-06-03 09:41:29 +02:00
parent 82667bd86b
commit 81068981aa
4 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/java/NativeStatic.txt
View file

@ -203,7 +203,7 @@ DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateRegisterDec
Z3_solver_propagate_decide((Z3_context)ctx, (Z3_solver)solver, decide_eh); Z3_solver_propagate_decide((Z3_context)ctx, (Z3_solver)solver, decide_eh);
} }
DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateConflict(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, jlong num_fixed, jlongArray fixed, jlong num_eqs, jlongArray eq_lhs, jlongArray eq_rhs, jlong conseq) { DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateConflict(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, long num_fixed, jlongArray fixed, long num_eqs, jlongArray eq_lhs, jlongArray eq_rhs, jlong conseq) {
JavaInfo *info = (JavaInfo*)javainfo; JavaInfo *info = (JavaInfo*)javainfo;
GETLONGAELEMS(Z3_ast, fixed, _fixed); GETLONGAELEMS(Z3_ast, fixed, _fixed);
GETLONGAELEMS(Z3_ast, eq_lhs, _eq_lhs); GETLONGAELEMS(Z3_ast, eq_lhs, _eq_lhs);
@ -226,7 +226,7 @@ DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateAdd(JNIEnv
} }
} }
DLL_VIS JNIEXPORT bool JNICALL Java_com_microsoft_z3_Native_propagateNextSplit(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, long e, long idx, int phase) { DLL_VIS JNIEXPORT bool JNICALL Java_com_microsoft_z3_Native_propagateNextSplit(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, jlong e, long idx, int phase) {
JavaInfo *info = (JavaInfo*)javainfo; JavaInfo *info = (JavaInfo*)javainfo;
Z3_solver_callback cb = info->cb; Z3_solver_callback cb = info->cb;
return Z3_solver_next_split((Z3_context)ctx, cb, (Z3_ast)e, idx, Z3_lbool(phase)); return Z3_solver_next_split((Z3_context)ctx, cb, (Z3_ast)e, idx, Z3_lbool(phase));

7
src/cmd_context/cmd_context.cpp
View file

@ -508,11 +508,12 @@ public:
m_owner.m_func_decls.contains(s); m_owner.m_func_decls.contains(s);
} }
format_ns::format * pp_sort(sort * s) override { format_ns::format * pp_sort(sort * s) override {
auto * f = m_owner.pp(s); auto * f = m_owner.try_pp(s);
if (f) if (f)
return f; return f;
return smt2_pp_environment::pp_sort(s); return smt2_pp_environment::pp_sort(s);
} }
format_ns::format * pp_fdecl(func_decl * f, unsigned & len) override { format_ns::format * pp_fdecl(func_decl * f, unsigned & len) override {
symbol s = f->get_name(); symbol s = f->get_name();
func_decls fs; func_decls fs;
@ -2264,6 +2265,10 @@ bool cmd_context::is_model_available(model_ref& md) const {
} }
format_ns::format * cmd_context::pp(sort * s) const { format_ns::format * cmd_context::pp(sort * s) const {
return get_pp_env().pp_sort(s);
}
format_ns::format* cmd_context::try_pp(sort* s) const {
TRACE("cmd_context", tout << "pp(sort * s), s: " << mk_pp(s, m()) << "\n";); TRACE("cmd_context", tout << "pp(sort * s), s: " << mk_pp(s, m()) << "\n";);
return pm().pp(get_pp_env(), s); return pm().pp(get_pp_env(), s);
} }

1
src/cmd_context/cmd_context.h
View file

@ -538,6 +538,7 @@ public:
} }
format_ns::format * pp(sort * s) const; format_ns::format * pp(sort * s) const;
format_ns::format* try_pp(sort* s) const;
void pp(sort * s, format_ns::format_ref & r) const override { r = pp(s); } void pp(sort * s, format_ns::format_ref & r) const override { r = pp(s); }
void pp(func_decl * f, format_ns::format_ref & r) const override; void pp(func_decl * f, format_ns::format_ref & r) const override;
void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const override; void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const override;