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

NativeContext, NativeSolver, NativeModel - updates for Pex (#5878)

Browse source 
* WiP:  Disposable, MkAdd, MkApp, MkBool, MkBoolSort, MkBound, MkBvSort, MkFalse, MkTrue, MkIntSort

* WiP: Native z3 mk_ functions

* WiP: mk_ functions for NativeContext

* WiP: add utility functions for getting values

* WiP: Adding more native utility functions

* native model pull

* WiP: NativeContext additions for array access

* WiP: use Z3_symbol in place of managed Symbol

* WiP: add solver, model, and array methods

* WiP: MkSimpleSolver, MkReal

* WiP: GetDomain GetRange

* WiP: MkExists

* Override for MkFuncDecl

* MkConstArray, MkSelect

* WiP: code cleanup

* migrate Context reference to NativeContext

* remove local signing from PR

* minor code cleanup

Co-authored-by: jfleisher <jofleish@microsoft.com>
This commit is contained in:
John Fleisher 2022-03-03 13:41:12 -05:00 committed by GitHub
parent 811cd9d48d
commit a08be497f7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 1361 additions and 310 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -231,7 +231,6 @@ namespace Microsoft.Z3
return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size)); return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
} }
/// <summary> /// <summary>
/// Create a new sequence sort. /// Create a new sequence sort.
/// </summary> /// </summary>
@ -485,7 +484,7 @@ namespace Microsoft.Z3
/// The function performs a record update at t. The field /// The function performs a record update at t. The field
/// that is passed in as argument is updated with value v, /// that is passed in as argument is updated with value v,
/// the remaining fields of t are unchanged. /// the remaining fields of t are unchanged.
/// </summary> /// </summary>
public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
{ {
return Expr.Create(this, Native.Z3_datatype_update_field( return Expr.Create(this, Native.Z3_datatype_update_field(
@ -560,14 +559,14 @@ namespace Microsoft.Z3
/// MkRecFuncDecl. The body may contain recursive uses of the function or /// MkRecFuncDecl. The body may contain recursive uses of the function or
/// other mutually recursive functions. /// other mutually recursive functions.
/// </summary> /// </summary>
public void AddRecDef(FuncDecl f, Expr[] args, Expr body) public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
{ {
CheckContextMatch(f); CheckContextMatch(f);
CheckContextMatch<Expr>(args); CheckContextMatch<Expr>(args);
CheckContextMatch(body); CheckContextMatch(body);
IntPtr[] argsNative = AST.ArrayToNative(args); IntPtr[] argsNative = AST.ArrayToNative(args);
Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
} }
/// <summary> /// <summary>
/// Creates a new function declaration. /// Creates a new function declaration.
@ -811,7 +810,7 @@ namespace Microsoft.Z3
public Expr MkApp(FuncDecl f, IEnumerable<Expr> args) public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
{ {
Debug.Assert(f != null); Debug.Assert(f != null);
Debug.Assert(args == null || args.All( a => a != null)); Debug.Assert(args == null || args.All(a => a != null));
CheckContextMatch(f); CheckContextMatch(f);
CheckContextMatch(args); CheckContextMatch(args);
@ -949,14 +948,15 @@ namespace Microsoft.Z3
Debug.Assert(ts.All(a => a != null)); Debug.Assert(ts.All(a => a != null));
CheckContextMatch<BoolExpr>(ts); CheckContextMatch<BoolExpr>(ts);
BoolExpr r = null; BoolExpr r = null;
foreach (var t in ts) { foreach (var t in ts)
{
if (r == null) if (r == null)
r = t; r = t;
else else
r = MkXor(r, t); r = MkXor(r, t);
} }
if (r == null) if (r == null)
r = MkTrue(); r = MkTrue();
return r; return r;
} }
@ -2343,7 +2343,7 @@ namespace Microsoft.Z3
CheckContextMatch(elem); CheckContextMatch(elem);
CheckContextMatch(set); CheckContextMatch(set);
return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject)); return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
} }
/// <summary> /// <summary>
@ -2356,7 +2356,7 @@ namespace Microsoft.Z3
CheckContextMatch(arg1); CheckContextMatch(arg1);
CheckContextMatch(arg2); CheckContextMatch(arg2);
return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject)); return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
} }
#endregion #endregion
@ -2413,7 +2413,8 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Convert a bit-vector expression, represented as an signed number, to a string. /// Convert a bit-vector expression, represented as an signed number, to a string.
/// </summary> /// </summary>
public SeqExpr SbvToString(Expr e) { public SeqExpr SbvToString(Expr e)
{
Debug.Assert(e != null); Debug.Assert(e != null);
Debug.Assert(e is ArithExpr); Debug.Assert(e is ArithExpr);
return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject)); return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject));
@ -2449,7 +2450,7 @@ namespace Microsoft.Z3
public IntExpr MkLength(SeqExpr s) public IntExpr MkLength(SeqExpr s)
{ {
Debug.Assert(s != null); Debug.Assert(s != null);
return (IntExpr) Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject)); return (IntExpr)Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
} }
/// <summary> /// <summary>
@ -2768,7 +2769,7 @@ namespace Microsoft.Z3
Debug.Assert(args != null); Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args); CheckContextMatch<BoolExpr>(args);
var ts = args.ToArray(); var ts = args.ToArray();
return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) ts.Length, return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length,
AST.ArrayToNative(ts), k)); AST.ArrayToNative(ts), k));
} }
@ -2780,7 +2781,7 @@ namespace Microsoft.Z3
Debug.Assert(args != null); Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args); CheckContextMatch<BoolExpr>(args);
var ts = args.ToArray(); var ts = args.ToArray();
return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) ts.Length, return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length,
AST.ArrayToNative(ts), k)); AST.ArrayToNative(ts), k));
} }
@ -2789,13 +2790,13 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k) public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
{ {
Debug.Assert(args != null); Debug.Assert(args != null);
Debug.Assert(coeffs != null); Debug.Assert(coeffs != null);
Debug.Assert(args.Length == coeffs.Length); Debug.Assert(args.Length == coeffs.Length);
CheckContextMatch<BoolExpr>(args); CheckContextMatch<BoolExpr>(args);
return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length, return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint)args.Length,
AST.ArrayToNative(args), AST.ArrayToNative(args),
coeffs, k)); coeffs, k));
} }
/// <summary> /// <summary>
@ -2803,26 +2804,26 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k) public BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
{ {
Debug.Assert(args != null); Debug.Assert(args != null);
Debug.Assert(coeffs != null); Debug.Assert(coeffs != null);
Debug.Assert(args.Length == coeffs.Length); Debug.Assert(args.Length == coeffs.Length);
CheckContextMatch<BoolExpr>(args); CheckContextMatch<BoolExpr>(args);
return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint) args.Length, return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint)args.Length,
AST.ArrayToNative(args), AST.ArrayToNative(args),
coeffs, k)); coeffs, k));
} }
/// <summary> /// <summary>
/// Create a pseudo-Boolean equal constraint. /// Create a pseudo-Boolean equal constraint.
/// </summary> /// </summary>
public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k) public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
{ {
Debug.Assert(args != null); Debug.Assert(args != null);
Debug.Assert(coeffs != null); Debug.Assert(coeffs != null);
Debug.Assert(args.Length == coeffs.Length); Debug.Assert(args.Length == coeffs.Length);
CheckContextMatch<BoolExpr>(args); CheckContextMatch<BoolExpr>(args);
return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length, return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint)args.Length,
AST.ArrayToNative(args), AST.ArrayToNative(args),
coeffs, k)); coeffs, k));
} }
#endregion #endregion
@ -4085,7 +4086,7 @@ namespace Microsoft.Z3
/// <param name="negative">indicates whether the result should be negative.</param> /// <param name="negative">indicates whether the result should be negative.</param>
public FPNum MkFPZero(FPSort s, bool negative) public FPNum MkFPZero(FPSort s, bool negative)
{ {
return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
} }
/// <summary> /// <summary>
@ -4127,7 +4128,7 @@ namespace Microsoft.Z3
/// <param name="s">FloatingPoint sort.</param> /// <param name="s">FloatingPoint sort.</param>
public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
{ {
return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
} }
/// <summary> /// <summary>
@ -4139,7 +4140,7 @@ namespace Microsoft.Z3
/// <param name="s">FloatingPoint sort.</param> /// <param name="s">FloatingPoint sort.</param>
public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
{ {
return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
} }
/// <summary> /// <summary>
@ -4825,12 +4826,12 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// ASTVector DRQ /// ASTVector DRQ
/// </summary> /// </summary>
public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } } public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } }
/// <summary> /// <summary>
/// ApplyResult DRQ /// ApplyResult DRQ
/// </summary> /// </summary>
public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } } public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } }
/// <summary> /// <summary>
/// FuncEntry DRQ /// FuncEntry DRQ

1204
src/api/dotnet/NativeContext.cs
View file

File diff suppressed because it is too large Load diff

51
src/api/dotnet/NativeModel.cs
View file

@ -19,20 +19,11 @@ Notes:
--*/ --*/
using System;
using System.Diagnostics;
using System.Collections.Generic;
namespace Microsoft.Z3 namespace Microsoft.Z3
{ {
using Z3_context = System.IntPtr;
using Z3_ast = System.IntPtr; using Z3_ast = System.IntPtr;
using Z3_app = System.IntPtr;
using Z3_sort = System.IntPtr;
using Z3_func_decl = System.IntPtr; using Z3_func_decl = System.IntPtr;
using Z3_model = System.IntPtr; using Z3_sort = System.IntPtr;
using Z3_func_interp = System.IntPtr;
using Z3_func_entry = System.IntPtr;
/// <summary> /// <summary>
/// A Model contains interpretations (assignments) of constants and functions. /// A Model contains interpretations (assignments) of constants and functions.
@ -67,7 +58,6 @@ namespace Microsoft.Z3
/// <returns>A FunctionInterpretation if the function has an interpretation in the model, null otherwise.</returns> /// <returns>A FunctionInterpretation if the function has an interpretation in the model, null otherwise.</returns>
public NativeFuncInterp FuncInterp(Z3_func_decl f) public NativeFuncInterp FuncInterp(Z3_func_decl f)
{ {
Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f)); Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f));
if (Native.Z3_get_arity(Context.nCtx, f) == 0) if (Native.Z3_get_arity(Context.nCtx, f) == 0)
@ -235,7 +225,6 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public Z3_ast Evaluate(Z3_ast t, bool completion = false) => Eval(t, completion); public Z3_ast Evaluate(Z3_ast t, bool completion = false) => Eval(t, completion);
/// <summary> /// <summary>
/// Evaluate expression to a double, assuming it is a numeral already. /// Evaluate expression to a double, assuming it is a numeral already.
/// </summary> /// </summary>
@ -253,12 +242,16 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// One dimensional array of indices where the array is updated /// One dimensional array of indices where the array is updated
/// </summary> /// </summary>
public KeyValuePair<Z3_ast,Z3_ast>[] Updates; public KeyValuePair<Z3_ast, Z3_ast>[] Updates;
/// <summary> /// <summary>
/// default Else case /// default Else case
/// </summary> /// </summary>
public Z3_ast Else; public Z3_ast Else;
public Z3_sort[] Domain;
public Z3_sort[] Range;
} }
/// <summary> /// <summary>
@ -266,26 +259,34 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
/// <param name="t"></param> /// <param name="t"></param>
/// <returns>null if the argument does evaluate to a sequence of stores to an array</returns> /// <returns>null if the argument does evaluate to a sequence of stores to an array</returns>
public ArrayValue TryGetArrayValue(Z3_ast t) public bool TryGetArrayValue(Z3_ast t, out ArrayValue result)
{ {
var r = Eval(t, true); var r = Eval(t, true);
// check that r is a sequence of store over a constant default array. // check that r is a sequence of store over a constant default array.
var updates = new List<KeyValuePair<Z3_ast, Z3_ast>>(); var updates = new List<KeyValuePair<Z3_ast, Z3_ast>>();
var result = new ArrayValue();
while (true) //while (true)
//{
// // check that r is an app, and the decl-kind is Z3_OP_ARRAY_CONST or Z3_OP_ARRAY_STORE
// // if it is Z3_OP_ARRAY_CONST then set result.Else and break;
// // if it is ARRAY_STORE, then append to 'updates' and continue
// // in other cases return null
// return false;
//}
if (updates.Any())
{ {
// check that r is an app, and the decl-kind is Z3_OP_ARRAY_CONST or Z3_OP_ARRAY_STORE result = new ArrayValue()
// if it is Z3_OP_ARRAY_CONST then set result.Else and break; {
// if it is ARRAY_STORE, then append to 'updates' and continue Updates = updates.ToArray()
// in other cases return null };
return null;
return true;
} }
#if false
result.Updates = updates.ToArray();
return null; result = null;
#endif return false;
} }
/// <summary> /// <summary>

257
src/api/dotnet/NativeSolver.cs
View file

@ -18,24 +18,16 @@ Notes:
--*/ --*/
using System;
using System.Diagnostics;
using System.Linq;
using System.Collections.Generic;
namespace Microsoft.Z3 namespace Microsoft.Z3
{ {
using Z3_context = System.IntPtr;
using Z3_ast = System.IntPtr; using Z3_ast = System.IntPtr;
using Z3_app = System.IntPtr; using Z3_context = System.IntPtr;
using Z3_sort = System.IntPtr;
using Z3_func_decl = System.IntPtr; using Z3_func_decl = System.IntPtr;
using Z3_model = System.IntPtr;
using Z3_ast_vector = System.IntPtr;
using Z3_solver = System.IntPtr;
using Z3_symbol = System.IntPtr;
using Z3_params = System.IntPtr; using Z3_params = System.IntPtr;
using Z3_solver = System.IntPtr;
using Z3_sort = System.IntPtr;
using Z3_symbol = System.IntPtr;
/// <summary> /// <summary>
/// Solvers. /// Solvers.
@ -45,21 +37,15 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// A string that describes all available solver parameters. /// A string that describes all available solver parameters.
/// </summary> /// </summary>
public string Help public string Help => Native.Z3_solver_get_help(nCtx, z3solver);
{
get
{
return Native.Z3_solver_get_help(Context.nCtx, NativeObject);
}
}
private void SetParam(Action<Z3_params> setter) private void SetParam(Action<Z3_params> setter)
{ {
Z3_params p = Native.Z3_mk_params(Context.nCtx); Z3_params p = Native.Z3_mk_params(nCtx);
Native.Z3_params_inc_ref(Context.nCtx, p); Native.Z3_params_inc_ref(nCtx, p);
setter(p); setter(p);
Native.Z3_solver_set_params(Context.nCtx, NativeObject, p); Native.Z3_solver_set_params(nCtx, z3solver, p);
Native.Z3_params_dec_ref(Context.nCtx, p); Native.Z3_params_dec_ref(nCtx, p);
} }
/// <summary> /// <summary>
@ -67,7 +53,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public void Set(string name, bool value) public void Set(string name, bool value)
{ {
SetParam((Z3_params p) => Native.Z3_params_set_bool(Context.nCtx, p, Native.Z3_mk_string_symbol(Context.nCtx, name), (byte)(value ? 1 : 0))); SetParam((Z3_params p) => Native.Z3_params_set_bool(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), (byte)(value ? 1 : 0)));
} }
/// <summary> /// <summary>
@ -75,7 +61,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public void Set(string name, uint value) public void Set(string name, uint value)
{ {
SetParam((Z3_params p) => Native.Z3_params_set_uint(Context.nCtx, p, Native.Z3_mk_string_symbol(Context.nCtx, name), value)); SetParam((Z3_params p) => Native.Z3_params_set_uint(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), value));
} }
/// <summary> /// <summary>
@ -83,7 +69,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public void Set(string name, double value) public void Set(string name, double value)
{ {
SetParam((Z3_params p) => Native.Z3_params_set_double(Context.nCtx, p, Native.Z3_mk_string_symbol(Context.nCtx, name), value)); SetParam((Z3_params p) => Native.Z3_params_set_double(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), value));
} }
/// <summary> /// <summary>
@ -91,43 +77,43 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public void Set(string name, string value) public void Set(string name, string value)
{ {
var value_sym = Native.Z3_mk_string_symbol(Context.nCtx, value); var value_sym = Native.Z3_mk_string_symbol(nCtx, value);
SetParam((Z3_params p) => Native.Z3_params_set_symbol(Context.nCtx, p, Native.Z3_mk_string_symbol(Context.nCtx, name), value_sym)); SetParam((Z3_params p) => Native.Z3_params_set_symbol(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), value_sym));
} }
#if false #if false
/// <summary> /// <summary>
/// Sets parameter on the solver /// Sets parameter on the solver
/// </summary> /// </summary>
public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); } public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary> /// <summary>
/// Sets parameter on the solver /// Sets parameter on the solver
/// </summary> /// </summary>
public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); } public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary> /// <summary>
/// Sets parameter on the solver /// Sets parameter on the solver
/// </summary> /// </summary>
public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); } public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary> /// <summary>
/// Sets parameter on the solver /// Sets parameter on the solver
/// </summary> /// </summary>
public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); } public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary> /// <summary>
/// Sets parameter on the solver /// Sets parameter on the solver
/// </summary> /// </summary>
public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); } public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary> /// <summary>
/// Sets parameter on the solver /// Sets parameter on the solver
/// </summary> /// </summary>
public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); } public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary> /// <summary>
/// Retrieves parameter descriptions for solver. /// Retrieves parameter descriptions for solver.
/// </summary> /// </summary>
public ParamDescrs ParameterDescriptions public ParamDescrs ParameterDescriptions
{ {
get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); } get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(nCtx, NativeObject)); }
} }
#endif #endif
/// <summary> /// <summary>
@ -135,38 +121,26 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
/// <seealso cref="Pop"/> /// <seealso cref="Pop"/>
/// <seealso cref="Push"/> /// <seealso cref="Push"/>
public uint NumScopes public uint NumScopes => Native.Z3_solver_get_num_scopes(nCtx, z3solver);
{
get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); }
}
/// <summary> /// <summary>
/// Creates a backtracking point. /// Creates a backtracking point.
/// </summary> /// </summary>
/// <seealso cref="Pop"/> /// <seealso cref="Pop"/>
public void Push() public void Push() => Native.Z3_solver_push(nCtx, z3solver);
{
Native.Z3_solver_push(Context.nCtx, NativeObject);
}
/// <summary> /// <summary>
/// Backtracks <paramref name="n"/> backtracking points. /// Backtracks <paramref name="n"/> backtracking points.
/// </summary> /// </summary>
/// <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <c>NumScopes</c></remarks> /// <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <c>NumScopes</c></remarks>
/// <seealso cref="Push"/> /// <seealso cref="Push"/>
public void Pop(uint n = 1) public void Pop(uint n = 1) => Native.Z3_solver_pop(nCtx, z3solver, n);
{
Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
}
/// <summary> /// <summary>
/// Resets the Solver. /// Resets the Solver.
/// </summary> /// </summary>
/// <remarks>This removes all assertions from the solver.</remarks> /// <remarks>This removes all assertions from the solver.</remarks>
public void Reset() public void Reset() => Native.Z3_solver_reset(nCtx, z3solver);
{
Native.Z3_solver_reset(Context.nCtx, NativeObject);
}
/// <summary> /// <summary>
/// Assert a constraint (or multiple) into the solver. /// Assert a constraint (or multiple) into the solver.
@ -178,25 +152,19 @@ namespace Microsoft.Z3
foreach (Z3_ast a in constraints) foreach (Z3_ast a in constraints)
{ {
Native.Z3_solver_assert(Context.nCtx, NativeObject, a); Native.Z3_solver_assert(nCtx, z3solver, a);
} }
} }
/// <summary> /// <summary>
/// Alias for Assert. /// Alias for Assert.
/// </summary> /// </summary>
public void Add(params Z3_ast[] constraints) public void Add(params Z3_ast[] constraints) => Assert(constraints);
{
Assert(constraints);
}
/// <summary> /// <summary>
/// Alias for Assert. /// Alias for Assert.
/// </summary> /// </summary>
public void Add(IEnumerable<Z3_ast> constraints) public void Add(IEnumerable<Z3_ast> constraints) => Assert(constraints.ToArray());
{
Assert(constraints.ToArray());
}
/// <summary> /// <summary>
/// Add constraints to ensure the function f can only be injective. /// Add constraints to ensure the function f can only be injective.
@ -209,28 +177,26 @@ namespace Microsoft.Z3
/// <param name="f"></param> /// <param name="f"></param>
public void AssertInjective(Z3_func_decl f) public void AssertInjective(Z3_func_decl f)
{ {
uint arity = Native.Z3_get_arity(Context.nCtx, f); uint arity = Native.Z3_get_arity(nCtx, f);
Z3_sort range = Native.Z3_get_range(Context.nCtx, f); Z3_sort range = Native.Z3_get_range(nCtx, f);
Z3_ast[] vars = new Z3_ast[arity]; Z3_ast[] vars = new Z3_ast[arity];
Z3_sort[] sorts = new Z3_sort[arity]; Z3_sort[] sorts = new Z3_sort[arity];
Z3_symbol[] names = new Z3_symbol[arity]; Z3_symbol[] names = new Z3_symbol[arity];
for (uint i = 0; i < arity; ++i) for (uint i = 0; i < arity; ++i)
{ {
Z3_sort domain = Native.Z3_get_domain(Context.nCtx, f, i); Z3_sort domain = Native.Z3_get_domain(nCtx, f, i);
//vars[i] = Context.MkBound(arity - i - 1, domain); vars[i] = ntvContext.MkBound(arity - i - 1, domain);
sorts[i] = domain; sorts[i] = domain;
names[i] = Native.Z3_mk_int_symbol(Context.nCtx, (int)i); names[i] = Native.Z3_mk_int_symbol(nCtx, (int)i);
} }
Z3_ast app_f = IntPtr.Zero; // Context.MkApp(f, vars); Z3_ast app_f = IntPtr.Zero; // Context.MkApp(f, vars);
for (uint i = 0; i < arity; ++i) for (uint i = 0; i < arity; ++i)
{ {
Z3_sort domain = Native.Z3_get_domain(Context.nCtx, f, i); Z3_sort domain = Native.Z3_get_domain(nCtx, f, i);
#if false Z3_func_decl proj = ntvContext.MkFreshFuncDecl("inv", new Z3_sort[] { range }, domain);
Z3_func_decl proj = Native.Z3_mk_fresh_func_decl("inv", new Z3_sort[] { range }, domain); Z3_ast body = ntvContext.MkEq(vars[i], ntvContext.MkApp(proj, app_f));
Z3_ast body = Context.MkEq(vars[i], Context.MkApp(proj, app_f)); Z3_ast q = ntvContext.MkForall(names, sorts, body);
Z3_ast q = Context.MkForall(names, sorts, body);
Assert(q); Assert(q);
#endif
} }
} }
@ -254,7 +220,7 @@ namespace Microsoft.Z3
throw new Z3Exception("Argument size mismatch"); throw new Z3Exception("Argument size mismatch");
for (int i = 0; i < constraints.Length; i++) for (int i = 0; i < constraints.Length; i++)
Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i], ps[i]); Native.Z3_solver_assert_and_track(nCtx, z3solver, constraints[i], ps[i]);
} }
/// <summary> /// <summary>
@ -273,57 +239,38 @@ namespace Microsoft.Z3
Debug.Assert(constraint != null); Debug.Assert(constraint != null);
Debug.Assert(p != null); Debug.Assert(p != null);
Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint, p); Native.Z3_solver_assert_and_track(nCtx, z3solver, constraint, p);
} }
/// <summary> /// <summary>
/// Load solver assertions from a file. /// Load solver assertions from a file.
/// </summary> /// </summary>
public void FromFile(string file) public void FromFile(string file)
{ => Native.Z3_solver_from_file(nCtx, z3solver, file);
Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);
}
/// <summary> /// <summary>
/// Load solver assertions from a string. /// Load solver assertions from a string.
/// </summary> /// </summary>
public void FromString(string str) public void FromString(string str)
{ => Native.Z3_solver_from_string(nCtx, z3solver, str);
Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);
}
/// <summary> /// <summary>
/// The number of assertions in the solver. /// The number of assertions in the solver.
/// </summary> /// </summary>
public uint NumAssertions public uint NumAssertions
{ => (uint)ntvContext.ToArray(Native.Z3_solver_get_assertions(nCtx, z3solver)).Length;
get
{
return (uint)Context.ToArray(Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)).Length;
}
}
/// <summary> /// <summary>
/// The set of asserted formulas. /// The set of asserted formulas.
/// </summary> /// </summary>
public Z3_ast[] Assertions public Z3_ast[] Assertions
{ => ntvContext.ToArray(Native.Z3_solver_get_assertions(nCtx, z3solver));
get
{
return Context.ToArray(Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
}
}
/// <summary> /// <summary>
/// Currently inferred units. /// Currently inferred units.
/// </summary> /// </summary>
public Z3_ast[] Units public Z3_ast[] Units
{ => ntvContext.ToArray(Native.Z3_solver_get_units(nCtx, z3solver));
get
{
return Context.ToArray(Native.Z3_solver_get_units(Context.nCtx, NativeObject));
}
}
/// <summary> /// <summary>
/// Checks whether the assertions in the solver are consistent or not. /// Checks whether the assertions in the solver are consistent or not.
@ -337,9 +284,9 @@ namespace Microsoft.Z3
{ {
Z3_lbool r; Z3_lbool r;
if (assumptions == null || assumptions.Length == 0) if (assumptions == null || assumptions.Length == 0)
r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject); r = (Z3_lbool)Native.Z3_solver_check(nCtx, z3solver);
else else
r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, assumptions); r = (Z3_lbool)Native.Z3_solver_check_assumptions(nCtx, z3solver, (uint)assumptions.Length, assumptions);
return lboolToStatus(r); return lboolToStatus(r);
} }
@ -356,13 +303,12 @@ namespace Microsoft.Z3
Z3_lbool r; Z3_lbool r;
Z3_ast[] asms = assumptions.ToArray(); Z3_ast[] asms = assumptions.ToArray();
if (asms.Length == 0) if (asms.Length == 0)
r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject); r = (Z3_lbool)Native.Z3_solver_check(nCtx, z3solver);
else else
r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)asms.Length, asms); r = (Z3_lbool)Native.Z3_solver_check_assumptions(nCtx, z3solver, (uint)asms.Length, asms);
return lboolToStatus(r); return lboolToStatus(r);
} }
/// <summary> /// <summary>
/// The model of the last <c>Check(params Expr[] assumptions)</c>. /// The model of the last <c>Check(params Expr[] assumptions)</c>.
/// </summary> /// </summary>
@ -374,11 +320,10 @@ namespace Microsoft.Z3
{ {
get get
{ {
IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject); IntPtr x = Native.Z3_solver_get_model(nCtx, z3solver);
if (x == IntPtr.Zero) return x == IntPtr.Zero
return null; ? null
else : new NativeModel(ntvContext, x);
return new NativeModel(Context, x);
} }
} }
@ -390,12 +335,7 @@ namespace Microsoft.Z3
/// if its results was not <c>UNSATISFIABLE</c>, or if proof production is disabled. /// if its results was not <c>UNSATISFIABLE</c>, or if proof production is disabled.
/// </remarks> /// </remarks>
public Z3_ast Proof public Z3_ast Proof
{ => Native.Z3_solver_get_proof(nCtx, z3solver);
get
{
return Native.Z3_solver_get_proof(Context.nCtx, NativeObject);
}
}
/// <summary> /// <summary>
/// The unsat core of the last <c>Check</c>. /// The unsat core of the last <c>Check</c>.
@ -406,23 +346,13 @@ namespace Microsoft.Z3
/// if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled. /// if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled.
/// </remarks> /// </remarks>
public Z3_ast[] UnsatCore public Z3_ast[] UnsatCore
{ => ntvContext.ToArray(Native.Z3_solver_get_unsat_core(nCtx, z3solver));
get
{
return Context.ToArray(Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
}
}
/// <summary> /// <summary>
/// A brief justification of why the last call to <c>Check</c> returned <c>UNKNOWN</c>. /// A brief justification of why the last call to <c>Check</c> returned <c>UNKNOWN</c>.
/// </summary> /// </summary>
public string ReasonUnknown public string ReasonUnknown
{ => Native.Z3_solver_get_reason_unknown(nCtx, z3solver);
get
{
return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
}
}
/// <summary> /// <summary>
/// Create a clone of the current solver with respect to <c>ctx</c>. /// Create a clone of the current solver with respect to <c>ctx</c>.
@ -430,7 +360,7 @@ namespace Microsoft.Z3
public NativeSolver Translate(NativeContext ctx) public NativeSolver Translate(NativeContext ctx)
{ {
Debug.Assert(ctx != null); Debug.Assert(ctx != null);
return new NativeSolver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx)); return new NativeSolver(ctx, Native.Z3_solver_translate(nCtx, z3solver, ctx.nCtx));
} }
/// <summary> /// <summary>
@ -438,9 +368,10 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public void ImportModelConverter(NativeSolver src) public void ImportModelConverter(NativeSolver src)
{ {
Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject); Debug.Assert(src != null);
}
Native.Z3_solver_import_model_converter(nCtx, src.z3solver, z3solver);
}
/// <summary> /// <summary>
/// Solver statistics. /// Solver statistics.
@ -449,8 +380,8 @@ namespace Microsoft.Z3
{ {
get get
{ {
var stats = Native.Z3_solver_get_statistics(Context.nCtx, NativeObject); var stats = Native.Z3_solver_get_statistics(nCtx, z3solver);
return Context.GetStatistics(stats); return ntvContext.GetStatistics(stats);
} }
} }
@ -459,19 +390,23 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public override string ToString() public override string ToString()
{ {
return Native.Z3_solver_to_string(Context.nCtx, NativeObject); return Native.Z3_solver_to_string(nCtx, z3solver);
} }
#region Internal #region Internal
NativeContext Context; readonly NativeContext ntvContext;
IntPtr NativeObject; Z3_solver z3solver;
internal NativeSolver(NativeContext ctx, Z3_solver obj) Z3_context nCtx => ntvContext.nCtx;
{
Context = ctx;
NativeObject = obj;
Debug.Assert(ctx != null); internal NativeSolver(NativeContext nativeCtx, Z3_solver z3solver)
Native.Z3_solver_inc_ref(ctx.nCtx, obj); {
Debug.Assert(nCtx != IntPtr.Zero);
Debug.Assert(z3solver != IntPtr.Zero);
this.ntvContext = nativeCtx;
this.z3solver = z3solver;
Native.Z3_solver_inc_ref(nCtx, z3solver);
} }
/// <summary> /// <summary>
@ -487,10 +422,10 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public void Dispose() public void Dispose()
{ {
if (NativeObject != IntPtr.Zero) if (z3solver != IntPtr.Zero)
{ {
Native.Z3_solver_dec_ref(Context.nCtx, NativeObject); Native.Z3_solver_dec_ref(nCtx, z3solver);
NativeObject = IntPtr.Zero; z3solver = IntPtr.Zero;
} }
GC.SuppressFinalize(this); GC.SuppressFinalize(this);
} }