mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

add operator for issue #860

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-04 09:14:09 -08:00
parent cb75a55095
commit ae9a3bfc24
3 changed files with 12 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/api/api_ast.cpp
View file

@ -1063,9 +1063,10 @@ extern "C" {
case OP_BV2INT: return Z3_OP_BV2INT;
case OP_CARRY: return Z3_OP_CARRY;
case OP_XOR3: return Z3_OP_XOR3;
case OP_BIT2BOOL: return Z3_OP_BIT2BOOL;
case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSDIV_I: return Z3_OP_BSDIV_I;
case OP_BUDIV_I: return Z3_OP_BUDIV_I;
case OP_BSREM_I: return Z3_OP_BSREM_I;

9
src/api/dotnet/Solver.cs
View file

@ -18,6 +18,7 @@ Notes:
--*/
using System;
using System.Linq;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
@ -126,6 +127,14 @@ namespace Microsoft.Z3
Assert(constraints);
}
/// <summary>
/// Alias for Assert.
/// </summary>
public void Add(IEnumerable<BoolExpr> constraints)
{
Assert(constraints.ToArray());
}
/// <summary>
/// Assert multiple constraints into the solver, and track them (in the unsat) core
/// using the Boolean constants in ps.

1
src/api/z3_api.h
View file

@ -1060,6 +1060,7 @@ typedef enum {
Z3_OP_EXT_ROTATE_LEFT,
Z3_OP_EXT_ROTATE_RIGHT,
Z3_OP_BIT2BOOL,
Z3_OP_INT2BV,
Z3_OP_BV2INT,
Z3_OP_CARRY,