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

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2014-10-11 09:46:14 -07:00
commit 4d1f3ca087
11 changed files with 369 additions and 287 deletions
Download patch file Download diff file Expand all files Collapse all files

10
examples/interp/iz3.cpp
View file

@ -90,12 +90,12 @@ int main(int argc, const char **argv) {
/* Read an interpolation problem */
int num;
unsigned num;
Z3_ast *constraints;
int *parents = 0;
unsigned *parents = 0;
const char *error;
bool ok;
int num_theory;
unsigned num_theory;
Z3_ast *theory;
ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory);
@ -144,7 +144,7 @@ int main(int argc, const char **argv) {
if(!incremental_mode){
/* In non-incremental mode, we just pass the constraints. */
result = Z3_interpolate(ctx, num, constraints, (unsigned int *)parents, options, interpolants, &model, 0, false, num_theory, theory);
result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &model, 0, false, num_theory, theory);
}
else {
@ -165,7 +165,7 @@ int main(int argc, const char **argv) {
for(int i = 0; i < num; i++){
asserted[i] = constraints[i];
Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint
result = Z3_interpolate(ctx, num, &asserted[0], (unsigned int *)parents, options, interpolants, &model, 0, true, 0, 0);
result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0);
if(result == Z3_L_FALSE){
for(unsigned j = 0; j < num-1; j++)
/* Since we want the interpolant formulas to survive a "pop", we

66
scripts/update_api.py
View file

@ -108,6 +108,7 @@ INOUT = 2
IN_ARRAY = 3
OUT_ARRAY = 4
INOUT_ARRAY = 5
OUT_MANAGED_ARRAY = 6
# Primitive Types
VOID = 0
@ -123,7 +124,6 @@ SYMBOL = 9
PRINT_MODE = 10
ERROR_CODE = 11
DOUBLE = 12
UINT_PTR = 13
FIRST_OBJ_ID = 100
@ -132,28 +132,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
@ -225,6 +225,10 @@ def _out_array2(cap, sz, ty):
def _inout_array(sz, ty):
return (INOUT_ARRAY, ty, sz, sz);
def _out_managed_array(sz,ty):
return (OUT_MANAGED_ARRAY, ty, 0, sz)
def param_kind(p):
return p[0]
@ -255,11 +259,11 @@ def param2dotnet(p):
return "out IntPtr"
else:
return "[In, Out] ref %s" % type2dotnet(param_type(p))
if k == IN_ARRAY:
elif k == IN_ARRAY:
return "[In] %s[]" % type2dotnet(param_type(p))
if k == INOUT_ARRAY:
elif k == INOUT_ARRAY:
return "[In, Out] %s[]" % type2dotnet(param_type(p))
if k == OUT_ARRAY:
elif k == OUT_ARRAY or k == OUT_MANAGED_ARRAY:
return "[Out] out %s[]" % type2dotnet(param_type(p))
else:
return type2dotnet(param_type(p))
@ -269,7 +273,7 @@ def param2java(p):
if k == OUT:
if param_type(p) == INT or param_type(p) == UINT:
return "IntPtr"
elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID:
elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) == VOID_PTR or param_type(p) >= FIRST_OBJ_ID:
return "LongPtr"
elif param_type(p) == STRING:
return "StringPtr"
@ -277,8 +281,13 @@ def param2java(p):
print("ERROR: unreachable code")
assert(False)
exit(1)
if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s[]" % type2java(param_type(p))
elif k == OUT_MANAGED_ARRAY:
if param_type(p) == UINT:
return "UIntArrayPtr"
else:
return "ObjArrayPtr"
else:
return type2java(param_type(p))
@ -467,7 +476,7 @@ def mk_dotnet_wrappers():
dotnet.write('out ');
else:
dotnet.write('ref ')
elif param_kind(param) == OUT_ARRAY:
elif param_kind(param) == OUT_ARRAY or param_kind(param) == OUT_MANAGED_ARRAY:
dotnet.write('out ');
dotnet.write('a%d' % i)
i = i + 1
@ -525,6 +534,8 @@ def mk_java():
java_native.write(' public static class IntPtr { public int value; }\n')
java_native.write(' public static class LongPtr { public long value; }\n')
java_native.write(' public static class StringPtr { public String value; }\n')
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)
@ -679,9 +690,11 @@ def mk_java():
if param_type(param) == INT or param_type(param) == UINT:
java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
else:
java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
elif k == IN and param_type(param) == STRING:
java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i))
elif k == OUT_MANAGED_ARRAY:
java_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i))
i = i + 1
# invoke procedure
java_wrapper.write(' ')
@ -700,6 +713,8 @@ def mk_java():
java_wrapper.write('&_a%s' % i)
elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY:
java_wrapper.write('_a%s' % i)
elif k == OUT_MANAGED_ARRAY:
java_wrapper.write('&_a%s' % i)
elif k == IN and param_type(param) == STRING:
java_wrapper.write('_a%s' % i)
else:
@ -735,6 +750,8 @@ def mk_java():
java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n')
java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i))
java_wrapper.write(' }\n')
elif k == OUT_MANAGED_ARRAY:
java_wrapper.write(' *(jlong**)a%s = (jlong*)_a%s;\n' % (i, i))
i = i + 1
# return
if result == STRING:
@ -935,6 +952,9 @@ def def_API(name, result, params):
elif ty == INT64:
log_c.write(" I(0);\n")
exe_c.write("in.get_int64_addr(%s)" % i)
elif ty == VOID_PTR:
log_c.write(" P(0);\n")
exe_c.write("in.get_obj_addr(%s)" % i)
else:
error("unsupported parameter for %s, %s" % (name, p))
elif kind == IN_ARRAY or kind == INOUT_ARRAY:
@ -964,7 +984,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,13 +997,22 @@ 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))
elif kind == OUT_MANAGED_ARRAY:
sz = param_array_size_pos(p)
sz_p = params[sz]
sz_p_k = param_kind(sz_p)
tstr = type2str(ty)
if sz_p_k == OUT or sz_p_k == INOUT:
sz_e = ("(*a%s)" % sz)
else:
sz_e = ("a%s" % sz)
log_c.write(" for (unsigned i = 0; i < %s; i++) { " % sz_e)
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))
i = i + 1

169
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);
@ -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

4
src/api/c++/z3++.h
View file

@ -1432,12 +1432,12 @@ namespace z3 {
t1.check_error();
return tactic(t1.ctx(), r);
}
friend tactic repeat(tactic const & t, unsigned max=UINT_MAX);
friend tactic repeat(tactic const & t, unsigned max);
friend tactic with(tactic const & t, params const & p);
friend tactic try_for(tactic const & t, unsigned ms);
};
inline tactic repeat(tactic const & t, unsigned max) {
inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
t.check_error();
return tactic(t.ctx(), r);

54
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,
@ -176,17 +135,13 @@ namespace Microsoft.Z3
IntPtr[] n_cnsts;
IntPtr[] n_theory;
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, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out 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];
}
for (int i = 0; i < num_theory; i++)
theory[i] = Expr.Create(this, n_theory[i]);
return r;
@ -198,9 +153,10 @@ namespace Microsoft.Z3
/// <remarks>For more information on interpolation please refer
/// too the function Z3_write_interpolation_problem in the C/C++ API, which is
/// well documented.</remarks>
public void WriteInterpolationProblem(string filename, Expr[] cnsts, int[] parents, string error, Expr[] theory)
public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory)
{
Contract.Requires(cnsts.Length == parents.Length);
Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory));
}
}
}

169
src/api/java/InterpolationContext.java Normal file
View file

@ -0,0 +1,169 @@
/**
*
*/
package com.microsoft.z3;
import java.util.Map;
import java.lang.String;
import com.microsoft.z3.Native.IntPtr;
import com.microsoft.z3.Native.UIntArrayPtr;
import com.microsoft.z3.enumerations.Z3_lbool;
/** <summary>
* The InterpolationContext is suitable for generation of interpolants.
* </summary>
* <remarks>For more information on interpolation please refer
* too the C/C++ API, which is well documented.</remarks>
**/
public class InterpolationContext extends Context
{
/**
* Constructor.
**/
public InterpolationContext() throws Z3Exception
{
m_ctx = Native.mkInterpolationContext(0);
initContext();
}
/**
* Constructor.
*
* <remarks><seealso cref="Context.Context(Dictionary&lt;string, string&gt;)"/></remarks>
**/
public InterpolationContext(Map<String, String> settings) throws Z3Exception
{
long cfg = Native.mkConfig();
for (Map.Entry<String, String> kv : settings.entrySet())
Native.setParamValue(cfg, kv.getKey(), kv.getValue());
m_ctx = Native.mkInterpolationContext(cfg);
Native.delConfig(cfg);
initContext();
}
/**
* Create an expression that marks a formula position for interpolation.
* @throws Z3Exception
**/
public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception
{
checkContextMatch(a);
return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
}
/**
* Computes an interpolant.
* <remarks>For more information on interpolation please refer
* too the function Z3_get_interpolant in the C/C++ API, which is
* well documented.</remarks>
* @throws Z3Exception
**/
Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception
{
checkContextMatch(pf);
checkContextMatch(pat);
checkContextMatch(p);
ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
int n = seq.size();
Expr[] res = new Expr[n];
for (int i = 0; i < n; i++)
res[i] = Expr.create(this, seq.get(i).getNativeObject());
return res;
}
/**
* Computes an interpolant.
* <remarks>For more information on interpolation please refer
* too the function Z3_compute_interpolant in the C/C++ API, which is
* well documented.</remarks>
* @throws Z3Exception
**/
Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception
{
checkContextMatch(pat);
checkContextMatch(p);
Native.LongPtr n_i = new Native.LongPtr();
Native.LongPtr n_m = new Native.LongPtr();
int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m);
interp = new ASTVector(this, n_i.value);
model = new Model(this, n_m.value);
return Z3_lbool.fromInt(r);
}
/// <summary>
/// Return a string summarizing cumulative time used for interpolation.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_interpolation_profile in the C/C++ API, which is
/// well documented.</remarks>
public String InterpolationProfile() throws Z3Exception
{
return Native.interpolationProfile(nCtx());
}
/// <summary>
/// Checks the correctness of an interpolant.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_check_interpolant in the C/C++ API, which is
/// well documented.</remarks>
public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception
{
Native.StringPtr n_err_str = new Native.StringPtr();
int r = Native.checkInterpolant(nCtx(),
cnsts.length,
Expr.arrayToNative(cnsts),
parents,
Expr.arrayToNative(interps),
n_err_str,
theory.length,
Expr.arrayToNative(theory));
error = n_err_str.value;
return r;
}
/// <summary>
/// Reads an interpolation problem from a file.
/// </summary>
/// <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, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
{
Native.IntPtr n_num = new Native.IntPtr();
Native.IntPtr n_num_theory = new Native.IntPtr();
Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
Native.StringPtr n_err_str = new Native.StringPtr();
int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
int num = n_num.value;
int num_theory = n_num_theory.value;
error = n_err_str.value;
cnsts = new Expr[num];
parents = new int[num];
theory = new Expr[num_theory];
for (int i = 0; i < num; i++)
{
cnsts[i] = Expr.create(this, n_cnsts.value[i]);
parents[i] = n_parents.value[i];
}
for (int i = 0; i < num_theory; i++)
theory[i] = Expr.create(this, n_theory.value[i]);
return r;
}
/// <summary>
/// Writes an interpolation problem to a file.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_write_interpolation_problem in the C/C++ API, which is
/// well documented.</remarks>
public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
{
Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));
}
}

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_managed_array(1, AST), _out_managed_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out_managed_array(6, 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
};

2
src/cmd_context/tactic_cmds.cpp
View file

@ -500,7 +500,7 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) {
symbol param_name = symbol(norm_param_name(c->get_symbol()).c_str());
c = n->get_child(i);
i++;
switch (descrs.get_kind(param_name)) {
switch (descrs.get_kind_in_module(param_name)) {
case CPK_INVALID:
throw cmd_exception("invalid using-params combinator, unknown parameter ", param_name, c->get_line(), c->get_pos());
case CPK_BOOL:

57
src/util/params.cpp
View file

@ -97,6 +97,35 @@ struct param_descrs::imp {
return CPK_INVALID;
}
bool split_name(symbol const& name, symbol & prefix, symbol & suffix) const {
if (name.is_numerical()) return false;
char const* str = name.bare_str();
char const* period = strchr(str,'.');
if (!period) return false;
svector<char> prefix_((unsigned)(period-str), str);
prefix_.push_back(0);
prefix = symbol(prefix_.c_ptr());
suffix = symbol(period + 1);
return true;
}
param_kind get_kind_in_module(symbol & name) const {
param_kind k = get_kind(name);
symbol prefix, suffix;
if (k == CPK_INVALID && split_name(name, prefix, suffix)) {
k = get_kind(suffix);
if (k != CPK_INVALID) {
if (symbol(get_module(suffix)) == prefix) {
name = suffix;
}
else {
k = CPK_INVALID;
}
}
}
return k;
}
char const* get_module(symbol const& name) const {
info i;
if (m_info.find(name, i))
@ -230,6 +259,10 @@ void param_descrs::erase(char const * name) {
erase(symbol(name));
}
param_kind param_descrs::get_kind_in_module(symbol & name) const {
return m_imp->get_kind_in_module(name);
}
param_kind param_descrs::get_kind(symbol const & name) const {
return m_imp->get_kind(name);
}
@ -311,35 +344,13 @@ public:
void reset(symbol const & k);
void reset(char const * k);
bool split_name(symbol const& name, symbol & prefix, symbol & suffix) {
if (name.is_numerical()) return false;
char const* str = name.bare_str();
char const* period = strchr(str,'.');
if (!period) return false;
svector<char> prefix_((unsigned)(period-str), str);
prefix_.push_back(0);
prefix = symbol(prefix_.c_ptr());
suffix = symbol(period + 1);
return true;
}
void validate(param_descrs const & p) {
svector<params::entry>::iterator it = m_entries.begin();
svector<params::entry>::iterator end = m_entries.end();
symbol suffix, prefix;
for (; it != end; ++it) {
param_kind expected = p.get_kind(it->first);
if (expected == CPK_INVALID && split_name(it->first, prefix, suffix)) {
expected = p.get_kind(suffix);
if (expected != CPK_INVALID) {
if (symbol(p.get_module(suffix)) == prefix) {
it->first = suffix;
}
else {
expected = CPK_INVALID;
}
}
}
param_kind expected = p.get_kind_in_module(it->first);
if (expected == CPK_INVALID) {
std::stringstream strm;
strm << "unknown parameter '" << it->first.str() << "'\n";

1
src/util/params.h
View file

@ -123,6 +123,7 @@ public:
void erase(symbol const & name);
param_kind get_kind(char const * name) const;
param_kind get_kind(symbol const & name) const;
param_kind get_kind_in_module(symbol & name) const;
char const * get_descr(char const * name) const;
char const * get_descr(symbol const & name) const;
char const * get_default(char const * name) const;