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] = new BoolExpr(getContext(), Native.goalFormula(getContext()
134  .nCtx(), getNativeObject(), i));
135  return res;
136  }
137 
141  public int getNumExprs()
142  {
143  return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
144  }
145 
150  public boolean isDecidedSat()
151  {
152  return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
153  }
154 
159  public boolean isDecidedUnsat()
160  {
161  return Native
162  .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
163  }
164 
170  public Goal translate(Context ctx)
171  {
172  return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
173  getNativeObject(), ctx.nCtx()));
174  }
175 
181  public Goal simplify()
182  {
183  Tactic t = getContext().mkTactic("simplify");
184  ApplyResult res = t.apply(this);
185 
186  if (res.getNumSubgoals() == 0)
187  throw new Z3Exception("No subgoals");
188  else
189  return res.getSubgoals()[0];
190  }
191 
197  public Goal simplify(Params p)
198  {
199  Tactic t = getContext().mkTactic("simplify");
200  ApplyResult res = t.apply(this, p);
201 
202  if (res.getNumSubgoals() == 0)
203  throw new Z3Exception("No subgoals");
204  else
205  return res.getSubgoals()[0];
206  }
207 
213  public String toString() {
214  return Native.goalToString(getContext().nCtx(), getNativeObject());
215  }
216 
222  public BoolExpr AsBoolExpr() {
223  int n = size();
224  if (n == 0) {
225  return getContext().mkTrue();
226  } else if (n == 1) {
227  return getFormulas()[0];
228  } else {
229  return getContext().mkAnd(getFormulas());
230  }
231  }
232 
233  Goal(Context ctx, long obj)
234  {
235  super(ctx, obj);
236  }
237 
238  Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) {
239  super(ctx, Native.mkGoal(ctx.nCtx(), (models),
240  (unsatCores), (proofs)));
241  }
242 
243  @Override
244  void incRef() {
245  Native.goalIncRef(getContext().nCtx(), getNativeObject());
246  }
247 
248  @Override
249  void addToReferenceQueue() {
250  getContext().getGoalDRQ().storeReference(getContext(), this);
251  }
252 }
void add(BoolExpr ... constraints)
Definition: Goal.java:79
boolean isDecidedUnsat()
Definition: Goal.java:159
Goal simplify(Params p)
Definition: Goal.java:197
static void goalReset(long a0, long a1)
Definition: Native.java:3662
static boolean goalIsDecidedUnsat(long a0, long a1)
Definition: Native.java:3706
static void goalAssert(long a0, long a1, long a2)
Definition: Native.java:3636
static boolean goalInconsistent(long a0, long a1)
Definition: Native.java:3644
BoolExpr AsBoolExpr()
Definition: Goal.java:222
static void goalIncRef(long a0, long a1)
Definition: Native.java:3611
static int goalPrecision(long a0, long a1)
Definition: Native.java:3627
Goal translate(Context ctx)
Definition: Goal.java:170
boolean isGarbage()
Definition: Goal.java:69
void storeReference(Context ctx, T obj)
static long goalTranslate(long a0, long a1, long a2)
Definition: Native.java:3715
static long goalFormula(long a0, long a1, int a2)
Definition: Native.java:3679
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:3688
static int goalDepth(long a0, long a1)
Definition: Native.java:3653
BoolExpr mkAnd(BoolExpr... t)
Definition: Context.java:757
String toString()
Definition: Goal.java:213
boolean isPrecise()
Definition: Goal.java:44
static String goalToString(long a0, long a1)
Definition: Native.java:3724
boolean isDecidedSat()
Definition: Goal.java:150
BoolExpr [] getFormulas()
Definition: Goal.java:128
boolean isUnderApproximation()
Definition: Goal.java:52
static boolean goalIsDecidedSat(long a0, long a1)
Definition: Native.java:3697
Tactic mkTactic(String name)
Definition: Context.java:2623
static int goalSize(long a0, long a1)
Definition: Native.java:3670
Z3_goal_prec getPrecision()
Definition: Goal.java:35
def String(name, ctx=None)
Definition: z3py.py:9443
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:3964
static long mkGoal(long a0, boolean a1, boolean a2, boolean a3)
Definition: Native.java:3602