mirror of
https://github.com/Z3Prover/z3
synced 2025-07-19 10:52:02 +00:00
Dispose of intermediate Z3Objects created in dotnet api. (#5901)
* Dispose of intermediate Z3Objects created in dotnet api. * Set C# LangVersion to 8.0. * Fix build errors. * Fix warning about empty using statement. * Fix Xor to only dispose of objects that it creates internally.
This commit is contained in:
Matt Thornton
GitHub
parent
bdf7de1703
commit
4e0a2f5968
13 changed files with 360 additions and 142 deletions
|
|
@ -18,10 +18,10 @@ Notes:
|
|||
--*/
|
||||
|
||||
using System;
|
||||
using System.Diagnostics;
|
||||
using System.Collections.Generic;
|
||||
using System.Runtime.InteropServices;
|
||||
using System.Diagnostics;
|
||||
using System.Linq;
|
||||
using System.Runtime.InteropServices;
|
||||
|
||||
namespace Microsoft.Z3
|
||||
{
|
||||
|
|
@ -202,7 +202,7 @@ namespace Microsoft.Z3
|
|||
/// </summary>
|
||||
public UninterpretedSort MkUninterpretedSort(string str)
|
||||
{
|
||||
using var sym = MkSymbol(str);
|
||||
using var sym = MkSymbol(str);
|
||||
return MkUninterpretedSort(sym);
|
||||
}
|
||||
|
||||
|
|
@ -312,9 +312,18 @@ namespace Microsoft.Z3
|
|||
public EnumSort MkEnumSort(string name, params string[] enumNames)
|
||||
{
|
||||
Debug.Assert(enumNames != null);
|
||||
using var sname = MkSymbol(name);
|
||||
using var snames = MkSymbols(enumNames);
|
||||
return new EnumSort(this, sname, snames);
|
||||
|
||||
var enumSymbols = MkSymbols(enumNames);
|
||||
try
|
||||
{
|
||||
using var symbol = MkSymbol(name);
|
||||
return new EnumSort(this, symbol, enumSymbols);
|
||||
}
|
||||
finally
|
||||
{
|
||||
foreach (var enumSymbol in enumSymbols)
|
||||
enumSymbol.Dispose();
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -338,8 +347,8 @@ namespace Microsoft.Z3
|
|||
Debug.Assert(elemSort != null);
|
||||
|
||||
CheckContextMatch(elemSort);
|
||||
using var sname = MkSymbol(name);
|
||||
return new ListSort(this, sname, elemSort);
|
||||
using var symbol = MkSymbol(name);
|
||||
return new ListSort(this, symbol, elemSort);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -366,8 +375,8 @@ namespace Microsoft.Z3
|
|||
/// <param name="size">The size of the sort</param>
|
||||
public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
|
||||
{
|
||||
using var sname = MkSymbol(name);
|
||||
return new FiniteDomainSort(this, sname, size);
|
||||
using var symbol = MkSymbol(name);
|
||||
return new FiniteDomainSort(this, symbol, size);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -401,10 +410,19 @@ namespace Microsoft.Z3
|
|||
/// <returns></returns>
|
||||
public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
|
||||
{
|
||||
using var sname = MkSymbol(name);
|
||||
using var srecognizer = MkSymbol(recognizer);
|
||||
using var sfieldNames = MkSymbols(fieldNames);
|
||||
return new Constructor(this, sname, srecognizer, sfieldNames, sorts, sortRefs);
|
||||
|
||||
using var nameSymbol = MkSymbol(name);
|
||||
using var recognizerSymbol = MkSymbol(recognizer);
|
||||
var fieldSymbols = MkSymbols(fieldNames);
|
||||
try
|
||||
{
|
||||
return new Constructor(this, nameSymbol, recognizerSymbol, fieldSymbols, sorts, sortRefs);
|
||||
}
|
||||
finally
|
||||
{
|
||||
foreach (var fieldSymbol in fieldSymbols)
|
||||
fieldSymbol.Dispose();
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -431,8 +449,8 @@ namespace Microsoft.Z3
|
|||
Debug.Assert(constructors.All(c => c != null));
|
||||
|
||||
CheckContextMatch<Constructor>(constructors);
|
||||
using var sname = MkSymbol(name);
|
||||
return new DatatypeSort(this, sname, constructors);
|
||||
using var symbol = MkSymbol(name);
|
||||
return new DatatypeSort(this, symbol, constructors);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -480,8 +498,17 @@ namespace Microsoft.Z3
|
|||
Debug.Assert(names.Length == c.Length);
|
||||
//Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
|
||||
//Debug.Assert(names.All(name => name != null));
|
||||
var snames = MkSymbols(names);
|
||||
return MkDatatypeSorts(snames, c);
|
||||
|
||||
var symbols = MkSymbols(names);
|
||||
try
|
||||
{
|
||||
return MkDatatypeSorts(symbols, c);
|
||||
}
|
||||
finally
|
||||
{
|
||||
foreach (var symbol in symbols)
|
||||
symbol.Dispose();
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -542,8 +569,8 @@ namespace Microsoft.Z3
|
|||
|
||||
CheckContextMatch<Sort>(domain);
|
||||
CheckContextMatch(range);
|
||||
using var sname = MkSymbol(name);
|
||||
return new FuncDecl(this, sname, domain, range);
|
||||
using var symbol = MkSymbol(name);
|
||||
return new FuncDecl(this, symbol, domain, range);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -556,8 +583,8 @@ namespace Microsoft.Z3
|
|||
|
||||
CheckContextMatch<Sort>(domain);
|
||||
CheckContextMatch(range);
|
||||
using var sname = MkSymbol(name);
|
||||
return new FuncDecl(this, sname, domain, range, true);
|
||||
using var symbol = MkSymbol(name);
|
||||
return new FuncDecl(this, symbol, domain, range, true);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -585,9 +612,9 @@ namespace Microsoft.Z3
|
|||
|
||||
CheckContextMatch(domain);
|
||||
CheckContextMatch(range);
|
||||
using var sname = MkSymbol(name);
|
||||
using var symbol = MkSymbol(name);
|
||||
Sort[] q = new Sort[] { domain };
|
||||
return new FuncDecl(this, sname, q, range);
|
||||
return new FuncDecl(this, symbol, q, range);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -626,8 +653,8 @@ namespace Microsoft.Z3
|
|||
Debug.Assert(range != null);
|
||||
|
||||
CheckContextMatch(range);
|
||||
using var sname = MkSymbol(name);
|
||||
return new FuncDecl(this, sname, null, range);
|
||||
using var symbol = MkSymbol(name);
|
||||
return new FuncDecl(this, symbol, null, range);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -694,8 +721,9 @@ namespace Microsoft.Z3
|
|||
public Expr MkConst(string name, Sort range)
|
||||
{
|
||||
Debug.Assert(range != null);
|
||||
using var sname = MkSymbol(name);
|
||||
return MkConst(sname, range);
|
||||
|
||||
using var symbol = MkSymbol(name);
|
||||
return MkConst(symbol, range);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -736,8 +764,8 @@ namespace Microsoft.Z3
|
|||
/// </summary>
|
||||
public BoolExpr MkBoolConst(string name)
|
||||
{
|
||||
using var sname = MkSymbol(name);
|
||||
return (BoolExpr)MkConst(sname, BoolSort);
|
||||
using var symbol = MkSymbol(name);
|
||||
return (BoolExpr)MkConst(symbol, BoolSort);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -785,8 +813,9 @@ namespace Microsoft.Z3
|
|||
public BitVecExpr MkBVConst(Symbol name, uint size)
|
||||
{
|
||||
Debug.Assert(name != null);
|
||||
using var sort = MkBitVecSort(size);
|
||||
return (BitVecExpr)MkConst(name, sort);
|
||||
|
||||
using var sort = MkBitVecSort(size);
|
||||
return (BitVecExpr)MkConst(name, sort);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -794,7 +823,7 @@ namespace Microsoft.Z3
|
|||
/// </summary>
|
||||
public BitVecExpr MkBVConst(string name, uint size)
|
||||
{
|
||||
using var sort = MkBitVecSort(size);
|
||||
using var sort = MkBitVecSort(size);
|
||||
return (BitVecExpr)MkConst(name, sort);
|
||||
}
|
||||
#endregion
|
||||
|
|
@ -956,17 +985,15 @@ namespace Microsoft.Z3
|
|||
Debug.Assert(ts != null);
|
||||
Debug.Assert(ts.All(a => a != null));
|
||||
CheckContextMatch<BoolExpr>(ts);
|
||||
BoolExpr r = null;
|
||||
foreach (var t in ts)
|
||||
{
|
||||
if (r == null)
|
||||
r = t;
|
||||
else
|
||||
r = MkXor(r, t);
|
||||
}
|
||||
if (r == null)
|
||||
r = MkTrue();
|
||||
return r;
|
||||
|
||||
return ts.Any()
|
||||
? ts
|
||||
.Aggregate(MkFalse(), (r, t) =>
|
||||
{
|
||||
using (r)
|
||||
return MkXor(r, t);
|
||||
})
|
||||
: MkTrue();
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -2041,7 +2068,8 @@ namespace Microsoft.Z3
|
|||
Debug.Assert(domain != null);
|
||||
Debug.Assert(range != null);
|
||||
|
||||
return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
|
||||
using var sort = MkArraySort(domain, range);
|
||||
return (ArrayExpr)MkConst(name, sort);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -2051,9 +2079,10 @@ namespace Microsoft.Z3
|
|||
{
|
||||
Debug.Assert(domain != null);
|
||||
Debug.Assert(range != null);
|
||||
using var sort = MkArraySort(domain, range);
|
||||
using var sname = MkSymbol(name);
|
||||
return (ArrayExpr)MkConst(sname, sort);
|
||||
|
||||
using var symbol = MkSymbol(name);
|
||||
using var sort = MkArraySort(domain, range);
|
||||
return (ArrayExpr)MkConst(symbol, sort);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -3051,8 +3080,8 @@ namespace Microsoft.Z3
|
|||
/// <param name="size">the size of the bit-vector</param>
|
||||
public BitVecNum MkBV(string v, uint size)
|
||||
{
|
||||
|
||||
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
|
||||
using var sort = MkBitVecSort(size);
|
||||
return (BitVecNum)MkNumeral(v, sort);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -3062,8 +3091,8 @@ namespace Microsoft.Z3
|
|||
/// <param name="size">the size of the bit-vector</param>
|
||||
public BitVecNum MkBV(int v, uint size)
|
||||
{
|
||||
|
||||
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
|
||||
using var sort = MkBitVecSort(size);
|
||||
return (BitVecNum)MkNumeral(v, sort);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -3073,8 +3102,8 @@ namespace Microsoft.Z3
|
|||
/// <param name="size">the size of the bit-vector</param>
|
||||
public BitVecNum MkBV(uint v, uint size)
|
||||
{
|
||||
|
||||
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
|
||||
using var sort = MkBitVecSort(size);
|
||||
return (BitVecNum)MkNumeral(v, sort);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -3084,8 +3113,8 @@ namespace Microsoft.Z3
|
|||
/// <param name="size">the size of the bit-vector</param>
|
||||
public BitVecNum MkBV(long v, uint size)
|
||||
{
|
||||
|
||||
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
|
||||
using var sort = MkBitVecSort(size);
|
||||
return (BitVecNum)MkNumeral(v, sort);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -3095,8 +3124,8 @@ namespace Microsoft.Z3
|
|||
/// <param name="size">the size of the bit-vector</param>
|
||||
public BitVecNum MkBV(ulong v, uint size)
|
||||
{
|
||||
|
||||
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
|
||||
using var sort = MkBitVecSort(size);
|
||||
return (BitVecNum)MkNumeral(v, sort);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -3343,7 +3372,7 @@ namespace Microsoft.Z3
|
|||
uint cd = AST.ArrayLength(decls);
|
||||
if (csn != cs || cdn != cd)
|
||||
throw new Z3Exception("Argument size mismatch");
|
||||
ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
|
||||
using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
|
||||
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
|
||||
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
|
||||
return assertions.ToBoolExprArray();
|
||||
|
|
@ -3362,7 +3391,7 @@ namespace Microsoft.Z3
|
|||
uint cd = AST.ArrayLength(decls);
|
||||
if (csn != cs || cdn != cd)
|
||||
throw new Z3Exception("Argument size mismatch");
|
||||
ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
|
||||
using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
|
||||
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
|
||||
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
|
||||
return assertions.ToBoolExprArray();
|
||||
|
|
@ -3847,8 +3876,8 @@ namespace Microsoft.Z3
|
|||
/// <seealso cref="MkSolver(Symbol)"/>
|
||||
public Solver MkSolver(string logic)
|
||||
{
|
||||
using var slogic = MkSymbol(logic);
|
||||
return MkSolver(slogic);
|
||||
using var symbol = MkSymbol(logic);
|
||||
return MkSolver(symbol);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
@ -4937,16 +4966,16 @@ namespace Microsoft.Z3
|
|||
Fixedpoint_DRQ.Clear(this);
|
||||
Optimize_DRQ.Clear(this);
|
||||
|
||||
if (m_boolSort != null) m_boolSort.Dispose();
|
||||
if (m_intSort != null) m_intSort.Dispose();
|
||||
if (m_realSort != null) m_realSort.Dispose();
|
||||
if (m_stringSort != null) m_stringSort.Dispose();
|
||||
if (m_charSort != null) m_charSort.Dispose();
|
||||
if (m_boolSort != null) m_boolSort.Dispose();
|
||||
if (m_intSort != null) m_intSort.Dispose();
|
||||
if (m_realSort != null) m_realSort.Dispose();
|
||||
if (m_stringSort != null) m_stringSort.Dispose();
|
||||
if (m_charSort != null) m_charSort.Dispose();
|
||||
m_boolSort = null;
|
||||
m_intSort = null;
|
||||
m_realSort = null;
|
||||
m_stringSort = null;
|
||||
m_charSort = null;
|
||||
m_charSort = null;
|
||||
if (refCount == 0 && m_ctx != IntPtr.Zero)
|
||||
{
|
||||
m_n_err_handler = null;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue