From d6964226c7f5d85f443becbf7e9c2d7144d1059f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Oct 2014 15:38:44 -0700 Subject: [PATCH 01/17] indentation Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 2 +- src/smt/smt_quantifier.cpp | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7940b17be..a9fc5c091 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -71,7 +71,7 @@ namespace smt { protected: ast_manager & m_manager; - smt_params & m_fparams; + smt_params & m_fparams; params_ref m_params; setup m_setup; volatile bool m_cancel_flag; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index e9b0e069a..b76fb6c74 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -453,9 +453,9 @@ namespace smt { instantiated. */ virtual void add(quantifier * q) { - if (m_fparams->m_mbqi && mbqi_enabled(q)) { - m_model_finder->register_quantifier(q); - } + if (m_fparams->m_mbqi && mbqi_enabled(q)) { + m_model_finder->register_quantifier(q); + } } virtual void del(quantifier * q) { From 136b172b5a3ef2dd943b1af1534416d9abbe956f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2014 09:58:54 -0700 Subject: [PATCH 02/17] move parameter validation for when solver object is actually crated Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6fc0c1c72..65b2a9047 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -40,6 +40,10 @@ extern "C" { params_ref p = s->m_params; mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled); s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); + + param_descrs r; + s->m_solver->collect_param_descrs(r); + p.validate(r); s->m_solver->updt_params(p); } @@ -130,14 +134,15 @@ extern "C" { Z3_TRY; LOG_Z3_solver_set_params(c, s, p); RESET_ERROR_CODE(); - param_descrs r; - to_solver_ref(s)->collect_param_descrs(r); - to_param_ref(p).validate(r); + if (to_solver(s)->m_solver) { bool old_model = to_solver(s)->m_params.get_bool("model", true); bool new_model = to_param_ref(p).get_bool("model", true); if (old_model != new_model) to_solver_ref(s)->set_produce_models(new_model); + param_descrs r; + to_solver_ref(s)->collect_param_descrs(r); + to_param_ref(p).validate(r); to_solver_ref(s)->updt_params(to_param_ref(p)); } to_solver(s)->m_params = to_param_ref(p); From c739d803ab0ea7543234d6300841b3809823ce2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2014 13:42:56 -0700 Subject: [PATCH 03/17] include model/proof/unsat_core as part of model parameters Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 4 ++++ src/cmd_context/context_params.cpp | 10 +++++++--- src/cmd_context/context_params.h | 2 ++ 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 65b2a9047..b9b3d8166 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -43,6 +43,7 @@ extern "C" { param_descrs r; s->m_solver->collect_param_descrs(r); + context_params::collect_solver_param_descrs(r); p.validate(r); s->m_solver->updt_params(p); } @@ -106,6 +107,7 @@ extern "C" { if (!initialized) init_solver(c, s); to_solver_ref(s)->collect_param_descrs(descrs); + context_params::collect_solver_param_descrs(descrs); if (!initialized) to_solver(s)->m_solver = 0; descrs.display(buffer); @@ -123,6 +125,7 @@ extern "C" { if (!initialized) init_solver(c, s); to_solver_ref(s)->collect_param_descrs(d->m_descrs); + context_params::collect_solver_param_descrs(d->m_descrs); if (!initialized) to_solver(s)->m_solver = 0; Z3_param_descrs r = of_param_descrs(d); @@ -142,6 +145,7 @@ extern "C" { to_solver_ref(s)->set_produce_models(new_model); param_descrs r; to_solver_ref(s)->collect_param_descrs(r); + context_params::collect_solver_param_descrs(r); to_param_ref(p).validate(r); to_solver_ref(s)->updt_params(to_param_ref(p)); } diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 0ec44e0cf..d796dc9b1 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -114,15 +114,19 @@ void context_params::collect_param_descrs(param_descrs & d) { d.insert("well_sorted_check", CPK_BOOL, "type checker", "true"); d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); - d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false"); d.insert("check_interpolants", CPK_BOOL, "check correctness of interpolants", "false"); - d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true"); d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false"); d.insert("trace", CPK_BOOL, "trace generation for VCC", "false"); d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log"); - d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false"); d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false"); d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false"); + collect_solver_param_descrs(d); +} + +void context_params::collect_solver_param_descrs(param_descrs & d) { + d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false"); + d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true"); + d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false"); } params_ref context_params::merge_default_params(params_ref const & p) { diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index 7271bb84f..e26fd3fe5 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -55,6 +55,8 @@ public: */ void get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled); + static void collect_solver_param_descrs(param_descrs & d); + /** \brief Include in p parameters derived from this context_params. These are parameters that are meaningful for tactics and solvers. From 7767a2362685e407a38b8efd5b534992a319a7c2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2014 21:37:37 -0700 Subject: [PATCH 04/17] improve error messages on incorrect parameter passing Signed-off-by: Nikolaj Bjorner --- src/cmd_context/context_params.cpp | 8 +++++++- src/smt/arith_eq_solver.cpp | 4 +++- src/util/gparams.cpp | 21 +++++++++++++++------ 3 files changed, 25 insertions(+), 8 deletions(-) diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index d796dc9b1..d1184fbc8 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -86,7 +86,13 @@ void context_params::set(char const * param, char const * value) { set_bool(m_smtlib2_compliant, param, value); } else { - throw default_exception("unknown parameter '%s'", p.c_str()); + param_descrs d; + collect_param_descrs(d); + std::stringstream strm; + strm << "unknown parameter '" << p << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); } } diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp index 41a61bf73..9a6868ff1 100644 --- a/src/smt/arith_eq_solver.cpp +++ b/src/smt/arith_eq_solver.cpp @@ -604,7 +604,9 @@ bool arith_eq_solver::solve_integer_equations_gcd( } SASSERT(g == r0[i]); } - SASSERT(abs(r0[i]).is_one()); + if (!abs(r0[i]).is_one()) { + return false; + } live.erase(live.begin()+live_pos); for (j = 0; j < live.size(); ++j) { row& r = rows[live[j]]; diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 1d9426390..04acf1ad9 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -201,7 +201,7 @@ public: } } - void throw_unknown_parameter(symbol const & param_name, symbol const & mod_name) { + void throw_unknown_parameter(symbol const & param_name, param_descrs const& d, symbol const & mod_name) { if (mod_name == symbol::null) { char const * new_name = get_new_param_name(param_name); if (new_name) { @@ -213,11 +213,20 @@ public: param_name.bare_str()); } else { - throw exception("unknown parameter '%s'", param_name.bare_str()); + std::stringstream strm; + strm << "unknown parameter '" << param_name << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); } } else { - throw exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str()); + std::stringstream strm; + strm << "unknown parameter '" << param_name << "' "; + strm << "at module '" << mod_name << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); } } @@ -225,7 +234,7 @@ public: param_kind k = d.get_kind(param_name); params_ref & ps = get_params(mod_name); if (k == CPK_INVALID) { - throw_unknown_parameter(param_name, mod_name); + throw_unknown_parameter(param_name, d, mod_name); } else if (k == CPK_UINT) { long val = strtol(value, 0, 10); @@ -312,7 +321,7 @@ public: std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) { if (!d.contains(p)) { - throw_unknown_parameter(p, m); + throw_unknown_parameter(p, d, m); } char const * r = d.get_default(p); if (r == 0) @@ -478,7 +487,7 @@ public: throw exception("unknown module '%s'", m.bare_str()); } if (!d->contains(p)) - throw_unknown_parameter(p, m); + throw_unknown_parameter(p, *d, m); out << " name: " << p << "\n"; if (m != symbol::null) { out << " module: " << m << "\n"; From fe4a8b44a51e3364f6006b3171973d43a2ba418d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Oct 2014 22:40:52 -0700 Subject: [PATCH 05/17] revert some changes to how 'out' parameters are annotated on API calls. Retain the 'out' annotation for so-called managed out parameters. The data-type examples in managed API fail with the out parameter annotation as no memory is allocated on instances of out parameters, other than the interpolation APIs that are new Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 8 +++++--- src/api/dotnet/Constructor.cs | 6 +++--- src/api/dotnet/Context.cs | 2 +- src/api/dotnet/EnumSort.cs | 2 +- src/api/dotnet/TupleSort.cs | 4 ++-- 5 files changed, 12 insertions(+), 10 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 837c2e1f4..e08adf111 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -263,8 +263,10 @@ def param2dotnet(p): return "[In] %s[]" % type2dotnet(param_type(p)) elif k == INOUT_ARRAY: return "[In, Out] %s[]" % type2dotnet(param_type(p)) - elif k == OUT_ARRAY or k == OUT_MANAGED_ARRAY: - return "[Out] out %s[]" % type2dotnet(param_type(p)) + elif k == OUT_ARRAY: + return "[Out] %s[]" % type2dotnet(param_type(p)) + elif k == OUT_MANAGED_ARRAY: + return "[Out] out %s[]" % type2dotnet(param_type(p)) else: return type2dotnet(param_type(p)) @@ -476,7 +478,7 @@ def mk_dotnet_wrappers(): dotnet.write('out '); else: dotnet.write('ref ') - elif param_kind(param) == OUT_ARRAY or param_kind(param) == OUT_MANAGED_ARRAY: + elif param_kind(param) == OUT_MANAGED_ARRAY: dotnet.write('out '); dotnet.write('a%d' % i) i = i + 1 diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs index 8d478dd85..527b8bc13 100644 --- a/src/api/dotnet/Constructor.cs +++ b/src/api/dotnet/Constructor.cs @@ -50,7 +50,7 @@ namespace Microsoft.Z3 IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; - Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors); + Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); return new FuncDecl(Context, constructor); } } @@ -66,7 +66,7 @@ namespace Microsoft.Z3 IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; - Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors); + Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); return new FuncDecl(Context, tester); } } @@ -82,7 +82,7 @@ namespace Microsoft.Z3 IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; - Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors); + Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); FuncDecl[] t = new FuncDecl[n]; for (uint i = 0; i < n; i++) t[i] = new FuncDecl(Context, accessors[i]); diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index a9e25de4f..2b88cbab7 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -424,7 +424,7 @@ namespace Microsoft.Z3 n_constr[i] = cla[i].NativeObject; } IntPtr[] n_res = new IntPtr[n]; - Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), out n_res, n_constr); + Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr); DatatypeSort[] res = new DatatypeSort[n]; for (uint i = 0; i < n; i++) res[i] = new DatatypeSort(this, n_res[i]); diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs index db3d5123f..e62043078 100644 --- a/src/api/dotnet/EnumSort.cs +++ b/src/api/dotnet/EnumSort.cs @@ -88,7 +88,7 @@ namespace Microsoft.Z3 IntPtr[] n_constdecls = new IntPtr[n]; IntPtr[] n_testers = new IntPtr[n]; NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n, - Symbol.ArrayToNative(enumNames), out n_constdecls, out n_testers); + Symbol.ArrayToNative(enumNames), n_constdecls, n_testers); } #endregion }; diff --git a/src/api/dotnet/TupleSort.cs b/src/api/dotnet/TupleSort.cs index 7d0b6a853..81a0eaf60 100644 --- a/src/api/dotnet/TupleSort.cs +++ b/src/api/dotnet/TupleSort.cs @@ -74,10 +74,10 @@ namespace Microsoft.Z3 Contract.Requires(name != null); IntPtr t = IntPtr.Zero; - IntPtr[] f; + IntPtr[] f = new IntPtr[numFields]; NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields, Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts), - ref t, out f); + ref t, f); } #endregion }; From f4a015602ca0b204ba72373301240eaa89e6fc08 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 18 Oct 2014 13:43:13 +0100 Subject: [PATCH 06/17] Disable FPA-min/max because of name clashes with user-defined functions. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index df26422c8..c6706b7b1 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -581,8 +581,9 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL)); op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS)); - op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); - op_names.push_back(builtin_name("max", OP_FLOAT_MAX)); + // Disabled min/max, clashes with user-defined min/max functions + // op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); + // op_names.push_back(builtin_name("max", OP_FLOAT_MAX)); op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT)); From de9f6d3e11d536e6dabf4247747214da96af3546 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 21 Oct 2014 16:52:16 +0100 Subject: [PATCH 07/17] FPA name clash fix Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index c6706b7b1..5466df069 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -314,8 +314,8 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete symbol name; switch (k) { case OP_FLOAT_REM: name = "remainder"; break; - case OP_FLOAT_MIN: name = "min"; break; - case OP_FLOAT_MAX: name = "max"; break; + case OP_FLOAT_MIN: name = "fp.min"; break; + case OP_FLOAT_MAX: name = "fp.max"; break; default: UNREACHABLE(); break; From 7f045290804ff9564f6db59cb1c6145bf0d6062c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Oct 2014 09:11:38 -0700 Subject: [PATCH 08/17] validate types of parameter values that get set globally Signed-off-by: Nikolaj Bjorner --- src/util/gparams.cpp | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 04acf1ad9..6397ad377 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -230,6 +230,43 @@ public: } } + void validate_type(symbol const& name, char const* value, param_descrs const& d) { + param_kind k = d.get_kind(name); + std::stringstream strm; + + switch (k) { + case CPK_UINT: + for (; *value; ++value) { + if (!('0' <= *value && *value <= '9')) { + strm << "Expected values for parameter " << name + << " is an unsigned integer. It was given argument '" << value << "'"; + throw default_exception(strm.str()); + } + } + break; + case CPK_DOUBLE: + for (; *value; ++value) { + if (!('0' <= *value && *value <= '9') && *value != '.' && *value != '-') { + strm << "Expected values for parameter " << name + << " is a double. It was given argument '" << value << "'"; + throw default_exception(strm.str()); + } + } + break; + + case CPK_BOOL: + if (strcmp(value, "true") != 0 && strcmp(value, "false") != 0) { + strm << "Expected values for parameter " << name + << " are 'true' or 'false'. It was given argument '" << value << "'"; + throw default_exception(strm.str()); + } + break; + case CPK_SYMBOL: + case CPK_STRING: + break; + } + } + void set(param_descrs const & d, symbol const & param_name, char const * value, symbol const & mod_name) { param_kind k = d.get_kind(param_name); params_ref & ps = get_params(mod_name); @@ -291,11 +328,13 @@ public: symbol m, p; normalize(name, m, p); if (m == symbol::null) { + validate_type(p, value, get_param_descrs()); set(get_param_descrs(), p, value, m); } else { param_descrs * d; if (get_module_param_descrs().find(m, d)) { + validate_type(p, value, *d); set(*d, p, value, m); } else { From 340f7659839ce492b7eb8483fd2bd91eb1ca9645 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Oct 2014 09:35:32 -0700 Subject: [PATCH 09/17] make sure that parameters are appended such that multiple paramters are not ignored on the solver Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index b9b3d8166..e57050e82 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -149,7 +149,7 @@ extern "C" { to_param_ref(p).validate(r); to_solver_ref(s)->updt_params(to_param_ref(p)); } - to_solver(s)->m_params = to_param_ref(p); + to_solver(s)->m_params.append(to_param_ref(p)); Z3_CATCH; } From 3ecffaa1e5c7706c196c2cd11db4f8c865c6846d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Oct 2014 11:12:50 -0700 Subject: [PATCH 10/17] remove unused and always failing get_param_value function Signed-off-by: Nikolaj Bjorner --- src/api/api_config_params.cpp | 6 ------ src/api/dotnet/Context.cs | 17 ----------------- src/api/z3_api.h | 9 --------- src/cmd_context/context_params.cpp | 14 +++++++------- 4 files changed, 7 insertions(+), 39 deletions(-) diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 48c2df4a9..c46e7363d 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -106,10 +106,4 @@ extern "C" { Z3_CATCH; } - Z3_bool Z3_API Z3_get_param_value(Z3_context c, Z3_string param_id, Z3_string* param_value) { - LOG_Z3_get_param_value(c, param_id, param_value); - // TODO - return Z3_FALSE; - } - }; diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 2b88cbab7..1c03d76b6 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3527,28 +3527,11 @@ namespace Microsoft.Z3 /// Only a few configuration parameters are mutable once the context is created. /// An exception is thrown when trying to modify an immutable parameter. /// - /// public void UpdateParamValue(string id, string value) { Native.Z3_update_param_value(nCtx, id, value); } - /// - /// Get a configuration parameter. - /// - /// - /// Returns null if the parameter value does not exist. - /// - /// - public string GetParamValue(string id) - { - IntPtr res = IntPtr.Zero; - if (Native.Z3_get_param_value(nCtx, id, out res) == 0) - return null; - else - return Marshal.PtrToStringAnsi(res); - } - #endregion #region Internal diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 04e2d38af..2e3ddf4b4 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1462,15 +1462,6 @@ extern "C" { */ void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value); - /** - \brief Return the value of a context parameter. - - \sa Z3_global_param_get - - def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING))) - */ - Z3_bool_opt Z3_API Z3_get_param_value(__in Z3_context c, __in Z3_string param_id, __out_opt Z3_string_ptr param_value); - #ifdef CorML4 /** \brief Interrupt the execution of a Z3 procedure. diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index d1184fbc8..254a1d931 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -86,13 +86,13 @@ void context_params::set(char const * param, char const * value) { set_bool(m_smtlib2_compliant, param, value); } else { - param_descrs d; - collect_param_descrs(d); - std::stringstream strm; - strm << "unknown parameter '" << p << "'\n"; - strm << "Legal parameters are:\n"; - d.display(strm, 2, false, false); - throw default_exception(strm.str()); + param_descrs d; + collect_param_descrs(d); + std::stringstream strm; + strm << "unknown parameter '" << p << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); } } From f3a04734d9cd685f5921c368f648899246b094fc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Oct 2014 12:48:49 -0700 Subject: [PATCH 11/17] add pretty printing to SMT2 from solver, add get_id to Ast objects Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 82ba85472..470280630 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -297,6 +297,11 @@ class AstRef(Z3PPObject): """Return a pointer to the corresponding C Z3_ast object.""" return self.ast + def get_id(self): + """Return unique identifier for object. It can be used for hash-tables and maps.""" + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + + def ctx_ref(self): """Return a reference to the C context where this AST node is stored.""" return self.ctx.ref() @@ -447,6 +452,10 @@ class SortRef(AstRef): def as_ast(self): return Z3_sort_to_ast(self.ctx_ref(), self.ast) + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + + def kind(self): """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. @@ -585,6 +594,9 @@ class FuncDeclRef(AstRef): def as_ast(self): return Z3_func_decl_to_ast(self.ctx_ref(), self.ast) + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + def as_func_decl(self): return self.ast @@ -730,6 +742,9 @@ class ExprRef(AstRef): def as_ast(self): return self.ast + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + def sort(self): """Return the sort of expression `self`. @@ -1524,6 +1539,9 @@ class PatternRef(ExprRef): def as_ast(self): return Z3_pattern_to_ast(self.ctx_ref(), self.ast) + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + def is_pattern(a): """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. @@ -1586,6 +1604,9 @@ class QuantifierRef(BoolRef): def as_ast(self): return self.ast + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + def sort(self): """Return the Boolean sort.""" return BoolSort(self.ctx) @@ -6011,6 +6032,24 @@ class Solver(Z3PPObject): """ return Z3_solver_to_string(self.ctx.ref(), self.solver) + def to_smt2(self): + """return SMTLIB2 formatted benchmark for solver's assertions""" + es = self.assertions() + sz = len(es) + sz1 = sz + if sz1 > 0: + sz1 -= 1 + v = (Ast * sz1)() + for i in range(sz1): + v[i] = es[i].as_ast() + if sz > 0: + e = es[sz1].as_ast() + else: + e = BoolVal(True, self.ctx).as_ast() + return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e) + + + def SolverFor(logic, ctx=None): """Create a solver customized for the given logic. From d77d6c6648a1aaf8cafefd1458500c71e2c271ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Oct 2014 13:24:31 -0700 Subject: [PATCH 12/17] update parameter checking for doubles, and fix error reporting Signed-off-by: Nikolaj Bjorner --- src/util/gparams.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 6397ad377..83157a0b0 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -233,22 +233,22 @@ public: void validate_type(symbol const& name, char const* value, param_descrs const& d) { param_kind k = d.get_kind(name); std::stringstream strm; - + char const* _value = value; switch (k) { case CPK_UINT: for (; *value; ++value) { if (!('0' <= *value && *value <= '9')) { strm << "Expected values for parameter " << name - << " is an unsigned integer. It was given argument '" << value << "'"; + << " is an unsigned integer. It was given argument '" << _value << "'"; throw default_exception(strm.str()); } } break; case CPK_DOUBLE: for (; *value; ++value) { - if (!('0' <= *value && *value <= '9') && *value != '.' && *value != '-') { + if (!('0' <= *value && *value <= '9') && *value != '.' && *value != '-' && *value != '/') { strm << "Expected values for parameter " << name - << " is a double. It was given argument '" << value << "'"; + << " is a double. It was given argument '" << _value << "'"; throw default_exception(strm.str()); } } From 1059d226e44d9ad65285e5e1a9aba58856a2ed57 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Oct 2014 13:25:19 -0700 Subject: [PATCH 13/17] add default statement instead of incomplete cases Signed-off-by: Nikolaj Bjorner --- src/util/gparams.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 83157a0b0..adffe6bde 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -261,8 +261,7 @@ public: throw default_exception(strm.str()); } break; - case CPK_SYMBOL: - case CPK_STRING: + default: break; } } From ae6121525a9c6dd8ba079001bd2fcfad4015d81b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 22 Oct 2014 13:57:07 +0100 Subject: [PATCH 14/17] Z3Py: improve readability of Z3 exceptions Signed-off-by: Nuno Lopes --- src/api/python/z3types.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py index 593312d68..5d59368ff 100644 --- a/src/api/python/z3types.py +++ b/src/api/python/z3types.py @@ -4,7 +4,7 @@ class Z3Exception(Exception): def __init__(self, value): self.value = value def __str__(self): - return repr(self.value) + return str(self.value) class ContextObj(ctypes.c_void_p): def __init__(self, context): self._as_parameter_ = context From 65ce445b7e209728c725997e140191ab16454bf2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Oct 2014 08:24:49 -0700 Subject: [PATCH 15/17] update Java API Signed-off-by: Nikolaj Bjorner --- src/api/java/Context.java | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 6b6c63ac3..cc5c07c5e 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2911,20 +2911,6 @@ public class Context extends IDisposable Native.updateParamValue(nCtx(), id, value); } - /** - * Get a configuration parameter. Returns null if the parameter - * value does not exist. - **/ - public String getParamValue(String id) throws Z3Exception - { - Native.StringPtr res = new Native.StringPtr(); - boolean r = Native.getParamValue(nCtx(), id, res); - if (!r) - return null; - else - return res.value; - } - long m_ctx = 0; long nCtx() From d91a114b8086d3f3d68d354b80bc62a9e7d5b3d6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 22 Oct 2014 16:29:13 +0100 Subject: [PATCH 16/17] Java API: removed Z3_get_param_value as in other APIs. Signed-off-by: Christoph M. Wintersteiger --- src/api/java/Context.java | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 6b6c63ac3..41a98e3d9 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2904,27 +2904,13 @@ public class Context extends IDisposable * configuration parameters can be obtained using the Z3 executable: * z3.exe -ini? Only a few configuration parameters are mutable * once the context is created. An exception is thrown when trying to modify - * an immutable parameter. + * an immutable parameter. **/ public void updateParamValue(String id, String value) throws Z3Exception { Native.updateParamValue(nCtx(), id, value); } - /** - * Get a configuration parameter. Returns null if the parameter - * value does not exist. - **/ - public String getParamValue(String id) throws Z3Exception - { - Native.StringPtr res = new Native.StringPtr(); - boolean r = Native.getParamValue(nCtx(), id, res); - if (!r) - return null; - else - return res.value; - } - long m_ctx = 0; long nCtx() From 4304012971ef5293a09d73b010bd3263d5b9d9a5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 22 Oct 2014 16:55:08 +0100 Subject: [PATCH 17/17] Java API: copyright notices Signed-off-by: Christoph M. Wintersteiger --- src/api/java/AST.java | 19 +++++++++++++++---- src/api/java/ASTDecRefQueue.java | 18 +++++++++++++++--- src/api/java/ASTMap.java | 19 +++++++++++++++---- src/api/java/ASTVector.java | 19 +++++++++++++++---- src/api/java/AlgebraicNum.java | 19 +++++++++++++++---- src/api/java/ApplyResult.java | 19 +++++++++++++++---- src/api/java/ApplyResultDecRefQueue.java | 18 +++++++++++++++--- src/api/java/ArithExpr.java | 19 +++++++++++++++---- src/api/java/ArithSort.java | 19 +++++++++++++++---- src/api/java/ArrayExpr.java | 19 +++++++++++++++---- src/api/java/ArraySort.java | 19 +++++++++++++++---- src/api/java/AstMapDecRefQueue.java | 18 +++++++++++++++--- src/api/java/AstVectorDecRefQueue.java | 18 +++++++++++++++--- src/api/java/BitVecExpr.java | 19 +++++++++++++++---- src/api/java/BitVecNum.java | 19 +++++++++++++++---- src/api/java/BitVecSort.java | 20 ++++++++++++++++---- src/api/java/BoolExpr.java | 19 +++++++++++++++---- src/api/java/BoolSort.java | 19 +++++++++++++++---- src/api/java/Constructor.java | 19 +++++++++++++++---- src/api/java/ConstructorList.java | 19 +++++++++++++++---- src/api/java/Context.java | 19 +++++++++++++++---- src/api/java/DatatypeExpr.java | 19 +++++++++++++++---- src/api/java/DatatypeSort.java | 19 +++++++++++++++---- src/api/java/EnumSort.java | 19 +++++++++++++++---- src/api/java/Expr.java | 19 +++++++++++++++---- src/api/java/FiniteDomainSort.java | 19 +++++++++++++++---- src/api/java/Fixedpoint.java | 19 +++++++++++++++---- src/api/java/FixedpointDecRefQueue.java | 18 +++++++++++++++--- src/api/java/FuncDecl.java | 19 +++++++++++++++---- src/api/java/FuncInterp.java | 19 +++++++++++++++---- src/api/java/FuncInterpDecRefQueue.java | 18 +++++++++++++++--- src/api/java/FuncInterpEntryDecRefQueue.java | 18 +++++++++++++++--- src/api/java/Global.java | 18 +++++++++++++++--- src/api/java/Goal.java | 19 +++++++++++++++---- src/api/java/GoalDecRefQueue.java | 18 +++++++++++++++--- src/api/java/IDecRefQueue.java | 19 +++++++++++++++---- src/api/java/IntExpr.java | 19 +++++++++++++++---- src/api/java/IntNum.java | 19 +++++++++++++++---- src/api/java/IntSort.java | 19 +++++++++++++++---- src/api/java/IntSymbol.java | 19 +++++++++++++++---- src/api/java/InterpolationContext.java | 18 ++++++++++++++++-- src/api/java/ListSort.java | 19 +++++++++++++++---- src/api/java/Log.java | 19 +++++++++++++++---- src/api/java/Model.java | 19 +++++++++++++++---- src/api/java/ModelDecRefQueue.java | 18 +++++++++++++++--- src/api/java/ParamDescrs.java | 19 +++++++++++++++---- src/api/java/ParamDescrsDecRefQueue.java | 18 +++++++++++++++--- src/api/java/Params.java | 20 ++++++++++++++++---- src/api/java/ParamsDecRefQueue.java | 18 +++++++++++++++--- src/api/java/Pattern.java | 19 +++++++++++++++---- src/api/java/Probe.java | 19 +++++++++++++++---- src/api/java/ProbeDecRefQueue.java | 18 +++++++++++++++--- src/api/java/Quantifier.java | 19 +++++++++++++++---- src/api/java/RatNum.java | 19 +++++++++++++++---- src/api/java/RealExpr.java | 19 +++++++++++++++---- src/api/java/RealSort.java | 19 +++++++++++++++---- src/api/java/RelationSort.java | 19 +++++++++++++++---- src/api/java/SetSort.java | 19 +++++++++++++++---- src/api/java/Solver.java | 19 +++++++++++++++---- src/api/java/SolverDecRefQueue.java | 18 +++++++++++++++--- src/api/java/Sort.java | 19 +++++++++++++++---- src/api/java/Statistics.java | 19 +++++++++++++++---- src/api/java/StatisticsDecRefQueue.java | 18 +++++++++++++++--- src/api/java/Status.java | 19 +++++++++++++++---- src/api/java/StringSymbol.java | 19 +++++++++++++++---- src/api/java/Symbol.java | 19 +++++++++++++++---- src/api/java/Tactic.java | 19 +++++++++++++++---- src/api/java/TacticDecRefQueue.java | 18 +++++++++++++++--- src/api/java/TupleSort.java | 19 +++++++++++++++---- src/api/java/UninterpretedSort.java | 19 +++++++++++++++---- src/api/java/Version.java | 19 +++++++++++++++---- src/api/java/Z3Exception.java | 19 +++++++++++++++---- src/api/java/Z3Object.java | 19 +++++++++++++++---- 73 files changed, 1098 insertions(+), 274 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index fa5cd8284..1f5463ec7 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from AST.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + AST.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java index e0711363d..6ae84eb41 100644 --- a/src/api/java/ASTDecRefQueue.java +++ b/src/api/java/ASTDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ASTDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index dbe7fbd02..6a4e6d56f 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ASTMap.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ASTMap.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 39e32f5d5..07b7dbf56 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ASTVector.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ASTVector.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/AlgebraicNum.java b/src/api/java/AlgebraicNum.java index eaeae933d..340f37f80 100644 --- a/src/api/java/AlgebraicNum.java +++ b/src/api/java/AlgebraicNum.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from AlgebraicNum.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + AlgebraicNum.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index e6c6b89fd..c550c05ae 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ApplyResult.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ApplyResult.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java index 275f4b8f0..78f74d6cc 100644 --- a/src/api/java/ApplyResultDecRefQueue.java +++ b/src/api/java/ApplyResultDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ApplyResultDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java index c429f2322..83ec35d01 100644 --- a/src/api/java/ArithExpr.java +++ b/src/api/java/ArithExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ArithExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - * **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ArithExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ArithSort.java b/src/api/java/ArithSort.java index 5e1780539..2346d9b74 100644 --- a/src/api/java/ArithSort.java +++ b/src/api/java/ArithSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ArithSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ArithSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java index b3bbb8d75..2d5a5a273 100644 --- a/src/api/java/ArrayExpr.java +++ b/src/api/java/ArrayExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ArrayExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ArrayExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java index 2ab8a9750..a371fa3cb 100644 --- a/src/api/java/ArraySort.java +++ b/src/api/java/ArraySort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ArraySort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ArraySort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java index f4c6b2ab5..a4e02d29f 100644 --- a/src/api/java/AstMapDecRefQueue.java +++ b/src/api/java/AstMapDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + AstMapDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java index bdabcdcb1..e0c7988a9 100644 --- a/src/api/java/AstVectorDecRefQueue.java +++ b/src/api/java/AstVectorDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + AstVectorDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java index 9602ea3a0..24b1cfdf3 100644 --- a/src/api/java/BitVecExpr.java +++ b/src/api/java/BitVecExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from BitVecExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BitVecExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index 2dd0dd75a..69ac5dadc 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from BitVecNum.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BitVecNum.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/BitVecSort.java b/src/api/java/BitVecSort.java index c2ec4c26e..be406c806 100644 --- a/src/api/java/BitVecSort.java +++ b/src/api/java/BitVecSort.java @@ -1,8 +1,20 @@ /** - * This file was automatically generated from BitVecSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BitVecSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + package com.microsoft.z3; /** diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java index 40786f76d..99453496a 100644 --- a/src/api/java/BoolExpr.java +++ b/src/api/java/BoolExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from BoolExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BoolExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/BoolSort.java b/src/api/java/BoolSort.java index 03711289a..85ca0a7f7 100644 --- a/src/api/java/BoolSort.java +++ b/src/api/java/BoolSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from BoolSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BoolSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 0c53da73c..4813c2b0a 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Constructor.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Constructor.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index a33276ebb..315a2e535 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ConstructorList.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ConstructorList.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 41a98e3d9..4fbd79be2 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Context.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Context.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/DatatypeExpr.java b/src/api/java/DatatypeExpr.java index 63cb02f80..806ceacab 100644 --- a/src/api/java/DatatypeExpr.java +++ b/src/api/java/DatatypeExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from DatatypeExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + DatatypeExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java index f7b2f7d32..9c339d932 100644 --- a/src/api/java/DatatypeSort.java +++ b/src/api/java/DatatypeSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from DatatypeSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + DatatypeSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index c0fb6d1d6..9715b9a97 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from EnumSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + EnumSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index f7edc6a2b..3773e749d 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Expr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Expr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FiniteDomainSort.java b/src/api/java/FiniteDomainSort.java index a8ba0d8c3..4cb2ab917 100644 --- a/src/api/java/FiniteDomainSort.java +++ b/src/api/java/FiniteDomainSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from FiniteDomainSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FiniteDomainSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 4710368aa..57e1e105a 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Fixedpoint.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Fixedpoint.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java index e52389b85..2ea40dd2c 100644 --- a/src/api/java/FixedpointDecRefQueue.java +++ b/src/api/java/FixedpointDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FixedpointDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index ada44bbd7..573ebd102 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from FuncDecl.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FuncDecl.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index b7fa118e9..243ade71f 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from FuncInterp.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FuncInterp.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java index e2814a9b8..8bdad4ad5 100644 --- a/src/api/java/FuncInterpDecRefQueue.java +++ b/src/api/java/FuncInterpDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FuncInterpDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java index 61488ec74..494c2695c 100644 --- a/src/api/java/FuncInterpEntryDecRefQueue.java +++ b/src/api/java/FuncInterpEntryDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FuncInterpEntryDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Global.java b/src/api/java/Global.java index 33a828fb8..b97e48721 100644 --- a/src/api/java/Global.java +++ b/src/api/java/Global.java @@ -1,7 +1,19 @@ /** - * Global.java - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Global.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index c486a57b3..aba8b0149 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Goal.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Goal.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java index 0c7b8f5d9..45992170f 100644 --- a/src/api/java/GoalDecRefQueue.java +++ b/src/api/java/GoalDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + GoalDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java index ddb679910..2190f8e4d 100644 --- a/src/api/java/IDecRefQueue.java +++ b/src/api/java/IDecRefQueue.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IDecRefQueue.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java index 78cc15f90..2e90c3cbf 100644 --- a/src/api/java/IntExpr.java +++ b/src/api/java/IntExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IntExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IntExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java index ebf237a2e..0fdcf1aa6 100644 --- a/src/api/java/IntNum.java +++ b/src/api/java/IntNum.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IntNum.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IntNum.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IntSort.java b/src/api/java/IntSort.java index 44e48ccd1..bcfc730c4 100644 --- a/src/api/java/IntSort.java +++ b/src/api/java/IntSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IntSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IntSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IntSymbol.java b/src/api/java/IntSymbol.java index 113b507c3..b0f1af685 100644 --- a/src/api/java/IntSymbol.java +++ b/src/api/java/IntSymbol.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IntSymbol.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IntSymbol.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 067871324..3e9996b3e 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -1,6 +1,20 @@ /** - * - */ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + InterpolationContext.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + package com.microsoft.z3; import java.util.Map; diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java index af1645187..52cb1a179 100644 --- a/src/api/java/ListSort.java +++ b/src/api/java/ListSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ListSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ListSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Log.java b/src/api/java/Log.java index 99581cedb..254da1bc6 100644 --- a/src/api/java/Log.java +++ b/src/api/java/Log.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Log.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Log.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 32247eb4a..11eed201e 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Model.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Model.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java index a0542714e..1200b29be 100644 --- a/src/api/java/ModelDecRefQueue.java +++ b/src/api/java/ModelDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ModelDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index 3b3e76e51..4afae9f76 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ParamDescrs.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ParamDescrs.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java index 70806041d..a29565e8e 100644 --- a/src/api/java/ParamDescrsDecRefQueue.java +++ b/src/api/java/ParamDescrsDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ParamDescrsDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Params.java b/src/api/java/Params.java index cf3d8c759..bbe6d66cf 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -1,8 +1,20 @@ /** - * This file was automatically generated from Params.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Params.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + package com.microsoft.z3; diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java index 361fdf133..7d71feb8f 100644 --- a/src/api/java/ParamsDecRefQueue.java +++ b/src/api/java/ParamsDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ParamDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java index cd9340c9d..797b387d0 100644 --- a/src/api/java/Pattern.java +++ b/src/api/java/Pattern.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Pattern.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Pattern.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index b68b0266f..17ad81b5c 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Probe.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Probe.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java index 0ae0b0e8e..fda5d37b4 100644 --- a/src/api/java/ProbeDecRefQueue.java +++ b/src/api/java/ProbeDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ProbeDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 78a0fc03f..e9aeefcca 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Quantifier.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Quantifier.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java index e1cb5b346..f937ea593 100644 --- a/src/api/java/RatNum.java +++ b/src/api/java/RatNum.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from RatNum.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + RatNum.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/RealExpr.java b/src/api/java/RealExpr.java index 20d603d9a..6188e2999 100644 --- a/src/api/java/RealExpr.java +++ b/src/api/java/RealExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from RealExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + RealExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/RealSort.java b/src/api/java/RealSort.java index ce7295ead..d76823a0d 100644 --- a/src/api/java/RealSort.java +++ b/src/api/java/RealSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from RealSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + RealSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/RelationSort.java b/src/api/java/RelationSort.java index bdc4d7804..77f6c595b 100644 --- a/src/api/java/RelationSort.java +++ b/src/api/java/RelationSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from RelationSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + RelationSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/SetSort.java b/src/api/java/SetSort.java index a94a34b26..69126933a 100644 --- a/src/api/java/SetSort.java +++ b/src/api/java/SetSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from SetSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + SetSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 3827de07a..e129189f9 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Solver.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Solver.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java index 1c715716a..993c99621 100644 --- a/src/api/java/SolverDecRefQueue.java +++ b/src/api/java/SolverDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + SolverDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 381b9b0ae..7bcc7ce7e 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Sort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Sort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index c36020bd6..315feeaa2 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Statistics.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Statistics.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java index d16bf3710..db3e32c86 100644 --- a/src/api/java/StatisticsDecRefQueue.java +++ b/src/api/java/StatisticsDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + StatisticsDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Status.java b/src/api/java/Status.java index e37631070..a08f47909 100644 --- a/src/api/java/Status.java +++ b/src/api/java/Status.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Status.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Status.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java index 951051aa0..09273c946 100644 --- a/src/api/java/StringSymbol.java +++ b/src/api/java/StringSymbol.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from StringSymbol.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + StringSymbol.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index 177409ec8..856c9b57e 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Symbol.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Symbol.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index e62096715..6573a1407 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Tactic.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Tactic.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java index 50fba156e..5557d03b8 100644 --- a/src/api/java/TacticDecRefQueue.java +++ b/src/api/java/TacticDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + TacticDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java index 554581d0f..523f8d676 100644 --- a/src/api/java/TupleSort.java +++ b/src/api/java/TupleSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from TupleSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + TupleSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/UninterpretedSort.java b/src/api/java/UninterpretedSort.java index 51df17543..07e4707f5 100644 --- a/src/api/java/UninterpretedSort.java +++ b/src/api/java/UninterpretedSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from UninterpretedSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + UninterpretedSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Version.java b/src/api/java/Version.java index b96fb50f9..3f019390b 100644 --- a/src/api/java/Version.java +++ b/src/api/java/Version.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Version.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Version.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Z3Exception.java b/src/api/java/Z3Exception.java index 24dc586d4..2522db627 100644 --- a/src/api/java/Z3Exception.java +++ b/src/api/java/Z3Exception.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Z3Exception.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Z3Exception.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index 6c2c11e25..03cfcd625 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Z3Object.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Z3Object.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3;