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

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-12-02 18:41:22 -08:00
parent e2565d8d82 d23dce4f7b
commit e9a2b7f9f0
16 changed files with 1425 additions and 1056 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

85
examples/dotnet/Program.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-16
Notes:
--*/
using System;
@ -41,7 +41,7 @@ namespace test_mapi
/// forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i
/// </c>
/// Where, <code>finv</code>is a fresh function declaration.
/// </summary>
/// </summary>
public static BoolExpr InjAxiom(Context ctx, FuncDecl f, int i)
{
Sort[] domain = f.Domain;
@ -155,11 +155,11 @@ namespace test_mapi
}
/// <summary>
/// Assert the axiom: function f is commutative.
/// Assert the axiom: function f is commutative.
/// </summary>
/// <remarks>
/// This example uses the SMT-LIB parser to simplify the axiom construction.
/// </remarks>
/// </remarks>
private static BoolExpr CommAxiom(Context ctx, FuncDecl f)
{
Sort t = f.Range;
@ -453,7 +453,7 @@ namespace test_mapi
/// <summary>
/// Sudoku solving example.
/// </summary>
/// </summary>
static void SudokuExample(Context ctx)
{
Console.WriteLine("SudokuExample");
@ -649,7 +649,7 @@ namespace test_mapi
}
/// <summary>
/// Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when
/// Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when
/// <code>f</code> is injective in the second argument. <seealso cref="inj_axiom"/>
/// </summary>
public static void QuantifierExample3(Context ctx)
@ -687,7 +687,7 @@ namespace test_mapi
}
/// <summary>
/// Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when
/// Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when
/// <code>f</code> is injective in the second argument. <seealso cref="inj_axiom"/>
/// </summary>
public static void QuantifierExample4(Context ctx)
@ -726,7 +726,7 @@ namespace test_mapi
/// <summary>
/// Some basic tests.
/// </summary>
/// </summary>
static void BasicTests(Context ctx)
{
Console.WriteLine("BasicTests");
@ -759,7 +759,7 @@ namespace test_mapi
foreach (BoolExpr a in g.Formulas)
solver.Assert(a);
if (solver.Check() != Status.SATISFIABLE)
if (solver.Check() != Status.SATISFIABLE)
throw new TestFailedException();
ApplyResult ar = ApplyTactic(ctx, ctx.MkTactic("simplify"), g);
@ -965,7 +965,7 @@ namespace test_mapi
/// <summary>
/// Shows how to read an SMT1 file.
/// </summary>
/// </summary>
static void SMT1FileTest(string filename)
{
Console.Write("SMT File test ");
@ -1020,7 +1020,7 @@ namespace test_mapi
// break;
// case Z3_ast_kind.Z3_QUANTIFIER_AST:
// q.Enqueue(((Quantifier)cur).Args[0]);
// break;
// break;
// case Z3_ast_kind.Z3_VAR_AST: break;
// case Z3_ast_kind.Z3_NUMERAL_AST: break;
// case Z3_ast_kind.Z3_FUNC_DECL_AST: break;
@ -1158,7 +1158,7 @@ namespace test_mapi
/// Prove <tt>x = y implies g(x) = g(y)</tt>, and
/// disprove <tt>x = y implies g(g(x)) = g(y)</tt>.
/// </summary>
/// <remarks>This function demonstrates how to create uninterpreted
/// <remarks>This function demonstrates how to create uninterpreted
/// types and functions.</remarks>
public static void ProveExample1(Context ctx)
{
@ -1203,8 +1203,8 @@ namespace test_mapi
/// Prove <tt>not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 </tt>.
/// Then, show that <tt>z < -1</tt> is not implied.
/// </summary>
/// <remarks>This example demonstrates how to combine uninterpreted functions
/// and arithmetic.</remarks>
/// <remarks>This example demonstrates how to combine uninterpreted functions
/// and arithmetic.</remarks>
public static void ProveExample2(Context ctx)
{
Console.WriteLine("ProveExample2");
@ -1255,7 +1255,7 @@ namespace test_mapi
/// <summary>
/// Show how push & pop can be used to create "backtracking" points.
/// </summary>
/// <remarks>This example also demonstrates how big numbers can be
/// <remarks>This example also demonstrates how big numbers can be
/// created in ctx.</remarks>
public static void PushPopExample1(Context ctx)
{
@ -1318,7 +1318,7 @@ namespace test_mapi
/// <summary>
/// Tuples.
/// </summary>
/// <remarks>Check that the projection of a tuple
/// <remarks>Check that the projection of a tuple
/// returns the corresponding element.</remarks>
public static void TupleExample(Context ctx)
{
@ -1328,7 +1328,7 @@ namespace test_mapi
TupleSort tuple = ctx.MkTupleSort(
ctx.MkSymbol("mk_tuple"), // name of tuple constructor
new Symbol[] { ctx.MkSymbol("first"), ctx.MkSymbol("second") }, // names of projection operators
new Sort[] { int_type, int_type } // types of projection operators
new Sort[] { int_type, int_type } // types of projection operators
);
FuncDecl first = tuple.FieldDecls[0]; // declarations are for projections
FuncDecl second = tuple.FieldDecls[1];
@ -1342,7 +1342,7 @@ namespace test_mapi
}
/// <summary>
/// Simple bit-vector example.
/// Simple bit-vector example.
/// </summary>
/// <remarks>
/// This example disproves that x - 10 &lt;= 0 IFF x &lt;= 10 for (32-bit) machine integers
@ -1366,7 +1366,7 @@ namespace test_mapi
/// <summary>
/// Find x and y such that: x ^ y - 103 == x * y
/// </summary>
/// </summary>
public static void BitvectorExample2(Context ctx)
{
Console.WriteLine("BitvectorExample2");
@ -1446,7 +1446,7 @@ namespace test_mapi
/// <summary>
/// Display the declarations, assumptions and formulas in a SMT-LIB string.
/// </summary>
/// </summary>
public static void ParserExample4(Context ctx)
{
Console.WriteLine("ParserExample4");
@ -1504,7 +1504,7 @@ namespace test_mapi
/// <summary>
/// Create an enumeration data type.
/// </summary>
/// </summary>
public static void EnumExample(Context ctx)
{
Console.WriteLine("EnumExample");
@ -1603,7 +1603,7 @@ namespace test_mapi
/// <summary>
/// Create a binary tree datatype.
/// </summary>
/// </summary>
public static void TreeExample(Context ctx)
{
Console.WriteLine("TreeExample");
@ -1681,14 +1681,14 @@ namespace test_mapi
//
// Declare the names of the accessors for cons.
// Then declare the sorts of the accessors.
// Then declare the sorts of the accessors.
// For this example, all sorts refer to the new types 'forest' and 'tree'
// being declared, so we pass in null for both sorts1 and sorts2.
// On the other hand, the sort_refs arrays contain the indices of the
// two new sorts being declared. The first element in sort1_refs
// points to 'tree', which has index 1, the second element in sort1_refs array
// points to 'forest', which has index 0.
//
//
Symbol[] head_tail1 = new Symbol[] { ctx.MkSymbol("head"), ctx.MkSymbol("tail") };
Sort[] sorts1 = new Sort[] { null, null };
uint[] sort1_refs = new uint[] { 1, 0 }; // the first item points to a tree, the second to a forest
@ -1860,7 +1860,7 @@ namespace test_mapi
}
/// <summary>
/// Demonstrate how to use <code>Push</code>and <code>Pop</code>to
/// Demonstrate how to use <code>Push</code>and <code>Pop</code>to
/// control the size of models.
/// </summary>
/// <remarks>Note: this test is specialized to 32-bit bitvectors.</remarks>
@ -1954,7 +1954,7 @@ namespace test_mapi
/// <summary>
/// Simplifier example.
/// </summary>
/// </summary>
public static void SimplifierExample(Context ctx)
{
Console.WriteLine("SimplifierExample");
@ -1970,7 +1970,7 @@ namespace test_mapi
}
/// <summary>
/// Extract unsatisfiable core example
/// Extract unsatisfiable core example
/// </summary>
public static void UnsatCoreAndProofExample(Context ctx)
{
@ -2023,7 +2023,7 @@ namespace test_mapi
BoolExpr pb = ctx.MkBoolConst("PredB");
BoolExpr pc = ctx.MkBoolConst("PredC");
BoolExpr pd = ctx.MkBoolConst("PredD");
BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc });
BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc });
BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc));
@ -2042,7 +2042,7 @@ namespace test_mapi
if (result == Status.UNSATISFIABLE)
{
Console.WriteLine("unsat");
Console.WriteLine("unsat");
Console.WriteLine("core: ");
foreach (Expr c in solver.UnsatCore)
{
@ -2055,18 +2055,19 @@ namespace test_mapi
{
Console.WriteLine("FiniteDomainExample");
var s = ctx.MkFiniteDomainSort("S", 10);
var t = ctx.MkFiniteDomainSort("T", 10);
var s1 = ctx.MkNumeral(1, s);
var t1 = ctx.MkNumeral(1, t);
Console.WriteLine("{0}", s);
Console.WriteLine("{0}", t);
FiniteDomainSort s = ctx.MkFiniteDomainSort("S", 10);
FiniteDomainSort t = ctx.MkFiniteDomainSort("T", 10);
FiniteDomainNum s1 = (FiniteDomainNum)ctx.MkNumeral(1, s);
FiniteDomainNum t1 = (FiniteDomainNum)ctx.MkNumeral(1, t);
Console.WriteLine("{0} of size {1}", s, s.Size);
Console.WriteLine("{0} of size {1}", t, t.Size);
Console.WriteLine("{0}", s1);
Console.WriteLine("{0}", ctx.MkNumeral(2, s));
Console.WriteLine("{0}", t1);
Console.WriteLine("{0}", s1.Int);
Console.WriteLine("{0}", t1.Int);
// But you cannot mix numerals of different sorts
// even if the size of their domains are the same:
// Console.WriteLine("{0}", ctx.MkEq(s1, t1));
// Console.WriteLine("{0}", ctx.MkEq(s1, t1));
}
public static void FloatingPointExample1(Context ctx)
@ -2084,7 +2085,7 @@ namespace test_mapi
BoolExpr a = ctx.MkAnd(ctx.MkFPEq(x, y), ctx.MkFPEq(y, z));
Check(ctx, ctx.MkNot(a), Status.UNSATISFIABLE);
/* nothing is equal to NaN according to floating-point
/* nothing is equal to NaN according to floating-point
* equality, so NaN == k should be unsatisfiable. */
FPExpr k = (FPExpr)ctx.MkConst("x", s);
FPExpr nan = ctx.MkFPNaN(s);
@ -2125,7 +2126,7 @@ namespace test_mapi
FPRMExpr rm = (FPRMExpr)ctx.MkConst(ctx.MkSymbol("rm"), rm_sort);
BitVecExpr x = (BitVecExpr)ctx.MkConst(ctx.MkSymbol("x"), ctx.MkBitVecSort(64));
FPExpr y = (FPExpr)ctx.MkConst(ctx.MkSymbol("y"), double_sort);
FPExpr y = (FPExpr)ctx.MkConst(ctx.MkSymbol("y"), double_sort);
FPExpr fp_val = ctx.MkFP(42, double_sort);
BoolExpr c1 = ctx.MkEq(y, fp_val);
@ -2138,7 +2139,7 @@ namespace test_mapi
/* Generic solver */
Solver s = ctx.MkSolver();
s.Assert(c5);
Console.WriteLine(s);
if (s.Check() != Status.SATISFIABLE)
@ -2210,8 +2211,8 @@ namespace test_mapi
}
// These examples need proof generation turned on and auto-config set to false.
using (Context ctx = new Context(new Dictionary<string, string>()
{ {"proof", "true" },
using (Context ctx = new Context(new Dictionary<string, string>()
{ {"proof", "true" },
{"auto-config", "false" } }))
{
QuantifierExample3(ctx);

9
examples/java/JavaExample.java
View file

@ -2163,13 +2163,14 @@ class JavaExample
FiniteDomainSort s = ctx.mkFiniteDomainSort("S", 10);
FiniteDomainSort t = ctx.mkFiniteDomainSort("T", 10);
Expr s1 = ctx.mkNumeral(1, s);
Expr t1 = ctx.mkNumeral(1, t);
FiniteDomainNum s1 = (FiniteDomainNum)ctx.mkNumeral(1, s);
FiniteDomainNum t1 = (FiniteDomainNum)ctx.mkNumeral(1, t);
System.out.println(s);
System.out.println(t);
System.out.println(s1);
System.out.println(ctx.mkNumeral(2, s));
System.out.println(s1);
System.out.println(t1);
System.out.println(s1.getInt());
System.out.println(t1.getInt());
// But you cannot mix numerals of different sorts
// even if the size of their domains are the same:
// System.out.println(ctx.mkEq(s1, t1));

257
src/api/api_ast.cpp
View file

@ -55,12 +55,12 @@ extern "C" {
return result;
Z3_CATCH_RETURN(0);
}
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, char const * str) {
Z3_TRY;
LOG_Z3_mk_string_symbol(c, str);
RESET_ERROR_CODE();
symbol s;
symbol s;
if (str == 0 || *str == 0)
s = symbol::null;
else
@ -69,12 +69,12 @@ extern "C" {
return result;
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2) {
RESET_ERROR_CODE();
return s1 == s2;
}
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol name) {
Z3_TRY;
LOG_Z3_mk_uninterpreted_sort(c, name);
@ -94,17 +94,17 @@ extern "C" {
RESET_ERROR_CODE();
return s1 == s2;
}
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const* domain,
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const* domain,
Z3_sort range) {
Z3_TRY;
LOG_Z3_mk_func_decl(c, s, domain_size, domain, range);
RESET_ERROR_CODE();
func_decl* d = mk_c(c)->m().mk_func_decl(to_symbol(s),
domain_size,
func_decl* d = mk_c(c)->m().mk_func_decl(to_symbol(s),
domain_size,
to_sorts(domain),
to_sort(range));
mk_c(c)->save_ast_trail(d);
RETURN_Z3(of_func_decl(d));
Z3_CATCH_RETURN(0);
@ -113,29 +113,29 @@ extern "C" {
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const * args) {
Z3_TRY;
LOG_Z3_mk_app(c, d, num_args, args);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
ptr_buffer<expr> arg_list;
for (unsigned i = 0; i < num_args; ++i) {
arg_list.push_back(to_expr(args[i]));
}
func_decl* _d = reinterpret_cast<func_decl*>(d);
app* a = mk_c(c)->m().mk_app(_d, num_args, arg_list.c_ptr());
app* a = mk_c(c)->m().mk_app(_d, num_args, arg_list.c_ptr());
mk_c(c)->save_ast_trail(a);
check_sorts(c, a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty) {
Z3_TRY;
LOG_Z3_mk_const(c, s, ty);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
app* a = mk_c(c)->m().mk_const(mk_c(c)->m().mk_const_decl(to_symbol(s), to_sort(ty)));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, const char * prefix, unsigned domain_size,
Z3_sort const domain[], Z3_sort range) {
@ -146,16 +146,16 @@ extern "C" {
prefix = "";
}
func_decl* d = mk_c(c)->m().mk_fresh_func_decl(prefix,
domain_size,
func_decl* d = mk_c(c)->m().mk_fresh_func_decl(prefix,
domain_size,
reinterpret_cast<sort*const*>(domain),
to_sort(range));
mk_c(c)->save_ast_trail(d);
RETURN_Z3(of_func_decl(d));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, const char * prefix, Z3_sort ty) {
Z3_TRY;
LOG_Z3_mk_fresh_const(c, prefix, ty);
@ -177,7 +177,7 @@ extern "C" {
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_false(Z3_context c) {
Z3_TRY;
LOG_Z3_mk_false(c);
@ -200,14 +200,14 @@ extern "C" {
Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3));
mk_c(c)->save_ast_trail(result);
check_sorts(c, result);
check_sorts(c, result);
return of_ast(result);
}
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
Z3_TRY;
LOG_Z3_mk_ite(c, t1, t2, t3);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
Z3_ast r = mk_ite_core(c, t1, t2, t3);
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
@ -221,21 +221,21 @@ extern "C" {
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a) {
RESET_ERROR_CODE();
return (Z3_ast)(a);
}
Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s) {
Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a) {
RESET_ERROR_CODE();
return (Z3_ast)(s);
}
return (Z3_ast)(a);
}
Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f) {
Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s) {
RESET_ERROR_CODE();
return (Z3_ast)(f);
}
return (Z3_ast)(s);
}
Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f) {
RESET_ERROR_CODE();
return (Z3_ast)(f);
}
// ------------------------
@ -273,7 +273,7 @@ extern "C" {
return _s.is_numerical() ? Z3_INT_SYMBOL : Z3_STRING_SYMBOL;
Z3_CATCH_RETURN(Z3_INT_SYMBOL);
}
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s) {
Z3_TRY;
LOG_Z3_get_symbol_int(c, s);
@ -286,7 +286,7 @@ extern "C" {
return -1;
Z3_CATCH_RETURN(-1);
}
Z3_API char const * Z3_get_symbol_string(Z3_context c, Z3_symbol s) {
Z3_TRY;
LOG_Z3_get_symbol_string(c, s);
@ -313,7 +313,7 @@ extern "C" {
case AST_APP: {
expr * e = to_expr(_a);
// Real algebraic numbers are not considered Z3_NUMERAL_AST
if (is_numeral_sort(c, of_sort(mk_c(c)->m().get_sort(e))) && mk_c(c)->m().is_unique_value(e))
if (is_numeral_sort(c, of_sort(mk_c(c)->m().get_sort(e))) && mk_c(c)->m().is_unique_value(e))
return Z3_NUMERAL_AST;
return Z3_APP_AST;
}
@ -331,46 +331,46 @@ extern "C" {
RESET_ERROR_CODE();
return to_ast(a)->hash();
}
Z3_bool Z3_API Z3_is_app(Z3_context c, Z3_ast a) {
LOG_Z3_is_app(c, a);
RESET_ERROR_CODE();
return is_app(reinterpret_cast<ast*>(a));
}
Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a) {
LOG_Z3_to_app(c, a);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
SASSERT(is_app(reinterpret_cast<ast*>(a)));
RETURN_Z3(of_app(reinterpret_cast<app*>(a)));
}
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a) {
LOG_Z3_to_func_decl(c, a);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
SASSERT(is_func_decl(reinterpret_cast<ast*>(a)));
RETURN_Z3(of_func_decl(reinterpret_cast<func_decl*>(a)));
}
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a) {
LOG_Z3_get_app_decl(c, a);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
if (!is_app(reinterpret_cast<ast*>(a))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
RETURN_Z3(of_func_decl(to_app(a)->get_decl()));
}
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a) {
LOG_Z3_get_app_num_args(c, a);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
return to_app(a)->get_num_args();
}
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i) {
LOG_Z3_get_app_arg(c, a, i);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
if (!is_app(reinterpret_cast<ast*>(a))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
@ -381,10 +381,10 @@ extern "C" {
}
RETURN_Z3(of_ast(to_app(a)->get_arg(i)));
}
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d) {
LOG_Z3_get_decl_name(c, d);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
return of_symbol(to_func_decl(d)->get_name());
}
@ -419,10 +419,10 @@ extern "C" {
return Z3_PARAMETER_SORT;
}
if (p.is_ast() && is_expr(p.get_ast())) {
return Z3_PARAMETER_AST;
return Z3_PARAMETER_AST;
}
SASSERT(p.is_ast() && is_func_decl(p.get_ast()));
return Z3_PARAMETER_FUNC_DECL;
return Z3_PARAMETER_FUNC_DECL;
Z3_CATCH_RETURN(Z3_PARAMETER_INT);
}
@ -433,13 +433,13 @@ extern "C" {
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB);
return 0;
}
}
parameter const& p = to_func_decl(d)->get_parameters()[idx];
if (!p.is_int()) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return p.get_int();
return p.get_int();
Z3_CATCH_RETURN(0);
}
@ -450,13 +450,13 @@ extern "C" {
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB);
return 0;
}
}
parameter const& p = to_func_decl(d)->get_parameters()[idx];
if (!p.is_double()) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return p.get_double();
return p.get_double();
Z3_CATCH_RETURN(0.0);
}
@ -467,13 +467,13 @@ extern "C" {
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB);
return 0;
}
}
parameter const& p = to_func_decl(d)->get_parameters()[idx];
if (!p.is_symbol()) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return of_symbol(p.get_symbol());
return of_symbol(p.get_symbol());
Z3_CATCH_RETURN(0);
}
@ -484,7 +484,7 @@ extern "C" {
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0);
}
}
parameter const& p = to_func_decl(d)->get_parameters()[idx];
if (!p.is_ast() || !is_sort(p.get_ast())) {
SET_ERROR_CODE(Z3_INVALID_ARG);
@ -501,7 +501,7 @@ extern "C" {
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0);
}
}
parameter const& p = to_func_decl(d)->get_parameters()[idx];
if (!p.is_ast()) {
SET_ERROR_CODE(Z3_INVALID_ARG);
@ -518,7 +518,7 @@ extern "C" {
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0);
}
}
parameter const& p = to_func_decl(d)->get_parameters()[idx];
if (!p.is_ast() || !is_func_decl(p.get_ast())) {
SET_ERROR_CODE(Z3_INVALID_ARG);
@ -535,7 +535,7 @@ extern "C" {
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB);
return "";
}
}
parameter const& p = to_func_decl(d)->get_parameters()[idx];
if (!p.is_rational()) {
SET_ERROR_CODE(Z3_INVALID_ARG);
@ -545,28 +545,28 @@ extern "C" {
Z3_CATCH_RETURN("");
}
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort t) {
Z3_TRY;
LOG_Z3_get_sort_name(c, t);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
return of_symbol(to_sort(t)->get_name());
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_get_sort(c, a);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
Z3_sort r = of_sort(mk_c(c)->m().get_sort(to_expr(a)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d) {
Z3_TRY;
LOG_Z3_get_arity(c, d);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
return to_func_decl(d)->get_arity();
Z3_CATCH_RETURN(0);
}
@ -574,15 +574,15 @@ extern "C" {
unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d) {
Z3_TRY;
LOG_Z3_get_domain_size(c, d);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
return to_func_decl(d)->get_arity();
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i) {
Z3_TRY;
LOG_Z3_get_domain(c, d, i);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
if (i >= to_func_decl(d)->get_arity()) {
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0);
@ -591,20 +591,20 @@ extern "C" {
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d) {
Z3_TRY;
LOG_Z3_get_range(c, d);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
Z3_sort r = of_sort(to_func_decl(d)->get_range());
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_sort_kind Z3_get_sort_kind(Z3_context c, Z3_sort t) {
LOG_Z3_get_sort_kind(c, t);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
CHECK_VALID_AST(t, Z3_UNKNOWN_SORT);
family_id fid = to_sort(t)->get_family_id();
decl_kind k = to_sort(t)->get_decl_kind();
@ -685,19 +685,19 @@ extern "C" {
}
}
mk_c(c)->save_ast_trail(result);
return of_ast(result.get());
return of_ast(result.get());
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast _a) {
LOG_Z3_simplify(c, _a);
RETURN_Z3(simplify(c, _a, 0));
}
}
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast _a, Z3_params p) {
LOG_Z3_simplify_ex(c, _a, p);
RETURN_Z3(simplify(c, _a, p));
}
}
Z3_string Z3_API Z3_simplify_get_help(Z3_context c) {
Z3_TRY;
@ -752,16 +752,16 @@ extern "C" {
}
default:
break;
}
}
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_substitute(Z3_context c,
Z3_ast _a,
unsigned num_exprs,
Z3_ast const _from[],
Z3_ast Z3_API Z3_substitute(Z3_context c,
Z3_ast _a,
unsigned num_exprs,
Z3_ast const _from[],
Z3_ast const _to[]) {
Z3_TRY;
LOG_Z3_substitute(c, _a, num_exprs, _from, _to);
@ -789,9 +789,9 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_substitute_vars(Z3_context c,
Z3_ast _a,
unsigned num_exprs,
Z3_ast Z3_API Z3_substitute_vars(Z3_context c,
Z3_ast _a,
unsigned num_exprs,
Z3_ast const _to[]) {
Z3_TRY;
LOG_Z3_substitute_vars(c, _a, num_exprs, _to);
@ -858,7 +858,7 @@ extern "C" {
return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(f));
}
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c,
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c,
Z3_string name,
Z3_string logic,
Z3_string status,
@ -889,7 +889,7 @@ extern "C" {
return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN("");
}
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d) {
Z3_TRY;
LOG_Z3_get_decl_kind(c, d);
@ -917,43 +917,43 @@ extern "C" {
case PR_UNDEF: return Z3_OP_PR_UNDEF;
case PR_TRUE: return Z3_OP_PR_TRUE;
case PR_ASSERTED: return Z3_OP_PR_ASSERTED;
case PR_GOAL: return Z3_OP_PR_GOAL;
case PR_MODUS_PONENS: return Z3_OP_PR_MODUS_PONENS;
case PR_REFLEXIVITY: return Z3_OP_PR_REFLEXIVITY;
case PR_SYMMETRY: return Z3_OP_PR_SYMMETRY;
case PR_TRANSITIVITY: return Z3_OP_PR_TRANSITIVITY;
case PR_TRANSITIVITY_STAR: return Z3_OP_PR_TRANSITIVITY_STAR;
case PR_MONOTONICITY: return Z3_OP_PR_MONOTONICITY;
case PR_ASSERTED: return Z3_OP_PR_ASSERTED;
case PR_GOAL: return Z3_OP_PR_GOAL;
case PR_MODUS_PONENS: return Z3_OP_PR_MODUS_PONENS;
case PR_REFLEXIVITY: return Z3_OP_PR_REFLEXIVITY;
case PR_SYMMETRY: return Z3_OP_PR_SYMMETRY;
case PR_TRANSITIVITY: return Z3_OP_PR_TRANSITIVITY;
case PR_TRANSITIVITY_STAR: return Z3_OP_PR_TRANSITIVITY_STAR;
case PR_MONOTONICITY: return Z3_OP_PR_MONOTONICITY;
case PR_QUANT_INTRO: return Z3_OP_PR_QUANT_INTRO;
case PR_DISTRIBUTIVITY: return Z3_OP_PR_DISTRIBUTIVITY;
case PR_AND_ELIM: return Z3_OP_PR_AND_ELIM;
case PR_NOT_OR_ELIM: return Z3_OP_PR_NOT_OR_ELIM;
case PR_REWRITE: return Z3_OP_PR_REWRITE;
case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR;
case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT;
case PR_PULL_QUANT_STAR: return Z3_OP_PR_PULL_QUANT_STAR;
case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT;
case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS;
case PR_DER: return Z3_OP_PR_DER;
case PR_DISTRIBUTIVITY: return Z3_OP_PR_DISTRIBUTIVITY;
case PR_AND_ELIM: return Z3_OP_PR_AND_ELIM;
case PR_NOT_OR_ELIM: return Z3_OP_PR_NOT_OR_ELIM;
case PR_REWRITE: return Z3_OP_PR_REWRITE;
case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR;
case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT;
case PR_PULL_QUANT_STAR: return Z3_OP_PR_PULL_QUANT_STAR;
case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT;
case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS;
case PR_DER: return Z3_OP_PR_DER;
case PR_QUANT_INST: return Z3_OP_PR_QUANT_INST;
case PR_HYPOTHESIS: return Z3_OP_PR_HYPOTHESIS;
case PR_LEMMA: return Z3_OP_PR_LEMMA;
case PR_UNIT_RESOLUTION: return Z3_OP_PR_UNIT_RESOLUTION;
case PR_IFF_TRUE: return Z3_OP_PR_IFF_TRUE;
case PR_IFF_FALSE: return Z3_OP_PR_IFF_FALSE;
case PR_COMMUTATIVITY: return Z3_OP_PR_COMMUTATIVITY;
case PR_HYPOTHESIS: return Z3_OP_PR_HYPOTHESIS;
case PR_LEMMA: return Z3_OP_PR_LEMMA;
case PR_UNIT_RESOLUTION: return Z3_OP_PR_UNIT_RESOLUTION;
case PR_IFF_TRUE: return Z3_OP_PR_IFF_TRUE;
case PR_IFF_FALSE: return Z3_OP_PR_IFF_FALSE;
case PR_COMMUTATIVITY: return Z3_OP_PR_COMMUTATIVITY;
case PR_DEF_AXIOM: return Z3_OP_PR_DEF_AXIOM;
case PR_DEF_INTRO: return Z3_OP_PR_DEF_INTRO;
case PR_APPLY_DEF: return Z3_OP_PR_APPLY_DEF;
case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
case PR_NNF_POS: return Z3_OP_PR_NNF_POS;
case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG;
case PR_NNF_STAR: return Z3_OP_PR_NNF_STAR;
case PR_SKOLEMIZE: return Z3_OP_PR_SKOLEMIZE;
case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR;
case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
case PR_DEF_INTRO: return Z3_OP_PR_DEF_INTRO;
case PR_APPLY_DEF: return Z3_OP_PR_APPLY_DEF;
case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
case PR_NNF_POS: return Z3_OP_PR_NNF_POS;
case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG;
case PR_NNF_STAR: return Z3_OP_PR_NNF_STAR;
case PR_SKOLEMIZE: return Z3_OP_PR_SKOLEMIZE;
case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR;
case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;
default:
UNREACHABLE();
@ -1013,7 +1013,7 @@ extern "C" {
case OP_BNEG: return Z3_OP_BNEG;
case OP_BADD: return Z3_OP_BADD;
case OP_BSUB: return Z3_OP_BSUB;
case OP_BMUL: return Z3_OP_BMUL;
case OP_BMUL: return Z3_OP_BMUL;
case OP_BSDIV: return Z3_OP_BSDIV;
case OP_BUDIV: return Z3_OP_BUDIV;
case OP_BSREM: return Z3_OP_BSREM;
@ -1023,7 +1023,7 @@ extern "C" {
case OP_BUDIV0: return Z3_OP_BUDIV0;
case OP_BSREM0: return Z3_OP_BUREM0;
case OP_BUREM0: return Z3_OP_BUREM0;
case OP_BSMOD0: return Z3_OP_BSMOD0;
case OP_BSMOD0: return Z3_OP_BSMOD0;
case OP_ULEQ: return Z3_OP_ULEQ;
case OP_SLEQ: return Z3_OP_SLEQ;
case OP_UGEQ: return Z3_OP_UGEQ;
@ -1058,7 +1058,7 @@ 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_BSMUL_NO_OVFL:
case OP_BSMUL_NO_OVFL:
case OP_BUMUL_NO_OVFL:
case OP_BSMUL_NO_UDFL:
case OP_BSDIV_I:
@ -1098,13 +1098,14 @@ extern "C" {
case datalog::OP_RA_COMPLEMENT: return Z3_OP_RA_COMPLEMENT;
case datalog::OP_RA_SELECT: return Z3_OP_RA_SELECT;
case datalog::OP_RA_CLONE: return Z3_OP_RA_CLONE;
case datalog::OP_DL_CONSTANT: return Z3_OP_FD_CONSTANT;
case datalog::OP_DL_LT: return Z3_OP_FD_LT;
default:
UNREACHABLE();
return Z3_OP_UNINTERPRETED;
}
}
if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) {
switch (_d->get_decl_kind()) {
case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;
@ -1167,7 +1168,7 @@ extern "C" {
case OP_LABEL_LIT: return Z3_OP_LABEL_LIT;
default:
UNREACHABLE();
return Z3_OP_UNINTERPRETED;
return Z3_OP_UNINTERPRETED;
}
}
@ -1180,7 +1181,7 @@ extern "C" {
}
}
return Z3_OP_UNINTERPRETED;
return Z3_OP_UNINTERPRETED;
Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED);
}
@ -1191,14 +1192,14 @@ extern "C" {
ast* _a = reinterpret_cast<ast*>(a);
if (!_a || _a->get_kind() != AST_VAR) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
return 0;
}
var* va = to_var(_a);
if (va) {
return va->get_idx();
}
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
return 0;
Z3_CATCH_RETURN(0);
}
@ -1212,7 +1213,7 @@ extern "C" {
RETURN_Z3(0);
}
SASSERT(mk_c(c)->m().contains(to_ast(a)));
ast_translation translator(mk_c(c)->m(), mk_c(target)->m());
ast_translation translator(mk_c(c)->m(), mk_c(target)->m());
ast * _result = translator(to_ast(a));
mk_c(target)->save_ast_trail(_result);
RETURN_Z3(of_ast(_result));

37
src/api/api_numeral.cpp
View file

@ -28,7 +28,7 @@ Revision History:
bool is_numeral_sort(Z3_context c, Z3_sort ty) {
sort * _ty = to_sort(ty);
family_id fid = _ty->get_family_id();
if (fid != mk_c(c)->get_arith_fid() &&
if (fid != mk_c(c)->get_arith_fid() &&
fid != mk_c(c)->get_bv_fid() &&
fid != mk_c(c)->get_datalog_fid() &&
fid != mk_c(c)->get_fpa_fid()) {
@ -149,7 +149,8 @@ extern "C" {
mk_c(c)->autil().is_numeral(e) ||
mk_c(c)->bvutil().is_numeral(e) ||
mk_c(c)->fpautil().is_numeral(e) ||
mk_c(c)->fpautil().is_rm_numeral(e);
mk_c(c)->fpautil().is_rm_numeral(e) ||
mk_c(c)->datalog_util().is_numeral_ext(e);
Z3_CATCH_RETURN(Z3_FALSE);
}
@ -160,7 +161,7 @@ extern "C" {
expr* e = to_expr(a);
if (!e) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return Z3_FALSE;
return Z3_FALSE;
}
if (mk_c(c)->autil().is_numeral(e, r)) {
return Z3_TRUE;
@ -174,11 +175,11 @@ extern "C" {
r = rational(v, rational::ui64());
return Z3_TRUE;
}
return Z3_FALSE;
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a) {
Z3_TRY;
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
@ -196,11 +197,11 @@ extern "C" {
mpf_rounding_mode rm;
if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) {
switch (rm) {
case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
return mk_c(c)->mk_external_string("roundNearestTiesToEven");
case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
return mk_c(c)->mk_external_string("roundNearestTiesToEven");
break;
case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
return mk_c(c)->mk_external_string("roundNearestTiesToAway");
return mk_c(c)->mk_external_string("roundNearestTiesToAway");
break;
case OP_FPA_RM_TOWARD_POSITIVE:
return mk_c(c)->mk_external_string("roundTowardPositive");
@ -212,7 +213,7 @@ extern "C" {
default:
return mk_c(c)->mk_external_string("roundTowardZero");
break;
}
}
}
else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) {
return mk_c(c)->mk_external_string(fu.fm().to_string(tmp));
@ -261,7 +262,7 @@ extern "C" {
Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, long long* num, long long* den) {
Z3_TRY;
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_small(c, a, num, den);
RESET_ERROR_CODE();
rational r;
@ -289,8 +290,8 @@ extern "C" {
// This function invokes Z3_get_numeral_int64, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_int(c, v, i);
RESET_ERROR_CODE();
if (!i) {
SET_ERROR_CODE(Z3_INVALID_ARG);
if (!i) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return Z3_FALSE;
}
long long l;
@ -301,17 +302,17 @@ extern "C" {
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u) {
Z3_TRY;
// This function invokes Z3_get_numeral_uint64, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_uint(c, v, u);
RESET_ERROR_CODE();
if (!u) {
SET_ERROR_CODE(Z3_INVALID_ARG);
if (!u) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return Z3_FALSE;
}
unsigned long long l;
unsigned long long l;
if (Z3_get_numeral_uint64(c, v, &l) && (l <= 0xFFFFFFFF)) {
*u = static_cast<unsigned>(l);
return Z3_TRUE;
@ -319,7 +320,7 @@ extern "C" {
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned long long* u) {
Z3_TRY;
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
@ -339,7 +340,7 @@ extern "C" {
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, long long* i) {
Z3_TRY;
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.

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

@ -309,7 +309,7 @@ namespace Microsoft.Z3
/// <summary>
/// Create a new finite domain sort.
/// <returns>The result is a sort</returns>
/// <returns>The result is a sort</returns>
/// </summary>
/// <param name="name">The name used to identify the sort</param>
/// <param name="size">The size of the sort</param>
@ -324,9 +324,9 @@ namespace Microsoft.Z3
/// <summary>
/// Create a new finite domain sort.
/// <returns>The result is a sort</returns>
/// Elements of the sort are created using <seealso cref="MkNumeral(ulong, Sort)"/>,
/// and the elements range from 0 to <tt>size-1</tt>.
/// <returns>The result is a sort</returns>
/// Elements of the sort are created using <seealso cref="MkNumeral(ulong, Sort)"/>,
/// and the elements range from 0 to <tt>size-1</tt>.
/// </summary>
/// <param name="name">The name used to identify the sort</param>
/// <param name="size">The size of the sort</param>
@ -457,16 +457,16 @@ namespace Microsoft.Z3
/// <summary>
/// Update a datatype field at expression t with value v.
/// The function performs a record update at t. The field
/// that is passed in as argument is updated with value v,
/// the remainig fields of t are unchanged.
/// </summary>
public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
{
return Expr.Create(this, Native.Z3_datatype_update_field(
nCtx, field.NativeObject,
t.NativeObject, v.NativeObject));
}
/// The function performs a record update at t. The field
/// that is passed in as argument is updated with value v,
/// the remainig fields of t are unchanged.
/// </summary>
public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
{
return Expr.Create(this, Native.Z3_datatype_update_field(
nCtx, field.NativeObject,
t.NativeObject, v.NativeObject));
}
#endregion
#endregion
@ -2613,13 +2613,13 @@ namespace Microsoft.Z3
/// <paramref name="patterns"/> is an array of patterns, <paramref name="sorts"/> is an array
/// with the sorts of the bound variables, <paramref name="names"/> is an array with the
/// 'names' of the bound variables, and <paramref name="body"/> is the body of the
/// quantifier. Quantifiers are associated with weights indicating the importance of
/// quantifier. Quantifiers are associated with weights indicating the importance of
/// using the quantifier during instantiation.
/// Note that the bound variables are de-Bruijn indices created using <see cref="MkBound"/>.
/// Z3 applies the convention that the last element in <paramref name="names"/> and
/// <paramref name="sorts"/> refers to the variable with index 0, the second to last element
/// of <paramref name="names"/> and <paramref name="sorts"/> refers to the variable
/// with index 1, etc.
/// Note that the bound variables are de-Bruijn indices created using <see cref="MkBound"/>.
/// Z3 applies the convention that the last element in <paramref name="names"/> and
/// <paramref name="sorts"/> refers to the variable with index 0, the second to last element
/// of <paramref name="names"/> and <paramref name="sorts"/> refers to the variable
/// with index 1, etc.
/// </remarks>
/// <param name="sorts">the sorts of the bound variables.</param>
/// <param name="names">names of the bound variables</param>
@ -2650,8 +2650,8 @@ namespace Microsoft.Z3
/// Create a universal Quantifier.
/// </summary>
/// <remarks>
/// Creates a universal quantifier using a list of constants that will
/// form the set of bound variables.
/// Creates a universal quantifier using a list of constants that will
/// form the set of bound variables.
/// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
/// </remarks>
public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
@ -2670,7 +2670,7 @@ namespace Microsoft.Z3
/// Create an existential Quantifier.
/// </summary>
/// <remarks>
/// Creates an existential quantifier using de-Brujin indexed variables.
/// Creates an existential quantifier using de-Brujin indexed variables.
/// (<see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>).
/// </remarks>
public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
@ -2692,8 +2692,8 @@ namespace Microsoft.Z3
/// Create an existential Quantifier.
/// </summary>
/// <remarks>
/// Creates an existential quantifier using a list of constants that will
/// form the set of bound variables.
/// Creates an existential quantifier using a list of constants that will
/// form the set of bound variables.
/// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
/// </remarks>
public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
@ -4499,7 +4499,7 @@ namespace Microsoft.Z3
readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10);
readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10);
/// <summary>
/// AST DRQ

186
src/api/dotnet/Expr.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-20
Notes:
--*/
using System;
@ -23,7 +23,7 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Expressions are terms.
/// Expressions are terms.
/// </summary>
[ContractVerification(true)]
public class Expr : AST
@ -74,7 +74,7 @@ namespace Microsoft.Z3
/// <summary>
/// The arguments of the expression.
/// </summary>
/// </summary>
public Expr[] Args
{
get
@ -109,9 +109,9 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// The result is the new expression. The arrays <c>from</c> and <c>to</c> must have size <c>num_exprs</c>.
/// For every <c>i</c> smaller than <c>num_exprs</c>, we must have that
/// For every <c>i</c> smaller than <c>num_exprs</c>, we must have that
/// sort of <c>from[i]</c> must be equal to sort of <c>to[i]</c>.
/// </remarks>
/// </remarks>
public Expr Substitute(Expr[] from, Expr[] to)
{
Contract.Requires(from != null);
@ -174,7 +174,7 @@ namespace Microsoft.Z3
/// <summary>
/// Returns a string representation of the expression.
/// </summary>
/// </summary>
public override string ToString()
{
return base.ToString();
@ -442,15 +442,15 @@ namespace Microsoft.Z3
get
{
return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
(Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
(Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
== Z3_sort_kind.Z3_ARRAY_SORT);
}
}
/// <summary>
/// Indicates whether the term is an array store.
/// Indicates whether the term is an array store.
/// </summary>
/// <remarks>It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j).
/// <remarks>It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j).
/// Array store takes at least 3 arguments. </remarks>
public bool IsStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
@ -480,7 +480,7 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is an as-array term.
/// </summary>
/// <remarks>An as-array term is n array value that behaves as the function graph of the
/// <remarks>An as-array term is n array value that behaves as the function graph of the
/// function passed as parameter.</remarks>
public bool IsAsArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
#endregion
@ -761,21 +761,21 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is a coercion from integer to bit-vector
/// </summary>
/// <remarks>This function is not supported by the decision procedures. Only the most
/// <remarks>This function is not supported by the decision procedures. Only the most
/// rudimentary simplification rules are applied to this function.</remarks>
public bool IsIntToBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
/// <summary>
/// Indicates whether the term is a coercion from bit-vector to integer
/// </summary>
/// <remarks>This function is not supported by the decision procedures. Only the most
/// <remarks>This function is not supported by the decision procedures. Only the most
/// rudimentary simplification rules are applied to this function.</remarks>
public bool IsBVToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
/// <summary>
/// Indicates whether the term is a bit-vector carry
/// </summary>
/// <remarks>Compute the carry bit in a full-adder. The meaning is given by the
/// <remarks>Compute the carry bit in a full-adder. The meaning is given by the
/// equivalence (carry l1 l2 l3) &lt;=&gt; (or (and l1 l2) (and l1 l3) (and l2 l3)))</remarks>
public bool IsBVCarry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
@ -795,15 +795,15 @@ namespace Microsoft.Z3
public bool IsLabel { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
/// <summary>
/// Indicates whether the term is a label literal (used by the Boogie Verification condition generator).
/// Indicates whether the term is a label literal (used by the Boogie Verification condition generator).
/// </summary>
/// <remarks>A label literal has a set of string parameters. It takes no arguments.</remarks>
public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
#endregion
#endregion
#region Proof Terms
/// <summary>
/// Indicates whether the term is a binary equivalence modulo namings.
/// Indicates whether the term is a binary equivalence modulo namings.
/// </summary>
/// <remarks>This binary predicate is used in proof terms.
/// It captures equisatisfiability and equivalence modulo renamings.</remarks>
@ -838,8 +838,8 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
/// </summary>
/// <remarks>This proof object has no antecedents.
/// The only reflexive relations that are used are
/// <remarks>This proof object has no antecedents.
/// The only reflexive relations that are used are
/// equivalence modulo namings, equality and equivalence.
/// That is, R is either '~', '=' or 'iff'.</remarks>
public bool IsProofReflexivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
@ -859,8 +859,8 @@ namespace Microsoft.Z3
/// Indicates whether the term is a proof by transitivity of a relation
/// </summary>
/// <remarks>
/// Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof
/// for (R t u).
/// Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof
/// for (R t u).
/// T1: (R t s)
/// T2: (R s u)
/// [trans T1 T2]: (R t u)
@ -872,17 +872,17 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
/// It combines several symmetry and transitivity proofs.
/// It combines several symmetry and transitivity proofs.
/// Example:
/// T1: (R a b)
/// T2: (R c b)
/// T3: (R c d)
/// [trans* T1 T2 T3]: (R a d)
/// [trans* T1 T2 T3]: (R a d)
/// R must be a symmetric and transitive relation.
///
///
/// Assuming that this proof object is a proof for (R s t), then
/// a proof checker must check if it is possible to prove (R s t)
/// using the antecedents, symmetry and transitivity. That is,
/// using the antecedents, symmetry and transitivity. That is,
/// if there is a path from s to t, if we view every
/// antecedent (R a b) as an edge between a and b.
/// </remarks>
@ -896,14 +896,14 @@ namespace Microsoft.Z3
/// T1: (R t_1 s_1)
/// ...
/// Tn: (R t_n s_n)
/// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
/// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
/// Remark: if t_i == s_i, then the antecedent Ti is suppressed.
/// That is, reflexivity proofs are supressed to save space.
/// </remarks>
public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
/// <summary>
/// Indicates whether the term is a quant-intro proof
/// Indicates whether the term is a quant-intro proof
/// </summary>
/// <remarks>
/// Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
@ -913,7 +913,7 @@ namespace Microsoft.Z3
public bool IsProofQuantIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
/// <summary>
/// Indicates whether the term is a distributivity proof object.
/// Indicates whether the term is a distributivity proof object.
/// </summary>
/// <remarks>
/// Given that f (= or) distributes over g (= and), produces a proof for
@ -923,9 +923,9 @@ namespace Microsoft.Z3
/// (= (f (g a b) (g c d))
/// (g (f a c) (f a d) (f b c) (f b d)))
/// where each f and g can have arbitrary number of arguments.
///
///
/// This proof object has no antecedents.
/// Remark. This rule is used by the CNF conversion pass and
/// Remark. This rule is used by the CNF conversion pass and
/// instantiated by f = or, and g = and.
/// </remarks>
public bool IsProofDistributivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
@ -946,7 +946,7 @@ namespace Microsoft.Z3
/// <remarks>
/// Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
/// T1: (not (or l_1 ... l_n))
/// [not-or-elim T1]: (not l_i)
/// [not-or-elim T1]: (not l_i)
/// </remarks>
public bool IsProofOrElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
@ -956,16 +956,16 @@ namespace Microsoft.Z3
/// <remarks>
/// A proof for a local rewriting step (= t s).
/// The head function symbol of t is interpreted.
///
///
/// This proof object has no antecedents.
/// The conclusion of a rewrite rule is either an equality (= t s),
/// The conclusion of a rewrite rule is either an equality (= t s),
/// an equivalence (iff t s), or equi-satisfiability (~ t s).
/// Remark: if f is bool, then = is iff.
///
///
/// Examples:
/// (= (+ x 0) x)
/// (= (+ x 1 2) (+ 3 x))
/// (iff (or x false) x)
/// (iff (or x false) x)
/// </remarks>
public bool IsProofRewrite { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
@ -997,8 +997,8 @@ namespace Microsoft.Z3
/// Indicates whether the term is a proof for pulling quantifiers out.
/// </summary>
/// <remarks>
/// A proof for (iff P Q) where Q is in prenex normal form.
/// This proof object is only used if the parameter PROOF_MODE is 1.
/// A proof for (iff P Q) where Q is in prenex normal form.
/// This proof object is only used if the parameter PROOF_MODE is 1.
/// This proof object has no antecedents
/// </remarks>
public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
@ -1010,8 +1010,8 @@ namespace Microsoft.Z3
/// A proof for:
/// (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m]))
/// (and (forall (x_1 ... x_m) p_1[x_1 ... x_m])
/// ...
/// (forall (x_1 ... x_m) p_n[x_1 ... x_m])))
/// ...
/// (forall (x_1 ... x_m) p_n[x_1 ... x_m])))
/// This proof object has no antecedents
/// </remarks>
public bool IsProofPushQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
@ -1021,8 +1021,8 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n])
/// (forall (x_1 ... x_n) p[x_1 ... x_n]))
///
/// (forall (x_1 ... x_n) p[x_1 ... x_n]))
///
/// It is used to justify the elimination of unused variables.
/// This proof object has no antecedents.
/// </remarks>
@ -1035,9 +1035,9 @@ namespace Microsoft.Z3
/// A proof for destructive equality resolution:
/// (iff (forall (x) (or (not (= x t)) P[x])) P[t])
/// if x does not occur in t.
///
///
/// This proof object has no antecedents.
///
///
/// Several variables can be eliminated simultaneously.
/// </remarks>
public bool IsProofDER { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
@ -1062,7 +1062,7 @@ namespace Microsoft.Z3
/// <remarks>
/// T1: false
/// [lemma T1]: (or (not l_1) ... (not l_n))
///
///
/// This proof object has one antecedent: a hypothetical proof for false.
/// It converts the proof in a proof for (or (not l_1) ... (not l_n)),
/// when T1 contains the hypotheses: l_1, ..., l_n.
@ -1104,9 +1104,9 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// [comm]: (= (f a b) (f b a))
///
///
/// f is a commutative operator.
///
///
/// This proof object has no antecedents.
/// Remark: if f is bool, then = is iff.
/// </remarks>
@ -1117,7 +1117,7 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// Proof object used to justify Tseitin's like axioms:
///
///
/// (or (not (and p q)) p)
/// (or (not (and p q)) q)
/// (or (not (and p q r)) p)
@ -1138,7 +1138,7 @@ namespace Microsoft.Z3
/// (or (ite a b c) a (not c))
/// (or (not (not a)) (not a))
/// (or (not a) a)
///
///
/// This proof object has no antecedents.
/// Note: all axioms are propositional tautologies.
/// Note also that 'and' and 'or' can take multiple arguments.
@ -1155,19 +1155,19 @@ namespace Microsoft.Z3
/// Introduces a name for a formula/term.
/// Suppose e is an expression with free variables x, and def-intro
/// introduces the name n(x). The possible cases are:
///
///
/// When e is of Boolean type:
/// [def-intro]: (and (or n (not e)) (or (not n) e))
///
///
/// or:
/// [def-intro]: (or (not n) e)
/// when e only occurs positively.
///
///
/// When e is of the form (ite cond th el):
/// [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))
///
///
/// Otherwise:
/// [def-intro]: (= n e)
/// [def-intro]: (= n e)
/// </remarks>
public bool IsProofDefIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
@ -1195,7 +1195,7 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// Proof for a (positive) NNF step. Example:
///
///
/// T1: (not s_1) ~ r_1
/// T2: (not s_2) ~ r_2
/// T3: s_1 ~ r_1'
@ -1207,9 +1207,9 @@ namespace Microsoft.Z3
/// (a) When creating the NNF of a positive force quantifier.
/// The quantifier is retained (unless the bound variables are eliminated).
/// Example
/// T1: q ~ q_new
/// T1: q ~ q_new
/// [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
///
///
/// (b) When recursively creating NNF over Boolean formulas, where the top-level
/// connective is changed during NNF conversion. The relevant Boolean connectives
/// for NNF_POS are 'implies', 'iff', 'xor', 'ite'.
@ -1223,7 +1223,7 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// Proof for a (negative) NNF step. Examples:
///
///
/// T1: (not s_1) ~ r_1
/// ...
/// Tn: (not s_n) ~ r_n
@ -1248,9 +1248,9 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// A proof for (~ P Q) where Q is in negation normal form.
///
/// This proof object is only used if the parameter PROOF_MODE is 1.
///
///
/// This proof object is only used if the parameter PROOF_MODE is 1.
///
/// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
/// </remarks>
public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
@ -1260,8 +1260,8 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// A proof for (~ P Q) where Q is in conjunctive normal form.
/// This proof object is only used if the parameter PROOF_MODE is 1.
/// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
/// This proof object is only used if the parameter PROOF_MODE is 1.
/// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
/// </remarks>
public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
@ -1269,11 +1269,11 @@ namespace Microsoft.Z3
/// Indicates whether the term is a proof for a Skolemization step
/// </summary>
/// <remarks>
/// Proof for:
///
/// Proof for:
///
/// [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y)))
/// [sk]: (~ (exists x (p x y)) (p (sk y) y))
///
///
/// This proof object has no antecedents.
/// </remarks>
public bool IsProofSkolemize { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
@ -1285,7 +1285,7 @@ namespace Microsoft.Z3
/// Modus ponens style rule for equi-satisfiability.
/// T1: p
/// T2: (~ p q)
/// [mp~ T1 T2]: q
/// [mp~ T1 T2]: q
/// </remarks>
public bool IsProofModusPonensOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
@ -1294,15 +1294,15 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// Generic proof for theory lemmas.
///
///
/// The theory lemma function comes with one or more parameters.
/// The first parameter indicates the name of the theory.
/// For the theory of arithmetic, additional parameters provide hints for
/// checking the theory lemma.
/// checking the theory lemma.
/// The hints for arithmetic are:
/// - farkas - followed by rational coefficients. Multiply the coefficients to the
/// inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
/// - triangle-eq - Indicates a lemma related to the equivalence:
/// - triangle-eq - Indicates a lemma related to the equivalence:
/// (iff (= t1 t2) (and (&lt;= t1 t2) (&lt;= t2 t1)))
/// - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
/// </remarks>
@ -1318,7 +1318,7 @@ namespace Microsoft.Z3
get
{
return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
== (uint)Z3_sort_kind.Z3_RELATION_SORT);
}
}
@ -1328,7 +1328,7 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// Insert a record into a relation.
/// The function takes <c>n+1</c> arguments, where the first argument is the relation and the remaining <c>n</c> elements
/// The function takes <c>n+1</c> arguments, where the first argument is the relation and the remaining <c>n</c> elements
/// correspond to the <c>n</c> columns of the relation.
/// </remarks>
public bool IsRelationStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
@ -1349,7 +1349,7 @@ namespace Microsoft.Z3
public bool IsRelationalJoin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
/// <summary>
/// Indicates whether the term is the union or convex hull of two relations.
/// Indicates whether the term is the union or convex hull of two relations.
/// </summary>
/// <remarks>The function takes two arguments.</remarks>
public bool IsRelationUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
@ -1371,7 +1371,7 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// Filter (restrict) a relation with respect to a predicate.
/// The first argument is a relation.
/// The first argument is a relation.
/// The second argument is a predicate with free de-Brujin indices
/// corresponding to the columns of the relation.
/// So the first column in the relation has index 0.
@ -1385,9 +1385,9 @@ namespace Microsoft.Z3
/// Intersect the first relation with respect to negation
/// of the second relation (the function takes two arguments).
/// Logically, the specification can be described by a function
///
///
/// target = filter_by_negation(pos, neg, columns)
///
///
/// where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that
/// target are elements in x in pos, such that there is no y in neg that agrees with
/// x on the columns c1, d1, .., cN, dN.
@ -1397,7 +1397,7 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is the renaming of a column in a relation
/// </summary>
/// <remarks>
/// <remarks>
/// The function takes one argument.
/// The parameters contain the renaming as a cycle.
/// </remarks>
@ -1422,10 +1422,10 @@ namespace Microsoft.Z3
/// Indicates whether the term is a relational clone (copy)
/// </summary>
/// <remarks>
/// Create a fresh copy (clone) of a relation.
/// Create a fresh copy (clone) of a relation.
/// The function is logically the identity, but
/// in the context of a register machine allows
/// for terms of kind <seealso cref="IsRelationUnion"/>
/// in the context of a register machine allows
/// for terms of kind <seealso cref="IsRelationUnion"/>
/// to perform destructive updates to the first argument.
/// </remarks>
public bool IsRelationClone { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
@ -1481,11 +1481,11 @@ namespace Microsoft.Z3
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
/// </summary>
public bool IsFPRMRoundNearestTiesToEven{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
/// </summary>
public bool IsFPRMRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
public bool IsFPRMRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
@ -1506,11 +1506,11 @@ namespace Microsoft.Z3
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
/// </summary>
public bool IsFPRMExprRNE{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
/// </summary>
public bool IsFPRMExprRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
public bool IsFPRMExprRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
@ -1530,9 +1530,9 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is a floating-point rounding mode numeral
/// </summary>
public bool IsFPRMExpr {
get {
return IsApp &&
public bool IsFPRMExpr {
get {
return IsApp &&
(FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY||
FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN ||
FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE ||
@ -1540,7 +1540,7 @@ namespace Microsoft.Z3
FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO);
}
}
/// <summary>
/// Indicates whether the term is a floating-point +oo
/// </summary>
@ -1586,7 +1586,7 @@ namespace Microsoft.Z3
/// Indicates whether the term is a floating-point multiplication term
/// </summary>
public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }
/// <summary>
/// Indicates whether the term is a floating-point divison term
/// </summary>
@ -1680,12 +1680,12 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is a floating-point isNegative predicate term
/// </summary>
public bool IsFPisNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } }
public bool IsFPisNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } }
/// <summary>
/// Indicates whether the term is a floating-point isPositive predicate term
/// </summary>
public bool IsFPisPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } }
public bool IsFPisPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } }
/// <summary>
/// Indicates whether the term is a floating-point constructor term
@ -1715,7 +1715,7 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is a floating-point conversion to real term
/// </summary>
public bool IsFPToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } }
public bool IsFPToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } }
/// <summary>
@ -1761,8 +1761,8 @@ namespace Microsoft.Z3
#endregion
#region Internal
/// <summary>
/// Constructor for Expr
/// <summary>
/// Constructor for Expr
/// </summary>
internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
@ -1815,6 +1815,7 @@ namespace Microsoft.Z3
case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj);
case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj);
case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainNum(ctx, obj);
}
}
@ -1828,6 +1829,7 @@ namespace Microsoft.Z3
case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj);
case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj);
case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainExpr(ctx, obj);
}
return new Expr(ctx, obj);

38
src/api/dotnet/FiniteDomainExpr.cs Normal file
View file

@ -0,0 +1,38 @@
/*++
Copyright (<c>) 2012 Microsoft Corporation
Module Name:
FiniteDomainExpr.cs
Abstract:
Z3 Managed API: Finite-domain Expressions
Author:
Christoph Wintersteiger (cwinter) 2015-12-02
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Finite-domain expressions
/// </summary>
public class FiniteDomainExpr : Expr
{
#region Internal
/// <summary> Constructor for DatatypeExpr </summary>
internal FiniteDomainExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

115
src/api/dotnet/FiniteDomainNum.cs Normal file
View file

@ -0,0 +1,115 @@
/*++
Copyright (<c>) 2012 Microsoft Corporation
Module Name:
FiniteDomainNum.cs
Abstract:
Z3 Managed API: Finite-domain Numerals
Author:
Christoph Wintersteiger (cwinter) 2015-12-02
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
#if !FRAMEWORK_LT_4
using System.Numerics;
#endif
namespace Microsoft.Z3
{
/// <summary>
/// Finite-domain numerals
/// </summary>
[ContractVerification(true)]
public class FiniteDomainNum : FiniteDomainExpr
{
/// <summary>
/// Retrieve the 64-bit unsigned integer value.
/// </summary>
public UInt64 UInt64
{
get
{
UInt64 res = 0;
if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public int Int
{
get
{
int res = 0;
if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int");
return res;
}
}
/// <summary>
/// Retrieve the 64-bit int value.
/// </summary>
public Int64 Int64
{
get
{
Int64 res = 0;
if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int64");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public uint UInt
{
get
{
uint res = 0;
if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a uint");
return res;
}
}
#if !FRAMEWORK_LT_4
/// <summary>
/// Retrieve the BigInteger value.
/// </summary>
public BigInteger BigInteger
{
get
{
return BigInteger.Parse(this.ToString());
}
}
#endif
/// <summary>
/// Returns a string representation of the numeral.
/// </summary>
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
}
#region Internal
internal FiniteDomainNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#endregion
}
}

2
src/api/dotnet/Microsoft.Z3.csproj
View file

@ -342,6 +342,8 @@
<Compile Include="ConstructorList.cs" />
<Compile Include="DatatypeExpr.cs" />
<Compile Include="DatatypeSort.cs" />
<Compile Include="FiniteDomainExpr.cs" />
<Compile Include="FiniteDomainNum.cs" />
<Compile Include="FPExpr.cs" />
<Compile Include="FPNum.cs" />
<Compile Include="FPRMExpr.cs" />

17
src/api/java/AST.java
View file

@ -22,7 +22,7 @@ import com.microsoft.z3.enumerations.Z3_ast_kind;
/**
* The abstract syntax tree (AST) class.
**/
public class AST extends Z3Object implements Comparable
public class AST extends Z3Object implements Comparable<AST>
{
/**
* Object comparison.
@ -56,23 +56,14 @@ public class AST extends Z3Object implements Comparable
* positive if after else zero.
* @throws Z3Exception on error
**/
public int compareTo(Object other)
public int compareTo(AST other)
{
if (other == null)
return 1;
AST oAST = null;
try
{
oAST = AST.class.cast(other);
} catch (ClassCastException e)
{
return 1;
}
if (getId() < oAST.getId())
if (getId() < other.getId())
return -1;
else if (getId() > oAST.getId())
else if (getId() > other.getId())
return +1;
else
return 0;

4
src/api/java/Expr.java
View file

@ -2165,6 +2165,8 @@ public class Expr extends AST
return new FPNum(ctx, obj);
case Z3_ROUNDING_MODE_SORT:
return new FPRMNum(ctx, obj);
case Z3_FINITE_DOMAIN_SORT:
return new FiniteDomainNum(ctx, obj);
default: ;
}
}
@ -2187,6 +2189,8 @@ public class Expr extends AST
return new FPExpr(ctx, obj);
case Z3_ROUNDING_MODE_SORT:
return new FPRMExpr(ctx, obj);
case Z3_FINITE_DOMAIN_SORT:
return new FiniteDomainExpr(ctx, obj);
default: ;
}

33
src/api/java/FiniteDomainExpr.java Normal file
View file

@ -0,0 +1,33 @@
/**
Copyright (c) 2012-2014 Microsoft Corporation
Module Name:
FiniteDomainExpr.java
Abstract:
Author:
@author Christoph Wintersteiger (cwinter) 2015-12-02
Notes:
**/
package com.microsoft.z3;
/**
* Finite-domain expressions
**/
public class FiniteDomainExpr extends Expr
{
/**
* Constructor for FiniteDomainExpr
* @throws Z3Exception on error
**/
FiniteDomainExpr(Context ctx, long obj)
{
super(ctx, obj);
}
}

76
src/api/java/FiniteDomainNum.java Normal file
View file

@ -0,0 +1,76 @@
/**
Copyright (c) 2012-2014 Microsoft Corporation
Module Name:
FiniteDomainNum.java
Abstract:
Author:
@author Christoph Wintersteiger (cwinter) 2015-12-02
Notes:
**/
package com.microsoft.z3;
import java.math.BigInteger;
/**
* Finite-domain Numerals
**/
public class FiniteDomainNum extends FiniteDomainExpr
{
FiniteDomainNum(Context ctx, long obj)
{
super(ctx, obj);
}
/**
* Retrieve the int value.
**/
public int getInt()
{
Native.IntPtr res = new Native.IntPtr();
if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not an int");
return res.value;
}
/**
* Retrieve the 64-bit int value.
**/
public long getInt64()
{
Native.LongPtr res = new Native.LongPtr();
if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not an int64");
return res.value;
}
/**
* Retrieve the BigInteger value.
**/
public BigInteger getBigInteger()
{
return new BigInteger(this.toString());
}
/**
* Returns a string representation of the numeral.
**/
public String toString()
{
try
{
return Native.getNumeralString(getContext().nCtx(), getNativeObject());
} catch (Z3Exception e)
{
return "Z3Exception: " + e.getMessage();
}
}
}

100
src/api/python/z3.py
View file

@ -912,6 +912,11 @@ def _to_expr_ref(a, ctx):
return FPNumRef(a, ctx)
else:
return FPRef(a, ctx)
if sk == Z3_FINITE_DOMAIN_SORT:
if k == Z3_NUMERAL_AST:
return FiniteDomainNumRef(a, ctx)
else:
return FiniteDomainRef(a, ctx)
if sk == Z3_ROUNDING_MODE_SORT:
return FPRMRef(a, ctx)
return ExprRef(a, ctx)
@ -6395,7 +6400,7 @@ class Fixedpoint(Z3PPObject):
#########################################
#
# Finite domain sorts
# Finite domains
#
#########################################
@ -6412,9 +6417,102 @@ class FiniteDomainSortRef(SortRef):
def FiniteDomainSort(name, sz, ctx=None):
"""Create a named finite domain sort of a given size sz"""
if not isinstance(name, Symbol):
name = to_symbol(name)
ctx = _get_ctx(ctx)
return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
def is_finite_domain_sort(s):
"""Return True if `s` is a Z3 finite-domain sort.
>>> is_finite_domain_sort(FiniteDomainSort('S', 100))
True
>>> is_finite_domain_sort(IntSort())
False
"""
return isinstance(s, FiniteDomainSortRef)
class FiniteDomainRef(ExprRef):
"""Finite-domain expressions."""
def sort(self):
"""Return the sort of the finite-domain expression `self`."""
return FiniteDomainSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
def as_string(self):
"""Return a Z3 floating point expression as a Python string."""
return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
def is_finite_domain(a):
"""Return `True` if `a` is a Z3 finite-domain expression.
>>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s)
>>> is_finite_domain(b)
True
>>> is_finite_domain(Int('x'))
False
"""
return isinstance(a, FiniteDomainRef)
class FiniteDomainNumRef(FiniteDomainRef):
"""Integer values."""
def as_long(self):
"""Return a Z3 finite-domain numeral as a Python long (bignum) numeral.
>>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(3, s)
>>> v
3
>>> v.as_long() + 1
4
"""
return int(self.as_string())
def as_string(self):
"""Return a Z3 finite-domain numeral as a Python string.
>>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(42, s)
>>> v.as_string()
'42'
"""
return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
def FiniteDomainVal(val, sort, ctx=None):
"""Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
>>> s = FiniteDomainSort('S', 256)
>>> FiniteDomainVal(255, s)
255
>>> FiniteDomainVal('100', s)
100
"""
if __debug__:
_z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort" )
ctx = sort.ctx
return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
def is_finite_domain_value(a):
"""Return `True` if `a` is a Z3 finite-domain value.
>>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s)
>>> is_finite_domain_value(b)
False
>>> b = FiniteDomainVal(10, s)
>>> b
10
>>> is_finite_domain_value(b)
True
"""
return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
#########################################
#
# Optimize

5
src/api/python/z3printer.py
View file

@ -573,6 +573,9 @@ class Formatter:
def pp_bv(self, a):
return to_format(a.as_string())
def pp_fd(self, a):
return to_format(a.as_string())
def pp_fprm_value(self, a):
z3._z3_assert(z3.is_fprm_value(a), 'expected FPRMNumRef')
if self.fpa_pretty and (a.decl().kind() in _z3_op_to_fpa_pretty_str):
@ -864,6 +867,8 @@ class Formatter:
return self.pp_algebraic(a)
elif z3.is_bv_value(a):
return self.pp_bv(a)
elif z3.is_finite_domain_value(a):
return self.pp_fd(a)
elif z3.is_fprm_value(a):
return self.pp_fprm_value(a)
elif z3.is_fp_value(a):

1465
src/api/z3_api.h
View file

File diff suppressed because it is too large Load diff