mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Add missing .NET API functions for parsing rules into fixedpoint object
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4957e71408
commit
44751c0ef8
|
@ -269,6 +269,14 @@ namespace Microsoft.Z3
|
|||
AST.ArrayLength(queries), AST.ArrayToNative(queries));
|
||||
}
|
||||
|
||||
BoolExpr[] ToBoolExprs(ASTVector v) {
|
||||
uint n = v.Size;
|
||||
BoolExpr[] res = new BoolExpr[n];
|
||||
for (uint i = 0; i < n; i++)
|
||||
res[i] = new BoolExpr(Context, v[i].NativeObject);
|
||||
return res;
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Retrieve set of rules added to fixedpoint context.
|
||||
/// </summary>
|
||||
|
@ -278,12 +286,7 @@ namespace Microsoft.Z3
|
|||
{
|
||||
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
|
||||
|
||||
ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
|
||||
uint n = v.Size;
|
||||
BoolExpr[] res = new BoolExpr[n];
|
||||
for (uint i = 0; i < n; i++)
|
||||
res[i] = new BoolExpr(Context, v[i].NativeObject);
|
||||
return res;
|
||||
return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)));
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -296,15 +299,27 @@ namespace Microsoft.Z3
|
|||
{
|
||||
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
|
||||
|
||||
ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
|
||||
uint n = v.Size;
|
||||
BoolExpr[] res = new BoolExpr[n];
|
||||
for (uint i = 0; i < n; i++)
|
||||
res[i] = new BoolExpr(Context, v[i].NativeObject);
|
||||
return res;
|
||||
return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)));
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Parse an SMT-LIB2 file with fixedpoint rules.
|
||||
/// Add the rules to the current fixedpoint context.
|
||||
/// Return the set of queries in the file.
|
||||
/// </summary>
|
||||
public BoolExpr[] ParseFile(string file) {
|
||||
return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)));
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Similar to ParseFile. Instead it takes as argument a string.
|
||||
/// </summary>
|
||||
|
||||
public BoolExpr[] ParseString(string s) {
|
||||
return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)));
|
||||
}
|
||||
|
||||
|
||||
#region Internal
|
||||
internal Fixedpoint(Context ctx, IntPtr obj)
|
||||
|
|
Loading…
Reference in a new issue