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

local changes to pdr_generalizer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-02-09 10:58:37 -08:00
parent 3ad43c60a9 473bc2bc81
commit ce9a098f16
7 changed files with 39 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/java/JavaExample.java
View file

@ -2155,7 +2155,7 @@ class JavaExample
// But you cannot mix numerals of different sorts
// even if the size of their domains are the same:
// System.out.println(ctx.mkEq(s1, t1));
}
}
public static void main(String[] args)
{
@ -2226,7 +2226,7 @@ class JavaExample
Context ctx = new Context(cfg);
p.quantifierExample3(ctx);
p.quantifierExample4(ctx);
}
}
Log.close();
if (Log.isOpen())

35
scripts/update_api.py
View file

@ -395,8 +395,7 @@ def mk_dotnet():
dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n')
dotnet.write(' public unsafe class LIB\n')
dotnet.write(' {\n')
dotnet.write(' '
' const string Z3_DLL_NAME = \"libz3.dll\";\n'
dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n'
' \n');
dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n')
dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n')
@ -420,7 +419,8 @@ def mk_dotnet():
dotnet.write(' }\n')
DotnetUnwrapped = [ 'Z3_del_context' ]
NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
Unwrapped = [ 'Z3_del_context' ]
def mk_dotnet_wrappers():
global Type2Str
@ -469,11 +469,15 @@ def mk_dotnet_wrappers():
dotnet.write('a%d' % i)
i = i + 1
dotnet.write(');\n');
if name not in DotnetUnwrapped:
if len(params) > 0 and param_type(params[0]) == CONTEXT:
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
if name not in Unwrapped:
if name in NULLWrapped:
dotnet.write(" if (r == IntPtr.Zero)\n")
dotnet.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
else:
if len(params) > 0 and param_type(params[0]) == CONTEXT:
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
if result == STRING:
dotnet.write(" return Marshal.PtrToStringAnsi(r);\n")
elif result != VOID:
@ -550,7 +554,7 @@ def mk_java():
java_native.write('%s a%d' % (param2java(param), i))
i = i + 1
java_native.write(')')
if len(params) > 0 and param_type(params[0]) == CONTEXT:
if (len(params) > 0 and param_type(params[0]) == CONTEXT) or name in NULLWrapped:
java_native.write(' throws Z3Exception')
java_native.write('\n')
java_native.write(' {\n')
@ -568,10 +572,15 @@ def mk_java():
java_native.write('a%d' % i)
i = i + 1
java_native.write(');\n')
if len(params) > 0 and param_type(params[0]) == CONTEXT:
java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
java_native.write(' if (err != Z3_error_code.Z3_OK)\n')
java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n')
if name not in Unwrapped:
if name in NULLWrapped:
java_native.write(" if (res == 0)\n")
java_native.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
else:
if len(params) > 0 and param_type(params[0]) == CONTEXT:
java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
java_native.write(' if (err != Z3_error_code.Z3_OK)\n')
java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n')
if result != VOID:
java_native.write(' return res;\n')
java_native.write(' }\n\n')

4
src/api/api_context.cpp
View file

@ -419,17 +419,21 @@ namespace api {
extern "C" {
Z3_context Z3_API Z3_mk_context(Z3_config c) {
Z3_TRY;
LOG_Z3_mk_context(c);
memory::initialize(UINT_MAX);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), false));
RETURN_Z3(r);
Z3_CATCH_RETURN_NO_HANDLE(0);
}
Z3_context Z3_API Z3_mk_context_rc(Z3_config c) {
Z3_TRY;
LOG_Z3_mk_context_rc(c);
memory::initialize(UINT_MAX);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), true));
RETURN_Z3(r);
Z3_CATCH_RETURN_NO_HANDLE(0);
}
void Z3_API Z3_del_context(Z3_context c) {

1
src/api/api_util.h
View file

@ -26,6 +26,7 @@ Revision History:
#define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE }
#define Z3_CATCH Z3_CATCH_CORE(return;)
#define Z3_CATCH_RETURN(VAL) Z3_CATCH_CORE(return VAL;)
#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; }
#define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
#define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a))

8
src/api/java/Context.java
View file

@ -3053,10 +3053,10 @@ public class Context extends IDisposable
// OK.
}
m_ctx = 0;
} else
/* re-queue the finalizer */
/* BUG: DRQ's need to be taken over too! */
new Context(m_ctx, m_refCount);
}
/*
else
CMW: re-queue the finalizer? */
}
/**

6
src/ast/ast_smt_pp.cpp
View file

@ -537,7 +537,7 @@ class smt_printer {
}
void print_bound(symbol const& name) {
if (name.is_numerical() || '?' != name.bare_str()[0]) {
if (!is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) {
m_out << "?";
}
m_out << name;
@ -642,7 +642,9 @@ class smt_printer {
m_out << m_var_names[m_num_var_names - idx - 1];
}
else {
m_out << "?" << idx;
if (!m_is_smt2) {
m_out << "?" << idx;
}
}
}

4
src/muz_qe/pdr_generalizers.cpp
View file

@ -270,8 +270,8 @@ namespace pdr {
vector<term_loc_t> & terms1 = it->m_value;
vector<term_loc_t> terms2;
if (r >= rational(2) && m_ub.find(r, terms2)) {
bool done = false;
for (unsigned i = 0; !done && i < terms1.size(); ++i) {
for (unsigned i = 0; i < terms1.size(); ++i) {
bool done = false;
for (unsigned j = 0; !done && j < terms2.size(); ++j) {
expr* t1 = terms1[i].first;
expr* t2 = terms2[j].first;