From db398eca7a45dd3f3f7cd747e83befb52a6dc68b Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 17 Sep 2017 17:50:05 +0100
Subject: [PATCH] Tabs, formatting.
---
src/api/dotnet/CMakeLists.txt | 144 +++++++++---------
src/api/dotnet/Context.cs | 6 +-
src/api/dotnet/Expr.cs | 18 +--
src/api/dotnet/Optimize.cs | 36 ++---
.../dotnet/dotnet35/Microsoft.Z3.NET35.sln | 74 ++++-----
src/api/java/ASTVector.java | 2 +-
src/api/java/AlgebraicNum.java | 92 +++++------
src/api/java/Context.java | 120 +++++++--------
src/api/java/EnumSort.java | 2 +-
src/api/java/Expr.java | 2 +-
src/api/java/Model.java | 2 +-
src/api/java/Optimize.java | 9 +-
src/api/java/ParamDescrs.java | 2 +-
src/api/java/Solver.java | 2 +-
src/api/java/Sort.java | 8 +-
src/api/ml/z3native_stubs.c.pre | 38 ++---
src/ast/rewriter/array_rewriter_params.pyg | 2 +-
src/ast/rewriter/fpa_rewriter_params.pyg | 2 +-
src/muz/base/fixedpoint_params.pyg | 44 +++---
src/opt/opt_params.pyg | 2 +-
src/tactic/sls/.#sls_params.pyg | 1 +
src/tactic/sls/sls_params.pyg | 44 +++---
src/util/lp/CMakeLists.txt | 2 +-
src/util/lp/lp_core_solver_base.hpp | 4 +-
src/util/lp/lp_primal_core_solver_tableau.h | 2 +-
src/util/lp/static_matrix.hpp | 6 +-
26 files changed, 331 insertions(+), 335 deletions(-)
create mode 100644 src/tactic/sls/.#sls_params.pyg
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;
/// <summary>
/// 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<SeqExpr>() != null);
return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
}
@@ -2690,7 +2690,7 @@ namespace Microsoft.Z3
/// <summary>
/// Create a range expression.
/// </summary>
- 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.
/// </summary>
/// <returns>a Boolean</returns>
- 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; } }
/// <summary>
/// Check whether expression is a prefix.
/// </summary>
/// <returns>a Boolean</returns>
- 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; } }
/// <summary>
/// Check whether expression is a suffix.
/// </summary>
/// <returns>a Boolean</returns>
- 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; } }
/// <summary>
/// Check whether expression is a contains.
/// </summary>
/// <returns>a Boolean</returns>
- 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; } }
/// <summary>
/// Check whether expression is an extract.
/// </summary>
/// <returns>a Boolean</returns>
- 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; } }
/// <summary>
/// Check whether expression is a replace.
/// </summary>
/// <returns>a Boolean</returns>
- 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; } }
/// <summary>
/// Check whether expression is an at.
/// </summary>
/// <returns>a Boolean</returns>
- 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; } }
/// <summary>
/// Check whether expression is a sequence length.
/// </summary>
/// <returns>a Boolean</returns>
- 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; } }
/// <summary>
/// Check whether expression is a sequence index.
/// </summary>
/// <returns>a Boolean</returns>
- 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
/// <summary>
/// Retrieve a lower bound for the objective handle.
- /// </summary>
+ /// </summary>
public ArithExpr Lower
{
get { return opt.GetLower(handle); }
@@ -131,7 +131,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve an upper bound for the objective handle.
- /// </summary>
+ /// </summary>
public ArithExpr Upper
{
get { return opt.GetUpper(handle); }
@@ -139,7 +139,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve the value of an objective.
- /// </summary>
+ /// </summary>
public ArithExpr Value
{
get { return Lower; }
@@ -147,7 +147,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve a lower bound for the objective handle.
- /// </summary>
+ /// </summary>
public ArithExpr[] LowerAsVector
{
get { return opt.GetLowerAsVector(handle); }
@@ -155,7 +155,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve an upper bound for the objective handle.
- /// </summary>
+ /// </summary>
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.
- /// </summary>
+ /// </summary>
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
/// <summary>
/// Declare an arithmetical minimization objective.
/// Similar to MkMaximize.
- /// </summary>
+ /// </summary>
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
/// <summary>
/// Retrieve a lower bound for the objective handle.
- /// </summary>
+ /// </summary>
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
/// <summary>
/// Retrieve an upper bound for the objective handle.
- /// </summary>
+ /// </summary>
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
/// <summary>
/// Retrieve a lower bound for the objective handle.
- /// </summary>
+ /// </summary>
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
/// <summary>
/// Retrieve an upper bound for the objective handle.
- /// </summary>
+ /// </summary>
private ArithExpr[] GetUpperAsVector(uint index)
{
ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index));
return v.ToArithExprArray();
}
- /// <summary>
- /// Return a string the describes why the last to check returned unknown
- /// </summary>
- public String ReasonUnknown
- {
+ /// <summary>
+ /// Return a string the describes why the last to check returned unknown
+ /// </summary>
+ public String ReasonUnknown
+ {
get
{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
}
- }
+ }
/// <summary>
/// Print the context to a string (SMT-LIB parseable benchmark).
- /// </summary>
+ /// </summary>
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..986736fb6 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()));
+ checkContextMatchb(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 <z3native_stubs.h>
#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/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/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/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index 110f081b0..0c2f03460 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -4,7 +4,7 @@ def_module_params('fixedpoint',
params=(('timeout', UINT, UINT_MAX, 'set timeout'),
('engine', SYMBOL, 'auto-config',
'Select: auto-config, datalog, duality, pdr, bmc, spacer'),
- ('datalog.default_table', SYMBOL, 'sparse',
+ ('datalog.default_table', SYMBOL, 'sparse',
'default table implementation: sparse, hashtable, bitvector, interval'),
('datalog.default_relation', SYMBOL, 'pentagon',
'default relation implementation: external_relation, pentagon'),
@@ -56,18 +56,18 @@ def_module_params('fixedpoint',
"table columns, if it would have been empty otherwise"),
('datalog.subsumption', BOOL, True,
"if true, removes/filters predicates with total transitions"),
- ('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
- ('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
- ('duality.feasible_edges', BOOL, True,
+ ('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
+ ('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
+ ('duality.feasible_edges', BOOL, True,
'Don\'t expand definitley infeasible edges'),
- ('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
- ('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
- ('duality.recursion_bound', UINT, UINT_MAX,
+ ('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
+ ('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
+ ('duality.recursion_bound', UINT, UINT_MAX,
'Recursion bound for stratified inlining'),
- ('duality.profile', BOOL, False, 'profile run time'),
- ('duality.mbqi', BOOL, True, 'use model-based quantifier instantiation'),
- ('duality.batch_expand', BOOL, False, 'use batch expansion'),
- ('duality.conjecture_file', STRING, '', 'save conjectures to file'),
+ ('duality.profile', BOOL, False, 'profile run time'),
+ ('duality.mbqi', BOOL, True, 'use model-based quantifier instantiation'),
+ ('duality.batch_expand', BOOL, False, 'use batch expansion'),
+ ('duality.conjecture_file', STRING, '', 'save conjectures to file'),
('pdr.bfs_model_search', BOOL, True,
"use BFS strategy for expanding model search"),
('pdr.farkas', BOOL, True,
@@ -92,9 +92,9 @@ def_module_params('fixedpoint',
"generalize lemmas using induction strengthening"),
('pdr.use_arith_inductive_generalizer', BOOL, False,
"generalize lemmas using arithmetic heuristics for induction strengthening"),
- ('pdr.use_convex_closure_generalizer', BOOL, False,
+ ('pdr.use_convex_closure_generalizer', BOOL, False,
"generalize using convex closures of lemmas"),
- ('pdr.use_convex_interior_generalizer', BOOL, False,
+ ('pdr.use_convex_interior_generalizer', BOOL, False,
"generalize using convex interiors of lemmas"),
('pdr.cache_mode', UINT, 0, "use no (0), symbolic (1) or explicit " +
"cache (2) for model search"),
@@ -104,7 +104,7 @@ def_module_params('fixedpoint',
('pdr.max_num_contexts', UINT, 500, "maximal number of contexts to create"),
('pdr.try_minimize_core', BOOL, False,
"try to reduce core size (before inductive minimization)"),
- ('pdr.utvpi', BOOL, True, 'Enable UTVPI strategy'),
+ ('pdr.utvpi', BOOL, True, 'Enable UTVPI strategy'),
('print_fixedpoint_extensions', BOOL, True,
"use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, " +
"when printing rules"),
@@ -123,7 +123,7 @@ def_module_params('fixedpoint',
('print_statistics', BOOL, False, 'print statistics'),
('print_aig', SYMBOL, '',
'Dump clauses in AIG text format (AAG) to the given file name'),
- ('tab.selection', SYMBOL, 'weight',
+ ('tab.selection', SYMBOL, 'weight',
'selection method for tabular strategy: weight (default), first, var-use'),
('xform.bit_blast', BOOL, False,
'bit-blast bit-vectors'),
@@ -140,7 +140,7 @@ def_module_params('fixedpoint',
('xform.unfold_rules', UINT, 0,
"unfold rules statically using iterative squarring"),
('xform.slice', BOOL, True, "simplify clause set using slicing"),
- ('xform.karr', BOOL, False,
+ ('xform.karr', BOOL, False,
"Add linear invariants to clauses using Karr's method"),
('spacer.use_eqclass', BOOL, False, "Generalizes equalities to equivalence classes"),
('xform.transform_arrays', BOOL, False,
@@ -153,24 +153,24 @@ def_module_params('fixedpoint',
"Gives the number of quantifiers per array"),
('xform.instantiate_arrays.slice_technique', SYMBOL, "no-slicing",
"<no-slicing>=> GetId(i) = i, <smash> => GetId(i) = true"),
- ('xform.quantify_arrays', BOOL, False,
+ ('xform.quantify_arrays', BOOL, False,
"create quantified Horn clauses from clauses with arrays"),
- ('xform.instantiate_quantifiers', BOOL, False,
+ ('xform.instantiate_quantifiers', BOOL, False,
"instantiate quantified Horn clauses using E-matching heuristic"),
('xform.coalesce_rules', BOOL, False, "coalesce rules"),
('xform.tail_simplifier_pve', BOOL, True, "propagate_variable_equivalences"),
('xform.subsumption_checker', BOOL, True, "Enable subsumption checker (no support for model conversion)"),
- ('xform.coi', BOOL, True, "use cone of influence simplificaiton"),
- ('duality.enable_restarts', BOOL, False, 'DUALITY: enable restarts'),
+ ('xform.coi', BOOL, True, "use cone of influence simplification"),
+ ('duality.enable_restarts', BOOL, False, 'DUALITY: enable restarts'),
('spacer.order_children', UINT, 0, 'SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse)'),
('spacer.eager_reach_check', BOOL, True, 'SPACER: eagerly check if a query is reachable using reachability facts of predecessors'),
('spacer.use_lemma_as_cti', BOOL, False, 'SPACER: use a lemma instead of a CTI in flexible_trace'),
('spacer.reset_obligation_queue', BOOL, True, 'SPACER: reset obligation queue when entering a new level'),
('spacer.init_reach_facts', BOOL, True, 'SPACER: initialize reachability facts with false'),
('spacer.use_array_eq_generalizer', BOOL, True, 'SPACER: attempt to generalize lemmas with array equalities'),
- ('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'),
+ ('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'),
('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"),
- ('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"),
+ ('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"),
('spacer.skip_propagate', BOOL, False, "Skip propagate/pushing phase. Turns PDR into a BMC that returns either reachable or unknown"),
('spacer.max_level', UINT, UINT_MAX, "Maximum level to explore"),
('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 13bf51313..cfcc5e47e 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -2,7 +2,7 @@ def_module_params('opt',
description='optimization parameters',
export=True,
params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
- ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
+ ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
diff --git a/src/tactic/sls/.#sls_params.pyg b/src/tactic/sls/.#sls_params.pyg
new file mode 100644
index 000000000..50991f6f4
--- /dev/null
+++ b/src/tactic/sls/.#sls_params.pyg
@@ -0,0 +1 @@
+winte@WINTERMUTE.13536:1505663874
\ No newline at end of file
diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg
index bf5bd181a..05405ef24 100644
--- a/src/tactic/sls/sls_params.pyg
+++ b/src/tactic/sls/sls_params.pyg
@@ -2,25 +2,25 @@ def_module_params('sls',
export=True,
description='Experimental Stochastic Local Search Solver (for QFBV only).',
params=(max_memory_param(),
- ('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'),
- ('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'),
- ('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'),
- ('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'),
- ('walksat_ucb_init', BOOL, 0, 'initialize total ucb touched to formula size'),
- ('walksat_ucb_forget', DOUBLE, 1.0, 'scale touched by this factor every base restart interval'),
- ('walksat_ucb_noise', DOUBLE, 0.0002, 'add noise 0 <= 256 * ucb_noise to ucb score for assertion selection'),
- ('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'),
- ('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'),
- ('paws_init', UINT, 40, 'initial/minimum assertion weights'),
- ('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'),
- ('wp', UINT, 100, 'random walk with probability wp / 1024'),
- ('vns_mc', UINT, 0, 'in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit'),
- ('vns_repick', BOOL, 0, 'in local minima, try picking a different assertion (only for walksat)'),
- ('restart_base', UINT, 100, 'base restart interval given by moves per run'),
- ('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'),
- ('early_prune', BOOL, 1, 'use early pruning for score prediction'),
- ('random_offset', BOOL, 1, 'use random offset for candidate evaluation'),
- ('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
- ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
- ('random_seed', UINT, 0, 'random seed')
- ))
+ ('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'),
+ ('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'),
+ ('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'),
+ ('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'),
+ ('walksat_ucb_init', BOOL, 0, 'initialize total ucb touched to formula size'),
+ ('walksat_ucb_forget', DOUBLE, 1.0, 'scale touched by this factor every base restart interval'),
+ ('walksat_ucb_noise', DOUBLE, 0.0002, 'add noise 0 <= 256 * ucb_noise to ucb score for assertion selection'),
+ ('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'),
+ ('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'),
+ ('paws_init', UINT, 40, 'initial/minimum assertion weights'),
+ ('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'),
+ ('wp', UINT, 100, 'random walk with probability wp / 1024'),
+ ('vns_mc', UINT, 0, 'in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit'),
+ ('vns_repick', BOOL, 0, 'in local minima, try picking a different assertion (only for walksat)'),
+ ('restart_base', UINT, 100, 'base restart interval given by moves per run'),
+ ('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'),
+ ('early_prune', BOOL, 1, 'use early pruning for score prediction'),
+ ('random_offset', BOOL, 1, 'use random offset for candidate evaluation'),
+ ('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
+ ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
+ ('random_seed', UINT, 0, 'random seed')
+ ))
diff --git a/src/util/lp/CMakeLists.txt b/src/util/lp/CMakeLists.txt
index ca8683434..70c5f9e3b 100644
--- a/src/util/lp/CMakeLists.txt
+++ b/src/util/lp/CMakeLists.txt
@@ -19,7 +19,7 @@ z3_add_component(lp
lu_instances.cpp
matrix_instances.cpp
permutation_matrix_instances.cpp
- quick_xplain.cpp
+ quick_xplain.cpp
row_eta_matrix_instances.cpp
scaler_instances.cpp
sparse_matrix_instances.cpp
diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp
index fa1c95850..b49dd0638 100644
--- a/src/util/lp/lp_core_solver_base.hpp
+++ b/src/util/lp/lp_core_solver_base.hpp
@@ -98,8 +98,8 @@ pivot_for_tableau_on_basis() {
// i is the pivot row, and j is the pivot column
template <typename T, typename X> void lp_core_solver_base<T, X>::
pivot_to_reduced_costs_tableau(unsigned i, unsigned j) {
- if (j >= m_d.size())
- return;
+ if (j >= m_d.size())
+ return;
T &a = m_d[j];
if (is_zero(a))
return;
diff --git a/src/util/lp/lp_primal_core_solver_tableau.h b/src/util/lp/lp_primal_core_solver_tableau.h
index 97fa2f9da..5c7d4d2c2 100644
--- a/src/util/lp/lp_primal_core_solver_tableau.h
+++ b/src/util/lp/lp_primal_core_solver_tableau.h
@@ -318,7 +318,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tab
this->m_basis_sort_counter = 0; // to initiate the sort of the basis
this->set_total_iterations(0);
this->iters_with_no_cost_growing() = 0;
- SASSERT(this->inf_set_is_correct());
+ SASSERT(this->inf_set_is_correct());
if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
return;
if (this->m_settings.backup_costs)
diff --git a/src/util/lp/static_matrix.hpp b/src/util/lp/static_matrix.hpp
index d8681ff93..846c2a19f 100644
--- a/src/util/lp/static_matrix.hpp
+++ b/src/util/lp/static_matrix.hpp
@@ -48,9 +48,9 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
SASSERT(i < row_count() && ii < column_count());
SASSERT(i != ii);
- m_became_zeros.reset();
+ m_became_zeros.reset();
T alpha = -get_val(c);
- SASSERT(!is_zero(alpha));
+ SASSERT(!is_zero(alpha));
auto & ii_row_vals = m_rows[ii];
remove_element(ii_row_vals, ii_row_vals[c.m_offset]);
scan_row_ii_to_offset_vector(ii);
@@ -61,7 +61,7 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
unsigned j = iv.m_j;
if (j == pivot_col) continue;
T alv = alpha * iv.m_value;
- SASSERT(!is_zero(iv.m_value));
+ SASSERT(!is_zero(iv.m_value));
int j_offs = m_vector_of_row_offsets[j];
if (j_offs == -1) { // it is a new element
add_new_element(ii, j, alv);