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..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 #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", "=> GetId(i) = i, => 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 void lp_core_solver_base:: 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 void lp_primal_core_solver::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 bool static_matrix::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 bool static_matrix::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);