mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Interpolation API bugfixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-10-09 18:08:07 +01:00
parent f0c63e56f3
commit 503ad78bf3
5 changed files with 126 additions and 255 deletions
Download patch file Download diff file Expand all files Collapse all files

17
scripts/update_api.py
View file

@ -123,7 +123,6 @@ SYMBOL = 9
PRINT_MODE = 10
ERROR_CODE = 11
DOUBLE = 12
UINT_PTR = 13
FIRST_OBJ_ID = 100
@ -132,28 +131,28 @@ def is_obj(ty):
Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : '__int64', UINT64 : '__uint64', DOUBLE : 'double',
STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'Z3_bool', SYMBOL : 'Z3_symbol',
PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code', UINT_PTR : 'unsigned*'
PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code'
}
Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctypes.c_uint', INT64 : 'ctypes.c_longlong',
UINT64 : 'ctypes.c_ulonglong', DOUBLE : 'ctypes.c_double',
STRING : 'ctypes.c_char_p', STRING_PTR : 'ctypes.POINTER(ctypes.c_char_p)', BOOL : 'ctypes.c_bool', SYMBOL : 'Symbol',
PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', UINT_PTR : 'ctypes.POINTER(ctypes.c_uint)'
PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint'
}
# Mapping to .NET types
Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double',
STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr',
PRINT_MODE : 'uint', ERROR_CODE : 'uint', UINT_PTR : 'uint[]'}
PRINT_MODE : 'uint', ERROR_CODE : 'uint' }
# Mapping to Java types
Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
STRING : 'String', STRING_PTR : 'StringPtr',
BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', UINT_PTR : 'int[]'}
BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int'}
Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble',
STRING : 'jstring', STRING_PTR : 'jobject',
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', UINT_PTR : 'jlong'}
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'}
next_type_id = FIRST_OBJ_ID
@ -964,7 +963,6 @@ def def_API(name, result, params):
tstr = type2str(ty)
if sz_p_k == OUT or sz_p_k == INOUT:
sz_e = ("(*a%s)" % sz)
tstr = tstr + '*'
else:
sz_e = ("a%s" % sz)
log_c.write(" for (unsigned i = 0; i < %s; i++) { " % sz_e)
@ -978,11 +976,6 @@ def def_API(name, result, params):
log_c.write(" }\n")
log_c.write(" Au(%s);\n" % sz_e)
exe_c.write("in.get_uint_array(%s)" % i)
elif ty == UINT_PTR:
log_c.write("P(0);")
log_c.write(" }\n")
log_c.write(" Ap(%s);\n" % sz_e)
exe_c.write("reinterpret_cast<%s>(in.get_obj_array(%s))" % (tstr, i))
else:
error ("unsupported parameter for %s, %s" % (name, p))
else:

177
src/api/api_interp.cpp
View file

@ -123,89 +123,6 @@ extern "C" {
}
}
Z3_lbool Z3_interpolate(Z3_context ctx,
unsigned num,
Z3_ast *cnsts,
unsigned *parents,
Z3_params options,
Z3_ast *interps,
Z3_model *model,
Z3_literals *labels,
unsigned incremental,
unsigned num_theory,
Z3_ast *theory
){
profiling::timer_start("Solve");
if (!incremental){
profiling::timer_start("Z3 assert");
Z3_push(ctx); // so we can rewind later
for (unsigned i = 0; i < num; i++)
Z3_assert_cnstr(ctx, cnsts[i]); // assert all the constraints
if (theory){
for (unsigned i = 0; i < num_theory; i++)
Z3_assert_cnstr(ctx, theory[i]);
}
profiling::timer_stop("Z3 assert");
}
// Get a proof of unsat
Z3_ast proof;
Z3_lbool result;
profiling::timer_start("Z3 solving");
result = Z3_check_assumptions(ctx, 0, 0, model, &proof, 0, 0);
profiling::timer_stop("Z3 solving");
switch (result) {
case Z3_L_FALSE:
Z3_interpolate_proof(ctx,
proof,
num,
cnsts,
parents,
options,
interps,
num_theory,
theory);
if (!incremental)
for (unsigned i = 0; i < num - 1; i++)
Z3_persist_ast(ctx, interps[i], 1);
break;
case Z3_L_UNDEF:
if (labels)
*labels = Z3_get_relevant_labels(ctx);
break;
case Z3_L_TRUE:
if (labels)
*labels = Z3_get_relevant_labels(ctx);
break;
}
profiling::timer_start("Z3 pop");
if (!incremental)
Z3_pop(ctx, 1);
profiling::timer_stop("Z3 pop");
profiling::timer_stop("Solve");
return result;
}
static std::ostringstream itp_err;
int Z3_check_interpolant(Z3_context ctx,
@ -603,7 +520,7 @@ extern "C" {
}
int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast **cnsts, unsigned **parents, const char *filename, const char **error, unsigned *ret_num_theory, Z3_ast **theory){
int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast cnsts[], unsigned parents[], const char *filename, Z3_string_ptr error, unsigned *ret_num_theory, Z3_ast theory[]){
hash_map<std::string, std::string> file_params;
get_file_params(filename, file_params);
@ -632,11 +549,11 @@ extern "C" {
if (ret_num_theory)
*ret_num_theory = num_theory;
if (theory)
*theory = &read_theory[0];
theory = &read_theory[0];
if (!parents){
*_num = num;
*cnsts = &read_cnsts[0];
cnsts = &read_cnsts[0];
return true;
}
@ -706,8 +623,8 @@ extern "C" {
}
*_num = num;
*cnsts = &read_cnsts[0];
*parents = &read_parents[0];
cnsts = &read_cnsts[0];
parents = &read_parents[0];
return true;
fail:
@ -717,3 +634,87 @@ extern "C" {
}
}
#if 0
/** Constant reprepresenting a root of a formula tree for tree interpolation */
#define IZ3_ROOT SHRT_MAX
/** This function uses Z3 to determine satisfiability of a set of
constraints. If UNSAT, an interpolant is returned, based on the
refutation generated by Z3. If SAT, a model is returned.
If "parents" is non-null, computes a tree interpolant. The tree is
defined by the array "parents". This array maps each formula in
the tree to its parent, where formulas are indicated by their
integer index in "cnsts". The parent of formula n must have index
greater than n. The last formula is the root of the tree. Its
parent entry should be the constant IZ3_ROOT.
If "parents" is null, computes a sequence interpolant.
\param ctx The Z3 context. Must be generated by iz3_mk_context
\param num The number of constraints in the sequence
\param cnsts Array of constraints (AST's in context ctx)
\param parents The parents vector defining the tree structure
\param options Interpolation options (may be NULL)
\param interps Array to return interpolants (size at least num-1, may be NULL)
\param model Returns a Z3 model if constraints SAT (may be NULL)
\param labels Returns relevant labels if SAT (may be NULL)
\param incremental
VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3
context ctx. The model and interpolants returned are also
in this context.
The return code is as in Z3_check_assumptions, that is,
Z3_L_FALSE = constraints UNSAT (interpolants returned)
Z3_L_TRUE = constraints SAT (model returned)
Z3_L_UNDEF = Z3 produced no result, or interpolation not possible
Currently, this function supports integer and boolean variables,
as well as arrays over these types, with linear arithmetic,
uninterpreted functions and quantifiers over integers (that is
AUFLIA). Interpolants are produced in AULIA. However, some
uses of array operations may cause quantifiers to appear in the
interpolants even when there are no quantifiers in the input formulas.
Although quantifiers may appear in the input formulas, Z3 may give up in
this case, returning Z3_L_UNDEF.
If "incremental" is true, cnsts must contain exactly the set of
formulas that are currently asserted in the context. If false,
there must be no formulas currently asserted in the context.
Setting "incremental" to true makes it posisble to incrementally
add and remove constraints from the context until the context
becomes UNSAT, at which point an interpolant is computed. Caution
must be used, however. Before popping the context, if you wish to
keep the interolant formulas, you *must* preserve them by using
Z3_persist_ast. Also, if you want to simplify the interpolant
formulas using Z3_simplify, you must first pop all of the
assertions in the context (or use a different context). Otherwise,
the formulas will be simplified *relative* to these constraints,
which is almost certainly not what you want.
Current limitations on tree interpolants. In a tree interpolation
problem, each constant (0-ary function symbol) must occur only
along one path from root to leaf. Function symbols (of arity > 0)
are considered to have global scope (i.e., may appear in any
interpolant formula).
def_API('Z3_interpolate', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST)))
*/
Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
__in unsigned num,
__in_ecount(num) Z3_ast *cnsts,
__in_ecount(num) unsigned *parents,
__in Z3_params options,
__out_ecount(num - 1) Z3_ast *interps,
__out Z3_model *model,
__out Z3_literals *labels,
__in unsigned incremental,
__in unsigned num_theory,
__in_ecount(num_theory) Z3_ast *theory);
#endif

63
src/api/dotnet/InterpolationContext.cs
View file

@ -89,47 +89,6 @@ namespace Microsoft.Z3
return (Z3_lbool)r;
}
/// <summary>
/// Computes an interpolant.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_compute_interpolant in the C/C++ API, which is
/// well documented.</remarks>
Z3_lbool Interpolate(Expr[] cnsts, uint[] parents, Params options, bool incremental, Expr[] theory, out Expr[] interps, out Model model)
{
Contract.Requires(cnsts != null);
Contract.Requires(parents != null);
Contract.Requires(cnsts.Length == parents.Length);
Contract.Ensures(Contract.ValueAtReturn(out interps) != null);
Contract.Ensures(Contract.ValueAtReturn(out model) != null);
CheckContextMatch(cnsts);
CheckContextMatch(theory);
uint sz = (uint)cnsts.Length;
IntPtr[] ni = new IntPtr[sz - 1];
IntPtr nm = IntPtr.Zero;
IntPtr z = IntPtr.Zero;
int r = Native.Z3_interpolate(nCtx,
sz, Expr.ArrayToNative(cnsts), parents,
options.NativeObject,
out ni,
ref nm,
ref z, // Z3_lterals are deprecated.
(uint)(incremental ? 1 : 0),
(uint)theory.Length, Expr.ArrayToNative(theory));
interps = new Expr[sz - 1];
for (uint i = 0; i < sz - 1; i++)
interps[i] = Expr.Create(this, ni[i]);
model = new Model(this, nm);
return (Z3_lbool)r;
}
/// <summary>
/// Return a string summarizing cumulative time used for interpolation.
/// </summary>
@ -150,7 +109,7 @@ namespace Microsoft.Z3
public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory)
{
Contract.Requires(cnsts.Length == parents.Length);
Contract.Requires(cnsts.Length == interps.Length+1);
Contract.Requires(cnsts.Length == interps.Length + 1);
IntPtr n_err_str;
int r = Native.Z3_check_interpolant(nCtx,
(uint)cnsts.Length,
@ -170,25 +129,27 @@ namespace Microsoft.Z3
/// <remarks>For more information on interpolation please refer
/// too the function Z3_read_interpolation_problem in the C/C++ API, which is
/// well documented.</remarks>
public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
public int ReadInterpolationProblem(string filename, out Expr[] cnsts, ref uint[] parents, out string error, out Expr[] theory)
{
uint num = 0, num_theory = 0;
IntPtr[] n_cnsts;
IntPtr[] n_theory;
IntPtr n_cnsts = new IntPtr();
IntPtr n_theory = new IntPtr();
IntPtr n_err_str;
uint[][] n_parents;
int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out n_parents, filename, out n_err_str, ref num_theory, out n_theory);
int r = Native.Z3_read_interpolation_problem(nCtx, ref num, ref n_cnsts, out parents, filename, out n_err_str, ref num_theory, ref n_theory);
error = Marshal.PtrToStringAnsi(n_err_str);
cnsts = new Expr[num];
parents = new uint[num];
theory = new Expr[num_theory];
theory = new Expr[num_theory];
for (int i = 0; i < num; i++)
{
cnsts[i] = Expr.Create(this, n_cnsts[i]);
parents[i] = n_parents[0][i];
IntPtr ce = new IntPtr(n_cnsts.ToInt64() + (IntPtr.Size * i));
cnsts[i] = Expr.Create(this, ce);
}
for (int i = 0; i < num_theory; i++)
theory[i] = Expr.Create(this, n_theory[i]);
{
IntPtr te = new IntPtr(n_theory.ToInt64() + (IntPtr.Size * i));
theory[i] = Expr.Create(this, te);
}
return r;
}

18
src/api/z3_api.h
View file

@ -1779,7 +1779,7 @@ extern "C" {
Z3_sort Z3_API Z3_mk_tuple_sort(__in Z3_context c,
__in Z3_symbol mk_tuple_name,
__in unsigned num_fields,
__in_ecount(num_fields) Z3_symbol const field_names[],
__in_ecount(num_fields) Z3_symbol const field_names[],
__in_ecount(num_fields) Z3_sort const field_sorts[],
__out Z3_func_decl * mk_tuple_decl,
__out_ecount(num_fields) Z3_func_decl proj_decl[]);
@ -4907,8 +4907,7 @@ END_MLAPI_EXCLUDE
__in_ecount(num_sorts) Z3_sort const sorts[],
__in unsigned num_decls,
__in_ecount(num_decls) Z3_symbol const decl_names[],
__in_ecount(num_decls) Z3_func_decl const decls[]
);
__in_ecount(num_decls) Z3_func_decl const decls[]);
/**
\brief Similar to #Z3_parse_smtlib2_string, but reads the benchmark from a file.
@ -4917,13 +4916,12 @@ END_MLAPI_EXCLUDE
*/
Z3_ast Z3_API Z3_parse_smtlib2_file(__in Z3_context c,
__in Z3_string file_name,
__in unsigned num_sorts,
__in_ecount(num_sorts) Z3_symbol const sort_names[],
__in_ecount(num_sorts) Z3_sort const sorts[],
__in unsigned num_decls,
__in_ecount(num_decls) Z3_symbol const decl_names[],
__in_ecount(num_decls) Z3_func_decl const decls[]
);
__in unsigned num_sorts,
__in_ecount(num_sorts) Z3_symbol const sort_names[],
__in_ecount(num_sorts) Z3_sort const sorts[],
__in unsigned num_decls,
__in_ecount(num_decls) Z3_symbol const decl_names[],
__in_ecount(num_decls) Z3_func_decl const decls[]);
#ifdef ML4only
#include <mlx_parse_smtlib.idl>

106
src/api/z3_interp.h
View file

@ -163,88 +163,6 @@ extern "C" {
__out Z3_ast_vector *interp,
__out Z3_model *model);
/** Constant reprepresenting a root of a formula tree for tree interpolation */
#define IZ3_ROOT SHRT_MAX
/** This function uses Z3 to determine satisfiability of a set of
constraints. If UNSAT, an interpolant is returned, based on the
refutation generated by Z3. If SAT, a model is returned.
If "parents" is non-null, computes a tree interpolant. The tree is
defined by the array "parents". This array maps each formula in
the tree to its parent, where formulas are indicated by their
integer index in "cnsts". The parent of formula n must have index
greater than n. The last formula is the root of the tree. Its
parent entry should be the constant IZ3_ROOT.
If "parents" is null, computes a sequence interpolant.
\param ctx The Z3 context. Must be generated by iz3_mk_context
\param num The number of constraints in the sequence
\param cnsts Array of constraints (AST's in context ctx)
\param parents The parents vector defining the tree structure
\param options Interpolation options (may be NULL)
\param interps Array to return interpolants (size at least num-1, may be NULL)
\param model Returns a Z3 model if constraints SAT (may be NULL)
\param labels Returns relevant labels if SAT (may be NULL)
\param incremental
VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3
context ctx. The model and interpolants returned are also
in this context.
The return code is as in Z3_check_assumptions, that is,
Z3_L_FALSE = constraints UNSAT (interpolants returned)
Z3_L_TRUE = constraints SAT (model returned)
Z3_L_UNDEF = Z3 produced no result, or interpolation not possible
Currently, this function supports integer and boolean variables,
as well as arrays over these types, with linear arithmetic,
uninterpreted functions and quantifiers over integers (that is
AUFLIA). Interpolants are produced in AULIA. However, some
uses of array operations may cause quantifiers to appear in the
interpolants even when there are no quantifiers in the input formulas.
Although quantifiers may appear in the input formulas, Z3 may give up in
this case, returning Z3_L_UNDEF.
If "incremental" is true, cnsts must contain exactly the set of
formulas that are currently asserted in the context. If false,
there must be no formulas currently asserted in the context.
Setting "incremental" to true makes it posisble to incrementally
add and remove constraints from the context until the context
becomes UNSAT, at which point an interpolant is computed. Caution
must be used, however. Before popping the context, if you wish to
keep the interolant formulas, you *must* preserve them by using
Z3_persist_ast. Also, if you want to simplify the interpolant
formulas using Z3_simplify, you must first pop all of the
assertions in the context (or use a different context). Otherwise,
the formulas will be simplified *relative* to these constraints,
which is almost certainly not what you want.
Current limitations on tree interpolants. In a tree interpolation
problem, each constant (0-ary function symbol) must occur only
along one path from root to leaf. Function symbols (of arity > 0)
are considered to have global scope (i.e., may appear in any
interpolant formula).
def_API('Z3_interpolate', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST)))
*/
Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
__in unsigned num,
__in_ecount(num) Z3_ast *cnsts,
__in_ecount(num) unsigned *parents,
__in Z3_params options,
__out_ecount(num - 1) Z3_ast *interps,
__out Z3_model *model,
__out Z3_literals *labels,
__in unsigned incremental,
__in unsigned num_theory,
__in_ecount(num_theory) Z3_ast *theory);
/** Return a string summarizing cumulative time used for
interpolation. This string is purely for entertainment purposes
and has no semantics.
@ -288,18 +206,18 @@ extern "C" {
where each value is represented using the common symbols between
the formulas in the subtree and the remainder of the formulas.
def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out_array(1, AST), _out_array(1, UINT_PTR), _in(STRING), _out(STRING), _out(UINT), _out_array(6, AST)))
def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out(AST), _out_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out(AST)))
*/
int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
__out unsigned *num,
__out_ecount(*num) Z3_ast **cnsts,
__out_ecount(*num) unsigned **parents,
__out Z3_ast *cnsts,
__out unsigned parents[],
__in Z3_string filename,
__out Z3_string *error,
__out_opt Z3_string_ptr error,
__out unsigned *num_theory,
__out_ecount(*num_theory) Z3_ast **theory);
__out Z3_ast theory[]);
@ -323,12 +241,12 @@ extern "C" {
int Z3_API Z3_check_interpolant(__in Z3_context ctx,
__in unsigned num,
__in_ecount(num) Z3_ast *cnsts,
__in_ecount(num) unsigned *parents,
__in_ecount(num) Z3_ast cnsts[],
__in_ecount(num) unsigned parents[],
__in_ecount(num - 1) Z3_ast *interps,
__out Z3_string *error,
__out_opt Z3_string_ptr error,
__in unsigned num_theory,
__in_ecount(num_theory) Z3_ast *theory);
__in_ecount(num_theory) Z3_ast theory[]);
/** Write an interpolation problem to file suitable for reading with
Z3_read_interpolation_problem. The output file is a sequence
@ -346,11 +264,11 @@ extern "C" {
void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx,
__in unsigned num,
__in_ecount(num) Z3_ast *cnsts,
__in_ecount(num) unsigned *parents,
__in_ecount(num) Z3_ast cnsts[],
__in_ecount(num) unsigned parents[],
__in Z3_string filename,
__in unsigned num_theory,
__in_ecount(num_theory) Z3_ast *theory);
__in_ecount(num_theory) Z3_ast theory[]);
#ifdef __cplusplus
};