Z3
Goal.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
26 public class Goal extends Z3Object
27 {
37  {
38  return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
39  getNativeObject()));
40  }
41 
45  public boolean isPrecise()
46  {
48  }
49 
53  public boolean isUnderApproximation()
54  {
56  }
57 
61  public boolean isOverApproximation()
62  {
64  }
65 
70  public boolean isGarbage()
71  {
73  }
74 
80  public void add(BoolExpr ... constraints)
81  {
82  getContext().checkContextMatch(constraints);
83  for (BoolExpr c : constraints)
84  {
85  Native.goalAssert(getContext().nCtx(), getNativeObject(),
86  c.getNativeObject());
87  }
88  }
89 
93  public boolean inconsistent()
94  {
95  return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
96  }
97 
103  public int getDepth()
104  {
105  return Native.goalDepth(getContext().nCtx(), getNativeObject());
106  }
107 
111  public void reset()
112  {
113  Native.goalReset(getContext().nCtx(), getNativeObject());
114  }
115 
119  public int size()
120  {
121  return Native.goalSize(getContext().nCtx(), getNativeObject());
122  }
123 
130  {
131  int n = size();
132  BoolExpr[] res = new BoolExpr[n];
133  for (int i = 0; i < n; i++)
134  res[i] = new BoolExpr(getContext(), Native.goalFormula(getContext()
135  .nCtx(), getNativeObject(), i));
136  return res;
137  }
138 
142  public int getNumExprs()
143  {
144  return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
145  }
146 
151  public boolean isDecidedSat()
152  {
153  return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
154  }
155 
160  public boolean isDecidedUnsat()
161  {
162  return Native
163  .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
164  }
165 
171  public Goal translate(Context ctx)
172  {
173  return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
174  getNativeObject(), ctx.nCtx()));
175  }
176 
182  public Goal simplify()
183  {
184  Tactic t = getContext().mkTactic("simplify");
185  ApplyResult res = t.apply(this);
186 
187  if (res.getNumSubgoals() == 0)
188  throw new Z3Exception("No subgoals");
189  else
190  return res.getSubgoals()[0];
191  }
192 
198  public Goal simplify(Params p)
199  {
200  Tactic t = getContext().mkTactic("simplify");
201  ApplyResult res = t.apply(this, p);
202 
203  if (res.getNumSubgoals() == 0)
204  throw new Z3Exception("No subgoals");
205  else
206  return res.getSubgoals()[0];
207  }
208 
214  public String toString()
215  {
216  try
217  {
218  return Native.goalToString(getContext().nCtx(), getNativeObject());
219  } catch (Z3Exception e)
220  {
221  return "Z3Exception: " + e.getMessage();
222  }
223  }
224 
230  public BoolExpr AsBoolExpr() {
231  int n = size();
232  if (n == 0)
233  return getContext().mkTrue();
234  else if (n == 1)
235  return getFormulas()[0];
236  else {
237  return getContext().mkAnd(getFormulas());
238  }
239  }
240 
241  Goal(Context ctx, long obj)
242  {
243  super(ctx, obj);
244  }
245 
246  Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
247 
248  {
249  super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false,
250  (unsatCores) ? true : false, (proofs) ? true : false));
251  }
252 
253  void incRef(long o)
254  {
255  getContext().getGoalDRQ().incAndClear(getContext(), o);
256  super.incRef(o);
257  }
258 
259  void decRef(long o)
260  {
261  getContext().getGoalDRQ().add(o);
262  super.decRef(o);
263  }
264 
265 }
boolean isDecidedUnsat()
Definition: Goal.java:160
Goal simplify(Params p)
Definition: Goal.java:198
static void goalReset(long a0, long a1)
Definition: Native.java:3970
static boolean goalIsDecidedUnsat(long a0, long a1)
Definition: Native.java:4014
BoolExpr mkAnd(BoolExpr...t)
Definition: Context.java:723
void add(BoolExpr...constraints)
Definition: Goal.java:80
static void goalAssert(long a0, long a1, long a2)
Definition: Native.java:3944
static boolean goalInconsistent(long a0, long a1)
Definition: Native.java:3952
BoolExpr AsBoolExpr()
Definition: Goal.java:230
static int goalPrecision(long a0, long a1)
Definition: Native.java:3935
Goal translate(Context ctx)
Definition: Goal.java:171
boolean isGarbage()
Definition: Goal.java:70
static long goalTranslate(long a0, long a1, long a2)
Definition: Native.java:4023
static long goalFormula(long a0, long a1, int a2)
Definition: Native.java:3987
static final Z3_goal_prec fromInt(int v)
ApplyResult apply(Goal g)
Definition: Tactic.java:51
boolean inconsistent()
Definition: Goal.java:93
boolean isOverApproximation()
Definition: Goal.java:61
void incAndClear(Context ctx, long o)
static int goalNumExprs(long a0, long a1)
Definition: Native.java:3996
static int goalDepth(long a0, long a1)
Definition: Native.java:3961
String toString()
Definition: Goal.java:214
boolean isPrecise()
Definition: Goal.java:45
IDecRefQueue getGoalDRQ()
Definition: Context.java:3714
static String goalToString(long a0, long a1)
Definition: Native.java:4032
boolean isDecidedSat()
Definition: Goal.java:151
BoolExpr[] getFormulas()
Definition: Goal.java:129
boolean isUnderApproximation()
Definition: Goal.java:53
static boolean goalIsDecidedSat(long a0, long a1)
Definition: Native.java:4005
Tactic mkTactic(String name)
Definition: Context.java:2392
static int goalSize(long a0, long a1)
Definition: Native.java:3978
Z3_goal_prec getPrecision()
Definition: Goal.java:36
static long mkGoal(long a0, boolean a1, boolean a2, boolean a3)
Definition: Native.java:3910