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

Tabs, formatting.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-09-17 17:50:05 +01:00
parent 56e20da3ce
commit db398eca7a
26 changed files with 331 additions and 335 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

144
src/api/dotnet/CMakeLists.txt
View file

@ -43,78 +43,78 @@ add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}"
) )
set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
AlgebraicNum.cs AlgebraicNum.cs
ApplyResult.cs ApplyResult.cs
ArithExpr.cs ArithExpr.cs
ArithSort.cs ArithSort.cs
ArrayExpr.cs ArrayExpr.cs
ArraySort.cs ArraySort.cs
AST.cs AST.cs
ASTMap.cs ASTMap.cs
ASTVector.cs ASTVector.cs
BitVecExpr.cs BitVecExpr.cs
BitVecNum.cs BitVecNum.cs
BitVecSort.cs BitVecSort.cs
BoolExpr.cs BoolExpr.cs
BoolSort.cs BoolSort.cs
Constructor.cs Constructor.cs
ConstructorList.cs ConstructorList.cs
Context.cs Context.cs
DatatypeExpr.cs DatatypeExpr.cs
DatatypeSort.cs DatatypeSort.cs
Deprecated.cs Deprecated.cs
EnumSort.cs EnumSort.cs
Expr.cs Expr.cs
FiniteDomainExpr.cs FiniteDomainExpr.cs
FiniteDomainNum.cs FiniteDomainNum.cs
FiniteDomainSort.cs FiniteDomainSort.cs
Fixedpoint.cs Fixedpoint.cs
FPExpr.cs FPExpr.cs
FPNum.cs FPNum.cs
FPRMExpr.cs FPRMExpr.cs
FPRMNum.cs FPRMNum.cs
FPRMSort.cs FPRMSort.cs
FPSort.cs FPSort.cs
FuncDecl.cs FuncDecl.cs
FuncInterp.cs FuncInterp.cs
Global.cs Global.cs
Goal.cs Goal.cs
IDecRefQueue.cs IDecRefQueue.cs
InterpolationContext.cs InterpolationContext.cs
IntExpr.cs IntExpr.cs
IntNum.cs IntNum.cs
IntSort.cs IntSort.cs
IntSymbol.cs IntSymbol.cs
ListSort.cs ListSort.cs
Log.cs Log.cs
Model.cs Model.cs
Optimize.cs Optimize.cs
ParamDescrs.cs ParamDescrs.cs
Params.cs Params.cs
Pattern.cs Pattern.cs
Probe.cs Probe.cs
Quantifier.cs Quantifier.cs
RatNum.cs RatNum.cs
RealExpr.cs RealExpr.cs
RealSort.cs RealSort.cs
ReExpr.cs ReExpr.cs
RelationSort.cs RelationSort.cs
ReSort.cs ReSort.cs
SeqExpr.cs SeqExpr.cs
SeqSort.cs SeqSort.cs
SetSort.cs SetSort.cs
Solver.cs Solver.cs
Sort.cs Sort.cs
Statistics.cs Statistics.cs
Status.cs Status.cs
StringSymbol.cs StringSymbol.cs
Symbol.cs Symbol.cs
Tactic.cs Tactic.cs
TupleSort.cs TupleSort.cs
UninterpretedSort.cs UninterpretedSort.cs
Version.cs Version.cs
Z3Exception.cs Z3Exception.cs
Z3Object.cs Z3Object.cs
) )
set(Z3_DOTNET_ASSEMBLY_SOURCES "") set(Z3_DOTNET_ASSEMBLY_SOURCES "")

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

@ -126,7 +126,7 @@ namespace Microsoft.Z3
private BoolSort m_boolSort = null; private BoolSort m_boolSort = null;
private IntSort m_intSort = null; private IntSort m_intSort = null;
private RealSort m_realSort = null; private RealSort m_realSort = null;
private SeqSort m_stringSort = null; private SeqSort m_stringSort = null;
/// <summary> /// <summary>
/// Retrieves the Boolean sort of the context. /// Retrieves the Boolean sort of the context.
@ -2426,7 +2426,7 @@ namespace Microsoft.Z3
public SeqExpr IntToString(Expr e) public SeqExpr IntToString(Expr e)
{ {
Contract.Requires(e != null); Contract.Requires(e != null);
Contract.Requires(e is ArithExpr); Contract.Requires(e is ArithExpr);
Contract.Ensures(Contract.Result<SeqExpr>() != null); Contract.Ensures(Contract.Result<SeqExpr>() != null);
return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject)); return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
} }
@ -2690,7 +2690,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create a range expression. /// Create a range expression.
/// </summary> /// </summary>
public ReExpr MkRange(SeqExpr lo, SeqExpr hi) public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
{ {
Contract.Requires(lo != null); Contract.Requires(lo != null);
Contract.Requires(hi != null); Contract.Requires(hi != null);

18
src/api/dotnet/Expr.cs
View file

@ -809,55 +809,55 @@ namespace Microsoft.Z3
/// Check whether expression is a concatentation. /// Check whether expression is a concatentation.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <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> /// <summary>
/// Check whether expression is a prefix. /// Check whether expression is a prefix.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <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> /// <summary>
/// Check whether expression is a suffix. /// Check whether expression is a suffix.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <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> /// <summary>
/// Check whether expression is a contains. /// Check whether expression is a contains.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <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> /// <summary>
/// Check whether expression is an extract. /// Check whether expression is an extract.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <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> /// <summary>
/// Check whether expression is a replace. /// Check whether expression is a replace.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <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> /// <summary>
/// Check whether expression is an at. /// Check whether expression is an at.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <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> /// <summary>
/// Check whether expression is a sequence length. /// Check whether expression is a sequence length.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <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> /// <summary>
/// Check whether expression is a sequence index. /// Check whether expression is a sequence index.
/// </summary> /// </summary>
/// <returns>a Boolean</returns> /// <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 #endregion

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

@ -291,17 +291,17 @@ namespace Microsoft.Z3
return v.ToArithExprArray(); return v.ToArithExprArray();
} }
/// <summary> /// <summary>
/// Return a string the describes why the last to check returned unknown /// Return a string the describes why the last to check returned unknown
/// </summary> /// </summary>
public String ReasonUnknown public String ReasonUnknown
{ {
get get
{ {
Contract.Ensures(Contract.Result<string>() != null); Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject); return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
} }
} }
/// <summary> /// <summary>

74
src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln
View file

@ -8,41 +8,41 @@ EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Example", "Example\Example.csproj", "{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}" Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Example", "Example\Example.csproj", "{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}"
EndProject EndProject
Global Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|Any CPU = Debug|Any CPU Debug|Any CPU = Debug|Any CPU
Debug|x64 = Debug|x64 Debug|x64 = Debug|x64
Debug|x86 = Debug|x86 Debug|x86 = Debug|x86
Release|Any CPU = Release|Any CPU Release|Any CPU = Release|Any CPU
Release|x64 = Release|x64 Release|x64 = Release|x64
Release|x86 = Release|x86 Release|x86 = Release|x86
EndGlobalSection EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution GlobalSection(ProjectConfigurationPlatforms) = postSolution
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {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|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.ActiveCfg = Debug|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.Build.0 = 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.ActiveCfg = Debug|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.Build.0 = 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.ActiveCfg = Release|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.Build.0 = 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.ActiveCfg = Release|x64
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.Build.0 = 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.ActiveCfg = Release|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.Build.0 = 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.ActiveCfg = Debug|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.Build.0 = 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.ActiveCfg = Debug|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.Build.0 = 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.ActiveCfg = Debug|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.Build.0 = 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.ActiveCfg = Release|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.Build.0 = 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.ActiveCfg = Release|x64
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.Build.0 = 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.ActiveCfg = Release|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.Build.0 = Release|Any CPU {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.Build.0 = Release|Any CPU
EndGlobalSection EndGlobalSection
GlobalSection(SolutionProperties) = preSolution GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE HideSolutionNode = FALSE
EndGlobalSection EndGlobalSection
EndGlobal EndGlobal

92
src/api/java/AlgebraicNum.java
View file

@ -22,57 +22,57 @@ package com.microsoft.z3;
**/ **/
public class AlgebraicNum extends ArithExpr public class AlgebraicNum extends ArithExpr
{ {
/** /**
* Return a upper bound for a given real algebraic number. The interval * Return a upper bound for a given real algebraic number. The interval
* isolating the number is smaller than 1/10^{@code precision}. * isolating the number is smaller than 1/10^{@code precision}.
* *
* @see Expr#isAlgebraicNumber * @see Expr#isAlgebraicNumber
* @param precision the precision of the result * @param precision the precision of the result
* *
* @return A numeral Expr of sort Real * @return A numeral Expr of sort Real
* @throws Z3Exception on error * @throws Z3Exception on error
**/ **/
public RatNum toUpper(int precision) public RatNum toUpper(int precision)
{ {
return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext() return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext()
.nCtx(), getNativeObject(), precision)); .nCtx(), getNativeObject(), precision));
} }
/** /**
* Return a lower bound for the given real algebraic number. The interval * Return a lower bound for the given real algebraic number. The interval
* isolating the number is smaller than 1/10^{@code precision}. * isolating the number is smaller than 1/10^{@code precision}.
* *
* @see Expr#isAlgebraicNumber * @see Expr#isAlgebraicNumber
* @param precision precision * @param precision precision
* *
* @return A numeral Expr of sort Real * @return A numeral Expr of sort Real
* @throws Z3Exception on error * @throws Z3Exception on error
**/ **/
public RatNum toLower(int precision) public RatNum toLower(int precision)
{ {
return new RatNum(getContext(), Native.getAlgebraicNumberLower(getContext() return new RatNum(getContext(), Native.getAlgebraicNumberLower(getContext()
.nCtx(), getNativeObject(), precision)); .nCtx(), getNativeObject(), precision));
} }
/** /**
* Returns a string representation in decimal notation. * Returns a string representation in decimal notation.
* Remarks: The result has at most {@code precision} decimal places. * Remarks: The result has at most {@code precision} decimal places.
* @param precision precision * @param precision precision
* @return String * @return String
* @throws Z3Exception on error * @throws Z3Exception on error
**/ **/
public String toDecimal(int precision) public String toDecimal(int precision)
{ {
return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(), return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
precision); precision);
} }
AlgebraicNum(Context ctx, long obj) AlgebraicNum(Context ctx, long obj)
{ {
super(ctx, obj); super(ctx, obj);
} }
} }

120
src/api/java/Context.java
View file

@ -1898,8 +1898,8 @@ public class Context implements AutoCloseable {
*/ */
public SeqExpr mkEmptySeq(Sort s) public SeqExpr mkEmptySeq(Sort s)
{ {
checkContextMatch(s); checkContextMatch(s);
return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject())); return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
} }
/** /**
@ -1907,8 +1907,8 @@ public class Context implements AutoCloseable {
*/ */
public SeqExpr mkUnit(Expr elem) public SeqExpr mkUnit(Expr elem)
{ {
checkContextMatch(elem); checkContextMatch(elem);
return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject())); return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
} }
/** /**
@ -1916,7 +1916,7 @@ public class Context implements AutoCloseable {
*/ */
public SeqExpr mkString(String s) 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) public SeqExpr mkConcat(SeqExpr... t)
{ {
checkContextMatch(t); checkContextMatch(t);
return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(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) public IntExpr mkLength(SeqExpr s)
{ {
checkContextMatch(s); checkContextMatch(s);
return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject())); 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) public BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
{ {
checkContextMatch(s1, s2); checkContextMatch(s1, s2);
return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject())); 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) public BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
{ {
checkContextMatch(s1, s2); checkContextMatch(s1, s2);
return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject())); 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) public BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
{ {
checkContextMatch(s1, s2); checkContextMatch(s1, s2);
return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject())); 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) public SeqExpr mkAt(SeqExpr s, IntExpr index)
{ {
checkContextMatch(s, index); checkContextMatch(s, index);
return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject())); 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) public SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
{ {
checkContextMatch(s, offset, length); checkContextMatch(s, offset, length);
return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject())); 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) public IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
{ {
checkContextMatch(s, substr, offset); checkContextMatch(s, substr, offset);
return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject())); 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) public SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
{ {
checkContextMatch(s, src, dst); checkContextMatch(s, src, dst);
return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject())); 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) public ReExpr mkToRe(SeqExpr s)
{ {
checkContextMatch(s); checkContextMatch(s);
return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject())); 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) public BoolExpr mkInRe(SeqExpr s, ReExpr re)
{ {
checkContextMatch(s, re); checkContextMatch(s, re);
return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject())); 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) public ReExpr mkStar(ReExpr re)
{ {
checkContextMatch(re); checkContextMatch(re);
return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject())); 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) 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) 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) public ReExpr mkPlus(ReExpr re)
{ {
checkContextMatch(re); checkContextMatch(re);
return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject())); return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
} }
/** /**
@ -2060,8 +2060,8 @@ public class Context implements AutoCloseable {
*/ */
public ReExpr mkOption(ReExpr re) public ReExpr mkOption(ReExpr re)
{ {
checkContextMatch(re); checkContextMatch(re);
return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject())); return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
} }
@ -2070,8 +2070,8 @@ public class Context implements AutoCloseable {
*/ */
public ReExpr mkComplement(ReExpr re) public ReExpr mkComplement(ReExpr re)
{ {
checkContextMatch(re); checkContextMatchb(re);
return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject())); return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
} }
/** /**
@ -2079,8 +2079,8 @@ public class Context implements AutoCloseable {
*/ */
public ReExpr mkConcat(ReExpr... t) public ReExpr mkConcat(ReExpr... t)
{ {
checkContextMatch(t); checkContextMatch(t);
return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(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) public ReExpr mkUnion(ReExpr... t)
{ {
checkContextMatch(t); checkContextMatch(t);
return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(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) public ReExpr mkIntersect(ReExpr... t)
{ {
checkContextMatch(t); checkContextMatch(t);
return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(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) public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
{ {
checkContextMatch(lo, hi); checkContextMatch(lo, hi);
return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject())); 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) public BoolExpr mkAtMost(BoolExpr[] args, int k)
{ {
checkContextMatch(args); checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k)); 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) public BoolExpr mkAtLeast(BoolExpr[] args, int k)
{ {
checkContextMatch(args); checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k)); 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) public BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
{ {
checkContextMatch(args); checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k)); 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) public BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
{ {
checkContextMatch(args); checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k)); 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) public BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
{ {
checkContextMatch(args); checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k)); 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) void checkContextMatch(Z3Object other1, Z3Object other2)
{ {
checkContextMatch(other1); checkContextMatch(other1);
checkContextMatch(other2); checkContextMatch(other2);
} }
void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3) void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
{ {
checkContextMatch(other1); checkContextMatch(other1);
checkContextMatch(other2); checkContextMatch(other2);
checkContextMatch(other3); checkContextMatch(other3);
} }
void checkContextMatch(Z3Object[] arr) void checkContextMatch(Z3Object[] arr)

2
src/api/java/EnumSort.java
View file

@ -65,7 +65,7 @@ public class EnumSort extends Sort
**/ **/
public Expr getConst(int inx) public Expr getConst(int inx)
{ {
return getContext().mkApp(getConstDecl(inx)); return getContext().mkApp(getConstDecl(inx));
} }
/** /**

2
src/api/java/Expr.java
View file

@ -1287,7 +1287,7 @@ public class Expr extends AST
*/ */
public String getString() public String getString()
{ {
return Native.getString(getContext().nCtx(), getNativeObject()); return Native.getString(getContext().nCtx(), getNativeObject());
} }
/** /**

2
src/api/java/Model.java
View file

@ -200,7 +200,7 @@ public class Model extends Z3Object {
* Remarks: This function may fail if {@code t} contains * 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 * quantifiers, is partial (MODEL_PARTIAL enabled), or if {@code t} is not well-sorted. In this case a
* {@code ModelEvaluationFailedException} is thrown. * {@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 * @param completion An expression {@code completion} When this flag
* is enabled, a model value will be assigned to any constant or function * is enabled, a model value will be assigned to any constant or function
* that does not have an interpretation in the model. * that does not have an interpretation in the model.

7
src/api/java/Optimize.java
View file

@ -285,8 +285,7 @@ public class Optimize extends Z3Object {
**/ **/
public String getReasonUnknown() public String getReasonUnknown()
{ {
return Native.optimizeGetReasonUnknown(getContext().nCtx(), return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
getNativeObject());
} }
/** /**
@ -304,7 +303,7 @@ public class Optimize extends Z3Object {
*/ */
public void fromFile(String file) 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) public void fromString(String s)
{ {
Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s); Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
} }

2
src/api/java/ParamDescrs.java
View file

@ -49,7 +49,7 @@ public class ParamDescrs extends Z3Object {
public String getDocumentation(Symbol name) public String getDocumentation(Symbol name)
{ {
return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject()); return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject());
} }
/** /**

2
src/api/java/Solver.java
View file

@ -302,7 +302,7 @@ public class Solver extends Z3Object {
*/ */
public Solver translate(Context ctx) 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()));
} }
/** /**

8
src/api/java/Sort.java
View file

@ -35,12 +35,8 @@ public class Sort extends AST
if (!(o instanceof Sort)) return false; if (!(o instanceof Sort)) return false;
Sort other = (Sort) o; Sort other = (Sort) o;
return (getContext().nCtx() == other.getContext().nCtx()) && return (getContext().nCtx() == other.getContext().nCtx()) &&
(Native.isEqSort( (Native.isEqSort(getContext().nCtx(), getNativeObject(), other.getNativeObject()));
getContext().nCtx(),
getNativeObject(),
other.getNativeObject()
));
} }
/** /**

38
src/api/ml/z3native_stubs.c.pre
View file

@ -25,34 +25,34 @@ extern "C" {
#include <z3native_stubs.h> #include <z3native_stubs.h>
#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \ #define CAMLlocal6(X1,X2,X3,X4,X5,X6) \
CAMLlocal5(X1,X2,X3,X4,X5); \ CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal1(X6) CAMLlocal1(X6)
#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \ #define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \
CAMLlocal5(X1,X2,X3,X4,X5); \ CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal2(X6,X7) CAMLlocal2(X6,X7)
#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \ #define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \
CAMLlocal5(X1,X2,X3,X4,X5); \ CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal3(X6,X7,X8) CAMLlocal3(X6,X7,X8)
#define CAMLparam6(X1,X2,X3,X4,X5,X6) \ #define CAMLparam6(X1,X2,X3,X4,X5,X6) \
CAMLparam5(X1,X2,X3,X4,X5); \ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam1(X6) CAMLxparam1(X6)
#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \ #define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \
CAMLparam5(X1,X2,X3,X4,X5); \ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam2(X6,X7) CAMLxparam2(X6,X7)
#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \ #define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \
CAMLparam5(X1,X2,X3,X4,X5); \ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam3(X6,X7,X8) CAMLxparam3(X6,X7,X8)
#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \ #define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \
CAMLparam5(X1,X2,X3,X4,X5); \ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam4(X6,X7,X8,X9) CAMLxparam4(X6,X7,X8,X9)
#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \ #define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \
CAMLparam5(X1,X2,X3,X4,X5); \ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam5(X6,X7,X8,X9,X10); \ CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam2(X11,X12) CAMLxparam2(X11,X12)
#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \ #define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \
CAMLparam5(X1,X2,X3,X4,X5); \ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam5(X6,X7,X8,X9,X10); \ CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam3(X11,X12,X13) CAMLxparam3(X11,X12,X13)

2
src/ast/rewriter/array_rewriter_params.pyg
View file

@ -2,5 +2,5 @@ def_module_params(module_name='rewriter',
class_name='array_rewriter_params', class_name='array_rewriter_params',
export=True, export=True,
params=(("expand_select_store", BOOL, False, "replace a (select (store ...) ...) term by an if-then-else term"), 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"))) ("sort_store", BOOL, False, "sort nested stores when the indices are known to be different")))

2
src/ast/rewriter/fpa_rewriter_params.pyg
View file

@ -1,5 +1,5 @@
def_module_params(module_name='rewriter', def_module_params(module_name='rewriter',
class_name='fpa_rewriter_params', class_name='fpa_rewriter_params',
export=True, 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"),
)) ))

42
src/muz/base/fixedpoint_params.pyg
View file

@ -4,7 +4,7 @@ def_module_params('fixedpoint',
params=(('timeout', UINT, UINT_MAX, 'set timeout'), params=(('timeout', UINT, UINT_MAX, 'set timeout'),
('engine', SYMBOL, 'auto-config', ('engine', SYMBOL, 'auto-config',
'Select: auto-config, datalog, duality, pdr, bmc, spacer'), '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'), 'default table implementation: sparse, hashtable, bitvector, interval'),
('datalog.default_relation', SYMBOL, 'pentagon', ('datalog.default_relation', SYMBOL, 'pentagon',
'default relation implementation: external_relation, pentagon'), 'default relation implementation: external_relation, pentagon'),
@ -56,18 +56,18 @@ def_module_params('fixedpoint',
"table columns, if it would have been empty otherwise"), "table columns, if it would have been empty otherwise"),
('datalog.subsumption', BOOL, True, ('datalog.subsumption', BOOL, True,
"if true, removes/filters predicates with total transitions"), "if true, removes/filters predicates with total transitions"),
('duality.full_expand', BOOL, False, 'Fully expand derivation trees'), ('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'), ('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
('duality.feasible_edges', BOOL, True, ('duality.feasible_edges', BOOL, True,
'Don\'t expand definitley infeasible edges'), 'Don\'t expand definitley infeasible edges'),
('duality.use_underapprox', BOOL, False, 'Use underapproximations'), ('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'), ('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
('duality.recursion_bound', UINT, UINT_MAX, ('duality.recursion_bound', UINT, UINT_MAX,
'Recursion bound for stratified inlining'), 'Recursion bound for stratified inlining'),
('duality.profile', BOOL, False, 'profile run time'), ('duality.profile', BOOL, False, 'profile run time'),
('duality.mbqi', BOOL, True, 'use model-based quantifier instantiation'), ('duality.mbqi', BOOL, True, 'use model-based quantifier instantiation'),
('duality.batch_expand', BOOL, False, 'use batch expansion'), ('duality.batch_expand', BOOL, False, 'use batch expansion'),
('duality.conjecture_file', STRING, '', 'save conjectures to file'), ('duality.conjecture_file', STRING, '', 'save conjectures to file'),
('pdr.bfs_model_search', BOOL, True, ('pdr.bfs_model_search', BOOL, True,
"use BFS strategy for expanding model search"), "use BFS strategy for expanding model search"),
('pdr.farkas', BOOL, True, ('pdr.farkas', BOOL, True,
@ -92,9 +92,9 @@ def_module_params('fixedpoint',
"generalize lemmas using induction strengthening"), "generalize lemmas using induction strengthening"),
('pdr.use_arith_inductive_generalizer', BOOL, False, ('pdr.use_arith_inductive_generalizer', BOOL, False,
"generalize lemmas using arithmetic heuristics for induction strengthening"), "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"), "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"), "generalize using convex interiors of lemmas"),
('pdr.cache_mode', UINT, 0, "use no (0), symbolic (1) or explicit " + ('pdr.cache_mode', UINT, 0, "use no (0), symbolic (1) or explicit " +
"cache (2) for model search"), "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.max_num_contexts', UINT, 500, "maximal number of contexts to create"),
('pdr.try_minimize_core', BOOL, False, ('pdr.try_minimize_core', BOOL, False,
"try to reduce core size (before inductive minimization)"), "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, ('print_fixedpoint_extensions', BOOL, True,
"use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, " + "use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, " +
"when printing rules"), "when printing rules"),
@ -123,7 +123,7 @@ def_module_params('fixedpoint',
('print_statistics', BOOL, False, 'print statistics'), ('print_statistics', BOOL, False, 'print statistics'),
('print_aig', SYMBOL, '', ('print_aig', SYMBOL, '',
'Dump clauses in AIG text format (AAG) to the given file name'), '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'), 'selection method for tabular strategy: weight (default), first, var-use'),
('xform.bit_blast', BOOL, False, ('xform.bit_blast', BOOL, False,
'bit-blast bit-vectors'), 'bit-blast bit-vectors'),
@ -140,7 +140,7 @@ def_module_params('fixedpoint',
('xform.unfold_rules', UINT, 0, ('xform.unfold_rules', UINT, 0,
"unfold rules statically using iterative squarring"), "unfold rules statically using iterative squarring"),
('xform.slice', BOOL, True, "simplify clause set using slicing"), ('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"), "Add linear invariants to clauses using Karr's method"),
('spacer.use_eqclass', BOOL, False, "Generalizes equalities to equivalence classes"), ('spacer.use_eqclass', BOOL, False, "Generalizes equalities to equivalence classes"),
('xform.transform_arrays', BOOL, False, ('xform.transform_arrays', BOOL, False,
@ -153,15 +153,15 @@ def_module_params('fixedpoint',
"Gives the number of quantifiers per array"), "Gives the number of quantifiers per array"),
('xform.instantiate_arrays.slice_technique', SYMBOL, "no-slicing", ('xform.instantiate_arrays.slice_technique', SYMBOL, "no-slicing",
"<no-slicing>=> GetId(i) = i, <smash> => GetId(i) = true"), "<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"), "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"), "instantiate quantified Horn clauses using E-matching heuristic"),
('xform.coalesce_rules', BOOL, False, "coalesce rules"), ('xform.coalesce_rules', BOOL, False, "coalesce rules"),
('xform.tail_simplifier_pve', BOOL, True, "propagate_variable_equivalences"), ('xform.tail_simplifier_pve', BOOL, True, "propagate_variable_equivalences"),
('xform.subsumption_checker', BOOL, True, "Enable subsumption checker (no support for model conversion)"), ('xform.subsumption_checker', BOOL, True, "Enable subsumption checker (no support for model conversion)"),
('xform.coi', BOOL, True, "use cone of influence simplificaiton"), ('xform.coi', BOOL, True, "use cone of influence simplification"),
('duality.enable_restarts', BOOL, False, 'DUALITY: enable restarts'), ('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.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.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.use_lemma_as_cti', BOOL, False, 'SPACER: use a lemma instead of a CTI in flexible_trace'),
@ -170,7 +170,7 @@ def_module_params('fixedpoint',
('spacer.use_array_eq_generalizer', BOOL, True, 'SPACER: attempt to generalize lemmas with array equalities'), ('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', 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.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.max_level', UINT, UINT_MAX, "Maximum level to explore"),
('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"), ('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),

2
src/opt/opt_params.pyg
View file

@ -2,7 +2,7 @@ def_module_params('opt',
description='optimization parameters', description='optimization parameters',
export=True, export=True,
params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), 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'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),

1
src/tactic/sls/.#sls_params.pyg Normal file
View file

@ -0,0 +1 @@
winte@WINTERMUTE.13536:1505663874

44
src/tactic/sls/sls_params.pyg
View file

@ -2,25 +2,25 @@ def_module_params('sls',
export=True, export=True,
description='Experimental Stochastic Local Search Solver (for QFBV only).', description='Experimental Stochastic Local Search Solver (for QFBV only).',
params=(max_memory_param(), params=(max_memory_param(),
('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'), ('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'),
('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'), ('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', 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_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_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_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_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'), ('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'),
('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'), ('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'),
('paws_init', UINT, 40, 'initial/minimum assertion weights'), ('paws_init', UINT, 40, 'initial/minimum assertion weights'),
('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'), ('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'),
('wp', UINT, 100, 'random walk with probability wp / 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_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)'), ('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_base', UINT, 100, 'base restart interval given by moves per run'),
('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'), ('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'),
('early_prune', BOOL, 1, 'use early pruning for score prediction'), ('early_prune', BOOL, 1, 'use early pruning for score prediction'),
('random_offset', BOOL, 1, 'use random offset for candidate evaluation'), ('random_offset', BOOL, 1, 'use random offset for candidate evaluation'),
('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'), ('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'), ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
('random_seed', UINT, 0, 'random seed') ('random_seed', UINT, 0, 'random seed')
)) ))

2
src/util/lp/CMakeLists.txt
View file

@ -19,7 +19,7 @@ z3_add_component(lp
lu_instances.cpp lu_instances.cpp
matrix_instances.cpp matrix_instances.cpp
permutation_matrix_instances.cpp permutation_matrix_instances.cpp
quick_xplain.cpp quick_xplain.cpp
row_eta_matrix_instances.cpp row_eta_matrix_instances.cpp
scaler_instances.cpp scaler_instances.cpp
sparse_matrix_instances.cpp sparse_matrix_instances.cpp

4
src/util/lp/lp_core_solver_base.hpp
View file

@ -98,8 +98,8 @@ pivot_for_tableau_on_basis() {
// i is the pivot row, and j is the pivot column // i is the pivot row, and j is the pivot column
template <typename T, typename X> void lp_core_solver_base<T, X>:: template <typename T, typename X> void lp_core_solver_base<T, X>::
pivot_to_reduced_costs_tableau(unsigned i, unsigned j) { pivot_to_reduced_costs_tableau(unsigned i, unsigned j) {
if (j >= m_d.size()) if (j >= m_d.size())
return; return;
T &a = m_d[j]; T &a = m_d[j];
if (is_zero(a)) if (is_zero(a))
return; return;

2
src/util/lp/lp_primal_core_solver_tableau.h
View file

@ -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->m_basis_sort_counter = 0; // to initiate the sort of the basis
this->set_total_iterations(0); this->set_total_iterations(0);
this->iters_with_no_cost_growing() = 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) if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
return; return;
if (this->m_settings.backup_costs) if (this->m_settings.backup_costs)

6
src/util/lp/static_matrix.hpp
View file

@ -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 < row_count() && ii < column_count());
SASSERT(i != ii); SASSERT(i != ii);
m_became_zeros.reset(); m_became_zeros.reset();
T alpha = -get_val(c); T alpha = -get_val(c);
SASSERT(!is_zero(alpha)); SASSERT(!is_zero(alpha));
auto & ii_row_vals = m_rows[ii]; auto & ii_row_vals = m_rows[ii];
remove_element(ii_row_vals, ii_row_vals[c.m_offset]); remove_element(ii_row_vals, ii_row_vals[c.m_offset]);
scan_row_ii_to_offset_vector(ii); 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; unsigned j = iv.m_j;
if (j == pivot_col) continue; if (j == pivot_col) continue;
T alv = alpha * iv.m_value; 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]; int j_offs = m_vector_of_row_offsets[j];
if (j_offs == -1) { // it is a new element if (j_offs == -1) { // it is a new element
add_new_element(ii, j, alv); add_new_element(ii, j, alv);