mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

overloading support for C# expressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-23 15:50:30 -07:00
parent e4b7ac37f3
commit 662e43d264
5 changed files with 225 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -21,6 +21,7 @@ using System;
using System.Collections.Generic;
using System.Runtime.InteropServices;
using System.Diagnostics.Contracts;
using System.Linq;
namespace Microsoft.Z3
{
@ -814,6 +815,20 @@ namespace Microsoft.Z3
return Expr.Create(this, f, args);
}
/// <summary>
/// Create a new function application.
/// </summary>
public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
{
Contract.Requires(f != null);
Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(f);
CheckContextMatch(args);
return Expr.Create(this, f, args.ToArray());
}
#region Propositional
/// <summary>
/// The true Term.
@ -959,6 +974,18 @@ namespace Microsoft.Z3
return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
/// <summary>
/// Create an expression representing <c>t[0] and t[1] and ...</c>.
/// </summary>
public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
{
Contract.Requires(t != null);
Contract.Requires(Contract.ForAll(t, a => a != null));
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t);
return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
}
/// <summary>
/// Create an expression representing <c>t[0] or t[1] or ...</c>.
/// </summary>
@ -973,6 +1000,19 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create an expression representing <c>t[0] or t[1] or ...</c>.
/// </summary>
public BoolExpr MkOr(IEnumerable<BoolExpr> t)
{
Contract.Requires(t != null);
Contract.Requires(Contract.ForAll(t, a => a != null));
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t);
return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
}
#endregion
#region Arithmetic
@ -989,6 +1029,19 @@ namespace Microsoft.Z3
return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
/// <summary>
/// Create an expression representing <c>t[0] + t[1] + ...</c>.
/// </summary>
public ArithExpr MkAdd(IEnumerable<ArithExpr> t)
{
Contract.Requires(t != null);
Contract.Requires(Contract.ForAll(t, a => a != null));
Contract.Ensures(Contract.Result<ArithExpr>() != null);
CheckContextMatch(t);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
}
/// <summary>
/// Create an expression representing <c>t[0] * t[1] * ...</c>.
/// </summary>
@ -4743,6 +4796,21 @@ namespace Microsoft.Z3
}
}
[Pure]
internal void CheckContextMatch(IEnumerable<Z3Object> arr)
{
Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
if (arr != null)
{
foreach (Z3Object a in arr)
{
Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
CheckContextMatch(a);
}
}
}
[ContractInvariantMethod]
private void ObjectInvariant()
{