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 
251  {
252  return new Model(getContext(),
253  Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject()));
254  }
255 
256 
257 
258  @Override
259  void incRef() {
260  Native.goalIncRef(getContext().nCtx(), getNativeObject());
261  }
262 
263  @Override
264  void addToReferenceQueue() {
265  getContext().getGoalDRQ().storeReference(getContext(), this);
266  }
267 }
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:3862
static boolean goalIsDecidedUnsat(long a0, long a1)
Definition: Native.java:3906
static void goalAssert(long a0, long a1, long a2)
Definition: Native.java:3836
static boolean goalInconsistent(long a0, long a1)
Definition: Native.java:3844
BoolExpr AsBoolExpr()
Definition: Goal.java:222
static void goalIncRef(long a0, long a1)
Definition: Native.java:3811
static int goalPrecision(long a0, long a1)
Definition: Native.java:3827
Goal translate(Context ctx)
Definition: Goal.java:170
boolean isGarbage()
Definition: Goal.java:69
def Model(ctx=None)
Definition: z3py.py:6167
void storeReference(Context ctx, T obj)
static long goalTranslate(long a0, long a1, long a2)
Definition: Native.java:3915
static long goalFormula(long a0, long a1, int a2)
Definition: Native.java:3879
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:3888
static long goalConvertModel(long a0, long a1, long a2)
Definition: Native.java:3924
static int goalDepth(long a0, long a1)
Definition: Native.java:3853
BoolExpr mkAnd(BoolExpr... t)
Definition: Context.java:780
String toString()
Definition: Goal.java:213
boolean isPrecise()
Definition: Goal.java:44
static String goalToString(long a0, long a1)
Definition: Native.java:3933
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:3897
Tactic mkTactic(String name)
Definition: Context.java:2715
static int goalSize(long a0, long a1)
Definition: Native.java:3870
Z3_goal_prec getPrecision()
Definition: Goal.java:35
Model convertModel(Model m)
Definition: Goal.java:250
def String(name, ctx=None)
Definition: z3py.py:9964
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:4056