Z3
Goal.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
26 public class Goal extends Z3Object {
36  {
37  return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
38  getNativeObject()));
39  }
40 
44  public boolean isPrecise()
45  {
47  }
48 
52  public boolean isUnderApproximation()
53  {
55  }
56 
60  public boolean isOverApproximation()
61  {
63  }
64 
69  public boolean isGarbage()
70  {
72  }
73 
79  public void add(BoolExpr ... constraints)
80  {
81  getContext().checkContextMatch(constraints);
82  for (BoolExpr c : constraints)
83  {
84  Native.goalAssert(getContext().nCtx(), getNativeObject(),
85  c.getNativeObject());
86  }
87  }
88 
92  public boolean inconsistent()
93  {
94  return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
95  }
96 
102  public int getDepth()
103  {
104  return Native.goalDepth(getContext().nCtx(), getNativeObject());
105  }
106 
110  public void reset()
111  {
112  Native.goalReset(getContext().nCtx(), getNativeObject());
113  }
114 
118  public int size()
119  {
120  return Native.goalSize(getContext().nCtx(), getNativeObject());
121  }
122 
129  {
130  int n = size();
131  BoolExpr[] res = new BoolExpr[n];
132  for (int i = 0; i < n; i++)
133  res[i] = (BoolExpr) Expr.create(getContext(), Native.goalFormula(getContext().nCtx(), getNativeObject(), i));
134  return res;
135  }
136 
140  public int getNumExprs()
141  {
142  return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
143  }
144 
149  public boolean isDecidedSat()
150  {
151  return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
152  }
153 
158  public boolean isDecidedUnsat()
159  {
160  return Native
161  .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
162  }
163 
169  public Goal translate(Context ctx)
170  {
171  return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
172  getNativeObject(), ctx.nCtx()));
173  }
174 
180  public Goal simplify()
181  {
182  Tactic t = getContext().mkTactic("simplify");
183  ApplyResult res = t.apply(this);
184 
185  if (res.getNumSubgoals() == 0)
186  throw new Z3Exception("No subgoals");
187  else
188  return res.getSubgoals()[0];
189  }
190 
196  public Goal simplify(Params p)
197  {
198  Tactic t = getContext().mkTactic("simplify");
199  ApplyResult res = t.apply(this, p);
200 
201  if (res.getNumSubgoals() == 0)
202  throw new Z3Exception("No subgoals");
203  else
204  return res.getSubgoals()[0];
205  }
206 
212  public String toString() {
213  return Native.goalToString(getContext().nCtx(), getNativeObject());
214  }
215 
221  public BoolExpr AsBoolExpr() {
222  int n = size();
223  if (n == 0) {
224  return getContext().mkTrue();
225  } else if (n == 1) {
226  return getFormulas()[0];
227  } else {
228  return getContext().mkAnd(getFormulas());
229  }
230  }
231 
232  Goal(Context ctx, long obj)
233  {
234  super(ctx, obj);
235  }
236 
237  Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) {
238  super(ctx, Native.mkGoal(ctx.nCtx(), (models),
239  (unsatCores), (proofs)));
240  }
241 
250  {
251  return new Model(getContext(),
252  Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject()));
253  }
254 
255 
256 
257  @Override
258  void incRef() {
259  Native.goalIncRef(getContext().nCtx(), getNativeObject());
260  }
261 
262  @Override
263  void addToReferenceQueue() {
264  getContext().getGoalDRQ().storeReference(getContext(), this);
265  }
266 }
void add(BoolExpr ... constraints)
Definition: Goal.java:79
boolean isDecidedUnsat()
Definition: Goal.java:158
Goal simplify(Params p)
Definition: Goal.java:196
static void goalReset(long a0, long a1)
Definition: Native.java:3984
static boolean goalIsDecidedUnsat(long a0, long a1)
Definition: Native.java:4028
static void goalAssert(long a0, long a1, long a2)
Definition: Native.java:3958
static boolean goalInconsistent(long a0, long a1)
Definition: Native.java:3966
BoolExpr AsBoolExpr()
Definition: Goal.java:221
static void goalIncRef(long a0, long a1)
Definition: Native.java:3933
static int goalPrecision(long a0, long a1)
Definition: Native.java:3949
Goal translate(Context ctx)
Definition: Goal.java:169
boolean isGarbage()
Definition: Goal.java:69
def Model(ctx=None)
Definition: z3py.py:6216
void storeReference(Context ctx, T obj)
static long goalTranslate(long a0, long a1, long a2)
Definition: Native.java:4037
static long goalFormula(long a0, long a1, int a2)
Definition: Native.java:4001
static final Z3_goal_prec fromInt(int v)
ApplyResult apply(Goal g)
Definition: Tactic.java:50
boolean inconsistent()
Definition: Goal.java:92
boolean isOverApproximation()
Definition: Goal.java:60
static int goalNumExprs(long a0, long a1)
Definition: Native.java:4010
static long goalConvertModel(long a0, long a1, long a2)
Definition: Native.java:4046
static int goalDepth(long a0, long a1)
Definition: Native.java:3975
BoolExpr mkAnd(BoolExpr... t)
Definition: Context.java:780
String toString()
Definition: Goal.java:212
boolean isPrecise()
Definition: Goal.java:44
static String goalToString(long a0, long a1)
Definition: Native.java:4055
boolean isDecidedSat()
Definition: Goal.java:149
BoolExpr [] getFormulas()
Definition: Goal.java:128
boolean isUnderApproximation()
Definition: Goal.java:52
static boolean goalIsDecidedSat(long a0, long a1)
Definition: Native.java:4019
Tactic mkTactic(String name)
Definition: Context.java:2715
static int goalSize(long a0, long a1)
Definition: Native.java:3992
Z3_goal_prec getPrecision()
Definition: Goal.java:35
Model convertModel(Model m)
Definition: Goal.java:249
def String(name, ctx=None)
Definition: z3py.py:10043
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:4056