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 {
36  {
37  return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
38  getNativeObject()));
39  }
40 
44  public boolean isPrecise() throws Z3Exception
45  {
47  }
48 
52  public boolean isUnderApproximation() throws Z3Exception
53  {
55  }
56 
60  public boolean isOverApproximation() throws Z3Exception
61  {
63  }
64 
69  public boolean isGarbage() throws Z3Exception
70  {
72  }
73 
79  public void add(BoolExpr ... constraints) throws Z3Exception
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() throws Z3Exception
93  {
94  return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
95  }
96 
101  public int getDepth() throws Z3Exception
102  {
103  return Native.goalDepth(getContext().nCtx(), getNativeObject());
104  }
105 
109  public void reset() throws Z3Exception
110  {
111  Native.goalReset(getContext().nCtx(), getNativeObject());
112  }
113 
117  public int size() throws Z3Exception
118  {
119  return Native.goalSize(getContext().nCtx(), getNativeObject());
120  }
121 
127  public BoolExpr[] getFormulas() throws Z3Exception
128  {
129  int n = size();
130  BoolExpr[] res = new BoolExpr[n];
131  for (int i = 0; i < n; i++)
132  res[i] = new BoolExpr(getContext(), Native.goalFormula(getContext()
133  .nCtx(), getNativeObject(), i));
134  return res;
135  }
136 
140  public int getNumExprs() throws Z3Exception
141  {
142  return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
143  }
144 
149  public boolean isDecidedSat() throws Z3Exception
150  {
151  return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
152  }
153 
158  public boolean isDecidedUnsat() throws Z3Exception
159  {
160  return Native
161  .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
162  }
163 
170  public Goal translate(Context ctx) throws Z3Exception
171  {
172  return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
173  getNativeObject(), ctx.nCtx()));
174  }
175 
180  public Goal simplify() throws Z3Exception
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 
195  public Goal simplify(Params p) throws Z3Exception
196  {
197  Tactic t = getContext().mkTactic("simplify");
198  ApplyResult res = t.apply(this, p);
199 
200  if (res.getNumSubgoals() == 0)
201  throw new Z3Exception("No subgoals");
202  else
203  return res.getSubgoals()[0];
204  }
205 
211  public String toString()
212  {
213  try
214  {
215  return Native.goalToString(getContext().nCtx(), getNativeObject());
216  } catch (Z3Exception e)
217  {
218  return "Z3Exception: " + e.getMessage();
219  }
220  }
221 
222  Goal(Context ctx, long obj) throws Z3Exception
223  {
224  super(ctx, obj);
225  }
226 
227  Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
228  throws Z3Exception
229  {
230  super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false,
231  (unsatCores) ? true : false, (proofs) ? true : false));
232  }
233 
234  void incRef(long o) throws Z3Exception
235  {
236  getContext().goal_DRQ().incAndClear(getContext(), o);
237  super.incRef(o);
238  }
239 
240  void decRef(long o) throws Z3Exception
241  {
242  getContext().goal_DRQ().add(o);
243  super.decRef(o);
244  }
245 
246 }
boolean isDecidedUnsat()
Definition: Goal.java:158
Goal simplify(Params p)
Definition: Goal.java:195
static void goalReset(long a0, long a1)
Definition: Native.java:3677
static boolean goalIsDecidedUnsat(long a0, long a1)
Definition: Native.java:3721
void add(BoolExpr...constraints)
Definition: Goal.java:79
static void goalAssert(long a0, long a1, long a2)
Definition: Native.java:3651
static boolean goalInconsistent(long a0, long a1)
Definition: Native.java:3659
static int goalPrecision(long a0, long a1)
Definition: Native.java:3642
Goal translate(Context ctx)
Definition: Goal.java:170
boolean isGarbage()
Definition: Goal.java:69
static long goalTranslate(long a0, long a1, long a2)
Definition: Native.java:3730
static long goalFormula(long a0, long a1, int a2)
Definition: Native.java:3694
static final Z3_goal_prec fromInt(int v)
ApplyResult apply(Goal g)
Definition: Tactic.java:51
boolean inconsistent()
Definition: Goal.java:92
boolean isOverApproximation()
Definition: Goal.java:60
static int goalNumExprs(long a0, long a1)
Definition: Native.java:3703
static int goalDepth(long a0, long a1)
Definition: Native.java:3668
String toString()
Definition: Goal.java:211
boolean isPrecise()
Definition: Goal.java:44
static String goalToString(long a0, long a1)
Definition: Native.java:3739
boolean isDecidedSat()
Definition: Goal.java:149
BoolExpr[] getFormulas()
Definition: Goal.java:127
boolean isUnderApproximation()
Definition: Goal.java:52
static boolean goalIsDecidedSat(long a0, long a1)
Definition: Native.java:3712
Tactic mkTactic(String name)
Definition: Context.java:2430
static int goalSize(long a0, long a1)
Definition: Native.java:3685
Z3_goal_prec getPrecision()
Definition: Goal.java:35