Z3
Deprecated.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Deprecated.cs
7 
8 Abstract:
9 
10  Expose deprecated features for use from the managed API
11  those who use them for experiments.
12 
13 Author:
14 
15  Christoph Wintersteiger (cwinter) 2012-03-15
16 
17 Notes:
18 
19 --*/
20 using System;
21 using System.Collections.Generic;
22 using System.Runtime.InteropServices;
23 using System.Diagnostics.Contracts;
24 
25 namespace Microsoft.Z3
26 {
30  [ContractVerification(true)]
31  public class Deprecated
32  {
33 
38  public static void Push(Context ctx) {
39  Native.Z3_push(ctx.nCtx);
40  }
41 
47  public static void Pop(Context ctx, uint n = 1) {
48  Native.Z3_pop(ctx.nCtx, n);
49  }
50 
54  public static void Assert(Context ctx, params BoolExpr[] constraints)
55  {
56  Contract.Requires(constraints != null);
57  Contract.Requires(Contract.ForAll(constraints, c => c != null));
58 
59  ctx.CheckContextMatch(constraints);
60  foreach (BoolExpr a in constraints)
61  {
62  Native.Z3_assert_cnstr(ctx.nCtx, a.NativeObject);
63  }
64  }
68  public static Status Check(Context ctx, List<BoolExpr> core, ref Model model, ref Expr proof, params Expr[] assumptions)
69  {
70  Z3_lbool r;
71  model = null;
72  proof = null;
73  if (assumptions == null || assumptions.Length == 0)
74  r = (Z3_lbool)Native.Z3_check(ctx.nCtx);
75  else {
76  IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero;
77  uint core_size = 0;
78  IntPtr[] native_core = new IntPtr[assumptions.Length];
79  r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx,
80  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
81  ref mdl, ref prf, ref core_size, native_core);
82 
83  for (uint i = 0; i < core_size; i++)
84  core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
85  if (mdl != IntPtr.Zero) {
86  model = new Model(ctx, mdl);
87  }
88  if (prf != IntPtr.Zero) {
89  proof = Expr.Create(ctx, prf);
90  }
91 
92  }
93  switch (r)
94  {
95  case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
96  case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
97  default: return Status.UNKNOWN;
98  }
99  }
100 
104  public static BoolExpr GetAssignment(Context ctx)
105  {
106  IntPtr x = Native.Z3_get_context_assignment(ctx.nCtx);
107  return (BoolExpr)Expr.Create(ctx, x);
108  }
109 
110  }
111 }
static BoolExpr GetAssignment(Context ctx)
Retrieves an assignment to atomic propositions for a satisfiable context.
Definition: Deprecated.cs:104
The main interaction with Z3 happens via the Context.
Definition: Deprecated.cs:31
using System
static int Z3_check_assumptions(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In, Out] ref Z3_model a3, [In, Out] ref Z3_ast a4, [In, Out] ref uint a5, [Out] Z3_ast[] a6)
Definition: Native.cs:5630
Boolean expressions
Definition: BoolExpr.cs:31
static void Push(Context ctx)
Creates a backtracking point.
Definition: Deprecated.cs:38
Expressions are terms.
Definition: Expr.cs:29
static void Assert(Context ctx, params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Definition: Deprecated.cs:54
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
static void Pop(Context ctx, uint n=1)
Backtracks n backtracking points.
Definition: Deprecated.cs:47
Status
Status values.
Definition: Status.cs:27
static void Z3_pop(Z3_context a0, uint a1)
Definition: Native.cs:5585
static void Z3_push(Z3_context a0)
Definition: Native.cs:5578
static int Z3_check(Z3_context a0)
Definition: Native.cs:5622
static void Z3_assert_cnstr(Z3_context a0, Z3_ast a1)
Definition: Native.cs:5607
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:29
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
static Status Check(Context ctx, List< BoolExpr > core, ref Model model, ref Expr proof, params Expr[] assumptions)
Checks whether the assertions in the context are consistent or not.
Definition: Deprecated.cs:68
The abstract syntax tree (AST) class.
Definition: AST.cs:31
static Z3_ast Z3_get_context_assignment(Z3_context a0)
Definition: Native.cs:5872