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 
225  Goal(Context ctx, long obj)
226  {
227  super(ctx, obj);
228  }
229 
230  Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
231 
232  {
233  super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false,
234  (unsatCores) ? true : false, (proofs) ? true : false));
235  }
236 
237  void incRef(long o)
238  {
239  getContext().getGoalDRQ().incAndClear(getContext(), o);
240  super.incRef(o);
241  }
242 
243  void decRef(long o)
244  {
245  getContext().getGoalDRQ().add(o);
246  super.decRef(o);
247  }
248 
249 }
boolean isDecidedUnsat()
Definition: Goal.java:160
Goal simplify(Params p)
Definition: Goal.java:198
static void goalReset(long a0, long a1)
Definition: Native.java:3746
static boolean goalIsDecidedUnsat(long a0, long a1)
Definition: Native.java:3790
void add(BoolExpr...constraints)
Definition: Goal.java:80
static void goalAssert(long a0, long a1, long a2)
Definition: Native.java:3720
static boolean goalInconsistent(long a0, long a1)
Definition: Native.java:3728
static int goalPrecision(long a0, long a1)
Definition: Native.java:3711
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:3799
static long goalFormula(long a0, long a1, int a2)
Definition: Native.java:3763
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:3772
static int goalDepth(long a0, long a1)
Definition: Native.java:3737
String toString()
Definition: Goal.java:214
boolean isPrecise()
Definition: Goal.java:45
IDecRefQueue getGoalDRQ()
Definition: Context.java:3695
static String goalToString(long a0, long a1)
Definition: Native.java:3808
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:3781
Tactic mkTactic(String name)
Definition: Context.java:2382
static int goalSize(long a0, long a1)
Definition: Native.java:3754
Z3_goal_prec getPrecision()
Definition: Goal.java:36