mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

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

Browse source
This commit is contained in:
Leonardo de Moura 2012-11-22 17:09:36 -08:00
parent 85b9d8c37a 7da026bad2
commit 8ea61dacda
85 changed files with 13373 additions and 1236 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/README
View file

@ -3,7 +3,7 @@ API documentation
To generate the API documentation for the C, .NET and Python APIs, we must execute
python mk_doc.py
python mk_api_doc.py
We must have doxygen installed in our system.

10
doc/mk_doc.py → doc/mk_api_doc.py
View file

@ -21,7 +21,7 @@ def cleanup_API(inf, outf):
_outf.write(line)
try:
mk_dir('html')
mk_dir('api/html')
cleanup_API('../src/api/z3_api.h', 'z3_api.h')
print "Removed annotations from z3_api.h."
DEVNULL = open(os.devnull, 'wb')
@ -33,15 +33,15 @@ try:
print "Generated C and .NET API documentation."
os.remove('z3_api.h')
print "Removed temporary file z3_api.h."
shutil.copy('z3.css', 'html/z3.css')
shutil.copy('z3.css', 'api/html/z3.css')
print "Copied z3.css."
shutil.copy('z3.png', 'html/z3.png')
shutil.copy('z3.png', 'api/html/z3.png')
print "Copied z3.png."
sys.path.append('../src/api/python')
pydoc.writedoc('z3')
shutil.move('z3.html', 'html/z3.html')
shutil.move('z3.html', 'api/html/z3.html')
print "Generated Python documentation."
print "Documentation was successfully generated at subdirectory './html'."
print "Documentation was successfully generated at subdirectory './api/html'."
except:
print "ERROR: failed to generate documentation"
exit(1)

2
scripts/mk_project.py
View file

@ -71,7 +71,7 @@ def init_project_def():
static=build_static_lib(),
export_files=API_files)
add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
add_java_dll('java', 'api/java', dll_name='libz3java')
add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.Microsoft.Z3")
add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
set_z3py_dir('api/python')
# Examples

106
scripts/mk_util.py
View file

@ -52,6 +52,7 @@ PATTERN_COMPONENT='pattern'
UTIL_COMPONENT='util'
API_COMPONENT='api'
DOTNET_COMPONENT='dotnet'
JAVA_COMPONENT='java'
CPP_COMPONENT='cpp'
#####################
IS_WINDOWS=False
@ -921,11 +922,12 @@ class DotNetDLLComponent(Component):
class JavaDLLComponent(Component):
def __init__(self, name, dll_name, path):
Component.__init__(self, name, path, [])
def __init__(self, name, dll_name, package_name, path, deps):
Component.__init__(self, name, path, deps)
if dll_name == None:
dll_name = name
self.dll_name = dll_name
self.dll_name = dll_name
self.package_name = package_name
def mk_makefile(self, out):
if is_java_enabled():
@ -942,6 +944,7 @@ class JavaDLLComponent(Component):
out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I%s %s/Z3Native.c\n' % (JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) -L. Z3Native$(OBJ_EXT) -lz3\n' % dllfile)
out.write('%s: %s\n\n' % (self.name, dllfile))
# TODO: Compile and package all the .class files.
def main_component(self):
return is_java_enabled()
@ -1080,8 +1083,8 @@ def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=N
c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir)
reg_component(name, c)
def add_java_dll(name, path=None, dll_name=None):
c = JavaDLLComponent(name, dll_name, path)
def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None):
c = JavaDLLComponent(name, dll_name, package_name, path, deps)
reg_component(name, c)
def add_cpp_example(name, path=None):
@ -1604,7 +1607,7 @@ def cp_z3pyc_to_build():
def mk_bindings(api_files):
if not ONLY_MAKEFILES:
mk_z3consts_py(api_files)
mk_z3consts_donet(api_files)
mk_z3consts_dotnet(api_files)
new_api_files = []
api = get_component(API_COMPONENT)
for api_file in api_files:
@ -1614,6 +1617,7 @@ def mk_bindings(api_files):
g["API_FILES"] = new_api_files
if is_java_enabled():
check_java()
mk_z3consts_java(api_files)
execfile('scripts/update_api.py', g) # HACK
cp_z3pyc_to_build()
@ -1696,7 +1700,7 @@ def mk_z3consts_py(api_files):
# Extract enumeration types from z3_api.h, and add .Net definitions
def mk_z3consts_donet(api_files):
def mk_z3consts_dotnet(api_files):
blank_pat = re.compile("^ *$")
comment_pat = re.compile("^ *//.*$")
typedef_pat = re.compile("typedef enum *")
@ -1779,6 +1783,94 @@ def mk_z3consts_donet(api_files):
if VERBOSE:
print "Generated '%s'" % ('%s/Enumerations.cs' % dotnet.src_dir)
# Extract enumeration types from z3_api.h, and add Java definitions
def mk_z3consts_java(api_files):
blank_pat = re.compile("^ *$")
comment_pat = re.compile("^ *//.*$")
typedef_pat = re.compile("typedef enum *")
typedef2_pat = re.compile("typedef enum { *")
openbrace_pat = re.compile("{ *")
closebrace_pat = re.compile("}.*;")
java = get_component(JAVA_COMPONENT)
DeprecatedEnums = [ 'Z3_search_failure' ]
gendir = java.src_dir + "/" + java.package_name.replace(".", "/") + "/Enumerations"
if not os.path.exists(gendir):
os.mkdir(gendir)
for api_file in api_files:
api_file_c = java.find_file(api_file, java.name)
api_file = '%s/%s' % (api_file_c.src_dir, api_file)
api = open(api_file, 'r')
SEARCHING = 0
FOUND_ENUM = 1
IN_ENUM = 2
mode = SEARCHING
decls = {}
idx = 0
linenum = 1
for line in api:
m1 = blank_pat.match(line)
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
mode = FOUND_ENUM
m = typedef2_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
elif mode == FOUND_ENUM:
m = openbrace_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
else:
assert False, "Invalid %s, line: %s" % (api_file, linenum)
else:
assert mode == IN_ENUM
words = re.split('[^\-a-zA-Z0-9_]+', line)
m = closebrace_pat.match(line)
if m:
name = words[1]
if name not in DeprecatedEnums:
efile = open('%s/%s.java' % (gendir, name), 'w')
efile.write('/**\n * Automatically generated file\n **/\n\n')
efile.write('package %s;\n\n' % java.package_name);
efile.write('/**\n')
efile.write(' * %s\n' % name)
efile.write(' **/\n')
efile.write('public enum %s {\n' % name)
efile.write
for k, i in decls.iteritems():
efile.write('%s (%s),\n' % (k, i))
efile.write('}\n\n')
efile.close()
mode = SEARCHING
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
idx = int(words[2], 16)
else:
idx = int(words[2])
decls[words[1]] = idx
idx = idx + 1
linenum = linenum + 1
if VERBOSE:
print "Generated '%s'" % ('%s' % gendir)
def mk_gui_str(id):
return '4D2F40D8-E5F9-473B-B548-%012d' % id

18
scripts/update_api.py
View file

@ -252,11 +252,11 @@ def param2java(p):
k = param_kind(p)
if k == OUT:
if param_type(p) == INT or param_type(p) == UINT:
return "IntPtr"
return "Integer"
elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID:
return "LongPtr"
return "Long"
elif param_type(p) == STRING:
return "StringPtr"
return "String"
else:
print "ERROR: unreachable code"
assert(False)
@ -496,14 +496,20 @@ def mk_java():
if not is_java_enabled():
return
java_dir = get_component('java').src_dir
java_nativef = '%s/Z3Native.java' % java_dir
java_wrapperf = '%s/Z3Native.c' % java_dir
try:
os.mkdir('%s/com/Microsoft/Z3/' % java_dir)
except:
pass # OK if it exists already.
java_nativef = '%s/com/Microsoft/Z3/Native.java' % java_dir
java_wrapperf = '%s/com/Microsoft/Z3/Native.c' % java_dir
java_native = open(java_nativef, 'w')
java_native.write('// Automatically generated file\n')
java_native.write('public final class Z3Native {\n')
java_native.write('package com.Microsoft.Z3;\n')
java_native.write('public final class Native {\n')
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')
if is_windows():
java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java'))
else:

18
src/api/api_datalog.cpp
View file

@ -363,6 +363,12 @@ extern "C" {
for (unsigned i = 0; i < coll.m_rules.size(); ++i) {
to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]);
}
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
for (; it != end; ++it) {
to_fixedpoint_ref(d)->ctx().assert_expr(*it);
}
return of_ast_vector(v);
}
@ -439,12 +445,12 @@ extern "C" {
ast_manager& m = mk_c(c)->m();
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
mk_c(c)->save_object(v);
datalog::rule_set const& rules = to_fixedpoint_ref(d)->ctx().get_rules();
datalog::rule_set::iterator it = rules.begin(), end = rules.end();
for (; it != end; ++it) {
expr_ref fml(m);
(*it)->to_formula(fml);
v->m_ast_vector.push_back(fml);
expr_ref_vector rules(m);
svector<symbol> names;
to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, names);
for (unsigned i = 0; i < rules.size(); ++i) {
v->m_ast_vector.push_back(rules[i].get());
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);

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

@ -28,6 +28,12 @@ Notes:
#include<z3.h>
#include<limits.h>
/**
\defgroup cppapi C++ API
*/
/*@{*/
namespace z3 {
class exception;
@ -73,10 +79,16 @@ namespace z3 {
~config() { Z3_del_config(m_cfg); }
operator Z3_config() const { return m_cfg; }
/**
\brief Add a global configuration.
\brief Set global parameter \c param with string \c value.
*/
void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
/**
\brief Set global parameter \c param with Boolean \c value.
*/
void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
/**
\brief Set global parameter \c param with integer \c value.
*/
void set(char const * param, int value) {
std::ostringstream oss;
oss << value;
@ -112,23 +124,58 @@ namespace z3 {
throw exception(Z3_get_error_msg_ex(m_ctx, e));
}
/**
\brief Update global parameter \c param with string \c value.
*/
void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
/**
\brief Update global parameter \c param with Boolean \c value.
*/
void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
/**
\brief Update global parameter \c param with Integer \c value.
*/
void set(char const * param, int value) {
std::ostringstream oss;
oss << value;
Z3_update_param_value(m_ctx, param, oss.str().c_str());
}
/**
\brief Interrupt the current procedure being executed by any object managed by this context.
This is a soft interruption: there is no guarantee the object will actualy stop.
*/
void interrupt() { Z3_interrupt(m_ctx); }
/**
\brief Create a Z3 symbol based on the given string.
*/
symbol str_symbol(char const * s);
/**
\brief Create a Z3 symbol based on the given integer.
*/
symbol int_symbol(int n);
/**
\brief Return the Boolean sort.
*/
sort bool_sort();
/**
\brief Return the integer sort.
*/
sort int_sort();
/**
\brief Return the Real sort.
*/
sort real_sort();
/**
\brief Return the Bit-vector sort of size \c sz. That is, the sort for bit-vectors of size \c sz.
*/
sort bv_sort(unsigned sz);
/**
\brief Return an array sort for arrays from \c d to \c r.
Example: Given a context \c c, <tt>c.array_sort(c.int_sort(), c.bool_sort())</tt> is an array sort from integer to Boolean.
*/
sort array_sort(sort d, sort r);
func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
@ -258,31 +305,86 @@ namespace z3 {
friend bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
};
/**
\brief A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
*/
class sort : public ast {
public:
sort(context & c):ast(c) {}
sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
sort(sort const & s):ast(s) {}
operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
/**
\brief Return true if this sort and \c s are equal.
*/
sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
/**
\brief Return the internal sort kind.
*/
Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
/**
\brief Return true if this sort is the Boolean sort.
*/
bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
/**
\brief Return true if this sort is the Integer sort.
*/
bool is_int() const { return sort_kind() == Z3_INT_SORT; }
/**
\brief Return true if this sort is the Real sort.
*/
bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
/**
\brief Return true if this sort is the Integer or Real sort.
*/
bool is_arith() const { return is_int() || is_real(); }
/**
\brief Return true if this sort is a Bit-vector sort.
*/
bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
/**
\brief Return true if this sort is a Array sort.
*/
bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
/**
\brief Return true if this sort is a Datatype sort.
*/
bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
/**
\brief Return true if this sort is a Relation sort.
*/
bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
/**
\brief Return true if this sort is a Finite domain sort.
*/
bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
/**
\brief Return the size of this Bit-vector sort.
\pre is_bv()
*/
unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
/**
\brief Return the domain of this Array sort.
\pre is_array()
*/
sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
/**
\brief Return the range of this Array sort.
\pre is_array()
*/
sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
};
/**
\brief Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3.
The basic building block in Z3 is the function application.
*/
class func_decl : public ast {
public:
func_decl(context & c):ast(c) {}
@ -310,6 +412,10 @@ namespace z3 {
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
};
/**
\brief A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean.
Every expression has a sort.
*/
class expr : public ast {
public:
expr(context & c):ast(c) {}
@ -317,33 +423,116 @@ namespace z3 {
expr(expr const & n):ast(n) {}
expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
/**
\brief Return the sort of this expression.
*/
sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
/**
\brief Return true if this is a Boolean expression.
*/
bool is_bool() const { return get_sort().is_bool(); }
/**
\brief Return true if this is an integer expression.
*/
bool is_int() const { return get_sort().is_int(); }
/**
\brief Return true if this is a real expression.
*/
bool is_real() const { return get_sort().is_real(); }
/**
\brief Return true if this is an integer or real expression.
*/
bool is_arith() const { return get_sort().is_arith(); }
/**
\brief Return true if this is a Bit-vector expression.
*/
bool is_bv() const { return get_sort().is_bv(); }
/**
\brief Return true if this is a Array expression.
*/
bool is_array() const { return get_sort().is_array(); }
/**
\brief Return true if this is a Datatype expression.
*/
bool is_datatype() const { return get_sort().is_datatype(); }
/**
\brief Return true if this is a Relation expression.
*/
bool is_relation() const { return get_sort().is_relation(); }
/**
\brief Return true if this is a Finite-domain expression.
\remark Finite-domain is special kind of interpreted sort:
is_bool(), is_bv() and is_finite_domain() are mutually
exclusive.
*/
bool is_finite_domain() const { return get_sort().is_finite_domain(); }
/**
\brief Return true if this expression is a numeral.
*/
bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
/**
\brief Return true if this expression is an application.
*/
bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
/**
\brief Return true if this expression is a constant (i.e., an application with 0 arguments).
*/
bool is_const() const { return is_app() && num_args() == 0; }
/**
\brief Return true if this expression is a quantifier.
*/
bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
/**
\brief Return true if this expression is a variable.
*/
bool is_var() const { return kind() == Z3_VAR_AST; }
/**
\brief Return true if this expression is well sorted (aka type correct).
*/
bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
/**
\brief Return the declaration associated with this application.
This method assumes the expression is an application.
\pre is_app()
*/
func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
/**
\brief Return the number of arguments in this application.
This method assumes the expression is an application.
\pre is_app()
*/
unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
/**
\brief Return the i-th argument of this application.
This method assumes the expression is an application.
\pre is_app()
\pre i < num_args()
*/
expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
/**
\brief Return the 'body' of this quantifier.
\pre is_quantifier()
*/
expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
/**
\brief Return an expression representing <tt>not(a)</tt>.
\pre a.is_bool()
*/
friend expr operator!(expr const & a) {
assert(a.is_bool());
Z3_ast r = Z3_mk_not(a.ctx(), a);
@ -351,6 +540,12 @@ namespace z3 {
return expr(a.ctx(), r);
}
/**
\brief Return an expression representing <tt>a and b</tt>.
\pre a.is_bool()
\pre b.is_bool()
*/
friend expr operator&&(expr const & a, expr const & b) {
check_context(a, b);
assert(a.is_bool() && b.is_bool());
@ -359,9 +554,28 @@ namespace z3 {
a.check_error();
return expr(a.ctx(), r);
}
/**
\brief Return an expression representing <tt>a and b</tt>.
The C++ Boolean value \c b is automatically converted into a Z3 Boolean constant.
\pre a.is_bool()
*/
friend expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
/**
\brief Return an expression representing <tt>a and b</tt>.
The C++ Boolean value \c a is automatically converted into a Z3 Boolean constant.
\pre b.is_bool()
*/
friend expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
/**
\brief Return an expression representing <tt>a or b</tt>.
\pre a.is_bool()
\pre b.is_bool()
*/
friend expr operator||(expr const & a, expr const & b) {
check_context(a, b);
assert(a.is_bool() && b.is_bool());
@ -370,7 +584,19 @@ namespace z3 {
a.check_error();
return expr(a.ctx(), r);
}
/**
\brief Return an expression representing <tt>a or b</tt>.
The C++ Boolean value \c b is automatically converted into a Z3 Boolean constant.
\pre a.is_bool()
*/
friend expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
/**
\brief Return an expression representing <tt>a or b</tt>.
The C++ Boolean value \c a is automatically converted into a Z3 Boolean constant.
\pre b.is_bool()
*/
friend expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
friend expr implies(expr const & a, expr const & b) {
@ -598,7 +824,13 @@ namespace z3 {
friend expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
/**
\brief Return a simplified version of this expression.
*/
expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
/**
\brief Return a simplified version of this expression. The parameter \c p is a set of parameters for the Z3 simplifier.
*/
expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
};
@ -1391,5 +1623,7 @@ template class z3::ast_vector_tpl<z3::expr>;
template class z3::ast_vector_tpl<z3::sort>;
template class z3::ast_vector_tpl<z3::func_decl>;
/*@}*/
#endif

2
src/api/dotnet/ASTVector.cs
View file

@ -51,7 +51,7 @@ namespace Microsoft.Z3
}
set
{
Contract.Requires(value!= null);
Contract.Requires(value != null);
Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
}

41
src/api/dotnet/Constructor.cs
View file

@ -33,7 +33,11 @@ namespace Microsoft.Z3
/// </summary>
public uint NumFields
{
get { init(); return n; }
get
{
init();
return n;
}
}
/// <summary>
@ -41,9 +45,12 @@ namespace Microsoft.Z3
/// </summary>
public FuncDecl ConstructorDecl
{
get {
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
init(); return m_constructorDecl; }
init();
return m_constructorDecl;
}
}
/// <summary>
@ -51,9 +58,12 @@ namespace Microsoft.Z3
/// </summary>
public FuncDecl TesterDecl
{
get {
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
init(); return m_testerDecl; }
init();
return m_testerDecl;
}
}
/// <summary>
@ -61,10 +71,13 @@ namespace Microsoft.Z3
/// </summary>
public FuncDecl[] AccessorDecls
{
get {
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
init(); return m_accessorDecls; }
}
init();
return m_accessorDecls;
}
}
/// <summary>
/// Destructor.
@ -79,10 +92,10 @@ namespace Microsoft.Z3
[ContractInvariantMethod]
private void ObjectInvariant()
{
Contract.Invariant(m_testerDecl == null || m_constructorDecl != null);
Contract.Invariant(m_testerDecl == null || m_constructorDecl != null);
Contract.Invariant(m_testerDecl == null || m_accessorDecls != null);
}
#endregion
#region Internal
@ -105,7 +118,7 @@ namespace Microsoft.Z3
throw new Z3Exception("Number of field names does not match number of sorts");
if (sortRefs != null && sortRefs.Length != n)
throw new Z3Exception("Number of field names does not match number of sort refs");
if (sortRefs == null) sortRefs = new uint[n];
NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
@ -116,7 +129,7 @@ namespace Microsoft.Z3
}
private void init()
private void init()
{
Contract.Ensures(m_constructorDecl != null);
Contract.Ensures(m_testerDecl != null);
@ -146,7 +159,7 @@ namespace Microsoft.Z3
/// Destructor.
/// </summary>
~ConstructorList()
{
{
Native.Z3_del_constructor_list(Context.nCtx, NativeObject);
}
@ -164,7 +177,7 @@ namespace Microsoft.Z3
Contract.Requires(constructors != null);
NativeObject = Native.Z3_mk_constructor_list(Context.nCtx, (uint)constructors.Length, Constructor.ArrayToNative(constructors));
}
}
#endregion
}
}

36
src/api/dotnet/Expr.cs
View file

@ -48,9 +48,11 @@ namespace Microsoft.Z3
/// </summary>
public FuncDecl FuncDecl
{
get {
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject)); }
return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject));
}
}
/// <summary>
@ -74,7 +76,7 @@ namespace Microsoft.Z3
/// The arguments of the expression.
/// </summary>
public Expr[] Args
{
{
get
{
Contract.Ensures(Contract.Result<Expr[]>() != null);
@ -176,7 +178,7 @@ namespace Microsoft.Z3
public override string ToString()
{
return base.ToString();
}
}
/// <summary>
/// Indicates whether the term is a numeral
@ -200,9 +202,11 @@ namespace Microsoft.Z3
/// </summary>
public Sort Sort
{
get {
get
{
Contract.Ensures(Contract.Result<Sort>() != null);
return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject)); }
return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
}
}
#region Constants
@ -243,7 +247,7 @@ namespace Microsoft.Z3
{
get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; }
}
#endregion
#endregion
#region Term Kind Tests
@ -1471,12 +1475,16 @@ namespace Microsoft.Z3
#endregion
#region Internal
/// <summary> Constructor for Expr </summary>
/// <summary>
/// Constructor for Expr
/// </summary>
internal protected Expr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
/// <summary> Constructor for Expr </summary>
/// <summary>
/// Constructor for Expr
/// </summary>
internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#if DEBUG
#if DEBUG
[Pure]
internal override void CheckNativeObject(IntPtr obj)
{
@ -1486,7 +1494,7 @@ namespace Microsoft.Z3
throw new Z3Exception("Underlying object is not a term");
base.CheckNativeObject(obj);
}
#endif
#endif
[Pure]
internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
@ -1495,11 +1503,11 @@ namespace Microsoft.Z3
Contract.Requires(f != null);
Contract.Ensures(Contract.Result<Expr>() != null);
IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
AST.ArrayLength(arguments),
IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
AST.ArrayLength(arguments),
AST.ArrayToNative(arguments));
return Create(ctx, obj);
}
}
[Pure]
new internal static Expr Create(Context ctx, IntPtr obj)

6
src/api/dotnet/Fixedpoint.cs
View file

@ -264,7 +264,8 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve set of rules added to fixedpoint context.
/// </summary>
public BoolExpr[] Rules {
public BoolExpr[] Rules
{
get
{
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
@ -281,7 +282,8 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve set of assertions added to fixedpoint context.
/// </summary>
public BoolExpr[] Assertions {
public BoolExpr[] Assertions
{
get
{
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);

35
src/api/dotnet/FuncDecl.cs
View file

@ -124,9 +124,11 @@ namespace Microsoft.Z3
/// </summary>
public Sort Range
{
get {
get
{
Contract.Ensures(Contract.Result<Sort>() != null);
return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject)); }
return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
}
}
/// <summary>
@ -142,9 +144,11 @@ namespace Microsoft.Z3
/// </summary>
public Symbol Name
{
get {
get
{
Contract.Ensures(Contract.Result<Symbol>() != null);
return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject)); }
return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject));
}
}
/// <summary>
@ -280,9 +284,10 @@ namespace Microsoft.Z3
}
#region Internal
internal FuncDecl(Context ctx, IntPtr obj) : base(ctx, obj)
{
Contract.Requires(ctx != null);
internal FuncDecl(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
@ -293,7 +298,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
Contract.Requires(name != null);
Contract.Requires(range != null);
}
}
internal FuncDecl(Context ctx, string prefix, Sort[] domain, Sort range)
: base(ctx, Native.Z3_mk_fresh_func_decl(ctx.nCtx, prefix,
@ -304,14 +309,14 @@ namespace Microsoft.Z3
Contract.Requires(range != null);
}
#if DEBUG
#if DEBUG
internal override void CheckNativeObject(IntPtr obj)
{
if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_FUNC_DECL_AST)
throw new Z3Exception("Underlying object is not a function declaration");
base.CheckNativeObject(obj);
}
#endif
#endif
#endregion
/// <summary>
@ -319,12 +324,14 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="args"></param>
/// <returns></returns>
public Expr this[params Expr[] args] {
get {
public Expr this[params Expr[] args]
{
get
{
Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
return Apply(args);
}
return Apply(args);
}
}
/// <summary>

128
src/api/dotnet/Version.cs
View file

@ -22,77 +22,77 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Version information.
/// </summary>
/// <remarks>Note that this class is static.</remarks>
/// <summary>
/// Version information.
/// </summary>
/// <remarks>Note that this class is static.</remarks>
[ContractVerification(true)]
public static class Version
{
static Version() { }
/// <summary>
/// The major version
/// </summary>
public static uint Major
{
get
{
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return major;
}
}
static Version() { }
/// <summary>
/// The minor version
/// </summary>
public static uint Minor
{
get
{
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return minor;
}
}
/// <summary>
/// The major version
/// </summary>
public static uint Major
{
get
{
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return major;
}
}
/// <summary>
/// The build version
/// </summary>
public static uint Build
{
get
{
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return build;
}
}
/// <summary>
/// The minor version
/// </summary>
public static uint Minor
{
get
{
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return minor;
}
}
/// <summary>
/// The revision
/// </summary>
public static uint Revision
{
get
{
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return revision;
}
}
/// <summary>
/// The build version
/// </summary>
public static uint Build
{
get
{
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return build;
}
}
/// <summary>
/// A string representation of the version information.
/// </summary>
new public static string ToString()
{
Contract.Ensures(Contract.Result<string>() != null);
/// <summary>
/// The revision
/// </summary>
public static uint Revision
{
get
{
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return revision;
}
}
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return major.ToString() + "." + minor.ToString() + "." + build.ToString() + "." + revision.ToString();
/// <summary>
/// A string representation of the version information.
/// </summary>
new public static string ToString()
{
Contract.Ensures(Contract.Result<string>() != null);
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
return major.ToString() + "." + minor.ToString() + "." + build.ToString() + "." + revision.ToString();
}
}
}
}

209
src/api/java/com/Microsoft/Z3/AST.java Normal file
View file

@ -0,0 +1,209 @@
/**
* This file was automatically generated from AST.cs
**/
package com.Microsoft.Z3;
/* using System; */
/* using System.Collections; */
/* using System.Collections.Generic; */
/**
* The abstract syntax tree (AST) class.
**/
public class AST extends Z3Object
{
/**
* Comparison operator.
* <param name="a">An AST</param>
* <param name="b">An AST</param>
* @return True if <paramref name="a"/> and <paramref name="b"/> are from the same context
* and represent the same sort; false otherwise.
**/
/* Overloaded operators are not translated. */
/**
* Comparison operator.
* <param name="a">An AST</param>
* <param name="b">An AST</param>
* @return True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
* or represent different sorts; false otherwise.
**/
/* Overloaded operators are not translated. */
/**
* Object comparison.
**/
public boolean Equals(object o)
{
AST casted = (AST) o;
if (casted == null) return false;
return this == casted;
}
/**
* Object Comparison.
* <param name="other">Another AST</param>
* @return Negative if the object should be sorted before <paramref name="other"/>, positive if after else zero.
**/
public int CompareTo(object other)
{
if (other == null) return 1;
AST oAST = (AST) other;
if (oAST == null)
return 1;
else
{
if (Id < oAST.Id)
return -1;
else if (Id > oAST.Id)
return +1;
else
return 0;
}
}
/**
* The AST's hash code.
* @return A hash code
**/
public int GetHashCode()
{
return (int)Native.getAstHash(Context.nCtx, NativeObject);
}
/**
* A unique identifier for the AST (unique among all ASTs).
**/
public long Id() { return Native.getAstId(Context.nCtx, NativeObject); }
/**
* Translates (copies) the AST to the Context <paramref name="ctx"/>.
* <param name="ctx">A context</param>
* @return A copy of the AST which is associated with <paramref name="ctx"/>
**/
public AST Translate(Context ctx)
{
if (ReferenceEquals(Context, ctx))
return this;
else
return new AST(ctx, Native.translate(Context.nCtx, NativeObject, ctx.nCtx));
}
/**
* The kind of the AST.
**/
public Z3_ast_kind ASTKind() { return (Z3_ast_kind)Native.getAstKind(Context.nCtx, NativeObject); }
/**
* Indicates whether the AST is an Expr
**/
public boolean IsExpr()
{
switch (ASTKind)
{
case Z3_ast_kind.Z3_APP_AST:
case Z3_ast_kind.Z3_NUMERAL_AST:
case Z3_ast_kind.Z3_QUANTIFIER_AST:
case Z3_ast_kind.Z3_VAR_AST: return true;
default: return false;
}
}
/**
* Indicates whether the AST is a BoundVariable
**/
public boolean IsVar() { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; }
/**
* Indicates whether the AST is a Quantifier
**/
public boolean IsQuantifier() { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; }
/**
* Indicates whether the AST is a Sort
**/
public boolean IsSort() { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; }
/**
* Indicates whether the AST is a FunctionDeclaration
**/
public boolean IsFuncDecl() { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; }
/**
* A string representation of the AST.
**/
public String toString()
{
return Native.asttoString(Context.nCtx, NativeObject);
}
/**
* A string representation of the AST in s-expression notation.
**/
public String SExpr()
{
return Native.asttoString(Context.nCtx, NativeObject);
}
AST(Context ctx) { super(ctx); }
AST(Context ctx, IntPtr obj) { super(ctx, obj); }
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.incRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.decRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
// Console.WriteLine("AST IncRef()");
if (Context == null)
throw new Z3Exception("inc() called on null context");
if (o == IntPtr.Zero)
throw new Z3Exception("inc() called on null AST");
Context.AST_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
// Console.WriteLine("AST DecRef()");
if (Context == null)
throw new Z3Exception("dec() called on null context");
if (o == IntPtr.Zero)
throw new Z3Exception("dec() called on null AST");
Context.AST_DRQ.Add(o);
super.DecRef(o);
}
static AST Create(Context ctx, IntPtr obj)
{
switch ((Z3_ast_kind)Native.getAstKind(ctx.nCtx, obj))
{
case Z3_ast_kind.Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj);
case Z3_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj);
case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj);
case Z3_ast_kind.Z3_APP_AST:
case Z3_ast_kind.Z3_NUMERAL_AST:
case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj);
default:
throw new Z3Exception("Unknown AST kind");
}
}
}

127
src/api/java/com/Microsoft/Z3/ASTMap.java Normal file
View file

@ -0,0 +1,127 @@
/**
* This file was automatically generated from ASTMap.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Map from AST to AST
**/
class ASTMap extends Z3Object
{
/**
* Checks whether the map contains the key <paramref name="k"/>.
* <param name="k">An AST</param>
* @return True if <paramref name="k"/> is a key in the map, false otherwise.
**/
public boolean Contains(AST k)
{
return Native.astMapContains(Context.nCtx, NativeObject, k.NativeObject) != 0;
}
/**
* Finds the value associated with the key <paramref name="k"/>.
* <remarks>
* This function signs an error when <paramref name="k"/> is not a key in the map.
* </remarks>
* <param name="k">An AST</param>
**/
public AST Find(AST k)
{
return new AST(Context, Native.astMapFind(Context.nCtx, NativeObject, k.NativeObject));
}
/**
* Stores or replaces a new key/value pair in the map.
* <param name="k">The key AST</param>
* <param name="v">The value AST</param>
**/
public void Insert(AST k, AST v)
{
Native.astMapInsert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject);
}
/**
* Erases the key <paramref name="k"/> from the map.
* <param name="k">An AST</param>
**/
public void Erase(AST k)
{
Native.astMapErase(Context.nCtx, NativeObject, k.NativeObject);
}
/**
* Removes all keys from the map.
**/
public void Reset()
{
Native.astMapReset(Context.nCtx, NativeObject);
}
/**
* The size of the map
**/
public long Size() { return Native.astMapSize(Context.nCtx, NativeObject); }
/**
* The keys stored in the map.
**/
public ASTVector Keys()
{
return new ASTVector(Context, Native.astMapKeys(Context.nCtx, NativeObject));
}
/**
* Retrieves a string representation of the map.
**/
public String toString()
{
return Native.astMaptoString(Context.nCtx, NativeObject);
}
ASTMap(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
ASTMap(Context ctx)
{ super(ctx, Native.mkAstMap(ctx.nCtx));
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.astMapIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.astMapDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.ASTMap_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.ASTMap_DRQ.Add(o);
super.DecRef(o);
}
}

107
src/api/java/com/Microsoft/Z3/ASTVector.java Normal file
View file

@ -0,0 +1,107 @@
/**
* This file was automatically generated from ASTVector.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Vectors of ASTs.
**/
class ASTVector extends Z3Object
{
/**
* The size of the vector
**/
public long Size() { return Native.astVectorSize(Context.nCtx, NativeObject); }
/**
* Retrieves the i-th object in the vector.
* <remarks>May throw an IndexOutOfBoundsException when <paramref name="i"/> is out of range.</remarks>
* <param name="i">Index</param>
* @return An AST
**/
public AST get(long i)
{
return new AST(Context, Native.astVectorGet(Context.nCtx, NativeObject, i));
}
public void set(long i, AST value)
{
Native.astVectorSet(Context.nCtx, NativeObject, i, value.NativeObject);
}
/**
* Resize the vector to <paramref name="newSize"/>.
* <param name="newSize">The new size of the vector.</param>
**/
public void Resize(long newSize)
{
Native.astVectorResize(Context.nCtx, NativeObject, newSize);
}
/**
* Add the AST <paramref name="a"/> to the back of the vector. The size
* is increased by 1.
* <param name="a">An AST</param>
**/
public void Push(AST a)
{
Native.astVectorPush(Context.nCtx, NativeObject, a.NativeObject);
}
/**
* Translates all ASTs in the vector to <paramref name="ctx"/>.
* <param name="ctx">A context</param>
* @return A new ASTVector
**/
public ASTVector Translate(Context ctx)
{
return new ASTVector(Context, Native.astVectorTranslate(Context.nCtx, NativeObject, ctx.nCtx));
}
/**
* Retrieves a string representation of the vector.
**/
public String toString()
{
return Native.astVectortoString(Context.nCtx, NativeObject);
}
ASTVector(Context ctx, IntPtr obj) { super(ctx, obj); }
ASTVector(Context ctx) { super(ctx, Native.mkAstVector(ctx.nCtx)); }
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.astVectorIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.astVectorDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.ASTVector_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.ASTVector_DRQ.Add(o);
super.DecRef(o);
}
}

84
src/api/java/com/Microsoft/Z3/ApplyResult.java Normal file
View file

@ -0,0 +1,84 @@
/**
* This file was automatically generated from ApplyResult.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* ApplyResult objects represent the result of an application of a
* tactic to a goal. It contains the subgoals that were produced.
**/
public class ApplyResult extends Z3Object
{
/**
* The number of Subgoals.
**/
public long NumSubgoals() { return Native.applyResultGetNumSubgoals(Context.nCtx, NativeObject); }
/**
* Retrieves the subgoals from the ApplyResult.
**/
public Goal[] Subgoals()
{
long n = NumSubgoals;
Goal[] res = new Goal[n];
for (long i = 0; i < n; i++)
res[i] = new Goal(Context, Native.applyResultGetSubgoal(Context.nCtx, NativeObject, i));
return res;
}
/**
* Convert a model for the subgoal <paramref name="i"/> into a model for the original
* goal <code>g</code>, that the ApplyResult was obtained from.
* @return A model for <code>g</code>
**/
public Model ConvertModel(long i, Model m)
{
return new Model(Context, Native.applyResultConvertModel(Context.nCtx, NativeObject, i, m.NativeObject));
}
/**
* A string representation of the ApplyResult.
**/
public String toString()
{
return Native.applyResulttoString(Context.nCtx, NativeObject);
}
ApplyResult(Context ctx, IntPtr obj) { super(ctx, obj);
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.applyResultIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.applyResultDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.ApplyResult_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.ApplyResult_DRQ.Add(o);
super.DecRef(o);
}
}

143
src/api/java/com/Microsoft/Z3/Constructor.java Normal file
View file

@ -0,0 +1,143 @@
/**
* This file was automatically generated from Constructor.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Constructors are used for datatype sorts.
**/
public class Constructor extends Z3Object
{
/**
* The number of fields of the constructor.
**/
public long NumFields()
{
init();
return n;
}
/**
* The function declaration of the constructor.
**/
public FuncDecl ConstructorDecl()
{
init();
return m_constructorDecl;
}
/**
* The function declaration of the tester.
**/
public FuncDecl TesterDecl()
{
init();
return m_testerDecl;
}
/**
* The function declarations of the accessors
**/
public FuncDecl[] AccessorDecls()
{
init();
return m_accessorDecls;
}
/**
* Destructor.
**/
protected void finalize()
{
Native.delConstructor(Context.nCtx, NativeObject);
}
private void ObjectInvariant()
{
}
private long n = 0;
private FuncDecl m_testerDecl = null;
private FuncDecl m_constructorDecl = null;
private FuncDecl[] m_accessorDecls = null;
Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
Sort[] sorts, long[] sortRefs)
{ super(ctx);
n = AST.ArrayLength(fieldNames);
if (n != AST.ArrayLength(sorts))
throw new Z3Exception("Number of field names does not match number of sorts");
if (sortRefs != null && sortRefs.Length != n)
throw new Z3Exception("Number of field names does not match number of sort refs");
if (sortRefs == null) sortRefs = new long[n];
NativeObject = Native.mkConstructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
n,
Symbol.ArrayToNative(fieldNames),
Sort.ArrayToNative(sorts),
sortRefs);
}
private void init()
{
if (m_testerDecl != null) return;
IntPtr constructor = IntPtr.Zero;
IntPtr tester = IntPtr.Zero;
IntPtr[] accessors = new IntPtr[n];
Native.queryConstructor(Context.nCtx, NativeObject, n, constructor, tester, accessors);
m_constructorDecl = new FuncDecl(Context, constructor);
m_testerDecl = new FuncDecl(Context, tester);
m_accessorDecls = new FuncDecl[n];
for (long i = 0; i < n; i++)
m_accessorDecls[i] = new FuncDecl(Context, accessors[i]);
}
}
/**
* Lists of constructors
**/
public class ConstructorList extends Z3Object
{
/**
* Destructor.
**/
protected void finalize()
{
Native.delConstructorList(Context.nCtx, NativeObject);
}
ConstructorList(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
ConstructorList(Context ctx, Constructor[] constructors)
{ super(ctx);
NativeObject = Native.mkConstructorList(Context.nCtx, (long)constructors.Length, Constructor.ArrayToNative(constructors));
}
}

3543
src/api/java/com/Microsoft/Z3/Context.java Normal file
View file

File diff suppressed because it is too large Load diff

70
src/api/java/com/Microsoft/Z3/DecRefQUeue.java Normal file
View file

@ -0,0 +1,70 @@
/**
* This file was automatically generated from DecRefQUeue.cs
**/
package com.Microsoft.Z3;
/* using System; */
/* using System.Collections; */
/* using System.Collections.Generic; */
/* using System.Threading; */
abstract class DecRefQueue
{
private void ObjectInvariant()
{
}
protected Object m_lock = new Object();
protected List<IntPtr> m_queue = new List<IntPtr>();
final long m_move_limit = 1024;
public abstract void IncRef(Context ctx, IntPtr obj);
public abstract void DecRef(Context ctx, IntPtr obj);
public void IncAndClear(Context ctx, IntPtr o)
{
IncRef(ctx, o);
if (m_queue.Count >= m_move_limit) Clear(ctx);
}
public void Add(IntPtr o)
{
if (o == IntPtr.Zero) return;
synchronized (m_lock)
{
m_queue.Add(o);
}
}
public void Clear(Context ctx)
{
synchronized (m_lock)
{
for (IntPtr.Iterator o = m_queue.iterator(); o.hasNext(); )
DecRef(ctx, o);
m_queue.Clear();
}
}
}
abstract class DecRefQueueContracts extends DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
}
public void DecRef(Context ctx, IntPtr obj)
{
}
}

19
src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java Normal file
View file

@ -0,0 +1,19 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_ast_kind
**/
public enum Z3_ast_kind {
Z3_VAR_AST (2),
Z3_SORT_AST (4),
Z3_QUANTIFIER_AST (3),
Z3_UNKNOWN_AST (1000),
Z3_FUNC_DECL_AST (5),
Z3_NUMERAL_AST (0),
Z3_APP_AST (1),
}

16
src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java Normal file
View file

@ -0,0 +1,16 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_ast_print_mode
**/
public enum Z3_ast_print_mode {
Z3_PRINT_SMTLIB2_COMPLIANT (3),
Z3_PRINT_SMTLIB_COMPLIANT (2),
Z3_PRINT_SMTLIB_FULL (0),
Z3_PRINT_LOW_LEVEL (1),
}

164
src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java Normal file
View file

@ -0,0 +1,164 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_decl_kind
**/
public enum Z3_decl_kind {
Z3_OP_LABEL (1792),
Z3_OP_PR_REWRITE (1294),
Z3_OP_UNINTERPRETED (2051),
Z3_OP_SUB (519),
Z3_OP_ZERO_EXT (1058),
Z3_OP_ADD (518),
Z3_OP_IS_INT (528),
Z3_OP_BREDOR (1061),
Z3_OP_BNOT (1051),
Z3_OP_BNOR (1054),
Z3_OP_PR_CNF_STAR (1315),
Z3_OP_RA_JOIN (1539),
Z3_OP_LE (514),
Z3_OP_SET_UNION (773),
Z3_OP_PR_UNDEF (1280),
Z3_OP_BREDAND (1062),
Z3_OP_LT (516),
Z3_OP_RA_UNION (1540),
Z3_OP_BADD (1028),
Z3_OP_BUREM0 (1039),
Z3_OP_OEQ (267),
Z3_OP_PR_MODUS_PONENS (1284),
Z3_OP_RA_CLONE (1548),
Z3_OP_REPEAT (1060),
Z3_OP_RA_NEGATION_FILTER (1544),
Z3_OP_BSMOD0 (1040),
Z3_OP_BLSHR (1065),
Z3_OP_BASHR (1066),
Z3_OP_PR_UNIT_RESOLUTION (1304),
Z3_OP_ROTATE_RIGHT (1068),
Z3_OP_ARRAY_DEFAULT (772),
Z3_OP_PR_PULL_QUANT (1296),
Z3_OP_PR_APPLY_DEF (1310),
Z3_OP_PR_REWRITE_STAR (1295),
Z3_OP_IDIV (523),
Z3_OP_PR_GOAL (1283),
Z3_OP_PR_IFF_TRUE (1305),
Z3_OP_LABEL_LIT (1793),
Z3_OP_BOR (1050),
Z3_OP_PR_SYMMETRY (1286),
Z3_OP_TRUE (256),
Z3_OP_SET_COMPLEMENT (776),
Z3_OP_CONCAT (1056),
Z3_OP_PR_NOT_OR_ELIM (1293),
Z3_OP_IFF (263),
Z3_OP_BSHL (1064),
Z3_OP_PR_TRANSITIVITY (1287),
Z3_OP_SGT (1048),
Z3_OP_RA_WIDEN (1541),
Z3_OP_PR_DEF_INTRO (1309),
Z3_OP_NOT (265),
Z3_OP_PR_QUANT_INTRO (1290),
Z3_OP_UGT (1047),
Z3_OP_DT_RECOGNISER (2049),
Z3_OP_SET_INTERSECT (774),
Z3_OP_BSREM (1033),
Z3_OP_RA_STORE (1536),
Z3_OP_SLT (1046),
Z3_OP_ROTATE_LEFT (1067),
Z3_OP_PR_NNF_NEG (1313),
Z3_OP_PR_REFLEXIVITY (1285),
Z3_OP_ULEQ (1041),
Z3_OP_BIT1 (1025),
Z3_OP_BIT0 (1026),
Z3_OP_EQ (258),
Z3_OP_BMUL (1030),
Z3_OP_ARRAY_MAP (771),
Z3_OP_STORE (768),
Z3_OP_PR_HYPOTHESIS (1302),
Z3_OP_RA_RENAME (1545),
Z3_OP_AND (261),
Z3_OP_TO_REAL (526),
Z3_OP_PR_NNF_POS (1312),
Z3_OP_PR_AND_ELIM (1292),
Z3_OP_MOD (525),
Z3_OP_BUDIV0 (1037),
Z3_OP_PR_TRUE (1281),
Z3_OP_BNAND (1053),
Z3_OP_PR_ELIM_UNUSED_VARS (1299),
Z3_OP_RA_FILTER (1543),
Z3_OP_FD_LT (1549),
Z3_OP_RA_EMPTY (1537),
Z3_OP_DIV (522),
Z3_OP_ANUM (512),
Z3_OP_MUL (521),
Z3_OP_UGEQ (1043),
Z3_OP_BSREM0 (1038),
Z3_OP_PR_TH_LEMMA (1318),
Z3_OP_BXOR (1052),
Z3_OP_DISTINCT (259),
Z3_OP_PR_IFF_FALSE (1306),
Z3_OP_BV2INT (1072),
Z3_OP_EXT_ROTATE_LEFT (1069),
Z3_OP_PR_PULL_QUANT_STAR (1297),
Z3_OP_BSUB (1029),
Z3_OP_PR_ASSERTED (1282),
Z3_OP_BXNOR (1055),
Z3_OP_EXTRACT (1059),
Z3_OP_PR_DER (1300),
Z3_OP_DT_CONSTRUCTOR (2048),
Z3_OP_GT (517),
Z3_OP_BUREM (1034),
Z3_OP_IMPLIES (266),
Z3_OP_SLEQ (1042),
Z3_OP_GE (515),
Z3_OP_BAND (1049),
Z3_OP_ITE (260),
Z3_OP_AS_ARRAY (778),
Z3_OP_RA_SELECT (1547),
Z3_OP_CONST_ARRAY (770),
Z3_OP_BSDIV (1031),
Z3_OP_OR (262),
Z3_OP_PR_HYPER_RESOLVE (1319),
Z3_OP_AGNUM (513),
Z3_OP_PR_PUSH_QUANT (1298),
Z3_OP_BSMOD (1035),
Z3_OP_PR_IFF_OEQ (1311),
Z3_OP_PR_LEMMA (1303),
Z3_OP_SET_SUBSET (777),
Z3_OP_SELECT (769),
Z3_OP_RA_PROJECT (1542),
Z3_OP_BNEG (1027),
Z3_OP_UMINUS (520),
Z3_OP_REM (524),
Z3_OP_TO_INT (527),
Z3_OP_PR_QUANT_INST (1301),
Z3_OP_SGEQ (1044),
Z3_OP_POWER (529),
Z3_OP_XOR3 (1074),
Z3_OP_RA_IS_EMPTY (1538),
Z3_OP_CARRY (1073),
Z3_OP_DT_ACCESSOR (2050),
Z3_OP_PR_TRANSITIVITY_STAR (1288),
Z3_OP_PR_NNF_STAR (1314),
Z3_OP_PR_COMMUTATIVITY (1307),
Z3_OP_ULT (1045),
Z3_OP_BSDIV0 (1036),
Z3_OP_SET_DIFFERENCE (775),
Z3_OP_INT2BV (1071),
Z3_OP_XOR (264),
Z3_OP_PR_MODUS_PONENS_OEQ (1317),
Z3_OP_BNUM (1024),
Z3_OP_BUDIV (1032),
Z3_OP_PR_MONOTONICITY (1289),
Z3_OP_PR_DEF_AXIOM (1308),
Z3_OP_FALSE (257),
Z3_OP_EXT_ROTATE_RIGHT (1070),
Z3_OP_PR_DISTRIBUTIVITY (1291),
Z3_OP_SIGN_EXT (1057),
Z3_OP_PR_SKOLEMIZE (1316),
Z3_OP_BCOMP (1063),
Z3_OP_RA_COMPLEMENT (1546),
}

25
src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java Normal file
View file

@ -0,0 +1,25 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_error_code
**/
public enum Z3_error_code {
Z3_INVALID_PATTERN (6),
Z3_MEMOUT_FAIL (7),
Z3_NO_PARSER (5),
Z3_OK (0),
Z3_INVALID_ARG (3),
Z3_EXCEPTION (12),
Z3_IOB (2),
Z3_INTERNAL_FATAL (9),
Z3_INVALID_USAGE (10),
Z3_FILE_ACCESS_ERROR (8),
Z3_SORT_ERROR (1),
Z3_PARSER_ERROR (4),
Z3_DEC_REF_ERROR (11),
}

16
src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java Normal file
View file

@ -0,0 +1,16 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_goal_prec
**/
public enum Z3_goal_prec {
Z3_GOAL_UNDER (1),
Z3_GOAL_PRECISE (0),
Z3_GOAL_UNDER_OVER (3),
Z3_GOAL_OVER (2),
}

15
src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java Normal file
View file

@ -0,0 +1,15 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_lbool
**/
public enum Z3_lbool {
Z3_L_TRUE (1),
Z3_L_UNDEF (0),
Z3_L_FALSE (-1),
}

19
src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java Normal file
View file

@ -0,0 +1,19 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_param_kind
**/
public enum Z3_param_kind {
Z3_PK_BOOL (1),
Z3_PK_SYMBOL (3),
Z3_PK_OTHER (5),
Z3_PK_INVALID (6),
Z3_PK_UINT (0),
Z3_PK_STRING (4),
Z3_PK_DOUBLE (2),
}

19
src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java Normal file
View file

@ -0,0 +1,19 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_parameter_kind
**/
public enum Z3_parameter_kind {
Z3_PARAMETER_FUNC_DECL (6),
Z3_PARAMETER_DOUBLE (1),
Z3_PARAMETER_SYMBOL (3),
Z3_PARAMETER_INT (0),
Z3_PARAMETER_AST (5),
Z3_PARAMETER_SORT (4),
Z3_PARAMETER_RATIONAL (2),
}

22
src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java Normal file
View file

@ -0,0 +1,22 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_sort_kind
**/
public enum Z3_sort_kind {
Z3_BV_SORT (4),
Z3_FINITE_DOMAIN_SORT (8),
Z3_ARRAY_SORT (5),
Z3_UNKNOWN_SORT (1000),
Z3_RELATION_SORT (7),
Z3_REAL_SORT (3),
Z3_INT_SORT (2),
Z3_UNINTERPRETED_SORT (0),
Z3_BOOL_SORT (1),
Z3_DATATYPE_SORT (6),
}

14
src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java Normal file
View file

@ -0,0 +1,14 @@
/**
* Automatically generated file
**/
package com.Microsoft.Z3;
/**
* Z3_symbol_kind
**/
public enum Z3_symbol_kind {
Z3_INT_SYMBOL (0),
Z3_STRING_SYMBOL (1),
}

1554
src/api/java/com/Microsoft/Z3/Expr.java Normal file
View file

File diff suppressed because it is too large Load diff

302
src/api/java/com/Microsoft/Z3/Fixedpoint.java Normal file
View file

@ -0,0 +1,302 @@
/**
* This file was automatically generated from Fixedpoint.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Object for managing fixedpoints
**/
public class Fixedpoint extends Z3Object
{
/**
* A string that describes all available fixedpoint solver parameters.
**/
public String Help()
{
return Native.fixedpointGetHelp(Context.nCtx, NativeObject);
}
/**
* Sets the fixedpoint solver parameters.
**/
public void setParameters(Params value)
{
Context.CheckContextMatch(value);
Native.fixedpointSetParams(Context.nCtx, NativeObject, value.NativeObject);
}
/**
* Retrieves parameter descriptions for Fixedpoint solver.
**/
public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context, Native.fixedpointGetParamDescrs(Context.nCtx, NativeObject)); }
/**
* Assert a constraint (or multiple) into the fixedpoint solver.
**/
public void Assert(BoolExpr[] constraints)
{
Context.CheckContextMatch(constraints);
for (BoolExpr.Iterator a = constraints.iterator(); a.hasNext(); )
{
Native.fixedpointAssert(Context.nCtx, NativeObject, a.NativeObject);
}
}
/**
* Register predicate as recursive relation.
**/
public void RegisterRelation(FuncDecl f)
{
Context.CheckContextMatch(f);
Native.fixedpointRegisterRelation(Context.nCtx, NativeObject, f.NativeObject);
}
/**
* Add rule into the fixedpoint solver.
**/
public void AddRule(BoolExpr rule, Symbol name)
{
Context.CheckContextMatch(rule);
Native.fixedpointAddRule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
}
/**
* Add table fact to the fixedpoint solver.
**/
public void AddFact(FuncDecl pred, long[] args)
{
Context.CheckContextMatch(pred);
Native.fixedpointAddFact(Context.nCtx, NativeObject, pred.NativeObject, (long)args.Length, args);
}
/**
* Query the fixedpoint solver.
* A query is a conjunction of constraints. The constraints may include the recursively defined relations.
* The query is satisfiable if there is an instance of the query variables and a derivation for it.
* The query is unsatisfiable if there are no derivations satisfying the query variables.
**/
public Status Query(BoolExpr query)
{
Context.CheckContextMatch(query);
Z3_lboolean r = (Z3_lboolean)Native.fixedpointQuery(Context.nCtx, NativeObject, query.NativeObject);
switch (r)
{
case Z3_lboolean.Z3_L_TRUE: return Status.SATISFIABLE;
case Z3_lboolean.Z3_L_FALSE: return Status.UNSATISFIABLE;
default: return Status.UNKNOWN;
}
}
/**
* Query the fixedpoint solver.
* A query is an array of relations.
* The query is satisfiable if there is an instance of some relation that is non-empty.
* The query is unsatisfiable if there are no derivations satisfying any of the relations.
**/
public Status Query(FuncDecl[] relations)
{
Context.CheckContextMatch(relations);
Z3_lboolean r = (Z3_lboolean)Native.fixedpointQueryRelations(Context.nCtx, NativeObject,
AST.ArrayLength(relations), AST.ArrayToNative(relations));
switch (r)
{
case Z3_lboolean.Z3_L_TRUE: return Status.SATISFIABLE;
case Z3_lboolean.Z3_L_FALSE: return Status.UNSATISFIABLE;
default: return Status.UNKNOWN;
}
}
/**
* Creates a backtracking point.
* <seealso cref="Pop"/>
**/
public void Push()
{
Native.fixedpointPush(Context.nCtx, NativeObject);
}
/**
* Backtrack one backtracking point.
* <remarks>Note that an exception is thrown if Pop is called without a corresponding <code>Push</code></remarks>
* <seealso cref="Push"/>
**/
public void Pop()
{
Native.fixedpointPop(Context.nCtx, NativeObject);
}
/**
* Update named rule into in the fixedpoint solver.
**/
public void UpdateRule(BoolExpr rule, Symbol name)
{
Context.CheckContextMatch(rule);
Native.fixedpointUpdateRule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
}
/**
* Retrieve satisfying instance or instances of solver,
* or definitions for the recursive predicates that show unsatisfiability.
**/
public Expr GetAnswer()
{
IntPtr ans = Native.fixedpointGetAnswer(Context.nCtx, NativeObject);
return (ans == IntPtr.Zero) ? null : Expr.Create(Context, ans);
}
/**
* Retrieve explanation why fixedpoint engine returned status Unknown.
**/
public String GetReasonUnknown()
{
return Native.fixedpointGetReasonUnknown(Context.nCtx, NativeObject);
}
/**
* Retrieve the number of levels explored for a given predicate.
**/
public long GetNumLevels(FuncDecl predicate)
{
return Native.fixedpointGetNumLevels(Context.nCtx, NativeObject, predicate.NativeObject);
}
/**
* Retrieve the cover of a predicate.
**/
public Expr GetCoverDelta(int level, FuncDecl predicate)
{
IntPtr res = Native.fixedpointGetCoverDelta(Context.nCtx, NativeObject, level, predicate.NativeObject);
return (res == IntPtr.Zero) ? null : Expr.Create(Context, res);
}
/**
* Add <tt>property</tt> about the <tt>predicate</tt>.
* The property is added at <tt>level</tt>.
**/
public void AddCover(int level, FuncDecl predicate, Expr property)
{
Native.fixedpointAddCover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
}
/**
* Retrieve internal string representation of fixedpoint object.
**/
public String toString()
{
return Native.fixedpointtoString(Context.nCtx, NativeObject, 0, null);
}
/**
* Instrument the Datalog engine on which table representation to use for recursive predicate.
**/
public void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds)
{
Native.fixedpointSetPredicateRepresentation(Context.nCtx, NativeObject,
f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds));
}
/**
* Convert benchmark given as set of axioms, rules and queries to a string.
**/
public String toString(BoolExpr[] queries)
{
return Native.fixedpointtoString(Context.nCtx, NativeObject,
AST.ArrayLength(queries), AST.ArrayToNative(queries));
}
/**
* Retrieve set of rules added to fixedpoint context.
**/
public BoolExpr[] Rules()
{
ASTVector v = new ASTVector(Context, Native.fixedpointGetRules(Context.nCtx, NativeObject));
long n = v.Size;
BoolExpr[] res = new BoolExpr[n];
for (long i = 0; i < n; i++)
res[i] = new BoolExpr(Context, v[i].NativeObject);
return res;
}
/**
* Retrieve set of assertions added to fixedpoint context.
**/
public BoolExpr[] Assertions()
{
ASTVector v = new ASTVector(Context, Native.fixedpointGetAssertions(Context.nCtx, NativeObject));
long n = v.Size;
BoolExpr[] res = new BoolExpr[n];
for (long i = 0; i < n; i++)
res[i] = new BoolExpr(Context, v[i].NativeObject);
return res;
}
Fixedpoint(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
Fixedpoint(Context ctx)
{ super(ctx, Native.mkFixedpoint(ctx.nCtx));
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.fixedpointIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.fixedpointDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.Fixedpoint_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.Fixedpoint_DRQ.Add(o);
super.DecRef(o);
}
}

292
src/api/java/com/Microsoft/Z3/FuncDecl.java Normal file
View file

@ -0,0 +1,292 @@
/**
* This file was automatically generated from FuncDecl.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Function declarations.
**/
public class FuncDecl extends AST
{
/**
* Comparison operator.
* @return True if <paramref name="a"/> and <paramref name="b"/> share the same context and are equal, false otherwise.
**/
/* Overloaded operators are not translated. */
/**
* Comparison operator.
* @return True if <paramref name="a"/> and <paramref name="b"/> do not share the same context or are not equal, false otherwise.
**/
/* Overloaded operators are not translated. */
/**
* Object comparison.
**/
public boolean Equals(object o)
{
FuncDecl casted = (FuncDecl) o;
if (casted == null) return false;
return this == casted;
}
/**
* A hash code.
**/
public int GetHashCode()
{
return super.GetHashCode();
}
/**
* A string representations of the function declaration.
**/
public String toString()
{
return Native.funcDecltoString(Context.nCtx, NativeObject);
}
/**
* Returns a unique identifier for the function declaration.
**/
public long Id() { return Native.getFuncDeclId(Context.nCtx, NativeObject); }
/**
* The arity of the function declaration
**/
public long Arity() { return Native.getArity(Context.nCtx, NativeObject); }
/**
* The size of the domain of the function declaration
* <seealso cref="Arity"/>
**/
public long DomainSize() { return Native.getDomainSize(Context.nCtx, NativeObject); }
/**
* The domain of the function declaration
**/
public Sort[] Domain()
{
var n = DomainSize;
Sort[] res = new Sort[n];
for (long i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.getDomain(Context.nCtx, NativeObject, i));
return res;
}
/**
* The range of the function declaration
**/
public Sort Range()
{
return Sort.Create(Context, Native.getRange(Context.nCtx, NativeObject));
}
/**
* The kind of the function declaration.
**/
public Z3_decl_kind DeclKind() { return (Z3_decl_kind)Native.getDeclKind(Context.nCtx, NativeObject); }
/**
* The name of the function declaration
**/
public Symbol Name()
{
return Symbol.Create(Context, Native.getDeclName(Context.nCtx, NativeObject));
}
/**
* The number of parameters of the function declaration
**/
public long NumParameters() { return Native.getDeclNumParameters(Context.nCtx, NativeObject); }
/**
* The parameters of the function declaration
**/
public Parameter[] Parameters()
{
long num = NumParameters;
Parameter[] res = new Parameter[num];
for (long i = 0; i < num; i++)
{
Z3_parameter_kind k = (Z3_parameter_kind)Native.getDeclParameterKind(Context.nCtx, NativeObject, i);
switch (k)
{
case Z3_parameter_kind.Z3_PARAMETER_INT:
res[i] = new Parameter(k, Native.getDeclIntParameter(Context.nCtx, NativeObject, i));
break;
case Z3_parameter_kind.Z3_PARAMETER_DOUBLE:
res[i] = new Parameter(k, Native.getDeclDoubleParameter(Context.nCtx, NativeObject, i));
break;
case Z3_parameter_kind.Z3_PARAMETER_SYMBOL:
res[i] = new Parameter(k, Symbol.Create(Context, Native.getDeclSymbolParameter(Context.nCtx, NativeObject, i)));
break;
case Z3_parameter_kind.Z3_PARAMETER_SORT:
res[i] = new Parameter(k, Sort.Create(Context, Native.getDeclSortParameter(Context.nCtx, NativeObject, i)));
break;
case Z3_parameter_kind.Z3_PARAMETER_AST:
res[i] = new Parameter(k, new AST(Context, Native.getDeclAstParameter(Context.nCtx, NativeObject, i)));
break;
case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL:
res[i] = new Parameter(k, new FuncDecl(Context, Native.getDeclFuncDeclParameter(Context.nCtx, NativeObject, i)));
break;
case Z3_parameter_kind.Z3_PARAMETER_RATIONAL:
res[i] = new Parameter(k, Native.getDeclRationalParameter(Context.nCtx, NativeObject, i));
break;
default:
throw new Z3Exception("Unknown function declaration parameter kind encountered");
}
return res;
}
}
/**
* Function declarations can have Parameters associated with them.
**/
public class Parameter
{
private Z3_parameter_kind kind;
private int i;
private double d;
private Symbol sym;
private Sort srt;
private AST ast;
private FuncDecl fd;
private String r;
/**The int value of the parameter.</summary>
**/
public int Int () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; }
/**The double value of the parameter.</summary>
**/
public double Double () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; }
/**The Symbol value of the parameter.</summary>
**/
public Symbol Symbol () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; }
/**The Sort value of the parameter.</summary>
**/
public Sort Sort () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; }
/**The AST value of the parameter.</summary>
**/
public AST AST () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); return ast; }
/**The FunctionDeclaration value of the parameter.</summary>
**/
public FuncDecl FuncDecl () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; }
/**The rational string value of the parameter.</summary>
**/
public String Rational () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational String"); return r; }
/**
* The kind of the parameter.
**/
public Z3_parameter_kind ParameterKind() { return kind; }
Parameter(Z3_parameter_kind k, int i)
{
this.kind = k;
this.i = i;
}
Parameter(Z3_parameter_kind k, double d)
{
this.kind = k;
this.d = d;
}
Parameter(Z3_parameter_kind k, Symbol s)
{
this.kind = k;
this.sym = s;
}
Parameter(Z3_parameter_kind k, Sort s)
{
this.kind = k;
this.srt = s;
}
Parameter(Z3_parameter_kind k, AST a)
{
this.kind = k;
this.ast = a;
}
Parameter(Z3_parameter_kind k, FuncDecl fd)
{
this.kind = k;
this.fd = fd;
}
Parameter(Z3_parameter_kind k, String r)
{
this.kind = k;
this.r = r;
}
}
FuncDecl(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
: base(ctx, Native.mkFuncDecl(ctx.nCtx, name.NativeObject,
AST.ArrayLength(domain), AST.ArrayToNative(domain),
range.NativeObject))
}
FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
: base(ctx, Native.mkFreshFuncDecl(ctx.nCtx, prefix,
AST.ArrayLength(domain), AST.ArrayToNative(domain),
range.NativeObject))
}
void CheckNativeObject(IntPtr obj)
{
if (Native.getAstKind(Context.nCtx, obj) != (long)Z3_ast_kind.Z3_FUNC_DECL_AST)
throw new Z3Exception("Underlying object is not a function declaration");
super.CheckNativeObject(obj);
}
/**
* Create expression that applies function to arguments.
* <param name="args"></param>
* @return
**/
public Expr this[params() lic Expr this[params Expr[] args
{
public Expr this[params()
{
return Apply(args);
}
/**
* Create expression that applies function to arguments.
* <param name="args"></param>
* @return
**/
public Expr Apply(Expr[] args)
{
Context.CheckContextMatch(args);
return Expr.Create(Context, this, args);
}
}

179
src/api/java/com/Microsoft/Z3/FuncInterp.java Normal file
View file

@ -0,0 +1,179 @@
/**
* This file was automatically generated from FuncInterp.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* A function interpretation is represented as a finite map and an 'else' value.
* Each entry in the finite map represents the value of a function given a set of arguments.
**/
public class FuncInterp extends Z3Object
{
/**
* An Entry object represents an element in the finite map used to encode
* a function interpretation.
**/
public class Entry extends Z3Object
{
/**
* Return the (symbolic) value of this entry.
**/
public Expr Value() {
return Expr.Create(Context, Native.funcEntryGetValue(Context.nCtx, NativeObject)); }
}
/**
* The number of arguments of the entry.
**/
public long NumArgs() { return Native.funcEntryGetNumArgs(Context.nCtx, NativeObject); }
/**
* The arguments of the function entry.
**/
public Expr[] Args()
{
long n = NumArgs;
Expr[] res = new Expr[n];
for (long i = 0; i < n; i++)
res[i] = Expr.Create(Context, Native.funcEntryGetArg(Context.nCtx, NativeObject, i));
return res;
}
/**
* A string representation of the function entry.
**/
public String toString()
{
long n = NumArgs;
String res = "[";
Expr[] args = Args;
for (long i = 0; i < n; i++)
res += args[i] + ", ";
return res + Value + "]";
}
Entry(Context ctx, IntPtr obj) { super(ctx, obj); }
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.funcEntryIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.funcEntryDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.FuncEntry_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.FuncEntry_DRQ.Add(o);
super.DecRef(o);
}
};
/**
* The number of entries in the function interpretation.
**/
public long NumEntries() { return Native.funcInterpGetNumEntries(Context.nCtx, NativeObject); }
/**
* The entries in the function interpretation
**/
public Entry[] Entries()
{
Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length,
j => Contract.Result<Entry[]>()[j] != null));
long n = NumEntries;
Entry[] res = new Entry[n];
for (long i = 0; i < n; i++)
res[i] = new Entry(Context, Native.funcInterpGetEntry(Context.nCtx, NativeObject, i));
return res;
}
/**
* The (symbolic) `else' value of the function interpretation.
**/
public Expr Else() {
return Expr.Create(Context, Native.funcInterpGetElse(Context.nCtx, NativeObject)); }
}
/**
* The arity of the function interpretation
**/
public long Arity() { return Native.funcInterpGetArity(Context.nCtx, NativeObject); }
/**
* A string representation of the function interpretation.
**/
public String toString()
{
String res = "";
res += "[";
for (Entry.Iterator e = Entries.iterator(); e.hasNext(); )
{
long n = e.NumArgs;
if (n > 1) res += "[";
Expr[] args = e.Args;
for (long i = 0; i < n; i++)
{
if (i != 0) res += ", ";
res += args[i];
}
if (n > 1) res += "]";
res += " -> " + e.Value + ", ";
}
res += "else -> " + Else;
res += "]";
return res;
}
FuncInterp(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.funcInterpIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.funcInterpDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.FuncInterp_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.FuncInterp_DRQ.Add(o);
super.DecRef(o);
}
}

182
src/api/java/com/Microsoft/Z3/Goal.java Normal file
View file

@ -0,0 +1,182 @@
/**
* This file was automatically generated from Goal.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* A goal (aka problem). A goal is essentially a set
* of formulas, that can be solved and/or transformed using
* tactics and solvers.
**/
public class Goal extends Z3Object
{
/**
* The precision of the goal.
* <remarks>
* Goals can be transformed using over and under approximations.
* An under approximation is applied when the objective is to find a model for a given goal.
* An over approximation is applied when the objective is to find a proof for a given goal.
* </remarks>
**/
public Z3_goal_prec Precision() { return (Z3_goal_prec)Native.goalPrecision(Context.nCtx, NativeObject); }
/**
* Indicates whether the goal is precise.
**/
public boolean IsPrecise() { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
/**
* Indicates whether the goal is an under-approximation.
**/
public boolean IsUnderApproximation() { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
/**
* Indicates whether the goal is an over-approximation.
**/
public boolean IsOverApproximation() { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
/**
* Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
**/
public boolean IsGarbage() { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
/**
* Adds the <paramref name="constraints"/> to the given goal.
**/
public void Assert(BoolExpr[] constraints)
{
Context.CheckContextMatch(constraints);
for (BoolExpr.Iterator c = constraints.iterator(); c.hasNext(); )
{
// It was an assume, now made an assert just to be sure we do not regress
Native.goalAssert(Context.nCtx, NativeObject, c.NativeObject);
}
}
/**
* Indicates whether the goal contains `false'.
**/
public boolean Inconsistent() { return Native.goalInconsistent(Context.nCtx, NativeObject) != 0; }
/**
* The depth of the goal.
* <remarks>
* This tracks how many transformations were applied to it.
* </remarks>
**/
public long Depth() { return Native.goalDepth(Context.nCtx, NativeObject); }
/**
* Erases all formulas from the given goal.
**/
public void Reset()
{
Native.goalReset(Context.nCtx, NativeObject);
}
/**
* The number of formulas in the goal.
**/
public long Size() { return Native.goalSize(Context.nCtx, NativeObject); }
/**
* The formulas in the goal.
**/
public BoolExpr[] Formulas()
{
long n = Size;
BoolExpr[] res = new BoolExpr[n];
for (long i = 0; i < n; i++)
res[i] = new BoolExpr(Context, Native.goalFormula(Context.nCtx, NativeObject, i));
return res;
}
/**
* The number of formulas, subformulas and terms in the goal.
**/
public long NumExprs() { return Native.goalNumExprs(Context.nCtx, NativeObject); }
/**
* Indicates whether the goal is empty, and it is precise or the product of an under approximation.
**/
public boolean IsDecidedSat() { return Native.goalIsDecidedSat(Context.nCtx, NativeObject) != 0; }
/**
* Indicates whether the goal contains `false', and it is precise or the product of an over approximation.
**/
public boolean IsDecidedUnsat() { return Native.goalIsDecidedUnsat(Context.nCtx, NativeObject) != 0; }
/**
* Translates (copies) the Goal to the target Context <paramref name="ctx"/>.
**/
public Goal Translate(Context ctx)
{
return new Goal(ctx, Native.goalTranslate(Context.nCtx, NativeObject, ctx.nCtx));
}
/**
* Simplifies the goal.
* <remarks>Essentially invokes the `simplify' tactic on the goal.</remarks>
**/
public Goal Simplify(Params p)
{
Tactic t = Context.MkTactic("simplify");
ApplyResult res = t.Apply(this, p);
if (res.NumSubgoals == 0)
return Context.MkGoal();
else
return res.Subgoals[0];
}
/**
* Goal to string conversion.
* @return A string representation of the Goal.
**/
public String toString()
{
return Native.goaltoString(Context.nCtx, NativeObject);
}
Goal(Context ctx, IntPtr obj) { super(ctx, obj); }
Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
{ super(ctx, Native.mkGoal(ctx.nCtx, (models); ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.goalIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.goalDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.Goal_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.Goal_DRQ.Add(o);
super.DecRef(o);
}
}

25
src/api/java/com/Microsoft/Z3/IDisposable.java Normal file
View file

@ -0,0 +1,25 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
IDisposable.java
Abstract:
Compatability interface (C# -> Java)
Author:
Christoph Wintersteiger (cwinter) 2012-03-16
Notes:
--*/
package com.Microsoft.Z3;
public class IDisposable
{
public void Dispose() {}
}

60
src/api/java/com/Microsoft/Z3/Log.java Normal file
View file

@ -0,0 +1,60 @@
/**
* This file was automatically generated from Log.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Interaction logging for Z3.
* <remarks>
* Note that this is a global, static log and if multiple Context
* objects are created, it logs the interaction with all of them.
* </remarks>
**/
public final class Log
{
private boolean m_is_open = false;
/**
* Open an interaction log file.
* <param name="filename">the name of the file to open</param>
* @return True if opening the log file succeeds, false otherwise.
**/
public boolean Open(String filename)
{
m_is_open = true;
return Native.openLog(filename) == 1;
}
/**
* Closes the interaction log.
**/
public void Close()
{
m_is_open = false;
Native.closeLog();
}
/**
* Appends the user-provided string <paramref name="s"/> to the interaction log.
**/
public void Append(String s)
{
if (!m_is_open)
throw new Z3Exception("Log cannot be closed.");
Native.appendLog(s);
}
/**
* Checks whether the interaction log is opened.
* @return True if the interaction log is open, false otherwise.
**/
public boolean isOpen()
{
return m_is_open;
}
}

279
src/api/java/com/Microsoft/Z3/Model.java Normal file
View file

@ -0,0 +1,279 @@
/**
* This file was automatically generated from Model.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* A Model contains interpretations (assignments) of constants and functions.
**/
public class Model extends Z3Object
{
/**
* Retrieves the interpretation (the assignment) of <paramref name="a"/> in the model.
* <param name="a">A Constant</param>
* @return An expression if the constant has an interpretation in the model, null otherwise.
**/
public Expr ConstInterp(Expr a)
{
Context.CheckContextMatch(a);
return ConstInterp(a.FuncDecl);
}
/**
* Retrieves the interpretation (the assignment) of <paramref name="f"/> in the model.
* <param name="f">A function declaration of zero arity</param>
* @return An expression if the function has an interpretation in the model, null otherwise.
**/
public Expr ConstInterp(FuncDecl f)
{
Context.CheckContextMatch(f);
if (f.Arity != 0 ||
Native.getSortKind(Context.nCtx, Native.getRange(Context.nCtx, f.NativeObject)) == (long)Z3_sort_kind.Z3_ARRAY_SORT)
throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
IntPtr n = Native.modelGetConstInterp(Context.nCtx, NativeObject, f.NativeObject);
if (n == IntPtr.Zero)
return null;
else
return Expr.Create(Context, n);
}
/**
* Retrieves the interpretation (the assignment) of a non-constant <paramref name="f"/> in the model.
* <param name="f">A function declaration of non-zero arity</param>
* @return A FunctionInterpretation if the function has an interpretation in the model, null otherwise.
**/
public FuncInterp FuncInterp(FuncDecl f)
{
Context.CheckContextMatch(f);
Z3_sort_kind sk = (Z3_sort_kind)Native.getSortKind(Context.nCtx, Native.getRange(Context.nCtx, f.NativeObject));
if (f.Arity == 0)
{
IntPtr n = Native.modelGetConstInterp(Context.nCtx, NativeObject, f.NativeObject);
if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
{
if (n == IntPtr.Zero)
return null;
else
{
if (Native.isAsArray(Context.nCtx, n) == 0)
throw new Z3Exception("Argument was not an array constant");
IntPtr fd = Native.getAsArrayFuncDecl(Context.nCtx, n);
return FuncInterp(new FuncDecl(Context, fd));
}
}
else
{
throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
}
}
else
{
IntPtr n = Native.modelGetFuncInterp(Context.nCtx, NativeObject, f.NativeObject);
if (n == IntPtr.Zero)
return null;
else
return new FuncInterp(Context, n);
}
}
/**
* The number of constants that have an interpretation in the model.
**/
public long NumConsts() { return Native.modelGetNumConsts(Context.nCtx, NativeObject); }
/**
* The function declarations of the constants in the model.
**/
public FuncDecl[] ConstDecls()
{
long n = NumConsts;
FuncDecl[] res = new FuncDecl[n];
for (long i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context.nCtx, NativeObject, i));
return res;
}
/**
* The number of function interpretations in the model.
**/
public long NumFuncs() { return Native.modelGetNumFuncs(Context.nCtx, NativeObject); }
/**
* The function declarations of the function interpretations in the model.
**/
public FuncDecl[] FuncDecls()
{
long n = NumFuncs;
FuncDecl[] res = new FuncDecl[n];
for (long i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context.nCtx, NativeObject, i));
return res;
}
/**
* All symbols that have an interpretation in the model.
**/
public FuncDecl[] Decls()
{
var nFuncs = NumFuncs;
var nConsts = NumConsts;
long n = nFuncs + nConsts;
FuncDecl[] res = new FuncDecl[n];
for (long i = 0; i < nConsts; i++)
res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context.nCtx, NativeObject, i));
for (long i = 0; i < nFuncs; i++)
res[nConsts + i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context.nCtx, NativeObject, i));
return res;
}
/**
* A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model.
**/
public class ModelEvaluationFailedException extends Z3Exception
{
/**
* An exception that is thrown when model evaluation fails.
**/
public ModelEvaluationFailedException() { super(); }
}
/**
* Evaluates the expression <paramref name="t"/> in the current model.
* <remarks>
* This function may fail if <paramref name="t"/> contains quantifiers,
* is partial (MODEL_PARTIAL enabled), or if <paramref name="t"/> is not well-sorted.
* In this case a <code>ModelEvaluationFailedException</code> is thrown.
* </remarks>
* <param name="t">An expression</param>
* <param name="completion">
* When this flag is enabled, a model value will be assigned to any constant
* or function that does not have an interpretation in the model.
* </param>
* @return The evaluation of <paramref name="t"/> in the model.
**/
public Expr Eval(Expr t, boolean completion)
{
IntPtr v = IntPtr.Zero;
if (Native.modelEval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, v) == 0)
throw new ModelEvaluationFailedException();
else
return Expr.Create(Context, v);
}
/**
* Alias for <code>Eval</code>.
**/
public Expr Evaluate(Expr t, boolean completion)
{
return Eval(t, completion);
}
/**
* The number of uninterpreted sorts that the model has an interpretation for.
**/
public long NumSorts () { return Native.modelGetNumSorts(Context.nCtx, NativeObject); }
/**
* The uninterpreted sorts that the model has an interpretation for.
* <remarks>
* Z3 also provides an intepretation for uninterpreted sorts used in a formula.
* The interpretation for a sort is a finite set of distinct values. We say this finite set is
* the "universe" of the sort.
* </remarks>
* <seealso cref="NumSorts"/>
* <seealso cref="SortUniverse"/>
**/
public Sort[] Sorts()
{
long n = NumSorts;
Sort[] res = new Sort[n];
for (long i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.modelGetSort(Context.nCtx, NativeObject, i));
return res;
}
/**
* The finite set of distinct values that represent the interpretation for sort <paramref name="s"/>.
* <seealso cref="Sorts"/>
* <param name="s">An uninterpreted sort</param>
* @return An array of expressions, where each is an element of the universe of <paramref name="s"/>
**/
public Expr[] SortUniverse(Sort s)
{
ASTVector nUniv = new ASTVector(Context, Native.modelGetSortUniverse(Context.nCtx, NativeObject, s.NativeObject));
long n = nUniv.Size;
Expr[] res = new Expr[n];
for (long i = 0; i < n; i++)
res[i] = Expr.Create(Context, nUniv[i].NativeObject);
return res;
}
/**
* Conversion of models to strings.
* @return A string representation of the model.
**/
public String toString()
{
return Native.modeltoString(Context.nCtx, NativeObject);
}
Model(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.modelIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.modelDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.Model_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.Model_DRQ.Add(o);
super.DecRef(o);
}
}

2259
src/api/java/com/Microsoft/Z3/Native.c Normal file
View file

File diff suppressed because it is too large Load diff

BIN
src/api/java/com/Microsoft/Z3/Native.class Normal file
View file

Binary file not shown.

497
src/api/java/com/Microsoft/Z3/Native.java Normal file
View file

@ -0,0 +1,497 @@
// Automatically generated file
package com.Microsoft.Z3;
public final class Native {
public static class IntPtr { public int value; }
public static class LongPtr { public long value; }
public static class StringPtr { public String value; }
static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0251B738>"); }
public static native long mkConfig();
public static native void delConfig(long a0);
public static native void setParamValue(long a0, String a1, String a2);
public static native long mkContext(long a0);
public static native long mkContextRc(long a0);
public static native void delContext(long a0);
public static native void incRef(long a0, long a1);
public static native void decRef(long a0, long a1);
public static native void updateParamValue(long a0, String a1, String a2);
public static native boolean getParamValue(long a0, String a1, String a2);
public static native void interrupt(long a0);
public static native long mkParams(long a0);
public static native void paramsIncRef(long a0, long a1);
public static native void paramsDecRef(long a0, long a1);
public static native void paramsSetBool(long a0, long a1, long a2, boolean a3);
public static native void paramsSetUint(long a0, long a1, long a2, int a3);
public static native void paramsSetDouble(long a0, long a1, long a2, double a3);
public static native void paramsSetSymbol(long a0, long a1, long a2, long a3);
public static native String paramsToString(long a0, long a1);
public static native void paramsValidate(long a0, long a1, long a2);
public static native void paramDescrsIncRef(long a0, long a1);
public static native void paramDescrsDecRef(long a0, long a1);
public static native int paramDescrsGetKind(long a0, long a1, long a2);
public static native int paramDescrsSize(long a0, long a1);
public static native long paramDescrsGetName(long a0, long a1, int a2);
public static native String paramDescrsToString(long a0, long a1);
public static native long mkIntSymbol(long a0, int a1);
public static native long mkStringSymbol(long a0, String a1);
public static native long mkUninterpretedSort(long a0, long a1);
public static native long mkBoolSort(long a0);
public static native long mkIntSort(long a0);
public static native long mkRealSort(long a0);
public static native long mkBvSort(long a0, int a1);
public static native long mkFiniteDomainSort(long a0, long a1, long a2);
public static native long mkArraySort(long a0, long a1, long a2);
public static native long mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, Long a5, long[] a6);
public static native long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5);
public static native long mkListSort(long a0, long a1, long a2, Long a3, Long a4, Long a5, Long a6, Long a7, Long a8);
public static native long mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6);
public static native void delConstructor(long a0, long a1);
public static native long mkDatatype(long a0, long a1, int a2, long[] a3);
public static native long mkConstructorList(long a0, int a1, long[] a2);
public static native void delConstructorList(long a0, long a1);
public static native void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4);
public static native void queryConstructor(long a0, long a1, int a2, Long a3, Long a4, long[] a5);
public static native long mkFuncDecl(long a0, long a1, int a2, long[] a3, long a4);
public static native long mkApp(long a0, long a1, int a2, long[] a3);
public static native long mkConst(long a0, long a1, long a2);
public static native long mkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4);
public static native long mkFreshConst(long a0, String a1, long a2);
public static native long mkTrue(long a0);
public static native long mkFalse(long a0);
public static native long mkEq(long a0, long a1, long a2);
public static native long mkDistinct(long a0, int a1, long[] a2);
public static native long mkNot(long a0, long a1);
public static native long mkIte(long a0, long a1, long a2, long a3);
public static native long mkIff(long a0, long a1, long a2);
public static native long mkImplies(long a0, long a1, long a2);
public static native long mkXor(long a0, long a1, long a2);
public static native long mkAnd(long a0, int a1, long[] a2);
public static native long mkOr(long a0, int a1, long[] a2);
public static native long mkAdd(long a0, int a1, long[] a2);
public static native long mkMul(long a0, int a1, long[] a2);
public static native long mkSub(long a0, int a1, long[] a2);
public static native long mkUnaryMinus(long a0, long a1);
public static native long mkDiv(long a0, long a1, long a2);
public static native long mkMod(long a0, long a1, long a2);
public static native long mkRem(long a0, long a1, long a2);
public static native long mkPower(long a0, long a1, long a2);
public static native long mkLt(long a0, long a1, long a2);
public static native long mkLe(long a0, long a1, long a2);
public static native long mkGt(long a0, long a1, long a2);
public static native long mkGe(long a0, long a1, long a2);
public static native long mkInt2real(long a0, long a1);
public static native long mkReal2int(long a0, long a1);
public static native long mkIsInt(long a0, long a1);
public static native long mkBvnot(long a0, long a1);
public static native long mkBvredand(long a0, long a1);
public static native long mkBvredor(long a0, long a1);
public static native long mkBvand(long a0, long a1, long a2);
public static native long mkBvor(long a0, long a1, long a2);
public static native long mkBvxor(long a0, long a1, long a2);
public static native long mkBvnand(long a0, long a1, long a2);
public static native long mkBvnor(long a0, long a1, long a2);
public static native long mkBvxnor(long a0, long a1, long a2);
public static native long mkBvneg(long a0, long a1);
public static native long mkBvadd(long a0, long a1, long a2);
public static native long mkBvsub(long a0, long a1, long a2);
public static native long mkBvmul(long a0, long a1, long a2);
public static native long mkBvudiv(long a0, long a1, long a2);
public static native long mkBvsdiv(long a0, long a1, long a2);
public static native long mkBvurem(long a0, long a1, long a2);
public static native long mkBvsrem(long a0, long a1, long a2);
public static native long mkBvsmod(long a0, long a1, long a2);
public static native long mkBvult(long a0, long a1, long a2);
public static native long mkBvslt(long a0, long a1, long a2);
public static native long mkBvule(long a0, long a1, long a2);
public static native long mkBvsle(long a0, long a1, long a2);
public static native long mkBvuge(long a0, long a1, long a2);
public static native long mkBvsge(long a0, long a1, long a2);
public static native long mkBvugt(long a0, long a1, long a2);
public static native long mkBvsgt(long a0, long a1, long a2);
public static native long mkConcat(long a0, long a1, long a2);
public static native long mkExtract(long a0, int a1, int a2, long a3);
public static native long mkSignExt(long a0, int a1, long a2);
public static native long mkZeroExt(long a0, int a1, long a2);
public static native long mkRepeat(long a0, int a1, long a2);
public static native long mkBvshl(long a0, long a1, long a2);
public static native long mkBvlshr(long a0, long a1, long a2);
public static native long mkBvashr(long a0, long a1, long a2);
public static native long mkRotateLeft(long a0, int a1, long a2);
public static native long mkRotateRight(long a0, int a1, long a2);
public static native long mkExtRotateLeft(long a0, long a1, long a2);
public static native long mkExtRotateRight(long a0, long a1, long a2);
public static native long mkInt2bv(long a0, int a1, long a2);
public static native long mkBv2int(long a0, long a1, boolean a2);
public static native long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3);
public static native long mkBvaddNoUnderflow(long a0, long a1, long a2);
public static native long mkBvsubNoOverflow(long a0, long a1, long a2);
public static native long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3);
public static native long mkBvsdivNoOverflow(long a0, long a1, long a2);
public static native long mkBvnegNoOverflow(long a0, long a1);
public static native long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3);
public static native long mkBvmulNoUnderflow(long a0, long a1, long a2);
public static native long mkSelect(long a0, long a1, long a2);
public static native long mkStore(long a0, long a1, long a2, long a3);
public static native long mkConstArray(long a0, long a1, long a2);
public static native long mkMap(long a0, long a1, int a2, long[] a3);
public static native long mkArrayDefault(long a0, long a1);
public static native long mkSetSort(long a0, long a1);
public static native long mkEmptySet(long a0, long a1);
public static native long mkFullSet(long a0, long a1);
public static native long mkSetAdd(long a0, long a1, long a2);
public static native long mkSetDel(long a0, long a1, long a2);
public static native long mkSetUnion(long a0, int a1, long[] a2);
public static native long mkSetIntersect(long a0, int a1, long[] a2);
public static native long mkSetDifference(long a0, long a1, long a2);
public static native long mkSetComplement(long a0, long a1);
public static native long mkSetMember(long a0, long a1, long a2);
public static native long mkSetSubset(long a0, long a1, long a2);
public static native long mkNumeral(long a0, String a1, long a2);
public static native long mkReal(long a0, int a1, int a2);
public static native long mkInt(long a0, int a1, long a2);
public static native long mkUnsignedInt(long a0, int a1, long a2);
public static native long mkInt64(long a0, long a1, long a2);
public static native long mkUnsignedInt64(long a0, long a1, long a2);
public static native long mkPattern(long a0, int a1, long[] a2);
public static native long mkBound(long a0, int a1, long a2);
public static native long mkForall(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7);
public static native long mkExists(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7);
public static native long mkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8);
public static native long mkQuantifierEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12);
public static native long mkForallConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6);
public static native long mkExistsConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6);
public static native long mkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7);
public static native long mkQuantifierConstEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11);
public static native int getSymbolKind(long a0, long a1);
public static native int getSymbolInt(long a0, long a1);
public static native String getSymbolString(long a0, long a1);
public static native long getSortName(long a0, long a1);
public static native int getSortId(long a0, long a1);
public static native long sortToAst(long a0, long a1);
public static native boolean isEqSort(long a0, long a1, long a2);
public static native int getSortKind(long a0, long a1);
public static native int getBvSortSize(long a0, long a1);
public static native boolean getFiniteDomainSortSize(long a0, long a1, Long a2);
public static native long getArraySortDomain(long a0, long a1);
public static native long getArraySortRange(long a0, long a1);
public static native long getTupleSortMkDecl(long a0, long a1);
public static native int getTupleSortNumFields(long a0, long a1);
public static native long getTupleSortFieldDecl(long a0, long a1, int a2);
public static native int getDatatypeSortNumConstructors(long a0, long a1);
public static native long getDatatypeSortConstructor(long a0, long a1, int a2);
public static native long getDatatypeSortRecognizer(long a0, long a1, int a2);
public static native long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3);
public static native int getRelationArity(long a0, long a1);
public static native long getRelationColumn(long a0, long a1, int a2);
public static native long funcDeclToAst(long a0, long a1);
public static native boolean isEqFuncDecl(long a0, long a1, long a2);
public static native int getFuncDeclId(long a0, long a1);
public static native long getDeclName(long a0, long a1);
public static native int getDeclKind(long a0, long a1);
public static native int getDomainSize(long a0, long a1);
public static native int getArity(long a0, long a1);
public static native long getDomain(long a0, long a1, int a2);
public static native long getRange(long a0, long a1);
public static native int getDeclNumParameters(long a0, long a1);
public static native int getDeclParameterKind(long a0, long a1, int a2);
public static native int getDeclIntParameter(long a0, long a1, int a2);
public static native double getDeclDoubleParameter(long a0, long a1, int a2);
public static native long getDeclSymbolParameter(long a0, long a1, int a2);
public static native long getDeclSortParameter(long a0, long a1, int a2);
public static native long getDeclAstParameter(long a0, long a1, int a2);
public static native long getDeclFuncDeclParameter(long a0, long a1, int a2);
public static native String getDeclRationalParameter(long a0, long a1, int a2);
public static native long appToAst(long a0, long a1);
public static native long getAppDecl(long a0, long a1);
public static native int getAppNumArgs(long a0, long a1);
public static native long getAppArg(long a0, long a1, int a2);
public static native boolean isEqAst(long a0, long a1, long a2);
public static native int getAstId(long a0, long a1);
public static native int getAstHash(long a0, long a1);
public static native long getSort(long a0, long a1);
public static native boolean isWellSorted(long a0, long a1);
public static native int getBoolValue(long a0, long a1);
public static native int getAstKind(long a0, long a1);
public static native boolean isApp(long a0, long a1);
public static native boolean isNumeralAst(long a0, long a1);
public static native boolean isAlgebraicNumber(long a0, long a1);
public static native long toApp(long a0, long a1);
public static native long toFuncDecl(long a0, long a1);
public static native String getNumeralString(long a0, long a1);
public static native String getNumeralDecimalString(long a0, long a1, int a2);
public static native long getNumerator(long a0, long a1);
public static native long getDenominator(long a0, long a1);
public static native boolean getNumeralSmall(long a0, long a1, Long a2, Long a3);
public static native boolean getNumeralInt(long a0, long a1, Integer a2);
public static native boolean getNumeralUint(long a0, long a1, Integer a2);
public static native boolean getNumeralUint64(long a0, long a1, Long a2);
public static native boolean getNumeralInt64(long a0, long a1, Long a2);
public static native boolean getNumeralRationalInt64(long a0, long a1, Long a2, Long a3);
public static native long getAlgebraicNumberLower(long a0, long a1, int a2);
public static native long getAlgebraicNumberUpper(long a0, long a1, int a2);
public static native long patternToAst(long a0, long a1);
public static native int getPatternNumTerms(long a0, long a1);
public static native long getPattern(long a0, long a1, int a2);
public static native int getIndexValue(long a0, long a1);
public static native boolean isQuantifierForall(long a0, long a1);
public static native int getQuantifierWeight(long a0, long a1);
public static native int getQuantifierNumPatterns(long a0, long a1);
public static native long getQuantifierPatternAst(long a0, long a1, int a2);
public static native int getQuantifierNumNoPatterns(long a0, long a1);
public static native long getQuantifierNoPatternAst(long a0, long a1, int a2);
public static native int getQuantifierNumBound(long a0, long a1);
public static native long getQuantifierBoundName(long a0, long a1, int a2);
public static native long getQuantifierBoundSort(long a0, long a1, int a2);
public static native long getQuantifierBody(long a0, long a1);
public static native long simplify(long a0, long a1);
public static native long simplifyEx(long a0, long a1, long a2);
public static native String simplifyGetHelp(long a0);
public static native long simplifyGetParamDescrs(long a0);
public static native long updateTerm(long a0, long a1, int a2, long[] a3);
public static native long substitute(long a0, long a1, int a2, long[] a3, long[] a4);
public static native long substituteVars(long a0, long a1, int a2, long[] a3);
public static native long translate(long a0, long a1, long a2);
public static native void modelIncRef(long a0, long a1);
public static native void modelDecRef(long a0, long a1);
public static native boolean modelEval(long a0, long a1, long a2, boolean a3, Long a4);
public static native long modelGetConstInterp(long a0, long a1, long a2);
public static native long modelGetFuncInterp(long a0, long a1, long a2);
public static native int modelGetNumConsts(long a0, long a1);
public static native long modelGetConstDecl(long a0, long a1, int a2);
public static native int modelGetNumFuncs(long a0, long a1);
public static native long modelGetFuncDecl(long a0, long a1, int a2);
public static native int modelGetNumSorts(long a0, long a1);
public static native long modelGetSort(long a0, long a1, int a2);
public static native long modelGetSortUniverse(long a0, long a1, long a2);
public static native boolean isAsArray(long a0, long a1);
public static native long getAsArrayFuncDecl(long a0, long a1);
public static native void funcInterpIncRef(long a0, long a1);
public static native void funcInterpDecRef(long a0, long a1);
public static native int funcInterpGetNumEntries(long a0, long a1);
public static native long funcInterpGetEntry(long a0, long a1, int a2);
public static native long funcInterpGetElse(long a0, long a1);
public static native int funcInterpGetArity(long a0, long a1);
public static native void funcEntryIncRef(long a0, long a1);
public static native void funcEntryDecRef(long a0, long a1);
public static native long funcEntryGetValue(long a0, long a1);
public static native int funcEntryGetNumArgs(long a0, long a1);
public static native long funcEntryGetArg(long a0, long a1, int a2);
public static native int openLog(String a0);
public static native void appendLog(String a0);
public static native void closeLog();
public static native void toggleWarningMessages(boolean a0);
public static native void setAstPrintMode(long a0, int a1);
public static native String astToString(long a0, long a1);
public static native String patternToString(long a0, long a1);
public static native String sortToString(long a0, long a1);
public static native String funcDeclToString(long a0, long a1);
public static native String modelToString(long a0, long a1);
public static native String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7);
public static native long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
public static native long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
public static native void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
public static native void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
public static native int getSmtlibNumFormulas(long a0);
public static native long getSmtlibFormula(long a0, int a1);
public static native int getSmtlibNumAssumptions(long a0);
public static native long getSmtlibAssumption(long a0, int a1);
public static native int getSmtlibNumDecls(long a0);
public static native long getSmtlibDecl(long a0, int a1);
public static native int getSmtlibNumSorts(long a0);
public static native long getSmtlibSort(long a0, int a1);
public static native String getSmtlibError(long a0);
public static native int getErrorCode(long a0);
public static native void setError(long a0, int a1);
public static native String getErrorMsg(int a0);
public static native String getErrorMsgEx(long a0, int a1);
public static native void getVersion(Integer a0, Integer a1, Integer a2, Integer a3);
public static native void enableTrace(String a0);
public static native void disableTrace(String a0);
public static native void resetMemory();
public static native long mkFixedpoint(long a0);
public static native void fixedpointIncRef(long a0, long a1);
public static native void fixedpointDecRef(long a0, long a1);
public static native void fixedpointAddRule(long a0, long a1, long a2, long a3);
public static native void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4);
public static native void fixedpointAssert(long a0, long a1, long a2);
public static native int fixedpointQuery(long a0, long a1, long a2);
public static native int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3);
public static native long fixedpointGetAnswer(long a0, long a1);
public static native String fixedpointGetReasonUnknown(long a0, long a1);
public static native void fixedpointUpdateRule(long a0, long a1, long a2, long a3);
public static native int fixedpointGetNumLevels(long a0, long a1, long a2);
public static native long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3);
public static native void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4);
public static native long fixedpointGetStatistics(long a0, long a1);
public static native void fixedpointRegisterRelation(long a0, long a1, long a2);
public static native void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4);
public static native long fixedpointGetRules(long a0, long a1);
public static native long fixedpointGetAssertions(long a0, long a1);
public static native void fixedpointSetParams(long a0, long a1, long a2);
public static native String fixedpointGetHelp(long a0, long a1);
public static native long fixedpointGetParamDescrs(long a0, long a1);
public static native String fixedpointToString(long a0, long a1, int a2, long[] a3);
public static native long fixedpointFromString(long a0, long a1, String a2);
public static native long fixedpointFromFile(long a0, long a1, String a2);
public static native void fixedpointPush(long a0, long a1);
public static native void fixedpointPop(long a0, long a1);
public static native long mkAstVector(long a0);
public static native void astVectorIncRef(long a0, long a1);
public static native void astVectorDecRef(long a0, long a1);
public static native int astVectorSize(long a0, long a1);
public static native long astVectorGet(long a0, long a1, int a2);
public static native void astVectorSet(long a0, long a1, int a2, long a3);
public static native void astVectorResize(long a0, long a1, int a2);
public static native void astVectorPush(long a0, long a1, long a2);
public static native long astVectorTranslate(long a0, long a1, long a2);
public static native String astVectorToString(long a0, long a1);
public static native long mkAstMap(long a0);
public static native void astMapIncRef(long a0, long a1);
public static native void astMapDecRef(long a0, long a1);
public static native boolean astMapContains(long a0, long a1, long a2);
public static native long astMapFind(long a0, long a1, long a2);
public static native void astMapInsert(long a0, long a1, long a2, long a3);
public static native void astMapErase(long a0, long a1, long a2);
public static native void astMapReset(long a0, long a1);
public static native int astMapSize(long a0, long a1);
public static native long astMapKeys(long a0, long a1);
public static native String astMapToString(long a0, long a1);
public static native long mkGoal(long a0, boolean a1, boolean a2, boolean a3);
public static native void goalIncRef(long a0, long a1);
public static native void goalDecRef(long a0, long a1);
public static native int goalPrecision(long a0, long a1);
public static native void goalAssert(long a0, long a1, long a2);
public static native boolean goalInconsistent(long a0, long a1);
public static native int goalDepth(long a0, long a1);
public static native void goalReset(long a0, long a1);
public static native int goalSize(long a0, long a1);
public static native long goalFormula(long a0, long a1, int a2);
public static native int goalNumExprs(long a0, long a1);
public static native boolean goalIsDecidedSat(long a0, long a1);
public static native boolean goalIsDecidedUnsat(long a0, long a1);
public static native long goalTranslate(long a0, long a1, long a2);
public static native String goalToString(long a0, long a1);
public static native long mkTactic(long a0, String a1);
public static native void tacticIncRef(long a0, long a1);
public static native void tacticDecRef(long a0, long a1);
public static native long mkProbe(long a0, String a1);
public static native void probeIncRef(long a0, long a1);
public static native void probeDecRef(long a0, long a1);
public static native long tacticAndThen(long a0, long a1, long a2);
public static native long tacticOrElse(long a0, long a1, long a2);
public static native long tacticParOr(long a0, int a1, long[] a2);
public static native long tacticParAndThen(long a0, long a1, long a2);
public static native long tacticTryFor(long a0, long a1, int a2);
public static native long tacticWhen(long a0, long a1, long a2);
public static native long tacticCond(long a0, long a1, long a2, long a3);
public static native long tacticRepeat(long a0, long a1, int a2);
public static native long tacticSkip(long a0);
public static native long tacticFail(long a0);
public static native long tacticFailIf(long a0, long a1);
public static native long tacticFailIfNotDecided(long a0);
public static native long tacticUsingParams(long a0, long a1, long a2);
public static native long probeConst(long a0, double a1);
public static native long probeLt(long a0, long a1, long a2);
public static native long probeGt(long a0, long a1, long a2);
public static native long probeLe(long a0, long a1, long a2);
public static native long probeGe(long a0, long a1, long a2);
public static native long probeEq(long a0, long a1, long a2);
public static native long probeAnd(long a0, long a1, long a2);
public static native long probeOr(long a0, long a1, long a2);
public static native long probeNot(long a0, long a1);
public static native int getNumTactics(long a0);
public static native String getTacticName(long a0, int a1);
public static native int getNumProbes(long a0);
public static native String getProbeName(long a0, int a1);
public static native String tacticGetHelp(long a0, long a1);
public static native long tacticGetParamDescrs(long a0, long a1);
public static native String tacticGetDescr(long a0, String a1);
public static native String probeGetDescr(long a0, String a1);
public static native double probeApply(long a0, long a1, long a2);
public static native long tacticApply(long a0, long a1, long a2);
public static native long tacticApplyEx(long a0, long a1, long a2, long a3);
public static native void applyResultIncRef(long a0, long a1);
public static native void applyResultDecRef(long a0, long a1);
public static native String applyResultToString(long a0, long a1);
public static native int applyResultGetNumSubgoals(long a0, long a1);
public static native long applyResultGetSubgoal(long a0, long a1, int a2);
public static native long applyResultConvertModel(long a0, long a1, int a2, long a3);
public static native long mkSolver(long a0);
public static native long mkSimpleSolver(long a0);
public static native long mkSolverForLogic(long a0, long a1);
public static native long mkSolverFromTactic(long a0, long a1);
public static native String solverGetHelp(long a0, long a1);
public static native long solverGetParamDescrs(long a0, long a1);
public static native void solverSetParams(long a0, long a1, long a2);
public static native void solverIncRef(long a0, long a1);
public static native void solverDecRef(long a0, long a1);
public static native void solverPush(long a0, long a1);
public static native void solverPop(long a0, long a1, int a2);
public static native void solverReset(long a0, long a1);
public static native int solverGetNumScopes(long a0, long a1);
public static native void solverAssert(long a0, long a1, long a2);
public static native void solverAssertAndTrack(long a0, long a1, long a2, long a3);
public static native long solverGetAssertions(long a0, long a1);
public static native int solverCheck(long a0, long a1);
public static native int solverCheckAssumptions(long a0, long a1, int a2, long[] a3);
public static native long solverGetModel(long a0, long a1);
public static native long solverGetProof(long a0, long a1);
public static native long solverGetUnsatCore(long a0, long a1);
public static native String solverGetReasonUnknown(long a0, long a1);
public static native long solverGetStatistics(long a0, long a1);
public static native String solverToString(long a0, long a1);
public static native String statsToString(long a0, long a1);
public static native void statsIncRef(long a0, long a1);
public static native void statsDecRef(long a0, long a1);
public static native int statsSize(long a0, long a1);
public static native String statsGetKey(long a0, long a1, int a2);
public static native boolean statsIsUint(long a0, long a1, int a2);
public static native boolean statsIsDouble(long a0, long a1, int a2);
public static native int statsGetUintValue(long a0, long a1, int a2);
public static native double statsGetDoubleValue(long a0, long a1, int a2);
public static native long mkInjectiveFunction(long a0, long a1, int a2, long[] a3, long a4);
public static native void setLogic(long a0, String a1);
public static native void push(long a0);
public static native void pop(long a0, int a1);
public static native int getNumScopes(long a0);
public static native void persistAst(long a0, long a1, int a2);
public static native void assertCnstr(long a0, long a1);
public static native int checkAndGetModel(long a0, Long a1);
public static native int check(long a0);
public static native int checkAssumptions(long a0, int a1, long[] a2, Long a3, Long a4, Integer a5, long[] a6);
public static native int getImpliedEqualities(long a0, int a1, long[] a2, int[] a3);
public static native void delModel(long a0, long a1);
public static native void softCheckCancel(long a0);
public static native int getSearchFailure(long a0);
public static native long mkLabel(long a0, long a1, boolean a2, long a3);
public static native long getRelevantLabels(long a0);
public static native long getRelevantLiterals(long a0);
public static native long getGuessedLiterals(long a0);
public static native void delLiterals(long a0, long a1);
public static native int getNumLiterals(long a0, long a1);
public static native long getLabelSymbol(long a0, long a1, int a2);
public static native long getLiteral(long a0, long a1, int a2);
public static native void disableLiteral(long a0, long a1, int a2);
public static native void blockLiterals(long a0, long a1);
public static native int getModelNumConstants(long a0, long a1);
public static native long getModelConstant(long a0, long a1, int a2);
public static native int getModelNumFuncs(long a0, long a1);
public static native long getModelFuncDecl(long a0, long a1, int a2);
public static native boolean evalFuncDecl(long a0, long a1, long a2, Long a3);
public static native boolean isArrayValue(long a0, long a1, long a2, Integer a3);
public static native void getArrayValue(long a0, long a1, long a2, int a3, long[] a4, long[] a5, Long a6);
public static native long getModelFuncElse(long a0, long a1, int a2);
public static native int getModelFuncNumEntries(long a0, long a1, int a2);
public static native int getModelFuncEntryNumArgs(long a0, long a1, int a2, int a3);
public static native long getModelFuncEntryArg(long a0, long a1, int a2, int a3, int a4);
public static native long getModelFuncEntryValue(long a0, long a1, int a2, int a3);
public static native boolean eval(long a0, long a1, long a2, Long a3);
public static native boolean evalDecl(long a0, long a1, long a2, int a3, long[] a4, Long a5);
public static native String contextToString(long a0);
public static native String statisticsToString(long a0);
public static native long getContextAssignment(long a0);
public static void main(String[] args) {
IntPtr major = new IntPtr(), minor = new IntPtr(), build = new IntPtr(), revision = new IntPtr();
getVersion(major, minor, build, revision);
System.out.format("Z3 (for Java) %d.%d.%d%n", major.value, minor.value, build.value);
}
}

264
src/api/java/com/Microsoft/Z3/Numeral.java Normal file
View file

@ -0,0 +1,264 @@
/**
* This file was automatically generated from Numeral.cs
**/
package com.Microsoft.Z3;
/* using System; */
/* using System.Numerics; */
/**
* Integer Numerals
**/
public class IntNum extends IntExpr
{
IntNum(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
/**
* Retrieve the 64-bit unsigned integer value.
**/
public UInt64 UInt64()
{
UInt64 res = 0;
if (Native.getNumeralLong64(Context.nCtx, NativeObject, res) == 0)
throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res;
}
/**
* Retrieve the int value.
**/
public int Int()
{
int res = 0;
if (Native.getNumeralInt(Context.nCtx, NativeObject, res) == 0)
throw new Z3Exception("Numeral is not an int");
return res;
}
/**
* Retrieve the 64-bit int value.
**/
public Int64 Int64()
{
Int64 res = 0;
if (Native.getNumeralInt64(Context.nCtx, NativeObject, res) == 0)
throw new Z3Exception("Numeral is not an int64");
return res;
}
/**
* Retrieve the int value.
**/
public long UInt()
{
long res = 0;
if (Native.getNumeralLong(Context.nCtx, NativeObject, res) == 0)
throw new Z3Exception("Numeral is not a long");
return res;
}
/**
* Retrieve the BigInteger value.
**/
public BigInteger BigInteger()
{
return BigInteger.Parse(this.toString());
}
/**
* Returns a string representation of the numeral.
**/
public String toString()
{
return Native.getNumeralString(Context.nCtx, NativeObject);
}
}
/**
* Rational Numerals
**/
public class RatNum extends RealExpr
{
/**
* The numerator of a rational numeral.
**/
public IntNum Numerator() {
return new IntNum(Context, Native.getNumerator(Context.nCtx, NativeObject)); }
}
/**
* The denominator of a rational numeral.
**/
public IntNum Denominator() {
return new IntNum(Context, Native.getDenominator(Context.nCtx, NativeObject)); }
}
/**
* Converts the numerator of the rational to a BigInteger
**/
public BigInteger BigIntNumerator()
{
IntNum n = Numerator;
return BigInteger.Parse(n.toString());
}
/**
* Converts the denominator of the rational to a BigInteger
**/
public BigInteger BigIntDenominator()
{
IntNum n = Denominator;
return BigInteger.Parse(n.toString());
}
/**
* Returns a string representation in decimal notation.
* <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
**/
public String ToDecimalString(long precision)
{
return Native.getNumeralDecimalString(Context.nCtx, NativeObject, precision);
}
/**
* Returns a string representation of the numeral.
**/
public String toString()
{
return Native.getNumeralString(Context.nCtx, NativeObject);
}
RatNum(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
}
/**
* Bit-vector numerals
**/
public class BitVecNum extends BitVecExpr
{
/**
* Retrieve the 64-bit unsigned integer value.
**/
public UInt64 UInt64()
{
UInt64 res = 0;
if (Native.getNumeralLong64(Context.nCtx, NativeObject, res) == 0)
throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res;
}
/**
* Retrieve the int value.
**/
public int Int()
{
int res = 0;
if (Native.getNumeralInt(Context.nCtx, NativeObject, res) == 0)
throw new Z3Exception("Numeral is not an int");
return res;
}
/**
* Retrieve the 64-bit int value.
**/
public Int64 Int64()
{
Int64 res = 0;
if (Native.getNumeralInt64(Context.nCtx, NativeObject, res) == 0)
throw new Z3Exception("Numeral is not an int64");
return res;
}
/**
* Retrieve the int value.
**/
public long UInt()
{
long res = 0;
if (Native.getNumeralLong(Context.nCtx, NativeObject, res) == 0)
throw new Z3Exception("Numeral is not a long");
return res;
}
/**
* Retrieve the BigInteger value.
**/
public BigInteger BigInteger()
{
return BigInteger.Parse(this.toString());
}
/**
* Returns a string representation of the numeral.
**/
public String toString()
{
return Native.getNumeralString(Context.nCtx, NativeObject);
}
BitVecNum(Context ctx, IntPtr obj) { super(ctx, obj); }
}
/**
* Algebraic numbers
**/
public class AlgebraicNum extends ArithExpr
{
/**
* Return a upper bound for a given real algebraic number.
* The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.
* <seealso cref="Expr.IsAlgebraicNumber"/>
* <param name="precision">the precision of the result</param>
* @return A numeral Expr of sort Real
**/
public RatNum ToUpper(long precision)
{
return new RatNum(Context, Native.getAlgebraicNumberUpper(Context.nCtx, NativeObject, precision));
}
/**
* Return a lower bound for the given real algebraic number.
* The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.
* <seealso cref="Expr.IsAlgebraicNumber"/>
* <param name="precision"></param>
* @return A numeral Expr of sort Real
**/
public RatNum ToLower(long precision)
{
return new RatNum(Context, Native.getAlgebraicNumberLower(Context.nCtx, NativeObject, precision));
}
/**
* Returns a string representation in decimal notation.
* <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
**/
public String ToDecimal(long precision)
{
return Native.getNumeralDecimalString(Context.nCtx, NativeObject, precision);
}
AlgebraicNum(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
}

87
src/api/java/com/Microsoft/Z3/ParamDescrs.java Normal file
View file

@ -0,0 +1,87 @@
/**
* This file was automatically generated from ParamDescrs.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* A ParamDescrs describes a set of parameters.
**/
public class ParamDescrs extends Z3Object
{
/**
* validate a set of parameters.
**/
public void Validate(Params p)
{
Native.paramsValidate(Context.nCtx, p.NativeObject, NativeObject);
}
/**
* Retrieve kind of parameter.
**/
public Z3_param_kind GetKind(Symbol name)
{
return (Z3_param_kind)Native.paramDescrsGetKind(Context.nCtx, NativeObject, name.NativeObject);
}
/**
* Retrieve all names of parameters.
**/
public Symbol[] Names()
{
long sz = Native.paramDescrsSize(Context.nCtx, NativeObject);
Symbol[] names = new Symbol[sz];
for (long i = 0; i < sz; ++i) {
names[i] = Symbol.Create(Context, Native.paramDescrsGetName(Context.nCtx, NativeObject, i));
}
return names;
}
/**
* The size of the ParamDescrs.
**/
public long Size() { return Native.paramDescrsSize(Context.nCtx, NativeObject); }
/**
* Retrieves a string representation of the ParamDescrs.
**/
public String toString()
{
return Native.paramDescrstoString(Context.nCtx, NativeObject);
}
ParamDescrs(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.paramDescrsIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.paramDescrsDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.ParamDescrs_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.ParamDescrs_DRQ.Add(o);
super.DecRef(o);
}
}

126
src/api/java/com/Microsoft/Z3/Params.java Normal file
View file

@ -0,0 +1,126 @@
/**
* This file was automatically generated from Params.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* A ParameterSet represents a configuration in the form of Symbol/value pairs.
**/
public class Params extends Z3Object
{
/**
* Adds a parameter setting.
**/
public void Add(Symbol name, boolean value)
{
Native.paramsSetBoolean(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0);
}
/**
* Adds a parameter setting.
**/
public void Add(Symbol name, long value)
{
Native.paramsSetLong(Context.nCtx, NativeObject, name.NativeObject, value);
}
/**
* Adds a parameter setting.
**/
public void Add(Symbol name, double value)
{
Native.paramsSetDouble(Context.nCtx, NativeObject, name.NativeObject, value);
}
/**
* Adds a parameter setting.
**/
public void Add(Symbol name, Symbol value)
{
Native.paramsSetSymbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
}
/**
* Adds a parameter setting.
**/
public void Add(String name, boolean value)
{
Native.paramsSetBoolean(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
}
/**
* Adds a parameter setting.
**/
public void Add(String name, long value)
{
Native.paramsSetLong(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
}
/**
* Adds a parameter setting.
**/
public void Add(String name, double value)
{
Native.paramsSetDouble(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
}
/**
* Adds a parameter setting.
**/
public void Add(String name, Symbol value)
{
Native.paramsSetSymbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
}
/**
* A string representation of the parameter set.
**/
public String toString()
{
return Native.paramstoString(Context.nCtx, NativeObject);
}
Params(Context ctx)
{ super(ctx, Native.mkParams(ctx.nCtx));
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.paramsIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.paramsDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.Params_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.Params_DRQ.Add(o);
super.DecRef(o);
}
}

48
src/api/java/com/Microsoft/Z3/Pattern.java Normal file
View file

@ -0,0 +1,48 @@
/**
* This file was automatically generated from Pattern.cs
**/
package com.Microsoft.Z3;
/* using System; */
/* using System.Runtime.InteropServices; */
/**
* Patterns comprise a list of terms. The list should be
* non-empty. If the list comprises of more than one term, it is
* also called a multi-pattern.
**/
public class Pattern extends AST
{
/**
* The number of terms in the pattern.
**/
public long NumTerms() { return Native.getPatternNumTerms(Context.nCtx, NativeObject); }
/**
* The terms in the pattern.
**/
public Expr[] Terms()
{
long n = NumTerms;
Expr[] res = new Expr[n];
for (long i = 0; i < n; i++)
res[i] = Expr.Create(Context, Native.getPattern(Context.nCtx, NativeObject, i));
return res;
}
/**
* A string representation of the pattern.
**/
public String toString()
{
return Native.patterntoString(Context.nCtx, NativeObject);
}
Pattern(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
}

72
src/api/java/com/Microsoft/Z3/Probe.java Normal file
View file

@ -0,0 +1,72 @@
/**
* This file was automatically generated from Probe.cs
**/
package com.Microsoft.Z3;
/* using System; */
/* using System.Runtime.InteropServices; */
/**
* Probes are used to inspect a goal (aka problem) and collect information that may be used to decide
* which solver and/or preprocessing step will be used.
* The complete list of probes may be obtained using the procedures <code>Context.NumProbes</code>
* and <code>Context.ProbeNames</code>.
* It may also be obtained using the command <code>(help-tactics)</code> in the SMT 2.0 front-end.
**/
public class Probe extends Z3Object
{
/**
* Execute the probe over the goal.
* @return A probe always produce a double value.
* "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.
**/
public double Apply(Goal g)
{
Context.CheckContextMatch(g);
return Native.probeApply(Context.nCtx, NativeObject, g.NativeObject);
}
/**
* Apply the probe to a goal.
**/
public double this[Goal()
return Apply(g); } }
Probe(Context ctx, IntPtr obj)
{ super(ctx, obj);
Probe(Context ctx, String name)
{ super(ctx, Native.mkProbe(ctx.nCtx, name));
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.probeIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.probeDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.Probe_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.Probe_DRQ.Add(o);
super.DecRef(o);
}
}

198
src/api/java/com/Microsoft/Z3/Quantifier.java Normal file
View file

@ -0,0 +1,198 @@
/**
* This file was automatically generated from Quantifier.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Quantifier expressions.
**/
public class Quantifier extends BoolExpr
{
/**
* Indicates whether the quantifier is universal.
**/
public boolean IsUniversal() { return Native.isQuantifierForall(Context.nCtx, NativeObject) != 0; }
/**
* Indicates whether the quantifier is existential.
**/
public boolean IsExistential() { return !IsUniversal; }
/**
* The weight of the quantifier.
**/
public long Weight() { return Native.getQuantifierWeight(Context.nCtx, NativeObject); }
/**
* The number of patterns.
**/
public long NumPatterns() { return Native.getQuantifierNumPatterns(Context.nCtx, NativeObject); }
/**
* The patterns.
**/
public Pattern[] Patterns()
{
long n = NumPatterns;
Pattern[] res = new Pattern[n];
for (long i = 0; i < n; i++)
res[i] = new Pattern(Context, Native.getQuantifierPatternAst(Context.nCtx, NativeObject, i));
return res;
}
/**
* The number of no-patterns.
**/
public long NumNoPatterns() { return Native.getQuantifierNumNoPatterns(Context.nCtx, NativeObject); }
/**
* The no-patterns.
**/
public Pattern[] NoPatterns()
{
long n = NumNoPatterns;
Pattern[] res = new Pattern[n];
for (long i = 0; i < n; i++)
res[i] = new Pattern(Context, Native.getQuantifierNoPatternAst(Context.nCtx, NativeObject, i));
return res;
}
/**
* The number of bound variables.
**/
public long NumBound() { return Native.getQuantifierNumBound(Context.nCtx, NativeObject); }
/**
* The symbols for the bound variables.
**/
public Symbol[] BoundVariableNames()
{
long n = NumBound;
Symbol[] res = new Symbol[n];
for (long i = 0; i < n; i++)
res[i] = Symbol.Create(Context, Native.getQuantifierBoundName(Context.nCtx, NativeObject, i));
return res;
}
/**
* The sorts of the bound variables.
**/
public Sort[] BoundVariableSorts()
{
long n = NumBound;
Sort[] res = new Sort[n];
for (long i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.getQuantifierBoundSort(Context.nCtx, NativeObject, i));
return res;
}
/**
* The body of the quantifier.
**/
public BoolExpr Body() {
return new BoolExpr(Context, Native.getQuantifierBody(Context.nCtx, NativeObject)); }
}
Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body,
long weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
Symbol quantifierID = null, Symbol skolemID = null
)
{ super(ctx);
Context.CheckContextMatch(patterns);
Context.CheckContextMatch(noPatterns);
Context.CheckContextMatch(sorts);
Context.CheckContextMatch(names);
Context.CheckContextMatch(body);
if (sorts.Length != names.Length)
throw new Z3Exception("Number of sorts does not match number of names");
IntPtr[] _patterns = AST.ArrayToNative(patterns);
if (noPatterns == null && quantifierID == null && skolemID == null)
{
NativeObject = Native.mkQuantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
Symbol.ArrayToNative(names),
body.NativeObject);
else
{
NativeObject = Native.mkQuantifierEx(ctx.nCtx, (isForall) ? 1 : 0, weight,
AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
Symbol.ArrayToNative(names),
body.NativeObject);
}
}
Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body,
long weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
Symbol quantifierID = null, Symbol skolemID = null
)
{ super(ctx);
Context.CheckContextMatch(noPatterns);
Context.CheckContextMatch(patterns);
//Context.CheckContextMatch(bound);
Context.CheckContextMatch(body);
if (noPatterns == null && quantifierID == null && skolemID == null)
{
NativeObject = Native.mkQuantifierConst(ctx.nCtx, (isForall) ? 1 : 0, weight,
AST.ArrayLength(bound), AST.ArrayToNative(bound),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
body.NativeObject);
}
else
{
NativeObject = Native.mkQuantifierConstEx(ctx.nCtx, (isForall) ? 1 : 0, weight,
AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
AST.ArrayLength(bound), AST.ArrayToNative(bound),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
body.NativeObject);
}
}
Quantifier(Context ctx, IntPtr obj) { super(ctx, obj); }
void CheckNativeObject(IntPtr obj)
{
if ((Z3_ast_kind)Native.getAstKind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
throw new Z3Exception("Underlying object is not a quantifier");
super.CheckNativeObject(obj);
}
}

247
src/api/java/com/Microsoft/Z3/Solver.java Normal file
View file

@ -0,0 +1,247 @@
/**
* This file was automatically generated from Solver.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Solvers.
**/
public class Solver extends Z3Object
{
/**
* A string that describes all available solver parameters.
**/
public String Help()
{
return Native.solverGetHelp(Context.nCtx, NativeObject);
}
/**
* Sets the solver parameters.
**/
public void setParameters(Params value)
{
Context.CheckContextMatch(value);
Native.solverSetParams(Context.nCtx, NativeObject, value.NativeObject);
}
/**
* Retrieves parameter descriptions for solver.
**/
public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context, Native.solverGetParamDescrs(Context.nCtx, NativeObject)); }
/**
* The current number of backtracking points (scopes).
* <seealso cref="Pop"/>
* <seealso cref="Push"/>
**/
public long NumScopes() { return Native.solverGetNumScopes(Context.nCtx, NativeObject); }
/**
* Creates a backtracking point.
* <seealso cref="Pop"/>
**/
public void Push()
{
Native.solverPush(Context.nCtx, NativeObject);
}
/**
* Backtracks <paramref name="n"/> backtracking points.
* <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <code>NumScopes</code></remarks>
* <seealso cref="Push"/>
**/
public void Pop(long n)
{
Native.solverPop(Context.nCtx, NativeObject, n);
}
/**
* Resets the Solver.
* <remarks>This removes all assertions from the solver.</remarks>
**/
public void Reset()
{
Native.solverReset(Context.nCtx, NativeObject);
}
/**
* Assert a constraint (or multiple) into the solver.
**/
public void Assert(BoolExpr[] constraints)
{
Context.CheckContextMatch(constraints);
for (BoolExpr.Iterator a = constraints.iterator(); a.hasNext(); )
{
Native.solverAssert(Context.nCtx, NativeObject, a.NativeObject);
}
}
/**
* The number of assertions in the solver.
**/
public long NumAssertions()
{
ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context.nCtx, NativeObject));
return ass.Size;
}
/**
* The set of asserted formulas.
**/
public BoolExpr[] Assertions()
{
ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context.nCtx, NativeObject));
long n = ass.Size;
BoolExpr[] res = new BoolExpr[n];
for (long i = 0; i < n; i++)
res[i] = new BoolExpr(Context, ass[i].NativeObject);
return res;
}
/**
* Checks whether the assertions in the solver are consistent or not.
* <remarks>
* <seealso cref="Model"/>
* <seealso cref="UnsatCore"/>
* <seealso cref="Proof"/>
* </remarks>
**/
public Status Check(Expr[] assumptions)
{
Z3_lboolean r;
if (assumptions == null)
r = (Z3_lboolean)Native.solverCheck(Context.nCtx, NativeObject);
else
r = (Z3_lboolean)Native.solverCheckAssumptions(Context.nCtx, NativeObject, (long)assumptions.Length, AST.ArrayToNative(assumptions));
switch (r)
{
case Z3_lboolean.Z3_L_TRUE: return Status.SATISFIABLE;
case Z3_lboolean.Z3_L_FALSE: return Status.UNSATISFIABLE;
default: return Status.UNKNOWN;
}
}
/**
* The model of the last <code>Check</code>.
* <remarks>
* The result is <code>null</code> if <code>Check</code> was not invoked before,
* if its results was not <code>SATISFIABLE</code>, or if model production is not enabled.
* </remarks>
**/
public Model Model()
{
IntPtr x = Native.solverGetModel(Context.nCtx, NativeObject);
if (x == IntPtr.Zero)
return null;
else
return new Model(Context, x);
}
/**
* The proof of the last <code>Check</code>.
* <remarks>
* The result is <code>null</code> if <code>Check</code> was not invoked before,
* if its results was not <code>UNSATISFIABLE</code>, or if proof production is disabled.
* </remarks>
**/
public Expr Proof()
{
IntPtr x = Native.solverGetProof(Context.nCtx, NativeObject);
if (x == IntPtr.Zero)
return null;
else
return Expr.Create(Context, x);
}
/**
* The unsat core of the last <code>Check</code>.
* <remarks>
* The unsat core is a subset of <code>Assertions</code>
* The result is empty if <code>Check</code> was not invoked before,
* if its results was not <code>UNSATISFIABLE</code>, or if core production is disabled.
* </remarks>
**/
public Expr[] UnsatCore()
{
ASTVector core = new ASTVector(Context, Native.solverGetUnsatCore(Context.nCtx, NativeObject));
long n = core.Size;
Expr[] res = new Expr[n];
for (long i = 0; i < n; i++)
res[i] = Expr.Create(Context, core[i].NativeObject);
return res;
}
/**
* A brief justification of why the last call to <code>Check</code> returned <code>UNKNOWN</code>.
**/
public String ReasonUnknown()
{
return Native.solverGetReasonUnknown(Context.nCtx, NativeObject);
}
/**
* Solver statistics.
**/
public Statistics Statistics()
{
return new Statistics(Context, Native.solverGetStatistics(Context.nCtx, NativeObject));
}
/**
* A string representation of the solver.
**/
public String toString()
{
return Native.solvertoString(Context.nCtx, NativeObject);
}
Solver(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.solverIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.solverDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.Solver_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.Solver_DRQ.Add(o);
super.DecRef(o);
}
}

583
src/api/java/com/Microsoft/Z3/Sort.java Normal file
View file

@ -0,0 +1,583 @@
/**
* This file was automatically generated from Sort.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* The Sort class implements type information for ASTs.
**/
public class Sort extends AST
{
/**
* Comparison operator.
* <param name="a">A Sort</param>
* <param name="b">A Sort</param>
* @return True if <paramref name="a"/> and <paramref name="b"/> are from the same context
* and represent the same sort; false otherwise.
**/
/* Overloaded operators are not translated. */
/**
* Comparison operator.
* <param name="a">A Sort</param>
* <param name="b">A Sort</param>
* @return True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
* or represent different sorts; false otherwise.
**/
/* Overloaded operators are not translated. */
/**
* Equality operator for objects of type Sort.
* <param name="o"></param>
* @return
**/
public boolean Equals(object o)
{
Sort casted = o as Sort;
if (casted == null) return false;
return this == casted;
}
/**
* Hash code generation for Sorts
* @return A hash code
**/
public int GetHashCode()
{
return super.GetHashCode();
}
/**
* Returns a unique identifier for the sort.
**/
public long Id() { return Native.getSortId(Context.nCtx, NativeObject); }
/**
* The kind of the sort.
**/
public Z3_sort_kind SortKind() { return (Z3_sort_kind)Native.getSortKind(Context.nCtx, NativeObject); }
/**
* The name of the sort
**/
public Symbol Name() {
return Symbol.Create(Context, Native.getSortName(Context.nCtx, NativeObject)); }
}
/**
* A string representation of the sort.
**/
public String toString()
{
return Native.sorttoString(Context.nCtx, NativeObject);
/**
* Sort constructor
**/
protected Sort(Context ctx) { super(ctx); }
Sort(Context ctx, IntPtr obj) { super(ctx, obj); }
void CheckNativeObject(IntPtr obj)
{
if (Native.getAstKind(Context.nCtx, obj) != (long)Z3_ast_kind.Z3_SORT_AST)
throw new Z3Exception("Underlying object is not a sort");
super.CheckNativeObject(obj);
}
static Sort Create(Context ctx, IntPtr obj)
{
switch ((Z3_sort_kind)Native.getSortKind(ctx.nCtx, obj))
{
case Z3_sort_kind.Z3_ARRAY_SORT: return new ArraySort(ctx, obj);
case Z3_sort_kind.Z3_BOOL_SORT: return new BoolSort(ctx, obj);
case Z3_sort_kind.Z3_BV_SORT: return new BitVecSort(ctx, obj);
case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj);
case Z3_sort_kind.Z3_INT_SORT: return new IntSort(ctx, obj);
case Z3_sort_kind.Z3_REAL_SORT: return new RealSort(ctx, obj);
case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
default:
throw new Z3Exception("Unknown sort kind");
}
}
}
/**
* A Boolean sort.
**/
public class BoolSort extends Sort
{
BoolSort(Context ctx, IntPtr obj) { super(ctx, obj); }
BoolSort(Context ctx) { super(ctx, Native.mkBooleanSort(ctx.nCtx)); }
};
/**
* An arithmetic sort, i.e., Int or Real.
**/
public class ArithSort extends Sort
{
ArithSort(Context ctx, IntPtr obj) { super(ctx, obj); }
};
/**
* An Integer sort
**/
public class IntSort extends ArithSort
{
IntSort(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
IntSort(Context ctx)
{ super(ctx, Native.mkIntSort(ctx.nCtx));
}
}
/**
* A real sort
**/
public class RealSort extends ArithSort
{
RealSort(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
RealSort(Context ctx)
{ super(ctx, Native.mkRealSort(ctx.nCtx));
}
}
/**
* Bit-vector sorts.
**/
public class BitVecSort extends Sort
{
/**
* The size of the bit-vector sort.
**/
public long Size() { return Native.getBvSortSize(Context.nCtx, NativeObject); }
BitVecSort(Context ctx, IntPtr obj) { super(ctx, obj); }
BitVecSort(Context ctx, long size) { super(ctx, Native.mkBvSort(ctx.nCtx, size)); }
};
/**
* Array sorts.
**/
public class ArraySort extends Sort
{
/**
* The domain of the array sort.
**/
public Sort Domain() {
return Sort.Create(Context, Native.getArraySortDomain(Context.nCtx, NativeObject)); }
}
/**
* The range of the array sort.
**/
public Sort Range() {
return Sort.Create(Context, Native.getArraySortRange(Context.nCtx, NativeObject)); }
}
ArraySort(Context ctx, IntPtr obj) { super(ctx, obj); }
ArraySort(Context ctx, Sort domain, Sort range)
{ super(ctx, Native.mkArraySort(ctx.nCtx, domain.NativeObject, range.NativeObject));
};
/**
* Datatype sorts.
**/
public class DatatypeSort extends Sort
{
/**
* The number of constructors of the datatype sort.
**/
public long NumConstructors() { return Native.getDatatypeSortNumConstructors(Context.nCtx, NativeObject); }
/**
* The constructors.
**/
public FuncDecl[] Constructors()
{
long n = NumConstructors;
FuncDecl[] res = new FuncDecl[n];
for (long i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context.nCtx, NativeObject, i));
return res;
}
/**
* The recognizers.
**/
public FuncDecl[] Recognizers()
{
long n = NumConstructors;
FuncDecl[] res = new FuncDecl[n];
for (long i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.getDatatypeSortRecognizer(Context.nCtx, NativeObject, i));
return res;
}
/**
* The constructor accessors.
**/
public FuncDecl[][] Accessors()
{
long n = NumConstructors;
FuncDecl[][] res = new FuncDecl[n][];
for (long i = 0; i < n; i++)
{
FuncDecl fd = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context.nCtx, NativeObject, i));
long ds = fd.DomainSize;
FuncDecl[] tmp = new FuncDecl[ds];
for (long j = 0; j < ds; j++)
tmp[j] = new FuncDecl(Context, Native.getDatatypeSortConstructorAccessor(Context.nCtx, NativeObject, i, j));
res[i] = tmp;
}
return res;
}
DatatypeSort(Context ctx, IntPtr obj) { super(ctx, obj); }
DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
{ super(ctx, Native.mkDatatype(ctx.nCtx, name.NativeObject, (long)constructors.Length, ArrayToNative(constructors)));
}
};
/**
* Uninterpreted Sorts
**/
public class UninterpretedSort extends Sort
{
UninterpretedSort(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
UninterpretedSort(Context ctx, Symbol s)
{ super(ctx, Native.mkUninterpretedSort(ctx.nCtx, s.NativeObject));
}
}
/**
* Tuple sorts.
**/
public class TupleSort extends Sort
{
/**
* The constructor function of the tuple.
**/
public FuncDecl MkDecl() {
return new FuncDecl(Context, Native.getTupleSortMkDecl(Context.nCtx, NativeObject)); }
}
/**
* The number of fields in the tuple.
**/
public long NumFields() { return Native.getTupleSortNumFields(Context.nCtx, NativeObject); }
/**
* The field declarations.
**/
public FuncDecl[] FieldDecls()
{
long n = NumFields;
FuncDecl[] res = new FuncDecl[n];
for (long i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.getTupleSortFieldDecl(Context.nCtx, NativeObject, i));
return res;
}
TupleSort(Context ctx, Symbol name, long numFields, Symbol[] fieldNames, Sort[] fieldSorts)
{ super(ctx);
IntPtr t = IntPtr.Zero;
NativeObject = Native.mkTupleSort(ctx.nCtx, name.NativeObject, numFields,
Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
t, new IntPtr[numFields]);
}
};
/**
* Enumeration sorts.
**/
public class EnumSort extends Sort
{
/**
* The function declarations of the constants in the enumeration.
**/
public FuncDecl[] ConstDecls() {
return _constdecls; }
}
/**
* The constants in the enumeration.
**/
public Expr[] Consts() {
return _consts; }
}
/**
* The test predicates for the constants in the enumeration.
**/
public FuncDecl[] TesterDecls() {
return _testerdecls;
}
private void ObjectInvariant()
{
}
private FuncDecl[] _constdecls = null, _testerdecls = null;
private Expr[] _consts = null;
EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
{ super(ctx);
int n = enumNames.Length;
IntPtr[] n_constdecls = new IntPtr[n];
IntPtr[] n_testers = new IntPtr[n];
NativeObject = Native.mkEnumerationSort(ctx.nCtx, name.NativeObject, (long)n,
Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
_constdecls = new FuncDecl[n];
for (long i = 0; i < n; i++)
_constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
_testerdecls = new FuncDecl[n];
for (long i = 0; i < n; i++)
_testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
_consts = new Expr[n];
for (long i = 0; i < n; i++)
_consts[i] = ctx.MkApp(_constdecls[i]);
}
};
/**
* List sorts.
**/
public class ListSort extends Sort
{
/**
* The declaration of the nil function of this list sort.
**/
public FuncDecl NilDecl()
return nilDecl; } }
/**
* The empty list.
**/
public Expr Nil()
{
return nilConst;
}
/**
* The declaration of the isNil function of this list sort.
**/
public FuncDecl IsNilDecl()
{
return isNilDecl;
}
/**
* The declaration of the cons function of this list sort.
**/
public FuncDecl ConsDecl()
{
return consDecl;
}
/**
* The declaration of the isCons function of this list sort.
*
**/
public FuncDecl IsConsDecl()
{
return isConsDecl;
}
/**
* The declaration of the head function of this list sort.
**/
public FuncDecl HeadDecl()
{
return headDecl;
}
/**
* The declaration of the tail function of this list sort.
**/
public FuncDecl TailDecl()
{
return tailDecl;
}
private void ObjectInvariant()
{
}
private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl;
private Expr nilConst;
ListSort(Context ctx, Symbol name, Sort elemSort)
{ super(ctx);
IntPtr inil = IntPtr.Zero,
iisnil = IntPtr.Zero,
icons = IntPtr.Zero,
iiscons = IntPtr.Zero,
ihead = IntPtr.Zero,
itail = IntPtr.Zero;
NativeObject = Native.mkListSort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
inil, iisnil, icons, iiscons, ihead, itail);
nilDecl = new FuncDecl(ctx, inil);
isNilDecl = new FuncDecl(ctx, iisnil);
consDecl = new FuncDecl(ctx, icons);
isConsDecl = new FuncDecl(ctx, iiscons);
headDecl = new FuncDecl(ctx, ihead);
tailDecl = new FuncDecl(ctx, itail);
nilConst = ctx.MkConst(nilDecl);
}
};
/**
* Relation sorts.
**/
public class RelationSort extends Sort
{
/**
* The arity of the relation sort.
**/
public long Arity() { return Native.getRelationArity(Context.nCtx, NativeObject); }
/**
* The sorts of the columns of the relation sort.
**/
public Sort[] ColumnSorts()
{
if (m_columnSorts != null)
return m_columnSorts;
long n = Arity;
Sort[] res = new Sort[n];
for (long i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.getRelationColumn(Context.nCtx, NativeObject, i));
return res;
}
private Sort[] m_columnSorts = null;
RelationSort(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
}
/**
* Finite domain sorts.
**/
public class FiniteDomainSort extends Sort
{
/**
* The size of the finite domain sort.
**/
public ulong Size() { ulong res = 0; Native.getFiniteDomainSortSize(Context.nCtx, NativeObject, ref res); return res; }
FiniteDomainSort(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
FiniteDomainSort(Context ctx, Symbol name, ulong size)
{ super(ctx, Native.mkFiniteDomainSort(ctx.nCtx, name.NativeObject, size));
}
}
/**
* Set sorts.
**/
public class SetSort extends Sort
{
SetSort(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
SetSort(Context ctx, Sort ty)
{ super(ctx, Native.mkSetSort(ctx.nCtx, ty.NativeObject));
}
}

167
src/api/java/com/Microsoft/Z3/Statistics.java Normal file
View file

@ -0,0 +1,167 @@
/**
* This file was automatically generated from Statistics.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Objects of this class track statistical information about solvers.
**/
public class Statistics extends Z3Object
{
/**
* Statistical data is organized into pairs of [Key, Entry], where every
* Entry is either a <code>DoubleEntry</code> or a <code>UIntEntry</code>
**/
public class Entry
{
/**
* The key of the entry.
**/
/**
* The uint-value of the entry.
**/
public long UIntValue() { return m_long; }
/**
* The double-value of the entry.
**/
public double DoubleValue() { return m_double; }
/**
* True if the entry is uint-valued.
**/
public boolean IsUInt() { return m_is_long; }
/**
* True if the entry is double-valued.
**/
public boolean IsDouble() { return m_is_double; }
/**
* The string representation of the the entry's value.
**/
public String Value()
{
if (IsUInt)
return m_long.toString();
else if (IsDouble)
return m_double.toString();
else
throw new Z3Exception("Unknown statistical entry type");
}
/**
* The string representation of the Entry.
**/
public String toString()
{
return Key + ": " + Value;
}
private boolean m_is_long = false;
private boolean m_is_double = false;
private long m_long = 0;
private double m_double = 0.0;
Entry(String k, long v) { Key = k; m_is_long = true; m_long = v; }
Entry(String k, double v) { Key = k; m_is_double = true; m_double = v; }
}
/**
* A string representation of the statistical data.
**/
public String toString()
{
return Native.statstoString(Context.nCtx, NativeObject);
}
/**
* The number of statistical data.
**/
public long Size() { return Native.statsSize(Context.nCtx, NativeObject); }
/**
* The data entries.
**/
public Entry[] Entries()
{
long n = Size;
Entry[] res = new Entry[n];
for (long i = 0; i < n; i++)
{
Entry e;
String k = Native.statsGetKey(Context.nCtx, NativeObject, i);
if (Native.statsIsLong(Context.nCtx, NativeObject, i) != 0)
e = new Entry(k, Native.statsGetLongValue(Context.nCtx, NativeObject, i));
else if (Native.statsIsDouble(Context.nCtx, NativeObject, i) != 0)
e = new Entry(k, Native.statsGetDoubleValue(Context.nCtx, NativeObject, i));
else
throw new Z3Exception("Unknown data entry value");
res[i] = e;
}
return res;
}
/**
* The statistical counters.
**/
public String[] Keys()
{
long n = Size;
String[] res = new String[n];
for (long i = 0; i < n; i++)
res[i] = Native.statsGetKey(Context.nCtx, NativeObject, i);
return res;
}
/**
* The value of a particular statistical counter.
* <remarks>Returns null if the key is unknown.</remarks>
**/
public Entry get(String key)
{
long n = Size;
Entry[] es = Entries;
for (long i = 0; i < n; i++)
if (es[i].Key == key)
return es[i];
return null;
}
Statistics(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.statsIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.statsDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.Statistics_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.Statistics_DRQ.Add(o);
super.DecRef(o);
}
}

26
src/api/java/com/Microsoft/Z3/Status.java Normal file
View file

@ -0,0 +1,26 @@
/**
* This file was automatically generated from Status.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Status values.
**/
/**
* Used to signify an unsatisfiable status.
**/
UNSATISFIABLE = -1,
/**
* Used to signify an unknown status.
**/
UNKNOWN = 0,
/**
* Used to signify a satisfiable status.
**/
SATISFIABLE = 1

140
src/api/java/com/Microsoft/Z3/Symbol.java Normal file
View file

@ -0,0 +1,140 @@
/**
* This file was automatically generated from Symbol.cs
**/
package com.Microsoft.Z3;
/* using System; */
/* using System.Runtime.InteropServices; */
/**
* Symbols are used to name several term and type constructors.
**/
public class Symbol extends Z3Object
{
/**
* The kind of the symbol (int or string)
**/
protected Z3_symbol_kind Kind
{
get { return (Z3_symbol_kind)Native.getSymbolKind(Context.nCtx, NativeObject); }
}
/**
* Indicates whether the symbol is of Int kind
**/
public boolean IsIntSymbol()
{
return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
}
/**
* Indicates whether the symbol is of string kind.
**/
public boolean IsStringSymbol()
{
return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
}
/**
* A string representation of the symbol.
**/
public String toString()
{
if (IsIntSymbol())
return ((IntSymbol)this).Int.toString();
else if (IsStringSymbol())
return ((StringSymbol)this).String;
else
throw new Z3Exception("Unknown symbol kind encountered");
}
/**
* Symbol constructor
**/
protected Symbol(Context ctx, IntPtr obj) { super(ctx, obj);
}
static Symbol Create(Context ctx, IntPtr obj)
{
switch ((Z3_symbol_kind)Native.getSymbolKind(ctx.nCtx, obj))
{
case Z3_symbol_kind.Z3_INT_SYMBOL: return new IntSymbol(ctx, obj);
case Z3_symbol_kind.Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj);
default:
throw new Z3Exception("Unknown symbol kind encountered");
}
}
}
/**
* Numbered symbols
**/
public class IntSymbol extends Symbol
{
/**
* The int value of the symbol.
* <remarks>Throws an exception if the symbol is not of int kind. </remarks>
**/
public int Int()
{
if (!IsIntSymbol())
throw new Z3Exception("Int requested from non-Int symbol");
return Native.getSymbolInt(Context.nCtx, NativeObject);
}
IntSymbol(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
IntSymbol(Context ctx, int i)
{ super(ctx, Native.mkIntSymbol(ctx.nCtx, i));
}
void CheckNativeObject(IntPtr obj)
{
if ((Z3_symbol_kind)Native.getSymbolKind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
throw new Z3Exception("Symbol is not of integer kind");
super.CheckNativeObject(obj);
}
}
/**
* Named symbols
**/
public class StringSymbol extends Symbol
{
/**
* The string value of the symbol.
* <remarks>Throws an exception if the symbol is not of string kind.</remarks>
**/
public String String()
{
if (!IsStringSymbol())
throw new Z3Exception("String requested from non-String symbol");
return Native.getSymbolString(Context.nCtx, NativeObject);
}
StringSymbol(Context ctx, IntPtr obj) { super(ctx, obj);
}
StringSymbol(Context ctx, String s) { super(ctx, Native.mkStringSymbol(ctx.nCtx, s));
}
void CheckNativeObject(IntPtr obj)
{
if ((Z3_symbol_kind)Native.getSymbolKind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
throw new Z3Exception("Symbol is not of String kind");
super.CheckNativeObject(obj);
}
}

107
src/api/java/com/Microsoft/Z3/Tactic.java Normal file
View file

@ -0,0 +1,107 @@
/**
* This file was automatically generated from Tactic.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Tactics are the basic building block for creating custom solvers for specific problem domains.
* The complete list of tactics may be obtained using <code>Context.NumTactics</code>
* and <code>Context.TacticNames</code>.
* It may also be obtained using the command <code>(help-tactics)</code> in the SMT 2.0 front-end.
**/
public class Tactic extends Z3Object
{
/**
* A string containing a description of parameters accepted by the tactic.
**/
public String Help()
{
return Native.tacticGetHelp(Context.nCtx, NativeObject);
}
/**
* Retrieves parameter descriptions for Tactics.
**/
public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context, Native.tacticGetParamDescrs(Context.nCtx, NativeObject)); }
/**
* Execute the tactic over the goal.
**/
public ApplyResult Apply(Goal g, Params p)
{
Context.CheckContextMatch(g);
if (p == null)
return new ApplyResult(Context, Native.tacticApply(Context.nCtx, NativeObject, g.NativeObject));
else
{
Context.CheckContextMatch(p);
return new ApplyResult(Context, Native.tacticApplyEx(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
}
}
/**
* Apply the tactic to a goal.
**/
public ApplyResult get(Goal g)
{
return Apply(g);
}
/**
* Creates a solver that is implemented using the given tactic.
* <seealso cref="Context.MkSolver(Tactic)"/>
**/
public Solver Solver()
{
return Context.MkSolver(this);
}
Tactic(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
Tactic(Context ctx, String name)
{ super(ctx, Native.mkTactic(ctx.nCtx, name));
}
class DecRefQueue extends Z3.DecRefQueue
{
public void IncRef(Context ctx, IntPtr obj)
{
Native.tacticIncRef(ctx.nCtx, obj);
}
public void DecRef(Context ctx, IntPtr obj)
{
Native.tacticDecRef(ctx.nCtx, obj);
}
};
void IncRef(IntPtr o)
{
Context.Tactic_DRQ.IncAndClear(Context, o);
super.IncRef(o);
}
void DecRef(IntPtr o)
{
Context.Tactic_DRQ.Add(o);
super.DecRef(o);
}
}

BIN
src/api/java/com/Microsoft/Z3/Version.class Normal file
View file

Binary file not shown.

68
src/api/java/com/Microsoft/Z3/Version.java Normal file
View file

@ -0,0 +1,68 @@
/**
* This file was automatically generated from Version.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Version information.
* <remarks>Note that this class is static.</remarks>
**/
public final class Version
{
Version() { }
/**
* The major version
**/
public long Major()
{
long major = 0, minor = 0, build = 0, revision = 0;
Native.getVersion(major, minor, build, revision);
return major;
}
/**
* The minor version
**/
public long Minor()
{
long major = 0, minor = 0, build = 0, revision = 0;
Native.getVersion(major, minor, build, revision);
return minor;
}
/**
* The build version
**/
public long Build()
{
long major = 0, minor = 0, build = 0, revision = 0;
Native.getVersion(major, minor, build, revision);
return build;
}
/**
* The revision
**/
public long Revision()
{
long major = 0, minor = 0, build = 0, revision = 0;
Native.getVersion(major, minor, build, revision);
return revision;
}
/**
* A string representation of the version information.
**/
public String toString()
{
long major = 0, minor = 0, build = 0, revision = 0;
Native.getVersion(major, minor, build, revision);
return major.toString() + "." + minor.toString() + "." + build.toString() + "." + revision.toString();
}
}

28
src/api/java/com/Microsoft/Z3/Z3Exception.java Normal file
View file

@ -0,0 +1,28 @@
/**
* This file was automatically generated from Z3Exception.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* The exception base class for error reporting from Z3
**/
public class Z3Exception extends Exception
{
/**
* Constructor.
**/
public Z3Exception() { super(); }
/**
* Constructor.
**/
public Z3Exception(String message) { super(message); }
/**
* Constructor.
**/
public Z3Exception(String message, System.Exception inner) { super(message, inner); }
}

120
src/api/java/com/Microsoft/Z3/Z3Object.java Normal file
View file

@ -0,0 +1,120 @@
/**
* This file was automatically generated from Z3Object.cs
**/
package com.Microsoft.Z3;
/* using System; */
/**
* Internal base class for interfacing with native Z3 objects.
* Should not be used externally.
**/
public class Z3Object extends IDisposable
{
/**
* Finalizer.
**/
protected void finalize()
{
Dispose();
}
/**
* Disposes of the underlying native Z3 object.
**/
public void Dispose()
{
if (m_n_obj != IntPtr.Zero)
{
DecRef(m_n_obj);
m_n_obj = IntPtr.Zero;
}
if (m_ctx != null)
{
m_ctx.refCount--;
if (m_ctx.refCount == 0)
GC.ReRegisterForFinalize(m_ctx);
m_ctx = null;
}
GC.SuppressFinalize(this);
}
private void ObjectInvariant()
{
}
private Context m_ctx = null;
private IntPtr m_n_obj = IntPtr.Zero;
Z3Object(Context ctx)
{
ctx.refCount++;
m_ctx = ctx;
}
Z3Object(Context ctx, IntPtr obj)
{
ctx.refCount++;
m_ctx = ctx;
IncRef(obj);
m_n_obj = obj;
}
void IncRef(IntPtr o) { }
void DecRef(IntPtr o) { }
void CheckNativeObject(IntPtr obj) { }
IntPtr NativeObject
{
get { return m_n_obj; }
set
{
if (value != IntPtr.Zero) { CheckNativeObject(value); IncRef(value); }
if (m_n_obj != IntPtr.Zero) { DecRef(m_n_obj); }
m_n_obj = value;
}
}
static IntPtr GetNativeObject(Z3Object s)
{
if (s == null) return new IntPtr();
return s.NativeObject;
}
Context Context
{
get
{
return m_ctx;
}
}
static IntPtr[] ArrayToNative(Z3Object[] a)
{
if (a == null) return null;
IntPtr[] an = new IntPtr[a.Length];
for (long i = 0; i < a.Length; i++)
if (a[i] != null) an[i] = a[i].NativeObject;
return an;
}
static long ArrayLength(Z3Object[] a)
{
return (a == null)?0:(long)a.Length;
}
}

279
src/api/java/mk_java.py Normal file
View file

@ -0,0 +1,279 @@
############################################
# Copyright (c) 2012 Microsoft Corporation
#
# Auxiliary scripts for generating Java bindings
# from the managed API.
#
# Author: Christoph M. Wintersteiger (cwinter)
############################################
CS="../dotnet/"
EXT=".cs"
EXCLUDE=["Enumerations.cs", "Native.cs", "AssemblyInfo.cs"]
OUTDIR="com/Microsoft/Z3/"
import os
import fileinput
import string
import re
def mk_java_bindings():
print "Generating Java bindings (from C# bindings in " + CS + ")."
for root, dirs, files in os.walk(CS):
for fn in files:
if not fn in EXCLUDE and fn.endswith(EXT):
translate(fn)
def subst_getters(s, getters):
for g in getters:
s = s.replace(g, g + "()")
def type_replace(s):
s = s.replace("bool", "boolean")
s = s.replace("uint", "long")
s = s.replace("string", "String")
return s
def rename_native(s):
while s.find("Native.Z3") != -1:
i0 = s.find("Native.Z3")
i1 = s.find("(", i0)
c0 = s[:i0]
c1 = s[i0:i1]
c1 = c1.replace("Native.Z3_", "Native.")
c2 = s[i1:]
lc_callback = lambda pat: pat.group("id").upper()
c1 = re.sub("_(?P<id>\w)", lc_callback, c1)
s = c0 + c1 + c2
return s
def translate(filename):
tgtfn = OUTDIR + filename.replace(EXT, ".java")
print "Translating " + filename + " to " + tgtfn
tgt = open(tgtfn, "w")
in_header = 0
in_class = 0
in_static_class = 0
in_javadoc = 0
lastindent = 0
skip_brace = 0
in_getter = ""
in_getter_type = ""
in_unsupported = 0
getters = []
in_bracket_op = 0
in_getter_get = 0
in_getter_set = 0
for line in fileinput.input(os.path.join(CS, filename)):
s = string.rstrip(string.lstrip(line))
if in_javadoc:
if s.startswith("///"):
lastindent = line.find(s);
if s.startswith("/// </summary>"):
pass
else:
a = line
a = a.replace("<c>", "<code>")
a = a.replace("</c>", "</code>")
a = a.replace("///"," *")
a = a.replace("<returns>","@return ")
a = a.replace("</returns>","")
tgt.write(a)
else:
t = ""
for i in range(0, lastindent):
t += " "
tgt.write(t + " **/\n")
in_javadoc = 0
if in_unsupported:
if s == "}":
in_unsupported = 0
elif not in_javadoc:
if not in_header and s.find("/*++") != -1:
in_header = 1
tgt.write("/**\n")
elif in_header and s.startswith("--*/"):
in_header = 0
tgt.write(" * This file was automatically generated from " + filename + " \n")
tgt.write(" **/\n")
tgt.write("\npackage com.Microsoft.Z3;\n")
elif in_header == 1:
# tgt.write(" * " + line.replace(filename, tgtfn))
pass
elif s.startswith("using"):
if s.find("System.Diagnostics.Contracts") == -1:
tgt.write("/* " + s + " */\n")
elif s.startswith("namespace"):
pass
elif s.startswith("public") and s.find("operator") != -1 and (s.find("==") != -1 or s.find("!=") != -1):
t = ""
for i in range(0, line.find(s)+1):
t += " "
tgt.write(t + "/* Overloaded operators are not translated. */\n")
in_unsupported = 1;
elif s.startswith("public class") or s.startswith("internal class") or s.startswith("internal abstract class"):
a = line.replace(":", "extends").replace("internal ", "")
a = a.replace(", IComparable", "")
tgt.write(a)
in_class = 1
in_static_class = 0
elif s.startswith("public static class") or s.startswith("abstract class"):
tgt.write(line.replace(":", "extends").replace("static", "final"))
in_class = 1
in_static_class = 1
elif s.startswith("/// <summary>"):
tgt.write(line.replace("/// <summary>", "/**"))
in_javadoc = 1
elif skip_brace and s == "{":
skip_brace = 0
elif s.find("public") != -1 and s.find("class") == -1 and s.find("event") == -1 and s.find("(") == -1:
if (s.startswith("new")):
s = s[3:]
tokens = s.split(" ")
if len(tokens) == 3:
in_getter = tokens[2]
in_getter_type = type_replace((tokens[0] + " " + tokens[1]))
if in_static_class:
in_getter_type = in_getter_type.replace("static", "")
lastindent = line.find(s)
skip_brace = 1
elif len(tokens) == 4:
if tokens[2].startswith("this["):
in_bracket_op = 1
in_getter = type_replace(tokens[2]).replace("this[", "get(")
in_getter += " " + tokens[3].replace("]", ")")
in_getter_type = type_replace(tokens[0] + " " + tokens[1])
else:
in_getter = tokens[3]
in_getter_type = type_replace(tokens[0] + " " + tokens[1] + " " + tokens[2])
if in_static_class:
in_getter_type = in_getter_type.replace("static", "")
lastindent = line.find(s)
skip_brace = 1
else:
in_getter = tokens[2]
in_getter_type = type_replace(tokens[0] + " " + tokens[1])
if in_static_class:
in_getter_type = in_getter_type.replace("static", "")
rest = s[s.find("get ") + 4:-1]
subst_getters(rest, getters)
rest = type_replace(rest)
rest = rename_native(rest)
t = ""
for i in range(0, lastindent):
t += " "
tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n")
getters.append(in_getter)
print "ACC: " + s + " --> " + in_getter
elif s.find("{ get {") != -1:
line = type_replace(line)
line = line.replace("internal ", "")
d = line[0:line.find("{ get")]
rest = line[line.find("{ get")+5:]
rest = rest.replace("} }", "}")
rest = re.sub("Contract.\w+\([\s\S]*\);", "", rest)
subst_getters(rest, getters)
rest = rename_native(rest)
if in_bracket_op:
tgt.write(d + rest)
else:
tgt.write(d + "()" + rest)
print "ACC: " + s + " --> " + in_getter
elif in_getter != "" and s.startswith("get"):
t = ""
for i in range(0, lastindent):
t += " "
if len(s) > 3: rest = s[3:]
else: rest = ""
subst_getters(rest, getters)
rest = type_replace(rest)
rest = rename_native(rest)
if in_bracket_op:
tgt.write(t + in_getter_type + " " + in_getter + " " + rest + "\n")
else:
tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n")
if rest.find("}") == -1:
in_getter_get = 1
elif in_getter != "" and s.startswith("set"):
t = ""
for i in range(0, lastindent):
t += " "
if len(s) > 3: rest = type_replace(s[3:])
else: rest = ""
subst_getters(rest, getters)
rest = rest.replace("(Integer)value", "Integer(value)")
rest = type_replace(rest)
rest = rename_native(rest)
ac_acc = in_getter_type[:in_getter_type.find(' ')]
ac_type = in_getter_type[in_getter_type.find(' ')+1:]
if in_bracket_op:
in_getter = in_getter.replace("get", "set").replace(")", "")
tgt.write(t + ac_acc + " void " + in_getter + ", " + ac_type + " value) " + rest + "\n")
else:
tgt.write(t + ac_acc + " void set" + in_getter + "(" + ac_type + " value) " + rest + "\n")
if rest.find("}") == -1:
in_getter_set = 1
elif in_getter != "" and in_getter_get and s == "}":
tgt.write(line)
in_getter_get = 0
elif in_getter != "" and in_getter_set and s == "}":
tgt.write(line)
in_getter_set = 0
elif in_getter != "" and not in_getter_get and not in_getter_set and s == "}":
in_getter = ""
in_getter_type == ""
in_bracket_op = 0
skip_brace = 0
elif s.startswith("uint ") and s.find("=") == -1:
line = line.replace("uint", "Integer", line)
line = re.sub("(?P<n>\w+)(?P<c>[,;])", "\g<n>\g<c>", line)
tgt.write(line);
elif (not in_class and (s.startswith("{") or s.startswith("}"))) or s.startswith("[") or s.startswith("#"):
# print "Skipping: " + s;
pass
elif line == "}\n":
pass
else:
# indent = line.find(s)
if line.find(": base") != -1:
line = re.sub(": base\((?P<p>[\w,.\(\) ]*)\)", "{ super(\g<p>);", line)
if line.find("; {") != -1:
line = line.replace("; {", ";")
else:
skip_brace = 1
if s.startswith("public"):
line = re.sub(" = [\w.]+(?P<d>[,;\)])", "\g<d>", line)
a = type_replace(line)
a = re.sub("(?P<d>[\(, ])params ", "\g<d>", a)
a = a.replace("base.", "super.")
a = re.sub("Contract.\w+\([\s\S]*\);", "", a)
a = rename_native(a)
a = re.sub("~\w+\(\)", "protected void finalize()", a)
a = re.sub("foreach\s*\((?P<t>[\w <>,]+)\s+(?P<i>\w+)\s+in\s+(?P<w>\w+)\)",
"for (\g<t>.Iterator \g<i> = \g<w>.iterator(); \g<i>.hasNext(); )", a)
a = a.replace("readonly ", "")
a = a.replace("const ", "final ")
a = a.replace("ToString", "toString")
a = a.replace("internal ", "")
a = a.replace("new static", "static")
a = a.replace("new public", "public")
a = a.replace("override ", "")
a = a.replace("virtual ", "")
a = a.replace("o as AST", "(AST) o")
a = a.replace("other as AST", "(AST) other")
a = a.replace("o as FuncDecl", "(FuncDecl) o")
a = a.replace("IntPtr res = IntPtr.Zero;", "Native.IntPtr res = new Native.IntPtr();")
a = a.replace("out res", "res")
a = a.replace("lock (", "synchronized (")
if in_static_class:
a = a.replace("static", "")
a = re.sub("ref (?P<id>\w+)", "\g<id>", a)
subst_getters(a, getters)
tgt.write(a)
tgt.close()
mk_java_bindings()

2
src/api/python/z3.py
View file

@ -825,7 +825,7 @@ class ExprRef(AstRef):
if is_app(self):
return [self.arg(i) for i in range(self.num_args())]
else:
return []
return []
def _to_expr_ref(a, ctx):
if isinstance(a, Pattern):

2
src/front_end_params/front_end_params.cpp
View file

@ -25,8 +25,6 @@ void front_end_params::register_params(ini_params & p) {
parser_params::register_params(p);
arith_simplifier_params::register_params(p);
model_params::register_params(p);
p.register_unsigned_param("MAX_COUNTEREXAMPLES", m_max_num_cex,
"set the maximum number of counterexamples when using Simplify front end");
p.register_bool_param("AT_LABELS_CEX", m_at_labels_cex,
"only use labels that contain '@' when building multiple counterexamples");
p.register_bool_param("CHECK_AT_LABELS", m_check_at_labels,

4
src/front_end_params/model_params.cpp
View file

@ -21,7 +21,6 @@ Revision History:
void model_params::register_params(ini_params & p) {
p.register_bool_param("MODEL_PARTIAL", m_model_partial, "enable/disable partial function interpretations", true);
p.register_bool_param("MODEL_HIDE_UNUSED_PARTITIONS", m_model_hide_unused_partitions, "hide unused partitions, some partitions are associated with internal terms/formulas created by Z3", true);
p.register_bool_param("MODEL_V1", m_model_v1_pp,
"use Z3 version 1.x pretty printer", true);
p.register_bool_param("MODEL_V2", m_model_v2_pp,
@ -30,8 +29,7 @@ void model_params::register_params(ini_params & p) {
"try to compact function graph (i.e., function interpretations that are lookup tables", true);
p.register_bool_param("MODEL_COMPLETION", m_model_completion,
"assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true);
p.register_bool_param("MODEL_DISPLAY_ARG_SORT", m_model_display_arg_sort,
"display the sort of each argument when printing function interpretations", true);
}

6
src/front_end_params/model_params.h
View file

@ -23,21 +23,17 @@ Revision History:
struct model_params {
bool m_model_partial;
bool m_model_hide_unused_partitions;
bool m_model_compact;
bool m_model_v1_pp;
bool m_model_v2_pp;
bool m_model_completion;
bool m_model_display_arg_sort;
model_params():
m_model_partial(false),
m_model_hide_unused_partitions(true),
m_model_compact(false),
m_model_v1_pp(false),
m_model_v2_pp(false),
m_model_completion(false),
m_model_display_arg_sort(true) {
m_model_completion(false) {
}
void register_params(ini_params & p);

2
src/front_end_params/params2front_end_params.cpp
View file

@ -27,7 +27,6 @@ Revision History:
the new strategy framework.
*/
void params2front_end_params(params_ref const & s, front_end_params & t) {
t.m_quant_elim = s.get_bool(":elim-quant", t.m_quant_elim);
t.m_relevancy_lvl = s.get_uint(":relevancy", t.m_relevancy_lvl);
TRACE("qi_cost", s.display(tout); tout << "\n";);
t.m_qi_cost = s.get_str(":qi-cost", t.m_qi_cost.c_str());
@ -40,7 +39,6 @@ void params2front_end_params(params_ref const & s, front_end_params & t) {
t.m_well_sorted_check = s.get_bool(":check-sorts", t.m_well_sorted_check);
t.m_qi_eager_threshold = s.get_double(":qi-eager-threshold", t.m_qi_eager_threshold);
t.m_qi_lazy_threshold = s.get_double(":qi-lazy-threshold", t.m_qi_lazy_threshold);
t.m_solver = s.get_bool(":solver", t.m_solver);
t.m_preprocess = s.get_bool(":preprocess", t.m_preprocess);
t.m_hi_div0 = s.get_bool(":hi-div0", t.m_hi_div0);
t.m_auto_config = s.get_bool(":auto-config", t.m_auto_config);

2
src/front_end_params/pattern_inference_params.cpp
View file

@ -21,7 +21,7 @@ Revision History:
void pattern_inference_params::register_params(ini_params & p) {
p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns,
"when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern");
p.register_bool_param("PI_BLOCK_LOOOP_PATTERNS", m_pi_block_loop_patterns,
p.register_bool_param("PI_BLOCK_LOOP_PATTERNS", m_pi_block_loop_patterns,
"block looping patterns during pattern inference");
p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast<int&>(m_pi_arith),
"0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms.");

37
src/front_end_params/preprocessor_params.h
View file

@ -31,13 +31,6 @@ enum lift_ite_kind {
LI_FULL
};
enum q_arith_kind {
QA_NONE,
QA_COOPER,
QA_OMEGA,
QA_ALTERNATE
};
struct preprocessor_params : public nnf_params, public cnf_params, public pattern_inference_params,
public bit_blaster_params, public bv_simplifier_params {
lift_ite_kind m_lift_ite;
@ -46,27 +39,20 @@ struct preprocessor_params : public nnf_params, public cnf_params, public patter
bool m_pull_nested_quantifiers;
bool m_eliminate_term_ite;
bool m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
bool m_reverse_implies; // translate (implies a b) into (or b (not a))
bool m_macro_finder;
bool m_solver;
bool m_propagate_values;
bool m_propagate_booleans;
bool m_context_simplifier;
bool m_strong_context_simplifier;
bool m_refine_inj_axiom;
bool m_eliminate_bounds;
bool m_quant_elim;
bool m_nlquant_elim;
bool m_der;
bool m_simplify_bit2int;
bool m_nnf_cnf;
bool m_distribute_forall;
bool m_reduce_args;
bool m_pre_demod;
bool m_quasi_macros;
bool m_restricted_quasi_macros;
bool m_max_bv_sharing;
bool m_pre_simplifier;
bool m_nlquant_elim;
public:
preprocessor_params():
@ -77,25 +63,19 @@ public:
m_eliminate_term_ite(false),
m_eliminate_and(true),
m_macro_finder(false),
m_solver(false),
m_propagate_values(true),
m_propagate_booleans(false), // TODO << check peformance
m_context_simplifier(false),
m_strong_context_simplifier(false),
m_refine_inj_axiom(true),
m_eliminate_bounds(false),
m_quant_elim(false),
m_nlquant_elim(false),
m_der(false),
m_simplify_bit2int(false),
m_nnf_cnf(true),
m_distribute_forall(false),
m_reduce_args(false),
m_pre_demod(false),
m_quasi_macros(false),
m_restricted_quasi_macros(false),
m_max_bv_sharing(true),
m_pre_simplifier(true) {
m_pre_simplifier(true),
m_nlquant_elim(false) {
}
void register_params(ini_params & p) {
@ -109,27 +89,16 @@ public:
p.register_bool_param("ELIM_TERM_ITE", m_eliminate_term_ite, "eliminate term if-then-else in the preprocessor");
p.register_bool_param("ELIM_AND", m_eliminate_and, "represent (and a b) as (not (or (not a) (not b)))");
p.register_bool_param("MACRO_FINDER", m_macro_finder, "try to find universally quantified formulas that can be viewed as macros");
p.register_bool_param("SOLVER", m_solver, "enable solver during preprocessing step", true);
p.register_bool_param("PROPAGATE_VALUES", m_propagate_values, "propagate values during preprocessing step");
p.register_bool_param("PROPAGATE_BOOLEANS", m_propagate_booleans, "propagate boolean values during preprocessing step");
p.register_bool_param("PULL_CHEAP_ITE_TREES", m_pull_cheap_ite_trees);
p.register_bool_param("PULL_NESTED_QUANTIFIERS", m_pull_nested_quantifiers, "eliminate nested quantifiers by moving nested quantified variables to the outermost quantifier, it is unnecessary if the formula is converted into CNF");
p.register_bool_param("CONTEXT_SIMPLIFIER", m_context_simplifier,
"Simplify Boolean sub-expressions if they already appear in context", true);
p.register_bool_param("STRONG_CONTEXT_SIMPLIFIER", m_strong_context_simplifier,
"Simplify Boolean sub-expressions by using full satisfiability queries", true);
p.register_bool_param("REFINE_INJ_AXIOM", m_refine_inj_axiom);
p.register_bool_param("ELIM_BOUNDS", m_eliminate_bounds, "cheap Fourier-Motzkin");
p.register_bool_param("ELIM_QUANTIFIERS", m_quant_elim,
"Use quantifier elimination procedures on Boolean, Bit-vector, Arithmetic and Array variables", true);
p.register_bool_param("ELIM_NLARITH_QUANTIFIERS", m_nlquant_elim,
"Eliminate non-linear quantifiers", true);
p.register_bool_param("DER", m_der);
p.register_bool_param("BIT2INT", m_simplify_bit2int, "hoist bit2int conversions over arithmetical expressions");
p.register_bool_param("DISTRIBUTE_FORALL", m_distribute_forall);
p.register_bool_param("REDUCE_ARGS", m_reduce_args);
p.register_bool_param("PRE_DEMODULATOR", m_pre_demod, "apply demodulators during preprocessing step");
p.register_bool_param("QUASI_MACROS", m_quasi_macros);
p.register_bool_param("RESTRICTED_QUASI_MACROS", m_restricted_quasi_macros);
p.register_bool_param("BV_MAX_SHARING", m_max_bv_sharing);

41
src/muz_qe/dl_context.cpp
View file

@ -352,11 +352,12 @@ namespace datalog {
svector<symbol> names;
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
sorts[i] = vars[i]->get_decl()->get_range();
}
names.push_back(symbol(i));
names.push_back(vars[i]->get_decl()->get_name());
}
quantifier_ref q(m);
sorts.reverse();
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
elim_unused_vars(m, q, result);
}
@ -953,7 +954,6 @@ namespace datalog {
p.insert(":default-relation", CPK_SYMBOL, "default relation implementation: 'external_relation', 'pentagon'");
p.insert(":generate-explanations", CPK_BOOL, "if true, signature of relations will be extended to contain explanations for facts");
p.insert(":explanations-on-relation-level", CPK_BOOL, "if true, explanations are generated as history of each relation, "
"rather than per fact (:generate-explanations must be set to true for this option to have any effect)");
@ -982,6 +982,7 @@ namespace datalog {
p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
PRIVATE_PARAMS(
p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL,
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
@ -1602,11 +1603,27 @@ namespace datalog {
for (unsigned i = 0; i < sz; ++i) {
expr* e = exprs[i];
for_each_expr(v, visited, e);
while (is_quantifier(e)) e = to_quantifier(e)->get_expr();
while (is_quantifier(e)) {
e = to_quantifier(e)->get_expr();
}
fresh_names.add(e);
}
}
void context::get_rules_as_formulas(expr_ref_vector& rules, svector<symbol>& names) {
expr_ref fml(m);
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
for (; it != end; ++it) {
(*it)->to_formula(fml);
rules.push_back(fml);
names.push_back((*it)->name());
}
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
rules.push_back(m_rule_fmls[i].get());
names.push_back(m_rule_names[i]);
}
}
void context::display_smt2(
unsigned num_queries,
expr* const* queries,
@ -1621,18 +1638,8 @@ namespace datalog {
expr_ref_vector rules(m);
svector<symbol> names;
bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
{
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
for (; it != end; ++it) {
(*it)->to_formula(fml);
rules.push_back(fml);
names.push_back((*it)->name());
}
}
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
rules.push_back(m_rule_fmls[i].get());
names.push_back(m_rule_names[i]);
}
get_rules_as_formulas(rules, names);
smt2_pp_environment_dbg env(m);
pp_params params;

5
src/muz_qe/dl_context.h
View file

@ -77,7 +77,6 @@ namespace datalog {
typedef obj_map<const sort, sort_domain*> sort_domain_map;
typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
ast_manager & m;
front_end_params& m_fparams;
params_ref m_params;
@ -250,7 +249,9 @@ namespace datalog {
bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); }
const decl_set & get_output_predicates() const { return m_output_preds; }
rule_set const & get_rules() { return m_rule_set; }
rule_set const & get_rules() { flush_add_rules(); return m_rule_set; }
void get_rules_as_formulas(expr_ref_vector& fmls, svector<symbol>& names);
void add_fact(app * head);
void add_fact(func_decl * pred, const relation_fact & fact);

12
src/muz_qe/dl_smt_relation.cpp
View file

@ -130,7 +130,9 @@ namespace datalog {
IF_VERBOSE(10, verbose_stream() << "Checking emptiness...\n"; );
front_end_params& params = get_plugin().get_fparams();
flet<bool> flet2(params.m_der, true);
// [Leo]: asserted_formulas do not have support for der.
// We should use the tactics der.
// flet<bool> flet2(params.m_der, true);
smt::kernel ctx(m, params);
expr_ref tmp(m);
instantiate(r, tmp);
@ -181,9 +183,13 @@ namespace datalog {
fml_free = m.mk_and(facts, m.mk_not(get_relation()));
instantiate(fml_free, fml_inst);
front_end_params& params = get_plugin().get_fparams();
flet<bool> flet0(params.m_quant_elim, true);
// [Leo]: asserted_formulas do not have support for qe nor der.
// We should use the tactics qe and der.
// BTW, qe at asserted_formulas was disabled when we moved to codeplex, but the field m_quant_elim was not deleted.
//
// flet<bool> flet0(params.m_quant_elim, true);
flet<bool> flet1(params.m_nnf_cnf, false);
flet<bool> flet2(params.m_der, true);
// flet<bool> flet2(params.m_der, true);
smt::kernel ctx(m, params);
ctx.assert_expr(fml_inst);
lbool result = ctx.check();

18
src/muz_qe/pdr_context.cpp
View file

@ -1140,6 +1140,19 @@ namespace pdr {
e->get_data().m_value->add_rule(pred_rules[i]);
}
}
datalog::rule_set::iterator rit = rules.begin(), rend = rules.end();
for (; rit != rend; ++rit) {
datalog::rule* r = *rit;
pred_transformer* pt;
unsigned utz = r->get_uninterpreted_tail_size();
for (unsigned i = 0; i < utz; ++i) {
func_decl* pred = r->get_decl(i);
if (!rels.find(pred, pt)) {
pt = alloc(pred_transformer, *this, get_pdr_manager(), pred);
rels.insert(pred, pt);
}
}
}
// Initialize use list dependencies
decl2rel::iterator it = rels.begin(), end = rels.end();
for (; it != end; ++it) {
@ -1149,10 +1162,7 @@ namespace pdr {
obj_hashtable<func_decl>::iterator itf = deps.begin(), endf = deps.end();
for (; itf != endf; ++itf) {
TRACE("pdr", tout << mk_pp(pred, m) << " " << mk_pp(*itf, m) << "\n";);
if (!rels.find(*itf, pt_user)) {
pt_user = alloc(pred_transformer, *this, get_pdr_manager(), *itf);
rels.insert(*itf, pt_user);
}
VERIFY (rels.find(*itf, pt_user));
pt_user->add_use(pt);
}
}

2
src/muz_qe/pdr_dl_interface.cpp
View file

@ -246,7 +246,7 @@ proof_ref dl_interface::get_proof() {
}
void dl_interface::collect_params(param_descrs& p) {
p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object");
p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract "

2
src/muz_qe/qe_lite.cpp
View file

@ -342,8 +342,6 @@ class der2 {
void flatten_args(quantifier* q, unsigned& num_args, expr*const*& args) {
expr * e = q->get_expr();
num_args = 1;
args = &e;
if ((q->is_forall() && m.is_or(e)) ||
(q->is_exists() && m.is_and(e))) {
num_args = to_app(e)->get_num_args();

104
src/smt/arith_solver_plugin.cpp
View file

@ -1,104 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
arith_solver_plugin.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-30.
Revision History:
--*/
#include"arith_solver_plugin.h"
#include"ast_pp.h"
arith_solver_plugin::arith_solver_plugin(arith_simplifier_plugin & simp):
solver_plugin(symbol("arith"), simp.get_manager()),
m_simplifier(simp) {
}
bool arith_solver_plugin::solve(expr * lhs, expr * rhs, expr_mark const & forbidden, app_ref & var, expr_ref & subst) {
rational k;
if (!m_simplifier.is_numeral(rhs, k))
return false;
bool _is_int = m_simplifier.is_int(lhs);
ptr_buffer<expr> monomials;
ptr_buffer<expr> todo;
bool already_found = false;
rational c;
todo.push_back(lhs);
while (!todo.empty()) {
expr * curr = todo.back();
todo.pop_back();
rational coeff;
if (m_simplifier.is_add(curr)) {
SASSERT(to_app(curr)->get_num_args() == 2);
todo.push_back(to_app(curr)->get_arg(1));
todo.push_back(to_app(curr)->get_arg(0));
}
else {
if (!already_found) {
if (m_simplifier.is_mul(curr) &&
m_simplifier.is_numeral(to_app(curr)->get_arg(0), coeff) && !coeff.is_zero() && (!_is_int || coeff.is_minus_one()) &&
is_uninterp_const(to_app(curr)->get_arg(1)) &&
!forbidden.is_marked(to_app(curr)->get_arg(1))) {
c = coeff;
var = to_app(to_app(curr)->get_arg(1));
already_found = true;
}
else if (is_uninterp_const(curr) && !forbidden.is_marked(curr)) {
c = rational::one();
var = to_app(curr);
already_found = true;
}
else {
monomials.push_back(curr);
}
}
else {
monomials.push_back(curr);
}
}
}
if (!already_found)
return false;
SASSERT(!c.is_zero());
k /= c;
expr_ref_vector new_monomials(m_manager);
if (!k.is_zero())
new_monomials.push_back(m_simplifier.mk_numeral(k, _is_int));
c.neg();
expr_ref inv_c(m_manager);
if (!c.is_one()) {
rational inv(1);
inv /= c;
inv_c = m_simplifier.mk_numeral(inv, _is_int);
}
// divide monomials by c
unsigned sz = monomials.size();
for (unsigned i = 0; i < sz; i++) {
expr * m = monomials[i];
expr_ref new_m(m_manager);
if (!c.is_one())
m_simplifier.mk_mul(inv_c, m, new_m);
else
new_m = m;
new_monomials.push_back(new_m);
}
if (new_monomials.empty())
subst = m_simplifier.mk_numeral(rational(0), _is_int);
else
m_simplifier.mk_add(new_monomials.size(), new_monomials.c_ptr(), subst);
TRACE("arith_solver", tout << "solving:\n" << mk_pp(lhs, m_manager) << "\n" << mk_pp(rhs, m_manager)
<< "\nresult:\n" << mk_pp(var, m_manager) << "\n" << mk_pp(subst, m_manager) << "\n";);
return true;
}

34
src/smt/arith_solver_plugin.h
View file

@ -1,34 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
arith_solver_plugin.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-30.
Revision History:
--*/
#ifndef _ARITH_SOLVER_PLUGIN_H_
#define _ARITH_SOLVER_PLUGIN_H_
#include"solver_plugin.h"
#include"arith_simplifier_plugin.h"
class arith_solver_plugin : public solver_plugin {
arith_simplifier_plugin & m_simplifier;
public:
arith_solver_plugin(arith_simplifier_plugin & simp);
virtual ~arith_solver_plugin() {}
virtual bool solve(expr * lhs, expr * rhs, expr_mark const & forbidden, app_ref & var, expr_ref & subst);
};
#endif /* _ARITH_SOLVER_PLUGIN_H_ */

597
src/smt/asserted_formulas.cpp
View file

@ -19,13 +19,10 @@ Revision History:
#include"asserted_formulas.h"
#include"ast_ll_pp.h"
#include"ast_pp.h"
#include"ast_smt2_pp.h"
#include"arith_simplifier_plugin.h"
#include"array_simplifier_plugin.h"
#include"datatype_simplifier_plugin.h"
#include"bv_simplifier_plugin.h"
#include"arith_solver_plugin.h"
#include"occurs.h"
#include"for_each_expr.h"
#include"well_sorted.h"
#include"pull_ite_tree.h"
@ -34,7 +31,6 @@ Revision History:
#include"pattern_inference.h"
#include"nnf.h"
#include"cnf.h"
#include"expr_context_simplifier.h"
#include"bv_elim.h"
#include"inj_axiom.h"
#include"der.h"
@ -54,8 +50,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, front_end_params & p):
m_asserted_formulas(m),
m_asserted_formula_prs(m),
m_asserted_qhead(0),
m_subst(m),
m_vars_qhead(0),
m_macro_manager(m, m_simplifier),
m_bit2int(m),
m_bv_sharing(m),
@ -68,7 +62,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, front_end_params & p):
setup_simplifier_plugins(m_simplifier, m_bsimp, arith_simp, m_bvsimp);
SASSERT(m_bsimp != 0);
SASSERT(arith_simp != 0);
m_simplifier.set_subst_map(&m_subst);
m_macro_finder = alloc(macro_finder, m_manager, m_macro_manager);
basic_simplifier_plugin * basic_simp = 0;
@ -171,7 +164,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
expr_ref r2(m_manager);
proof_ref pr2(m_manager);
TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m_manager) << "\n";);
TRACE("assert_expr_bug", tout << mk_ismt2_pp(e, m_manager) << "\n";);
TRACE("assert_expr_bug", tout << mk_pp(e, m_manager) << "\n";);
if (m_params.m_pre_simplifier) {
m_pre_simplifier(e, r1, pr1);
}
@ -181,7 +174,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
}
set_eliminate_and(false); // do not eliminate and before nnf.
m_simplifier(r1, r2, pr2);
TRACE("assert_expr_bug", tout << "after...\n" << mk_ismt2_pp(r1, m_manager) << "\n";);
TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m_manager) << "\n";);
if (m_manager.proofs_enabled()) {
if (e == r2)
pr2 = in_pr;
@ -211,8 +204,6 @@ void asserted_formulas::push_scope() {
scope & s = m_scopes.back();
s.m_asserted_formulas_lim = m_asserted_formulas.size();
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead);
s.m_vars_lim = m_vars.size();
s.m_forbidden_vars_lim = m_forbidden_vars.size();
s.m_inconsistent_old = m_inconsistent;
m_defined_names.push_scope();
m_bv_sharing.push_scope();
@ -226,54 +217,21 @@ void asserted_formulas::pop_scope(unsigned num_scopes) {
unsigned new_lvl = m_scopes.size() - num_scopes;
scope & s = m_scopes[new_lvl];
m_inconsistent = s.m_inconsistent_old;
restore_subst(s.m_vars_lim);
restore_forbidden_vars(s.m_forbidden_vars_lim);
m_defined_names.pop_scope(num_scopes);
m_asserted_formulas.shrink(s.m_asserted_formulas_lim);
if (m_manager.proofs_enabled())
m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim);
m_asserted_qhead = s.m_asserted_formulas_lim;
m_vars_qhead = m_vars.size();
m_scopes.shrink(new_lvl);
flush_cache();
TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n"; display(tout););
}
void asserted_formulas::restore_subst(unsigned old_size) {
unsigned sz = m_vars.size();
SASSERT(sz >= old_size);
TRACE("asserted_formulas_bug", tout << "restore_subst, old_size: " << old_size << ", curr_size: " << sz << "\n";);
for (unsigned i = old_size; i < sz; i++) {
SASSERT(is_app(m_vars[i]));
TRACE("asserted_formulas_bug", tout << "removing subst: " << mk_pp(m_vars[i], m_manager) << "\n";);
m_subst.erase(m_vars[i]);
SASSERT(!m_subst.contains(m_vars[i]));
}
if (old_size != sz)
flush_cache();
m_vars.shrink(old_size);
}
void asserted_formulas::restore_forbidden_vars(unsigned old_size) {
unsigned sz = m_forbidden_vars.size();
SASSERT(sz >= old_size);
for (unsigned i = old_size; i < sz; i++) {
TRACE("solver_bug", tout << "unmarking: " << m_forbidden_vars[i]->get_decl()->get_name() << "\n";);
m_forbidden.mark(m_forbidden_vars[i], false);
}
m_forbidden_vars.shrink(old_size);
}
void asserted_formulas::reset() {
m_defined_names.reset();
m_asserted_qhead = 0;
m_asserted_formulas.reset();
m_asserted_formula_prs.reset();
m_subst.reset();
m_vars.reset();
m_vars_qhead = 0;
m_forbidden.reset();
m_forbidden_vars.reset();
m_macro_manager.reset();
m_bv_sharing.reset();
m_inconsistent = false;
@ -315,33 +273,22 @@ void asserted_formulas::reduce() {
INVOKE(m_params.m_propagate_booleans, propagate_booleans());
INVOKE(m_params.m_propagate_values, propagate_values());
INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros());
INVOKE((m_params.m_quant_elim && has_quantifiers()), quant_elim());
INVOKE(m_params.m_nnf_cnf, nnf_cnf());
INVOKE(m_params.m_context_simplifier, context_simplifier());
INVOKE(m_params.m_strong_context_simplifier, strong_context_simplifier());
INVOKE(m_params.m_eliminate_and, eliminate_and());
INVOKE(m_params.m_pull_cheap_ite_trees, pull_cheap_ite_trees());
INVOKE(m_params.m_pull_nested_quantifiers && has_quantifiers(), pull_nested_quantifiers());
INVOKE(m_params.m_ng_lift_ite != LI_NONE, ng_lift_ite());
INVOKE(m_params.m_lift_ite != LI_NONE, lift_ite());
INVOKE(m_params.m_solver, solve());
INVOKE(m_params.m_eliminate_term_ite && m_params.m_lift_ite != LI_FULL, eliminate_term_ite());
INVOKE(m_params.m_refine_inj_axiom && has_quantifiers(), refine_inj_axiom());
TRACE("der_bug", tout << "before DER:\n"; display(tout););
INVOKE(m_params.m_der && has_quantifiers(), apply_der());
TRACE("der_bug", tout << "after DER:\n"; display(tout););
INVOKE(m_params.m_distribute_forall && has_quantifiers(), apply_distribute_forall());
TRACE("qbv_bug", tout << "after distribute_forall:\n"; display(tout););
INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros());
TRACE("qbv_bug", tout << "before demod:\n"; display(tout););
INVOKE(m_params.m_pre_demod && has_quantifiers(), apply_demodulators());
TRACE("qbv_bug", tout << "after demod:\n"; display(tout););
INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros());
INVOKE(m_params.m_simplify_bit2int, apply_bit2int());
INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin());
INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing());
INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers());
INVOKE(m_params.m_bb_quantifiers && m_params.m_der && has_quantifiers(), apply_der()); // bit-vector elimination + bit-blasting creates new opportunities for der.
// temporary HACK: make sure that arith & bv are list-assoc
// this may destroy some simplification steps such as max_bv_sharing
reduce_asserted_formulas();
@ -362,46 +309,6 @@ void asserted_formulas::eliminate_and() {
TRACE("after_elim_and", display(tout););
}
bool asserted_formulas::trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & subst, proof_ref& pr) {
if (is_uninterp_const(lhs) && !m_forbidden.is_marked(lhs)) {
var = to_app(lhs);
subst = rhs;
if (m_manager.proofs_enabled()) {
app* n = m_manager.mk_eq(lhs,rhs);
pr = m_manager.mk_reflexivity(m_manager.mk_iff(n,n));
}
TRACE("solve_bug",
tout << "trivial solve " <<
mk_pp(var, m_manager) << " |-> " <<
mk_pp(subst, m_manager) << "\n";);
return true;
}
else if (is_uninterp_const(rhs) && !m_forbidden.is_marked(rhs)) {
var = to_app(rhs);
subst = lhs;
if (m_manager.proofs_enabled()) {
app* m = m_manager.mk_eq(lhs,rhs);
pr = m_manager.mk_commutativity(m);
}
TRACE("solve_bug",
tout << "trivial solve " <<
mk_pp(var, m_manager) << " |-> " <<
mk_pp(subst, m_manager) << "\n";);
return true;
}
return false;
}
bool asserted_formulas::is_pos_literal(expr * n) {
return is_app(n) && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id;
}
bool asserted_formulas::is_neg_literal(expr * n) {
if (m_manager.is_not(n))
return is_pos_literal(to_app(n)->get_arg(0));
return false;
}
unsigned asserted_formulas::get_formulas_last_level() const {
if (m_scopes.empty()) {
return 0;
@ -411,121 +318,6 @@ unsigned asserted_formulas::get_formulas_last_level() const {
}
}
/**
\brief (ite x (= c1 y) (= c2 y)) where y is a constant. -> (= y (ite x c1 c2))
*/
bool asserted_formulas::solve_ite_definition_core(expr * lhs1, expr * rhs1, expr * lhs2, expr * rhs2, expr * cond, app_ref & var, expr_ref & subst) {
if (rhs1 == rhs2 && is_uninterp_const(rhs1) && !occurs(rhs1, cond) && !occurs(rhs1, lhs1) && !occurs(rhs1, lhs2)) {
var = to_app(rhs1);
m_bsimp->mk_ite(cond, lhs1, lhs2, subst);
return true;
}
return false;
}
bool asserted_formulas::solve_ite_definition(expr * arg1, expr * arg2, expr * arg3, app_ref & var, expr_ref & subst) {
if (!m_manager.is_eq(arg2) || !m_manager.is_eq(arg3))
return false;
app * app2 = to_app(arg2);
app * app3 = to_app(arg3);
expr * lhs1 = app2->get_arg(0);
expr * rhs1 = app2->get_arg(1);
expr * lhs2 = app3->get_arg(0);
expr * rhs2 = app3->get_arg(1);
if (solve_ite_definition_core(lhs1, rhs1, lhs2, rhs2, arg1, var, subst))
return true;
if (solve_ite_definition_core(rhs1, lhs1, lhs2, rhs2, arg1, var, subst))
return true;
if (solve_ite_definition_core(lhs1, rhs1, rhs2, lhs2, arg1, var, subst))
return true;
if (solve_ite_definition_core(rhs1, lhs1, rhs2, lhs2, arg1, var, subst))
return true;
return false;
}
bool asserted_formulas::solve_core(expr * n, app_ref & var, expr_ref & subst, proof_ref& pr) {
if (m_manager.is_eq(n)) {
// equality case
app * eq = to_app(n);
expr * lhs = eq->get_arg(0);
expr * rhs = eq->get_arg(1);
TRACE("solve_bug", tout << mk_bounded_pp(n, m_manager) << "\n" << mk_bounded_pp(lhs, m_manager) << "\n" << mk_bounded_pp(rhs, m_manager) << "\n";);
if (trivial_solve(lhs, rhs, var, subst, pr)) {
return true;
}
else {
sort * s = m_manager.get_sort(lhs);
family_id fid = s->get_family_id();
solver_plugin * p = m_solver_plugins.get_plugin(fid);
if (p != 0 && p->solve(lhs, rhs, m_forbidden, var, subst)) {
if (m_manager.proofs_enabled()) {
app* new_eq = m_manager.mk_eq(var,subst);
pr = m_manager.mk_th_lemma(p->get_family_id(), m_manager.mk_iff(n,new_eq),0,0);
}
TRACE("solve_bug", tout << "theory solve\n";);
return true;
}
}
return false;
}
else if (m_manager.is_iff(n)) {
// <=> case
app * iff = to_app(n);
expr * lhs = iff->get_arg(0);
expr * rhs = iff->get_arg(1);
if (trivial_solve(lhs, rhs, var, subst, pr)) {
return true;
}
return false;
}
else {
if (m_manager.is_ite(n)) {
//
// (ite x (= c1 y) (= c2 y)) where y is a constant. -> (= y (ite x c1 c2))
//
app * ite = to_app(n);
if (solve_ite_definition(ite->get_arg(0), ite->get_arg(1), ite->get_arg(2), var, subst)) {
if (m_manager.proofs_enabled()) {
pr = m_manager.mk_rewrite(n, m_manager.mk_eq(var, subst));
}
return true;
}
}
// check if literal
expr * lit = n;
if (is_pos_literal(lit)) {
var = to_app(lit);
subst = m_manager.mk_true();
if (m_manager.proofs_enabled()) {
// [rewrite]: (iff (iff l true) l)
// [symmetry T1]: (iff l (iff l true))
pr = m_manager.mk_rewrite(m_manager.mk_eq(var, subst), n);
pr = m_manager.mk_symmetry(pr);
}
return true;
}
else if (is_neg_literal(lit)) {
var = to_app(to_app(lit)->get_arg(0));
subst = m_manager.mk_false();
if (m_manager.proofs_enabled()) {
// [rewrite]: (iff (iff l false) ~l)
// [symmetry T1]: (iff ~l (iff l false))
pr = m_manager.mk_rewrite(m_manager.mk_eq(var, subst), n);
pr = m_manager.mk_symmetry(pr);
}
return true;
}
}
return false;
}
void asserted_formulas::collect_static_features() {
if (m_params.m_display_features) {
unsigned sz = m_asserted_formulas.size();
@ -545,7 +337,7 @@ void asserted_formulas::display(std::ostream & out) const {
for (unsigned i = 0; i < m_asserted_formulas.size(); i++) {
if (i == m_asserted_qhead)
out << "[HEAD] ==>\n";
out << mk_ismt2_pp(m_asserted_formulas.get(i), m_manager) << "\n";
out << mk_pp(m_asserted_formulas.get(i), m_manager) << "\n";
}
out << "inconsistent: " << inconsistent() << "\n";
}
@ -563,316 +355,6 @@ void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) co
}
void asserted_formulas::collect_statistics(statistics & st) const {
// m_quant_elim.collect_statistics(st);
}
/**
\brief Functor used to order solved equations x = t, in a way they can be solved
efficiently.
*/
class top_sort {
enum color { White, Grey, Black };
ast_manager & m_manager;
family_id m_bfid;
expr_map * m_candidate_map; // Set of candidate substitutions var -> ast
obj_map<app, unsigned> m_var2idx; // var -> index in vars;
ptr_vector<app> * m_ordered_vars; // Result1: set of variables ordered for applying substitution efficiently.
unsigned_vector * m_failed_idxs; // Result2: indices of substitutions that cannot be applied.
svector<color> m_colors;
ptr_vector<expr> m_todo;
expr * get_candidate_def(expr * n) const {
if (is_app(n) && to_app(n)->get_num_args() == 0 && m_candidate_map->contains(n)) {
expr * d = 0;
proof * p = 0;
m_candidate_map->get(n, d, p);
SASSERT(d);
return d;
}
return 0;
}
bool is_candidate(expr * n) const {
return get_candidate_def(n) != 0;
}
void remove_candidate(app * n) {
TRACE("solve", tout << "removing candidate #" << n->get_id() << " " << mk_bounded_pp(n, m_manager) << "\n";);
unsigned idx = UINT_MAX;
m_var2idx.find(n, idx);
SASSERT(idx != UINT_MAX);
m_candidate_map->erase(n);
m_failed_idxs->push_back(idx);
}
color get_color(expr * n) const {
return m_colors.get(n->get_id(), White);
}
void set_color(expr * n, color c) {
unsigned id = n->get_id();
m_colors.reserve(id+1, White);
m_colors[id] = c;
if (c == Black && is_candidate(n))
m_ordered_vars->push_back(to_app(n));
}
void main_loop(app * n) {
m_todo.push_back(n);
expr * def;
while (!m_todo.empty()) {
expr * n = m_todo.back();
switch (get_color(n)) {
case Black:
m_todo.pop_back();
break;
case White:
set_color(n, Grey);
if (visit_children(n)) {
set_color(n, Black);
}
break;
case Grey:
if (all_black_children(n)) {
set_color(n, Black);
}
else {
def = get_candidate_def(n);
if (def) {
// Break loop
remove_candidate(to_app(n));
set_color(n, Black);
}
// there is another occurrence of n on the stack
SASSERT(std::find(m_todo.begin(), m_todo.end() - 1, n) != m_todo.end());
}
m_todo.pop_back();
}
}
}
void visit(expr * n, bool & visited) {
if (get_color(n) != Black) {
m_todo.push_back(n);
visited = false;
}
}
bool visit_children(expr * n) {
bool visited = true;
unsigned j;
expr * def;
switch (n->get_kind()) {
case AST_VAR:
break;
case AST_APP:
j = to_app(n)->get_num_args();
if (j == 0) {
def = get_candidate_def(n);
if (def)
visit(def, visited);
}
else {
while (j > 0) {
--j;
visit(to_app(n)->get_arg(j), visited);
}
}
break;
case AST_QUANTIFIER:
visit(to_quantifier(n)->get_expr(), visited);
break;
default:
UNREACHABLE();
}
return visited;
}
bool is_black(expr * n) const {
return get_color(n) == Black;
}
bool all_black_children(expr * n) const {
expr * def;
unsigned j;
switch (n->get_kind()) {
case AST_VAR:
return true;
case AST_APP:
j = to_app(n)->get_num_args();
if (j == 0) {
def = get_candidate_def(n);
if (def)
return is_black(def);
return true;
}
else {
while (j > 0) {
--j;
if (!is_black(to_app(n)->get_arg(j))) {
return false;
}
}
}
return true;
case AST_QUANTIFIER:
return is_black(to_quantifier(n)->get_expr());
default:
UNREACHABLE();
return true;
}
}
public:
top_sort(ast_manager & m):m_manager(m), m_bfid(m.get_basic_family_id()) {}
void operator()(ptr_vector<app> const & vars,
expr_map & candidates,
ptr_vector<app> & ordered_vars,
unsigned_vector & failed_idxs) {
m_var2idx.reset();
ptr_vector<app>::const_iterator it = vars.begin();
ptr_vector<app>::const_iterator end = vars.end();
for (unsigned idx = 0; it != end; ++it, ++idx)
m_var2idx.insert(*it, idx);
m_candidate_map = &candidates;
m_ordered_vars = &ordered_vars;
m_failed_idxs = &failed_idxs;
m_colors.reset();
it = vars.begin();
end = vars.end();
for (; it != end; ++it) {
TRACE("top_sort", tout << "processing: " << (*it)->get_decl()->get_name() << "\n";);
main_loop(*it);
}
}
};
void asserted_formulas::get_ordered_subst_vars(ptr_vector<app> & ordered_vars) {
top_sort sort(m_manager);
unsigned_vector failed_idxs;
sort(m_vars, m_subst, ordered_vars, failed_idxs);
SASSERT(failed_idxs.empty());
}
bool asserted_formulas::solve_core() {
flush_cache();
expr_map tmp_subst(m_manager);
ptr_vector<app> tmp_vars; // domain of m_tmp_subst
expr_ref_vector candidates(m_manager);
proof_ref_vector candidate_prs(m_manager);
IF_IVERBOSE(10, verbose_stream() << "solving...\n";);
bool has_subst = false;
app_ref var(m_manager);
expr_ref subst(m_manager);
proof_ref pr1(m_manager);
unsigned i = m_asserted_qhead;
unsigned j = i;
unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
TRACE("solve", tout << "processing... #" << n->get_id() << "\n";);
TRACE("solve", tout << mk_bounded_pp(n, m_manager, 3) << "\n";
if (pr) tout << mk_bounded_pp(pr, m_manager, 3) << "\n";);
if (solve_core(n, var, subst, pr1) && !m_forbidden.is_marked(var)) {
if (m_manager.proofs_enabled()) {
// TODO: refine potentially useless rewrite step
if (m_manager.is_eq(n) && to_app(n)->get_arg(0) == var &&
to_app(n)->get_arg(1) == subst) {
// skip useless rewrite step.
}
else {
TRACE("solve", tout << mk_bounded_pp(n, m_manager, 3) << "\n";
tout << mk_bounded_pp(pr1.get(), m_manager, 5) << "\n";);
pr = m_manager.mk_modus_ponens(pr, pr1.get());
}
candidate_prs.push_back(pr);
}
tmp_subst.insert(var, subst, pr);
SASSERT(!m_forbidden.is_marked(var));
TRACE("solve_subst", tout << mk_pp(var, m_manager) << "\n" << mk_pp(subst, m_manager) << "\n";);
TRACE("solver_bug", tout << mk_pp(var, m_manager) << "\n" << mk_pp(subst, m_manager) << "\n";);
tmp_vars.push_back(var);
m_forbidden.mark(var, true);
candidates.push_back(n);
has_subst = true;
continue;
}
if (j < i) {
m_asserted_formulas.set(j, n);
if (m_manager.proofs_enabled())
m_asserted_formula_prs.set(j, pr);
}
j++;
}
m_asserted_formulas.shrink(j);
if (m_manager.proofs_enabled())
m_asserted_formula_prs.shrink(j);
if (!has_subst)
return false;
ptr_vector<app> ordered_vars;
unsigned_vector failed_idxs;
top_sort sort(m_manager);
sort(tmp_vars, tmp_subst, ordered_vars, failed_idxs);
// restore substitutions that cannot be applied due to loops.
unsigned_vector::iterator it = failed_idxs.begin();
unsigned_vector::iterator end = failed_idxs.end();
for (; it != end; ++it) {
unsigned idx = *it;
m_asserted_formulas.push_back(candidates.get(idx));
if (m_manager.proofs_enabled())
m_asserted_formula_prs.push_back(candidate_prs.get(idx));
app * var = tmp_vars[idx];
m_forbidden.mark(var, false);
}
IF_IVERBOSE(10, verbose_stream() << "num. eliminated vars: " << ordered_vars.size() << "\n";);
ptr_vector<app>::iterator it2 = ordered_vars.begin();
ptr_vector<app>::iterator end2 = ordered_vars.end();
for (; it2 != end2; ++it2) {
app * var = *it2;
TRACE("solve_res", tout << "var: " << mk_pp(var, m_manager) << "\n";);
expr * def = 0;
proof * pr = 0;
tmp_subst.get(var, def, pr);
SASSERT(def != 0);
SASSERT(m_forbidden.is_marked(var));
m_forbidden.mark(var, false);
expr_ref new_def(m_manager);
proof_ref def_eq_new_def_pr(m_manager);
proof_ref new_pr(m_manager);
TRACE("solve_res", tout << "reducing:\n" << mk_ll_pp(def, m_manager););
m_simplifier(def, new_def, def_eq_new_def_pr);
TRACE("solve_res", tout << "reducing:\n" << mk_ll_pp(new_def, m_manager););
new_pr = m_manager.mk_transitivity(pr, def_eq_new_def_pr);
m_subst.insert(var, new_def, new_pr);
m_vars.push_back(var);
TRACE("solve_res", tout << "new substitution:\n" << mk_ll_pp(var, m_manager) << "======>\n" << mk_ll_pp(new_def, m_manager););
}
return !ordered_vars.empty();
}
void asserted_formulas::solve() {
// This method is buggy when unsatisfiable cores are enabled.
// It may eliminate answer literals.
// Since I will remove asserted_formulas.cpp in the future, I just disabled it.
// Note: asserted_formulas.cpp is based on the obsolete preprocessing stack.
// Users should the solve-eqs tactic if they want to eliminate variables.
#if 0
while (solve_core()) {
IF_IVERBOSE(10, verbose_stream() << "reducing...\n";);
flush_cache(); // collect garbage
reduce_asserted_formulas();
}
#endif
}
void asserted_formulas::reduce_asserted_formulas() {
@ -937,24 +419,6 @@ void asserted_formulas::expand_macros() {
find_macros_core();
}
void asserted_formulas::apply_demodulators() {
#if 0
IF_IVERBOSE(10, verbose_stream() << "applying demodulators...\n";);
TRACE("before_apply_demodulators", display(tout););
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
unsigned sz = m_asserted_formulas.size();
ufbv_rewriter proc(m_manager, *m_bsimp);
proc(sz - m_asserted_qhead,
m_asserted_formulas.c_ptr() + m_asserted_qhead,
m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
new_exprs, new_prs);
swap_asserted_formulas(new_exprs, new_prs);
TRACE("after_apply_demodulators", display(tout););
reduce_and_solve();
#endif
}
void asserted_formulas::apply_quasi_macros() {
IF_IVERBOSE(10, verbose_stream() << "finding quasi macros...\n";);
TRACE("before_quasi_macros", display(tout););
@ -1090,8 +554,6 @@ void asserted_formulas::reduce_and_solve() {
IF_IVERBOSE(10, verbose_stream() << "reducing...\n";);
flush_cache(); // collect garbage
reduce_asserted_formulas();
if (m_params.m_solver)
solve();
}
void asserted_formulas::infer_patterns() {
@ -1123,41 +585,8 @@ void asserted_formulas::infer_patterns() {
TRACE("after_pattern_inference", display(tout););
}
struct mark_forbidden_proc {
expr_mark & m_forbidden;
ptr_vector<app> & m_forbidden_vars;
mark_forbidden_proc(expr_mark & f, ptr_vector<app> & v):m_forbidden(f), m_forbidden_vars(v) {}
void operator()(var * n) {}
void operator()(quantifier * n) {}
void operator()(app * n) {
if (is_uninterp(n) && !m_forbidden.is_marked(n)) {
TRACE("solver_bug", tout << "marking: " << n->get_decl()->get_name() << "\n";);
m_forbidden.mark(n, true);
m_forbidden_vars.push_back(n);
SASSERT(m_forbidden.is_marked(n));
}
}
};
void asserted_formulas::commit() {
expr_fast_mark1 uf_visited; // marks used for update_forbidden
mark_forbidden_proc p(m_forbidden, m_forbidden_vars);
unsigned sz = m_asserted_formulas.size();
for (unsigned i = m_asserted_qhead; i < sz; i++)
quick_for_each_expr(p, uf_visited, m_asserted_formulas.get(i));
m_macro_manager.mark_forbidden(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead);
ptr_vector<app>::const_iterator it2 = m_vars.begin() + m_vars_qhead;
ptr_vector<app>::const_iterator end2 = m_vars.end();
for (; it2 != end2; ++it2) {
app * var = *it2;
expr * def = get_subst(var);
m_forbidden.mark(var, true);
m_forbidden_vars.push_back(var);
quick_for_each_expr(p, uf_visited, def);
}
m_vars_qhead = m_vars.size();
m_macro_manager.mark_forbidden(m_asserted_formulas.size() - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead);
m_asserted_qhead = m_asserted_formulas.size();
}
@ -1376,11 +805,6 @@ proof * asserted_formulas::get_inconsistency_proof() const {
return 0;
}
MK_SIMPLE_SIMPLIFIER(context_simplifier, expr_context_simplifier functor(m_manager), "context_simplifier", "context simplifier");
MK_SIMPLE_SIMPLIFIER(strong_context_simplifier, expr_strong_context_simplifier functor(m_params, m_manager), "strong_context_simplifier", "strong context simplifier");
void asserted_formulas::refine_inj_axiom() {
IF_IVERBOSE(10, verbose_stream() << "refining injectivity...\n";);
TRACE("inj_axiom", display(tout););
@ -1406,19 +830,6 @@ void asserted_formulas::refine_inj_axiom() {
MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate bit-vector over integers", true);
MK_SIMPLIFIER(apply_der_core, der_star functor(m_manager), "der", "destructive equality resolution", true);
void asserted_formulas::apply_der() {
// Keep applying DER until it cannot be applied anymore.
// The simplifications applied by REDUCE may create new opportunities for applying DER.
while(!inconsistent() && apply_der_core()) {
}
TRACE("a_der", for (unsigned i = 0; i<m_asserted_formulas.size(); i++)
tout << mk_pp(m_asserted_formulas.get(i), m_manager) << std::endl; );
}
MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap fourier-motzkin", true);
// MK_SIMPLIFIER(quant_elim, qe::expr_quant_elim_star1 &functor = m_quant_elim,

44
src/smt/asserted_formulas.h
View file

@ -26,7 +26,6 @@ Revision History:
#include"macro_manager.h"
#include"macro_finder.h"
#include"defined_names.h"
#include"solver_plugin.h"
#include"maximise_ac_sharing.h"
#include"bit2int.h"
#include"statistics.h"
@ -39,7 +38,7 @@ class asserted_formulas {
ast_manager & m_manager;
front_end_params & m_params;
simplifier m_pre_simplifier;
subst_simplifier m_simplifier;
simplifier m_simplifier;
basic_simplifier_plugin * m_bsimp;
bv_simplifier_plugin * m_bvsimp;
defined_names m_defined_names;
@ -48,19 +47,9 @@ class asserted_formulas {
proof_ref_vector m_asserted_formula_prs; // proofs for the asserted formulas.
unsigned m_asserted_qhead;
expr_map m_subst;
ptr_vector<app> m_vars; // domain of m_subst
unsigned m_vars_qhead;
expr_mark m_forbidden;
ptr_vector<app> m_forbidden_vars;
macro_manager m_macro_manager;
scoped_ptr<macro_finder> m_macro_finder;
typedef plugin_manager<solver_plugin> solver_plugins;
solver_plugins m_solver_plugins;
bit2int m_bit2int;
maximise_bv_sharing m_bv_sharing;
@ -70,50 +59,33 @@ class asserted_formulas {
struct scope {
unsigned m_asserted_formulas_lim;
unsigned m_vars_lim;
unsigned m_forbidden_vars_lim;
bool m_inconsistent_old;
};
svector<scope> m_scopes;
volatile bool m_cancel_flag;
void setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp);
bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & subst, proof_ref& pr);
bool is_pos_literal(expr * n);
bool is_neg_literal(expr * n);
bool solve_ite_definition_core(expr * lhs1, expr * rhs1, expr * lhs2, expr * rhs2, expr * cond, app_ref & var, expr_ref & subst);
bool solve_ite_definition(expr * arg1, expr * arg2, expr * arg3, app_ref & var, expr_ref & subst);
bool solve_core(expr * n, app_ref & var, expr_ref & subst, proof_ref& pr);
bool solve_core();
void solve();
void reduce_asserted_formulas();
void swap_asserted_formulas(expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
void find_macros_core();
void find_macros();
void expand_macros();
void apply_demodulators();
void apply_quasi_macros();
void nnf_cnf();
void infer_patterns();
void eliminate_term_ite();
void reduce_and_solve();
void flush_cache() { m_pre_simplifier.reset(); m_simplifier.reset(); }
void restore_subst(unsigned old_size);
void restore_forbidden_vars(unsigned old_size);
void set_eliminate_and(bool flag);
void propagate_values();
void propagate_booleans();
bool pull_cheap_ite_trees();
bool pull_nested_quantifiers();
void push_assertion(expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs);
void context_simplifier();
void strong_context_simplifier();
void eliminate_and();
void refine_inj_axiom();
bool cheap_quant_fourier_motzkin();
bool quant_elim();
bool apply_der_core();
void apply_der();
void apply_distribute_forall();
bool apply_bit2int();
void lift_ite();
@ -174,20 +146,6 @@ public:
// auxiliary function used to create a logic context based on a model.
void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_macro_manager.insert(f, m, pr); }
// -----------------------------------
//
// Eliminated vars
//
// -----------------------------------
ptr_vector<app>::const_iterator begin_subst_vars() const { return m_vars.begin(); }
ptr_vector<app>::const_iterator end_subst_vars() const { return m_vars.end(); }
ptr_vector<app>::const_iterator begin_subst_vars_last_level() const {
unsigned sidx = m_scopes.empty() ? 0 : m_scopes.back().m_vars_lim;
return m_vars.begin() + sidx;
}
expr * get_subst(app * var) { expr * def = 0; proof * pr; m_subst.get(var, def, pr); return def; }
bool is_subst(app * var) const { return m_subst.contains(var); }
void get_ordered_subst_vars(ptr_vector<app> & ordered_vars);
};
#endif /* _ASSERTED_FORMULAS_H_ */

2
src/smt/expr_context_simplifier.cpp
View file

@ -329,7 +329,6 @@ void expr_strong_context_simplifier::simplify_basic(expr* fml, expr_ref& result)
result = fml;
return;
}
flet<bool> fl1(m_params.m_strong_context_simplifier, false);
ptr_vector<expr> todo;
ptr_vector<expr> names;
@ -480,7 +479,6 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r
result = fml;
return;
}
flet<bool> fl1(m_params.m_strong_context_simplifier, false);
ptr_vector<expr> todo;
ptr_vector<expr> names;

13
src/smt/smt_context.h
View file

@ -1431,19 +1431,6 @@ namespace smt {
func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_asserted_formulas.get_macro_interpretation(i, interp); }
quantifier * get_macro_quantifier(func_decl * f) const { return m_asserted_formulas.get_macro_quantifier(f); }
void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_asserted_formulas.insert_macro(f, m, pr); }
// -----------------------------------
//
// Eliminated vars
//
// -----------------------------------
public:
ptr_vector<app>::const_iterator begin_subst_vars() const { return m_asserted_formulas.begin_subst_vars(); }
ptr_vector<app>::const_iterator end_subst_vars() const { return m_asserted_formulas.end_subst_vars(); }
ptr_vector<app>::const_iterator begin_subst_vars_last_level() const { return m_asserted_formulas.begin_subst_vars_last_level(); }
expr * get_subst(app * var) { return m_asserted_formulas.get_subst(var); }
bool is_subst(app * var) const { return m_asserted_formulas.is_subst(var); }
void get_ordered_subst_vars(ptr_vector<app> & ordered_vars) { return m_asserted_formulas.get_ordered_subst_vars(ordered_vars); }
};
};

73
src/smt/smt_model_generator.cpp
View file

@ -526,8 +526,6 @@ namespace smt {
func_decl * d = n->get_decl();
if (m_model.has_interpretation(d))
return; // declaration already has an interpretation.
if (n->get_num_args() == 0 && m_context.is_subst(n) != 0)
return; // an interpretation will be generated for this variable using the evaluator.
if (n->get_num_args() == 0) {
sort * r = d->get_range();
expr * v = m_model.get_some_value(r);
@ -544,61 +542,6 @@ namespace smt {
};
/**
\brief Generate an interpretation for variables that were eliminated indirectly.
When a variable is eliminated by substitution and it does not occur anywhere, then
its definition may contain declarations that do not occur anywhere else.
This method will assign an arbitrary interpretation for these declarations.
Example: consider the formula
(= x (f y))
This formula is satisfiable. If the solver is used during preprocessing step,
this formula is reduced to "true", and the substitution set contains the entry (x -> (f y)).
The declarations f and y will not have an interpretation. This method will traverse the
definition of each eliminated variable, and generate an arbitrary interpretations for
declarations that do not have one yet.
*/
void model_generator::register_indirect_elim_decls() {
expr_mark visited;
mk_interp_proc proc(*m_context, *m_model);
ptr_vector<app>::const_iterator it = m_context->begin_subst_vars();
ptr_vector<app>::const_iterator end = m_context->end_subst_vars();
for (; it != end; ++it) {
app * var = *it;
if (var->get_num_args() > 0)
continue;
expr * subst = m_context->get_subst(var);
for_each_expr(proc, visited, subst);
}
}
void model_generator::register_subst_vars() {
ptr_vector<app> ordered_subst_vars;
m_context->get_ordered_subst_vars(ordered_subst_vars);
ptr_vector<app>::const_iterator it = ordered_subst_vars.begin();
ptr_vector<app>::const_iterator end = ordered_subst_vars.end();
for (; it != end; ++it) {
app * var = *it;
TRACE("model_subst_vars", tout << "processing: " << mk_pp(var, m_manager) << "\n";);
if (var->get_num_args() > 0) {
TRACE("model_subst_vars", tout << "not a constant...\n";);
continue;
}
expr * subst = m_context->get_subst(var);
if (subst == 0) {
TRACE("model_subst_vars", tout << "no definition...\n";);
continue;
}
TRACE("model_subst_vars", tout << "definition: " << mk_pp(subst, m_manager) << "\n";);
expr_ref r(m_manager);
m_model->eval(subst, r);
TRACE("model_subst_vars", tout << "result: " << mk_pp(r, m_manager) << "\n";);
m_model->register_decl(var->get_decl(), r);
}
}
proto_model * model_generator::mk_model() {
SASSERT(!m_model);
TRACE("func_interp_bug", m_context->display(tout););
@ -609,22 +552,6 @@ namespace smt {
mk_func_interps();
finalize_theory_models();
register_macros();
TRACE("model_subst_vars",
tout << "substitution vars:\n";
ptr_vector<app>::const_iterator it = m_context->begin_subst_vars();
ptr_vector<app>::const_iterator end = m_context->end_subst_vars();
for (; it != end; ++it) {
app * var = *it;
tout << mk_pp(var, m_manager) << "\n";
if (var->get_num_args() > 0)
continue;
expr * subst = m_context->get_subst(var);
if (subst == 0)
continue;
tout << "-> " << mk_bounded_pp(subst, m_manager, 10) << "\n";
});
register_indirect_elim_decls();
register_subst_vars();
return m_model;
}

3
src/smt/smt_model_generator.h
View file

@ -193,8 +193,6 @@ namespace smt {
void display(std::ostream & out);
void register_existing_model_values();
void register_macros();
void register_indirect_elim_decls();
void register_subst_vars();
bool visit_children(source const & src, ptr_vector<enode> const & roots, obj_map<enode, model_value_proc *> const & root2proc,
source2color & colors, obj_hashtable<sort> & already_traversed, svector<source> & todo);
@ -227,3 +225,4 @@ namespace smt {
#endif /* _SMT_MODEL_GENERATOR_H_ */

20
src/smt/smt_setup.cpp
View file

@ -188,7 +188,6 @@ namespace smt {
void setup::setup_QF_UF() {
m_params.m_relevancy_lvl = 0;
m_params.m_solver = true;
m_params.m_nnf_cnf = false;
}
@ -201,7 +200,6 @@ namespace smt {
void setup::setup_QF_UF(static_features const & st) {
check_no_arithmetic(st, "QF_UF");
m_params.m_relevancy_lvl = 0;
m_params.m_solver = true;
m_params.m_nnf_cnf = false;
m_params.m_restart_strategy = RS_LUBY;
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
@ -215,7 +213,6 @@ namespace smt {
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_reflect = false;
m_params.m_solver = true;
m_params.m_arith_propagate_eqs = false;
m_params.m_nnf_cnf = false;
setup_mi_arith();
@ -256,7 +253,6 @@ namespace smt {
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_reflect = false;
m_params.m_solver = true;
m_params.m_arith_propagate_eqs = false;
m_params.m_nnf_cnf = false;
if (is_dense(st)) {
@ -308,7 +304,6 @@ namespace smt {
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_reflect = false;
m_params.m_solver = true;
m_params.m_arith_propagate_eqs = false;
m_params.m_arith_small_lemma_size = 30;
m_params.m_nnf_cnf = false;
@ -327,7 +322,6 @@ namespace smt {
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_reflect = false;
m_params.m_solver = true;
m_params.m_arith_propagate_eqs = false;
m_params.m_arith_small_lemma_size = 30;
m_params.m_nnf_cnf = false;
@ -377,7 +371,6 @@ namespace smt {
TRACE("setup", tout << "setup_QF_UFIDL()\n";);
m_params.m_relevancy_lvl = 0;
m_params.m_arith_reflect = false;
m_params.m_solver = true;
m_params.m_nnf_cnf = false;
m_params.m_arith_eq_bounds = true;
m_params.m_phase_selection = PS_ALWAYS_FALSE;
@ -393,7 +386,6 @@ namespace smt {
throw default_exception("Benchmark has real variables but it is marked as QF_UFIDL (uninterpreted functions and difference logic).");
m_params.m_relevancy_lvl = 0;
m_params.m_arith_reflect = false;
m_params.m_solver = true;
m_params.m_nnf_cnf = false;
if (st.m_num_uninterpreted_functions == 0) {
m_params.m_arith_expand_eqs = true;
@ -434,7 +426,6 @@ namespace smt {
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_eliminate_term_ite = true;
m_params.m_solver = true;
m_params.m_nnf_cnf = false;
setup_mi_arith();
}
@ -446,7 +437,6 @@ namespace smt {
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_eliminate_term_ite = true;
m_params.m_solver = true;
m_params.m_nnf_cnf = false;
if (numerator(st.m_arith_k_sum) > rational(2000000) && denominator(st.m_arith_k_sum) > rational(500)) {
m_params.m_relevancy_lvl = 2;
@ -519,7 +509,6 @@ namespace smt {
void setup::setup_QF_UFLIA() {
m_params.m_relevancy_lvl = 0;
m_params.m_arith_reflect = false;
m_params.m_solver = true;
m_params.m_nnf_cnf = false;
m_params.m_arith_propagation_threshold = 1000;
setup_i_arith();
@ -534,7 +523,6 @@ namespace smt {
void setup::setup_QF_UFLRA() {
m_params.m_relevancy_lvl = 0;
m_params.m_arith_reflect = false;
m_params.m_solver = true;
m_params.m_nnf_cnf = false;
setup_mi_arith();
}
@ -542,7 +530,6 @@ namespace smt {
void setup::setup_QF_BV() {
m_params.m_relevancy_lvl = 0;
m_params.m_arith_reflect = false;
m_params.m_solver = true;
m_params.m_bv_cc = false;
m_params.m_bb_ext_gates = true;
m_params.m_nnf_cnf = false;
@ -552,7 +539,6 @@ namespace smt {
void setup::setup_QF_AUFBV() {
m_params.m_array_mode = AR_SIMPLE;
m_params.m_relevancy_lvl = 0;
m_params.m_solver = true;
m_params.m_bv_cc = false;
m_params.m_bb_ext_gates = true;
m_params.m_nnf_cnf = false;
@ -575,7 +561,6 @@ namespace smt {
}
else {
m_params.m_relevancy_lvl = 2;
m_params.m_solver = true;
}
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
}
@ -609,7 +594,6 @@ namespace smt {
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
m_params.m_random_initial_activity = IA_ZERO;
}
// m_params.m_solver = true;
// if (st.m_num_arith_ineqs == st.m_num_diff_ineqs && st.m_num_arith_eqs == st.m_num_diff_eqs && st.m_arith_k_sum < rational(INT_MAX / 8))
// m_context.register_plugin(new smt::theory_si_arith(m_manager, m_params));
// else
@ -688,14 +672,10 @@ namespace smt {
}
void setup::setup_LRA() {
m_params.m_quant_elim = true;
// after quantifier elimination, the result is a QF_LRA benchmark
m_params.m_relevancy_lvl = 0;
// m_params.m_arith_expand_eqs = true; << may affect quant_elim
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_eliminate_term_ite = true;
m_params.m_solver = true;
setup_mi_arith();
}

51
src/smt/solver_plugin.h
View file

@ -1,51 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
solver_plugin.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-30.
Revision History:
--*/
#ifndef _SOLVER_PLUGIN_H_
#define _SOLVER_PLUGIN_H_
#include"ast.h"
/**
\brief Abstract solver used during preprocessing step.
*/
class solver_plugin {
protected:
ast_manager & m_manager;
family_id m_fid;
public:
solver_plugin(symbol const & fname, ast_manager & m):m_manager(m), m_fid(m.get_family_id(fname)) {}
virtual ~solver_plugin() {}
/**
\brief Return true if it is possible to solve lhs = rhs. The
arg. forbidden contains the set of variables that cannot be
used. Store the result (var = subst) in var and subst.
\remark Only simple solvers are supported. That is, the solution set has only one entry.
*/
virtual bool solve(expr * lhs, expr * rhs, expr_mark const & forbidden, app_ref & var, expr_ref & subst) = 0;
family_id get_family_id() const { return m_fid; }
ast_manager & get_manager() { return m_manager; }
};
#endif /* _SOLVER_PLUGIN_H_ */

2
src/smt/tactic/smt_tactic.cpp
View file

@ -151,7 +151,7 @@ public:
SASSERT(in->is_well_sorted());
ast_manager & m = in->m();
TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
<< " PREPROCESS: " << fparams().m_preprocess << ", SOLVER:" << fparams().m_solver << "\n";
<< " PREPROCESS: " << fparams().m_preprocess << "\n";
tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
tout << "params_ref: " << m_params_ref << "\n";);
TRACE("smt_tactic_detail", in->display(tout););

61
src/tactic/sls/sls_strategy.h
View file

@ -1,61 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
sls_strategy.h
Abstract:
A Stochastic Local Search (SLS) strategy
Author:
Christoph (cwinter) 2011-09-23
Notes:
--*/
#ifndef _SLS_STRATEGY_H_
#define _SLS_STRATEGY_H_
#include"assertion_set_strategy.h"
MK_ST_EXCEPTION(sls_exception);
class sls_st : public assertion_set_strategy {
struct imp;
imp * m_imp;
params_ref m_params;
public:
sls_st(ast_manager & m, params_ref const & p = params_ref());
virtual ~sls_st();
ast_manager & m () const;
virtual void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r);
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
bool is_target(assertion_set const & s) const;
virtual void operator()(assertion_set & s, model_converter_ref & mc);
virtual void cleanup();
virtual void collect_statistics(statistics & st) const;
virtual void reset_statistics();
protected:
virtual void set_cancel(bool f);
};
inline as_st * mk_sls(ast_manager & m, params_ref const & p = params_ref()) {
return clean(alloc(sls_st, m, p));
}
as_st * mk_qfbv_sls_strategy(ast_manager & m, params_ref const & p);
MK_SIMPLE_ST_FACTORY(qfbv_sls_stf, mk_qfbv_sls_strategy(m, p));
#endif

2
src/test/quant_elim.cpp
View file

@ -34,7 +34,7 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons
simplifier simp(m);
front_end_params params;
params.m_quant_elim = true;
// params.m_quant_elim = true;
std::cout << mk_pp(fml, m) << "\n";
qe::expr_quant_elim qe(m, params);

23
src/util/debug.h
View file

@ -74,29 +74,6 @@ bool is_debug_enabled(const char * tag);
#define COMPILE_TIME_ASSERT(expr) extern char DBG_UNIQUE_NAME[expr]
#endif
template<class T>
class class_invariant
{
T* m_class;
char const* m_module;
public:
class_invariant(T* cls) : m_class(cls), m_module(0) {
SASSERT(cls->invariant());
}
class_invariant(T* cls, char const* module) : m_class(cls), m_module(module) {
CASSERT(module, cls->invariant());
}
~class_invariant() {
if (m_module) {
CASSERT(m_module, m_class->invariant());
}
else {
SASSERT(m_class->invariant());
}
}
private:
};
void finalize_debug();
/*
ADD_FINALIZER('finalize_debug();')