mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-12-08 15:42:13 +01:00
parent 38b5e6de56 f1d1e728ff
commit 2ca83d0095
11 changed files with 38 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
scripts/mk_nuget_release.py
View file

@ -52,7 +52,7 @@ def classify_package(f):
return None
def unpack():
shutil.rmtree("out")
shutil.rmtree("out", ignore_errors=True)
# unzip files in packages
# out
# +- runtimes
@ -70,9 +70,9 @@ def unpack():
path = os.path.abspath(os.path.join("packages", f))
zip_ref = zipfile.ZipFile(path, 'r')
zip_ref.extract("%s/bin/libz3.%s" % (package_dir, ext), "tmp")
mk_dir("out/runtimes/%s" % dst)
shutil.move("tmp/%s/bin/libz3.%s" % (package_dir, ext), "out/runtimes/%s/." % dst, "/y")
if "win" in f:
mk_dir("out/runtimes/%s/native" % dst)
shutil.move("tmp/%s/bin/libz3.%s" % (package_dir, ext), "out/runtimes/%s/native/." % dst, "/y")
if "x64-win" in f:
mk_dir("out/lib/netstandard1.4/")
for b in ["Microsoft.Z3.dll"]:
zip_ref.extract("%s/bin/%s" % (package_dir, b), "tmp")

12
src/api/api_fpa.cpp
View file

@ -242,8 +242,8 @@ extern "C" {
RETURN_Z3(nullptr);
}
api::context * ctx = mk_c(c);
expr * a = negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) :
ctx->fpautil().mk_pinf(to_sort(s));
expr * a = negative ? ctx->fpautil().mk_ninf(to_sort(s)) :
ctx->fpautil().mk_pinf(to_sort(s));
ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(nullptr);
@ -259,8 +259,8 @@ extern "C" {
RETURN_Z3(nullptr);
}
api::context * ctx = mk_c(c);
expr * a = negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) :
ctx->fpautil().mk_pzero(to_sort(s));
expr * a = negative ? ctx->fpautil().mk_nzero(to_sort(s)) :
ctx->fpautil().mk_pzero(to_sort(s));
ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(nullptr);
@ -351,7 +351,7 @@ extern "C" {
ctx->fpautil().fm().set(tmp,
ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)),
sgn != 0, exp, sig);
sgn, exp, sig);
expr * a = ctx->fpautil().mk_value(tmp);
ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
@ -371,7 +371,7 @@ extern "C" {
ctx->fpautil().fm().set(tmp,
ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)),
sgn != 0, exp, sig);
sgn, exp, sig);
expr * a = ctx->fpautil().mk_value(tmp);
ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));

10
src/api/api_numeral.cpp
View file

@ -198,19 +198,19 @@ extern "C" {
mpf_rounding_mode rm;
if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) {
switch (rm) {
case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
case MPF_ROUND_NEAREST_TEVEN:
return mk_c(c)->mk_external_string("roundNearestTiesToEven");
break;
case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
case MPF_ROUND_NEAREST_TAWAY:
return mk_c(c)->mk_external_string("roundNearestTiesToAway");
break;
case OP_FPA_RM_TOWARD_POSITIVE:
case MPF_ROUND_TOWARD_POSITIVE:
return mk_c(c)->mk_external_string("roundTowardPositive");
break;
case OP_FPA_RM_TOWARD_NEGATIVE:
case MPF_ROUND_TOWARD_NEGATIVE:
return mk_c(c)->mk_external_string("roundTowardNegative");
break;
case OP_FPA_RM_TOWARD_ZERO:
case MPF_ROUND_TOWARD_ZERO:
default:
return mk_c(c)->mk_external_string("roundTowardZero");
break;

2
src/api/api_params.cpp
View file

@ -66,7 +66,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_params_set_bool(c, p, k, v);
RESET_ERROR_CODE();
to_params(p)->m_params.set_bool(norm_param_name(to_symbol(k)).c_str(), v != 0);
to_params(p)->m_params.set_bool(norm_param_name(to_symbol(k)).c_str(), v);
Z3_CATCH;
}

2
src/api/api_rcf.cpp
View file

@ -274,7 +274,7 @@ extern "C" {
RESET_ERROR_CODE();
reset_rcf_cancel(c);
std::ostringstream buffer;
rcfm(c).display(buffer, to_rcnumeral(a), compact != 0, html != 0);
rcfm(c).display(buffer, to_rcnumeral(a), compact, html);
return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN("");
}

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

@ -505,7 +505,7 @@ namespace z3 {
out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
}
inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }
/**
@ -713,10 +713,10 @@ namespace z3 {
small integers, 64 bit integers or rational or decimal strings.
*/
bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
bool is_numeral_i64(int64_t& i) const { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u64(uint64_t& i) const { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_i(int& i) const { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_i64(int64_t& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u64(uint64_t& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
@ -736,15 +736,15 @@ namespace z3 {
/**
\brief Return true if this expression is a universal quantifier.
*/
bool is_forall() const { return 0 != Z3_is_quantifier_forall(ctx(), m_ast); }
bool is_forall() const { return Z3_is_quantifier_forall(ctx(), m_ast); }
/**
\brief Return true if this expression is an existential quantifier.
*/
bool is_exists() const { return 0 != Z3_is_quantifier_exists(ctx(), m_ast); }
bool is_exists() const { return Z3_is_quantifier_exists(ctx(), m_ast); }
/**
\brief Return true if this expression is a lambda expression.
*/
bool is_lambda() const { return 0 != Z3_is_lambda(ctx(), m_ast); }
bool is_lambda() const { return Z3_is_lambda(ctx(), m_ast); }
/**
\brief Return true if this expression is a variable.
@ -753,12 +753,12 @@ namespace z3 {
/**
\brief Return true if expression is an algebraic number.
*/
bool is_algebraic() const { return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_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; }
bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
/**
\brief Return string representation of numeral or algebraic number
@ -2073,7 +2073,7 @@ namespace z3 {
// for function f.
bool has_interp(func_decl f) const {
check_context(*this, f);
return 0 != Z3_model_has_interp(ctx(), m_model, f);
return Z3_model_has_interp(ctx(), m_model, f);
}
func_interp add_func_interp(func_decl& f, expr& else_val) {
@ -2112,8 +2112,8 @@ namespace z3 {
}
unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
friend std::ostream & operator<<(std::ostream & out, stats const & s);
@ -2353,12 +2353,12 @@ namespace z3 {
unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal); }
unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
void reset() { Z3_goal_reset(ctx(), m_goal); }
unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal); }
bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal); }
model convert_model(model const & m) const {
check_context(*this, m);
Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);

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

@ -475,7 +475,7 @@ namespace Microsoft.Z3
/// Update a datatype field at expression t with value v.
/// The function performs a record update at t. The field
/// that is passed in as argument is updated with value v,
/// the remainig fields of t are unchanged.
/// the remaining fields of t are unchanged.
/// </summary>
public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
{

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

@ -25,7 +25,7 @@ using System.Linq;
namespace Microsoft.Z3
{
/// <summary>
/// Object for managing optimizization context
/// Object for managing optimization context
/// </summary>
public class Optimize : Z3Object
{

2
src/api/dotnet/dotnet35/Readme.NET35
View file

@ -4,7 +4,7 @@ instructions are as follows:
In the project properties of Microsoft.Z3.csproj:
- Under 'Application': Change Target framework to .NET Framework 3.5
- Under 'Build': Add FRAMEWORK_LT_4 to the condidional compilation symbols
- Under 'Build': Add FRAMEWORK_LT_4 to the conditional compilation symbols
- Remove the reference to System.Numerics
- Install the NuGet Package "Microsoft Code Contracts for Net3.5":
In the Package Manager Console enter Install-Package Code.Contract

2
src/qe/qe.h
View file

@ -253,7 +253,7 @@ namespace qe {
/**
\brief Guarded definitions.
A realizer to a an existential quantified formula is a disjunction
A realizer to an existential quantified formula is a disjunction
together with a substitution from the existentially quantified variables
to terms such that:
1. The original formula (exists (vars) fml) is equivalent to the disjunction of guards.

2
src/util/memory_manager.cpp
View file

@ -18,7 +18,7 @@ Copyright (c) 2015 Microsoft Corporation
// ADD_INITIALIZER('rational::initialize();')
// ADD_FINALIZER('rational::finalize();')
// Thus, any executable or shared object (DLL) that depends on rational.h
// will have an automalically generated file mem_initializer.cpp containing
// will have an automatically generated file mem_initializer.cpp containing
// mem_initialize()
// mem_finalize()
// and these functions will include the statements: