mirror of
https://github.com/Z3Prover/z3
synced 2025-06-18 20:03:38 +00:00
missing public
This commit is contained in:
parent
b43965bf05
commit
9836d5e6fc
1 changed files with 5 additions and 5 deletions
|
@ -207,16 +207,16 @@ namespace Microsoft.Z3
|
||||||
/// <summary>
|
/// <summary>
|
||||||
/// Declare combination of assigned expressions a conflict
|
/// Declare combination of assigned expressions a conflict
|
||||||
/// </summary>
|
/// </summary>
|
||||||
void Conflict(params Expr[] terms) {
|
public void Conflict(params Expr[] terms) {
|
||||||
Propagate(terms, ctx.MkFalse());
|
Propagate(terms, ctx.MkFalse());
|
||||||
}
|
}
|
||||||
|
|
||||||
/// <summary>
|
/// <summary>
|
||||||
/// Propagate consequence
|
/// Propagate consequence
|
||||||
/// </summary>
|
/// </summary>
|
||||||
void Propagate(Expr[] terms, Expr conseq) {
|
public void Propagate(Expr[] terms, Expr conseq) {
|
||||||
var nTerms = Z3Object.ArrayToNative(terms);
|
var nTerms = Z3Object.ArrayToNative(terms);
|
||||||
Native.Z3_solver_propagate_consequence(ctx.nCtx, this.callback, (uint)nTerms.Length, nTerms, 0u, null, null, conseq.NativeObject);
|
Native.Z3_solver_propagate_consequence(ctx.nCtx, this.callback, (uint)nTerms.Length, nTerms, 0u, null, null, conseq.NativeObject);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue