diff --git a/src/api/dll/dll.cpp b/src/api/dll/dll.cpp
index a0bd25d2e..74dc48153 100644
--- a/src/api/dll/dll.cpp
+++ b/src/api/dll/dll.cpp
@@ -15,16 +15,16 @@ Copyright (c) 2015 Microsoft Corporation
BOOL APIENTRY DllMain( HMODULE hModule,
DWORD ul_reason_for_call,
LPVOID lpReserved
- )
+ )
{
- switch (ul_reason_for_call)
- {
- case DLL_PROCESS_ATTACH:
- case DLL_THREAD_ATTACH:
- case DLL_THREAD_DETACH:
- case DLL_PROCESS_DETACH:
- break;
- }
+ switch (ul_reason_for_call)
+ {
+ case DLL_PROCESS_ATTACH:
+ case DLL_THREAD_ATTACH:
+ case DLL_THREAD_DETACH:
+ case DLL_PROCESS_DETACH:
+ break;
+ }
return TRUE;
}
diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index 93f5929d9..add1b0ded 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -43,78 +43,78 @@ add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}"
)
set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
- AlgebraicNum.cs
- ApplyResult.cs
- ArithExpr.cs
- ArithSort.cs
- ArrayExpr.cs
- ArraySort.cs
- AST.cs
- ASTMap.cs
- ASTVector.cs
- BitVecExpr.cs
- BitVecNum.cs
- BitVecSort.cs
- BoolExpr.cs
- BoolSort.cs
- Constructor.cs
- ConstructorList.cs
- Context.cs
- DatatypeExpr.cs
- DatatypeSort.cs
- Deprecated.cs
- EnumSort.cs
- Expr.cs
- FiniteDomainExpr.cs
- FiniteDomainNum.cs
- FiniteDomainSort.cs
- Fixedpoint.cs
- FPExpr.cs
- FPNum.cs
- FPRMExpr.cs
- FPRMNum.cs
- FPRMSort.cs
- FPSort.cs
- FuncDecl.cs
- FuncInterp.cs
- Global.cs
- Goal.cs
- IDecRefQueue.cs
- InterpolationContext.cs
- IntExpr.cs
- IntNum.cs
- IntSort.cs
- IntSymbol.cs
- ListSort.cs
- Log.cs
- Model.cs
- Optimize.cs
- ParamDescrs.cs
- Params.cs
- Pattern.cs
- Probe.cs
- Quantifier.cs
- RatNum.cs
- RealExpr.cs
- RealSort.cs
- ReExpr.cs
- RelationSort.cs
- ReSort.cs
- SeqExpr.cs
- SeqSort.cs
- SetSort.cs
- Solver.cs
- Sort.cs
- Statistics.cs
- Status.cs
- StringSymbol.cs
- Symbol.cs
- Tactic.cs
- TupleSort.cs
- UninterpretedSort.cs
- Version.cs
- Z3Exception.cs
- Z3Object.cs
+ AlgebraicNum.cs
+ ApplyResult.cs
+ ArithExpr.cs
+ ArithSort.cs
+ ArrayExpr.cs
+ ArraySort.cs
+ AST.cs
+ ASTMap.cs
+ ASTVector.cs
+ BitVecExpr.cs
+ BitVecNum.cs
+ BitVecSort.cs
+ BoolExpr.cs
+ BoolSort.cs
+ Constructor.cs
+ ConstructorList.cs
+ Context.cs
+ DatatypeExpr.cs
+ DatatypeSort.cs
+ Deprecated.cs
+ EnumSort.cs
+ Expr.cs
+ FiniteDomainExpr.cs
+ FiniteDomainNum.cs
+ FiniteDomainSort.cs
+ Fixedpoint.cs
+ FPExpr.cs
+ FPNum.cs
+ FPRMExpr.cs
+ FPRMNum.cs
+ FPRMSort.cs
+ FPSort.cs
+ FuncDecl.cs
+ FuncInterp.cs
+ Global.cs
+ Goal.cs
+ IDecRefQueue.cs
+ InterpolationContext.cs
+ IntExpr.cs
+ IntNum.cs
+ IntSort.cs
+ IntSymbol.cs
+ ListSort.cs
+ Log.cs
+ Model.cs
+ Optimize.cs
+ ParamDescrs.cs
+ Params.cs
+ Pattern.cs
+ Probe.cs
+ Quantifier.cs
+ RatNum.cs
+ RealExpr.cs
+ RealSort.cs
+ ReExpr.cs
+ RelationSort.cs
+ ReSort.cs
+ SeqExpr.cs
+ SeqSort.cs
+ SetSort.cs
+ Solver.cs
+ Sort.cs
+ Statistics.cs
+ Status.cs
+ StringSymbol.cs
+ Symbol.cs
+ Tactic.cs
+ TupleSort.cs
+ UninterpretedSort.cs
+ Version.cs
+ Z3Exception.cs
+ Z3Object.cs
)
set(Z3_DOTNET_ASSEMBLY_SOURCES "")
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index a656be3eb..d7699c961 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -126,7 +126,7 @@ namespace Microsoft.Z3
private BoolSort m_boolSort = null;
private IntSort m_intSort = null;
private RealSort m_realSort = null;
- private SeqSort m_stringSort = null;
+ private SeqSort m_stringSort = null;
///
/// Retrieves the Boolean sort of the context.
@@ -2426,7 +2426,7 @@ namespace Microsoft.Z3
public SeqExpr IntToString(Expr e)
{
Contract.Requires(e != null);
- Contract.Requires(e is ArithExpr);
+ Contract.Requires(e is ArithExpr);
Contract.Ensures(Contract.Result() != null);
return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
}
@@ -2690,7 +2690,7 @@ namespace Microsoft.Z3
///
/// Create a range expression.
///
- public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
+ public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
{
Contract.Requires(lo != null);
Contract.Requires(hi != null);
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 6c52b83c8..4fd306052 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -809,55 +809,55 @@ namespace Microsoft.Z3
/// Check whether expression is a concatentation.
///
/// a Boolean
- public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } }
+ public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } }
///
/// Check whether expression is a prefix.
///
/// a Boolean
- public bool IsPrefix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } }
+ public bool IsPrefix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } }
///
/// Check whether expression is a suffix.
///
/// a Boolean
- public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } }
+ public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } }
///
/// Check whether expression is a contains.
///
/// a Boolean
- public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } }
+ public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } }
///
/// Check whether expression is an extract.
///
/// a Boolean
- public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } }
+ public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } }
///
/// Check whether expression is a replace.
///
/// a Boolean
- public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } }
+ public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } }
///
/// Check whether expression is an at.
///
/// a Boolean
- public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } }
+ public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } }
///
/// Check whether expression is a sequence length.
///
/// a Boolean
- public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } }
+ public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } }
///
/// Check whether expression is a sequence index.
///
/// a Boolean
- public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } }
+ public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } }
#endregion
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 99dd9aac0..9d0636425 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -123,7 +123,7 @@ namespace Microsoft.Z3
///
/// Retrieve a lower bound for the objective handle.
- ///
+ ///
public ArithExpr Lower
{
get { return opt.GetLower(handle); }
@@ -131,7 +131,7 @@ namespace Microsoft.Z3
///
/// Retrieve an upper bound for the objective handle.
- ///
+ ///
public ArithExpr Upper
{
get { return opt.GetUpper(handle); }
@@ -139,7 +139,7 @@ namespace Microsoft.Z3
///
/// Retrieve the value of an objective.
- ///
+ ///
public ArithExpr Value
{
get { return Lower; }
@@ -147,7 +147,7 @@ namespace Microsoft.Z3
///
/// Retrieve a lower bound for the objective handle.
- ///
+ ///
public ArithExpr[] LowerAsVector
{
get { return opt.GetLowerAsVector(handle); }
@@ -155,7 +155,7 @@ namespace Microsoft.Z3
///
/// Retrieve an upper bound for the objective handle.
- ///
+ ///
public ArithExpr[] UpperAsVector
{
get { return opt.GetUpperAsVector(handle); }
@@ -240,7 +240,7 @@ namespace Microsoft.Z3
/// Declare an arithmetical maximization objective.
/// Return a handle to the objective. The handle is used as
/// to retrieve the values of objectives after calling Check.
- ///
+ ///
public Handle MkMaximize(ArithExpr e)
{
return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
@@ -249,7 +249,7 @@ namespace Microsoft.Z3
///
/// Declare an arithmetical minimization objective.
/// Similar to MkMaximize.
- ///
+ ///
public Handle MkMinimize(ArithExpr e)
{
return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
@@ -257,7 +257,7 @@ namespace Microsoft.Z3
///
/// Retrieve a lower bound for the objective handle.
- ///
+ ///
private ArithExpr GetLower(uint index)
{
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
@@ -266,7 +266,7 @@ namespace Microsoft.Z3
///
/// Retrieve an upper bound for the objective handle.
- ///
+ ///
private ArithExpr GetUpper(uint index)
{
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
@@ -274,7 +274,7 @@ namespace Microsoft.Z3
///
/// Retrieve a lower bound for the objective handle.
- ///
+ ///
private ArithExpr[] GetLowerAsVector(uint index)
{
ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_lower_as_vector(Context.nCtx, NativeObject, index));
@@ -284,29 +284,29 @@ namespace Microsoft.Z3
///
/// Retrieve an upper bound for the objective handle.
- ///
+ ///
private ArithExpr[] GetUpperAsVector(uint index)
{
ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index));
return v.ToArithExprArray();
}
- ///
- /// Return a string the describes why the last to check returned unknown
- ///
- public String ReasonUnknown
- {
+ ///
+ /// Return a string the describes why the last to check returned unknown
+ ///
+ public String ReasonUnknown
+ {
get
{
Contract.Ensures(Contract.Result() != null);
return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
}
- }
+ }
///
/// Print the context to a string (SMT-LIB parseable benchmark).
- ///
+ ///
public override string ToString()
{
return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
diff --git a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln
index b6e252684..1e33f136e 100644
--- a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln
+++ b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln
@@ -8,41 +8,41 @@ EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Example", "Example\Example.csproj", "{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}"
EndProject
Global
- GlobalSection(SolutionConfigurationPlatforms) = preSolution
- Debug|Any CPU = Debug|Any CPU
- Debug|x64 = Debug|x64
- Debug|x86 = Debug|x86
- Release|Any CPU = Release|Any CPU
- Release|x64 = Release|x64
- Release|x86 = Release|x86
- EndGlobalSection
- GlobalSection(ProjectConfigurationPlatforms) = postSolution
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.ActiveCfg = Debug|Any CPU
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.Build.0 = Debug|Any CPU
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.ActiveCfg = Debug|Any CPU
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.Build.0 = Debug|Any CPU
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.Build.0 = Release|Any CPU
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.ActiveCfg = Release|x64
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.Build.0 = Release|x64
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.ActiveCfg = Release|Any CPU
- {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.Build.0 = Release|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.ActiveCfg = Debug|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.Build.0 = Debug|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.ActiveCfg = Debug|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.Build.0 = Debug|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.Build.0 = Release|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.ActiveCfg = Release|x64
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.Build.0 = Release|x64
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.ActiveCfg = Release|Any CPU
- {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.Build.0 = Release|Any CPU
- EndGlobalSection
- GlobalSection(SolutionProperties) = preSolution
- HideSolutionNode = FALSE
- EndGlobalSection
+ GlobalSection(SolutionConfigurationPlatforms) = preSolution
+ Debug|Any CPU = Debug|Any CPU
+ Debug|x64 = Debug|x64
+ Debug|x86 = Debug|x86
+ Release|Any CPU = Release|Any CPU
+ Release|x64 = Release|x64
+ Release|x86 = Release|x86
+ EndGlobalSection
+ GlobalSection(ProjectConfigurationPlatforms) = postSolution
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.ActiveCfg = Debug|Any CPU
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.Build.0 = Debug|Any CPU
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.Build.0 = Debug|Any CPU
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.Build.0 = Release|Any CPU
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.ActiveCfg = Release|x64
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.Build.0 = Release|x64
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.ActiveCfg = Release|Any CPU
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.Build.0 = Release|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.ActiveCfg = Debug|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.Build.0 = Debug|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.Build.0 = Debug|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.Build.0 = Release|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.ActiveCfg = Release|x64
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.Build.0 = Release|x64
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.ActiveCfg = Release|Any CPU
+ {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.Build.0 = Release|Any CPU
+ EndGlobalSection
+ GlobalSection(SolutionProperties) = preSolution
+ HideSolutionNode = FALSE
+ EndGlobalSection
EndGlobal
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 4d9ab291a..b78f714b2 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -131,7 +131,7 @@ public class ASTVector extends Z3Object {
Expr[] res = new Expr[n];
for (int i = 0; i < n; i++)
res[i] = Expr.create(getContext(), get(i).getNativeObject());
- return res;
+ return res;
}
/**
diff --git a/src/api/java/AlgebraicNum.java b/src/api/java/AlgebraicNum.java
index 6725d3937..7369e06e3 100644
--- a/src/api/java/AlgebraicNum.java
+++ b/src/api/java/AlgebraicNum.java
@@ -22,57 +22,57 @@ package com.microsoft.z3;
**/
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^{@code precision}.
- *
- * @see Expr#isAlgebraicNumber
- * @param precision the precision of the result
- *
- * @return A numeral Expr of sort Real
- * @throws Z3Exception on error
- **/
- public RatNum toUpper(int precision)
- {
+ /**
+ * Return a upper bound for a given real algebraic number. The interval
+ * isolating the number is smaller than 1/10^{@code precision}.
+ *
+ * @see Expr#isAlgebraicNumber
+ * @param precision the precision of the result
+ *
+ * @return A numeral Expr of sort Real
+ * @throws Z3Exception on error
+ **/
+ public RatNum toUpper(int precision)
+ {
- return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext()
- .nCtx(), getNativeObject(), precision));
- }
+ return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext()
+ .nCtx(), getNativeObject(), precision));
+ }
- /**
- * Return a lower bound for the given real algebraic number. The interval
- * isolating the number is smaller than 1/10^{@code precision}.
- *
- * @see Expr#isAlgebraicNumber
- * @param precision precision
- *
- * @return A numeral Expr of sort Real
- * @throws Z3Exception on error
- **/
- public RatNum toLower(int precision)
- {
+ /**
+ * Return a lower bound for the given real algebraic number. The interval
+ * isolating the number is smaller than 1/10^{@code precision}.
+ *
+ * @see Expr#isAlgebraicNumber
+ * @param precision precision
+ *
+ * @return A numeral Expr of sort Real
+ * @throws Z3Exception on error
+ **/
+ public RatNum toLower(int precision)
+ {
- return new RatNum(getContext(), Native.getAlgebraicNumberLower(getContext()
- .nCtx(), getNativeObject(), precision));
- }
+ return new RatNum(getContext(), Native.getAlgebraicNumberLower(getContext()
+ .nCtx(), getNativeObject(), precision));
+ }
- /**
- * Returns a string representation in decimal notation.
- * Remarks: The result has at most {@code precision} decimal places.
- * @param precision precision
- * @return String
- * @throws Z3Exception on error
- **/
- public String toDecimal(int precision)
- {
+ /**
+ * Returns a string representation in decimal notation.
+ * Remarks: The result has at most {@code precision} decimal places.
+ * @param precision precision
+ * @return String
+ * @throws Z3Exception on error
+ **/
+ public String toDecimal(int precision)
+ {
- return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
- precision);
- }
+ return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
+ precision);
+ }
- AlgebraicNum(Context ctx, long obj)
- {
- super(ctx, obj);
+ AlgebraicNum(Context ctx, long obj)
+ {
+ super(ctx, obj);
- }
+ }
}
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 2609dbb29..72866a0ba 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -1898,8 +1898,8 @@ public class Context implements AutoCloseable {
*/
public SeqExpr mkEmptySeq(Sort s)
{
- checkContextMatch(s);
- return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
+ checkContextMatch(s);
+ return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
}
/**
@@ -1907,8 +1907,8 @@ public class Context implements AutoCloseable {
*/
public SeqExpr mkUnit(Expr elem)
{
- checkContextMatch(elem);
- return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
+ checkContextMatch(elem);
+ return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
}
/**
@@ -1916,7 +1916,7 @@ public class Context implements AutoCloseable {
*/
public SeqExpr mkString(String s)
{
- return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
+ return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
}
/**
@@ -1924,8 +1924,8 @@ public class Context implements AutoCloseable {
*/
public SeqExpr mkConcat(SeqExpr... t)
{
- checkContextMatch(t);
- return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
+ checkContextMatch(t);
+ return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
}
@@ -1934,8 +1934,8 @@ public class Context implements AutoCloseable {
*/
public IntExpr mkLength(SeqExpr s)
{
- checkContextMatch(s);
- return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
+ checkContextMatch(s);
+ return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
}
/**
@@ -1943,8 +1943,8 @@ public class Context implements AutoCloseable {
*/
public BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
{
- checkContextMatch(s1, s2);
- return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+ checkContextMatch(s1, s2);
+ return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
}
/**
@@ -1952,8 +1952,8 @@ public class Context implements AutoCloseable {
*/
public BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
{
- checkContextMatch(s1, s2);
- return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+ checkContextMatch(s1, s2);
+ return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
}
/**
@@ -1961,8 +1961,8 @@ public class Context implements AutoCloseable {
*/
public BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
{
- checkContextMatch(s1, s2);
- return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+ checkContextMatch(s1, s2);
+ return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
}
/**
@@ -1970,8 +1970,8 @@ public class Context implements AutoCloseable {
*/
public SeqExpr mkAt(SeqExpr s, IntExpr index)
{
- checkContextMatch(s, index);
- return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
+ checkContextMatch(s, index);
+ return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
}
/**
@@ -1979,8 +1979,8 @@ public class Context implements AutoCloseable {
*/
public SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
{
- checkContextMatch(s, offset, length);
- return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
+ checkContextMatch(s, offset, length);
+ return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
}
/**
@@ -1988,8 +1988,8 @@ public class Context implements AutoCloseable {
*/
public IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
{
- checkContextMatch(s, substr, offset);
- return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
+ checkContextMatch(s, substr, offset);
+ return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
}
/**
@@ -1997,8 +1997,8 @@ public class Context implements AutoCloseable {
*/
public SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
{
- checkContextMatch(s, src, dst);
- return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
+ checkContextMatch(s, src, dst);
+ return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
}
/**
@@ -2006,8 +2006,8 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkToRe(SeqExpr s)
{
- checkContextMatch(s);
- return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
+ checkContextMatch(s);
+ return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
}
@@ -2016,8 +2016,8 @@ public class Context implements AutoCloseable {
*/
public BoolExpr mkInRe(SeqExpr s, ReExpr re)
{
- checkContextMatch(s, re);
- return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
+ checkContextMatch(s, re);
+ return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
}
/**
@@ -2025,8 +2025,8 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkStar(ReExpr re)
{
- checkContextMatch(re);
- return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
+ checkContextMatch(re);
+ return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
}
/**
@@ -2034,7 +2034,7 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkLoop(ReExpr re, int lo, int hi)
{
- return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
+ return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
}
/**
@@ -2042,7 +2042,7 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkLoop(ReExpr re, int lo)
{
- return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
+ return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
}
@@ -2051,8 +2051,8 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkPlus(ReExpr re)
{
- checkContextMatch(re);
- return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
+ checkContextMatch(re);
+ return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
}
/**
@@ -2060,8 +2060,8 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkOption(ReExpr re)
{
- checkContextMatch(re);
- return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
+ checkContextMatch(re);
+ return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
}
@@ -2070,8 +2070,8 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkComplement(ReExpr re)
{
- checkContextMatch(re);
- return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
+ checkContextMatch(re);
+ return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
}
/**
@@ -2079,8 +2079,8 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkConcat(ReExpr... t)
{
- checkContextMatch(t);
- return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
+ checkContextMatch(t);
+ return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
}
/**
@@ -2088,8 +2088,8 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkUnion(ReExpr... t)
{
- checkContextMatch(t);
- return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
+ checkContextMatch(t);
+ return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
}
/**
@@ -2097,8 +2097,8 @@ public class Context implements AutoCloseable {
*/
public ReExpr mkIntersect(ReExpr... t)
{
- checkContextMatch(t);
- return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
+ checkContextMatch(t);
+ return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
}
/**
@@ -2106,8 +2106,8 @@ public class Context implements AutoCloseable {
*/
public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
{
- checkContextMatch(lo, hi);
- return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
+ checkContextMatch(lo, hi);
+ return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
}
@@ -2116,8 +2116,8 @@ public class Context implements AutoCloseable {
*/
public BoolExpr mkAtMost(BoolExpr[] args, int k)
{
- checkContextMatch(args);
- return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
+ checkContextMatch(args);
+ return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
}
/**
@@ -2125,8 +2125,8 @@ public class Context implements AutoCloseable {
*/
public BoolExpr mkAtLeast(BoolExpr[] args, int k)
{
- checkContextMatch(args);
- return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
+ checkContextMatch(args);
+ return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
}
/**
@@ -2134,8 +2134,8 @@ public class Context implements AutoCloseable {
*/
public BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
{
- checkContextMatch(args);
- return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
+ checkContextMatch(args);
+ return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
}
/**
@@ -2143,8 +2143,8 @@ public class Context implements AutoCloseable {
*/
public BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
{
- checkContextMatch(args);
- return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
+ checkContextMatch(args);
+ return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
}
/**
@@ -2152,8 +2152,8 @@ public class Context implements AutoCloseable {
*/
public BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
{
- checkContextMatch(args);
- return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
+ checkContextMatch(args);
+ return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
}
@@ -3988,15 +3988,15 @@ public class Context implements AutoCloseable {
void checkContextMatch(Z3Object other1, Z3Object other2)
{
- checkContextMatch(other1);
- checkContextMatch(other2);
+ checkContextMatch(other1);
+ checkContextMatch(other2);
}
void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
{
- checkContextMatch(other1);
- checkContextMatch(other2);
- checkContextMatch(other3);
+ checkContextMatch(other1);
+ checkContextMatch(other2);
+ checkContextMatch(other3);
}
void checkContextMatch(Z3Object[] arr)
diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java
index ce2f8d578..e0bd0f617 100644
--- a/src/api/java/EnumSort.java
+++ b/src/api/java/EnumSort.java
@@ -65,7 +65,7 @@ public class EnumSort extends Sort
**/
public Expr getConst(int inx)
{
- return getContext().mkApp(getConstDecl(inx));
+ return getContext().mkApp(getConstDecl(inx));
}
/**
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 6cabbb1b8..d3793a24b 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -1287,7 +1287,7 @@ public class Expr extends AST
*/
public String getString()
{
- return Native.getString(getContext().nCtx(), getNativeObject());
+ return Native.getString(getContext().nCtx(), getNativeObject());
}
/**
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index 60abb001d..9c7013aca 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -200,7 +200,7 @@ public class Model extends Z3Object {
* Remarks: This function may fail if {@code t} contains
* quantifiers, is partial (MODEL_PARTIAL enabled), or if {@code t} is not well-sorted. In this case a
* {@code ModelEvaluationFailedException} is thrown.
- * @param t the expression to evaluate
+ * @param t the expression to evaluate
* @param completion An expression {@code 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.
diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java
index bc2232888..3edbff73e 100644
--- a/src/api/java/Optimize.java
+++ b/src/api/java/Optimize.java
@@ -213,7 +213,7 @@ public class Optimize extends Z3Object {
* Declare an arithmetical maximization objective.
* Return a handle to the objective. The handle is used as
* to retrieve the values of objectives after calling Check.
- **/
+ **/
public Handle MkMaximize(ArithExpr e)
{
return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
@@ -285,8 +285,7 @@ public class Optimize extends Z3Object {
**/
public String getReasonUnknown()
{
- return Native.optimizeGetReasonUnknown(getContext().nCtx(),
- getNativeObject());
+ return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
}
/**
@@ -304,7 +303,7 @@ public class Optimize extends Z3Object {
*/
public void fromFile(String file)
{
- Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
+ Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
}
/**
@@ -312,7 +311,7 @@ public class Optimize extends Z3Object {
*/
public void fromString(String s)
{
- Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
+ Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
}
diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java
index 0008515e3..fdaf29647 100644
--- a/src/api/java/ParamDescrs.java
+++ b/src/api/java/ParamDescrs.java
@@ -49,7 +49,7 @@ public class ParamDescrs extends Z3Object {
public String getDocumentation(Symbol name)
{
- return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject());
+ return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject());
}
/**
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index a98fcbf94..19f3b01da 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -302,7 +302,7 @@ public class Solver extends Z3Object {
*/
public Solver translate(Context ctx)
{
- return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
+ return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
}
/**
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index e7a186ad2..a89417059 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -35,12 +35,8 @@ public class Sort extends AST
if (!(o instanceof Sort)) return false;
Sort other = (Sort) o;
- return (getContext().nCtx() == other.getContext().nCtx()) &&
- (Native.isEqSort(
- getContext().nCtx(),
- getNativeObject(),
- other.getNativeObject()
- ));
+ return (getContext().nCtx() == other.getContext().nCtx()) &&
+ (Native.isEqSort(getContext().nCtx(), getNativeObject(), other.getNativeObject()));
}
/**
diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre
index 1b1ea3fde..c1c772c85 100644
--- a/src/api/ml/z3native_stubs.c.pre
+++ b/src/api/ml/z3native_stubs.c.pre
@@ -25,34 +25,34 @@ extern "C" {
#include
#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \
- CAMLlocal5(X1,X2,X3,X4,X5); \
+ CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal1(X6)
-#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \
- CAMLlocal5(X1,X2,X3,X4,X5); \
+#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \
+ CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal2(X6,X7)
-#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \
- CAMLlocal5(X1,X2,X3,X4,X5); \
+#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \
+ CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal3(X6,X7,X8)
-#define CAMLparam6(X1,X2,X3,X4,X5,X6) \
- CAMLparam5(X1,X2,X3,X4,X5); \
+#define CAMLparam6(X1,X2,X3,X4,X5,X6) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam1(X6)
-#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \
- CAMLparam5(X1,X2,X3,X4,X5); \
+#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam2(X6,X7)
-#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \
- CAMLparam5(X1,X2,X3,X4,X5); \
+#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam3(X6,X7,X8)
-#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \
- CAMLparam5(X1,X2,X3,X4,X5); \
+#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam4(X6,X7,X8,X9)
-#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \
- CAMLparam5(X1,X2,X3,X4,X5); \
- CAMLxparam5(X6,X7,X8,X9,X10); \
+#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
+ CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam2(X11,X12)
-#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \
- CAMLparam5(X1,X2,X3,X4,X5); \
- CAMLxparam5(X6,X7,X8,X9,X10); \
+#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
+ CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam3(X11,X12,X13)
diff --git a/src/api/ml/z3native_stubs.h b/src/api/ml/z3native_stubs.h
index ef81ac239..ec498dafe 100644
--- a/src/api/ml/z3native_stubs.h
+++ b/src/api/ml/z3native_stubs.h
@@ -36,5 +36,5 @@ Notes:
#define DLL_LOCAL
#endif
#endif
-
+
#endif
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index cd3b0ccca..bc0364994 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -3240,10 +3240,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
// NaN, Inf, or negative (except -0) -> unspecified
expr_ref c1(m), v1(m), unspec_v(m);
- if (!is_signed)
- c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
- else
- c1 = m.mk_or(x_is_nan, x_is_inf);
+ c1 = m.mk_or(x_is_nan, x_is_inf);
mk_to_bv_unspecified(f, num, args, unspec_v);
v1 = unspec_v;
dbg_decouple("fpa2bv_to_bv_c1", c1);
@@ -3335,18 +3332,18 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
dbg_decouple("fpa2bv_to_bv_inc", inc);
dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
- expr_ref in_range(m);
+ pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded);
+
+ expr_ref ll(m), ul(m), in_range(m);
if (!is_signed) {
- expr_ref ul(m);
+ ll = m_bv_util.mk_numeral(0, bv_sz+3);
ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz));
- in_range = m_bv_util.mk_ule(pre_rounded, ul);
}
else {
- expr_ref ll(m), ul(m);
ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_numeral(-1, bv_sz-1));
- in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
}
+ in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
dbg_decouple("fpa2bv_to_bv_in_range", in_range);
expr_ref rounded(m);
diff --git a/src/ast/rewriter/array_rewriter_params.pyg b/src/ast/rewriter/array_rewriter_params.pyg
index a43fadecf..3b4af7fb7 100644
--- a/src/ast/rewriter/array_rewriter_params.pyg
+++ b/src/ast/rewriter/array_rewriter_params.pyg
@@ -2,5 +2,5 @@ def_module_params(module_name='rewriter',
class_name='array_rewriter_params',
export=True,
params=(("expand_select_store", BOOL, False, "replace a (select (store ...) ...) term by an if-then-else term"),
- ("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"),
+ ("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"),
("sort_store", BOOL, False, "sort nested stores when the indices are known to be different")))
diff --git a/src/ast/rewriter/bit2int.h b/src/ast/rewriter/bit2int.h
index fe15d1ec5..fbbf2e6d1 100644
--- a/src/ast/rewriter/bit2int.h
+++ b/src/ast/rewriter/bit2int.h
@@ -75,7 +75,7 @@ protected:
bool mk_mul(expr* a, expr* b, expr_ref& result);
bool mk_comp(eq_type ty, expr* e1, expr* e2, expr_ref& result);
bool mk_add(expr* e1, expr* e2, expr_ref& result);
-
+
expr * get_cached(expr * n) const;
bool is_cached(expr * n) const { return get_cached(n) != 0; }
void cache_result(expr * n, expr * r);
diff --git a/src/ast/rewriter/bv_bounds.h b/src/ast/rewriter/bv_bounds.h
index 3d8ec9ebb..4a7226fa7 100644
--- a/src/ast/rewriter/bv_bounds.h
+++ b/src/ast/rewriter/bv_bounds.h
@@ -38,7 +38,7 @@ public:
bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {};
~bv_bounds();
public: // bounds addition methods
- br_status rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result);
+ br_status rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result);
/** \brief Add a constraint to the system.
@@ -82,7 +82,7 @@ protected:
bv_util m_bv_util;
bool m_okay;
bool is_sat(app * v);
- bool is_sat_core(app * v);
+bool is_sat_core(app * v);
inline bool in_range(app *v, numeral l);
inline bool is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val);
void record_singleton(app * v, numeral& singleton_value);
@@ -94,7 +94,7 @@ protected:
inline bool bv_bounds::is_okay() { return m_okay; }
inline bool bv_bounds::to_bound(const expr * e) const {
- return is_app(e) && m_bv_util.is_bv(e)
+ return is_app(e) && m_bv_util.is_bv(e)
&& !m_bv_util.is_bv_add(e)
&& !m_bv_util.is_numeral(e);
}
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 09307cbf2..6420dd968 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -772,7 +772,6 @@ br_status fpa_rewriter::mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool i
if (m_util.is_rm_numeral(arg1, rmv) &&
m_util.is_numeral(arg2, v)) {
- const mpf & x = v.get();
if (m_fm.is_nan(v) || m_fm.is_inf(v))
return mk_to_bv_unspecified(f, result);
diff --git a/src/ast/rewriter/fpa_rewriter_params.pyg b/src/ast/rewriter/fpa_rewriter_params.pyg
index f0cfbdf55..487c50a85 100644
--- a/src/ast/rewriter/fpa_rewriter_params.pyg
+++ b/src/ast/rewriter/fpa_rewriter_params.pyg
@@ -1,5 +1,5 @@
def_module_params(module_name='rewriter',
class_name='fpa_rewriter_params',
export=True,
- params=(("hi_fp_unspecified", BOOL, False, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, fp.to_real, and fp.to_ieee_bv"),
+ params=(("hi_fp_unspecified", BOOL, False, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, fp.to_real, and fp.to_ieee_bv"),
))
diff --git a/src/duality/duality.h b/src/duality/duality.h
index 0ef6be30e..657fa18b4 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -21,6 +21,7 @@
#pragma once
#include "duality/duality_wrapper.h"
+#include
#include
#include