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] = (BoolExpr) Expr.create(getContext(), Native.goalFormula(getContext().nCtx(), getNativeObject(), i));
134  return res;
135  }
136 
140  public int getNumExprs()
141  {
142  return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
143  }
144 
149  public boolean isDecidedSat()
150  {
151  return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
152  }
153 
158  public boolean isDecidedUnsat()
159  {
160  return Native
161  .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
162  }
163 
169  public Goal translate(Context ctx)
170  {
171  return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
172  getNativeObject(), ctx.nCtx()));
173  }
174 
180  public Goal simplify()
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 
196  public Goal simplify(Params p)
197  {
198  Tactic t = getContext().mkTactic("simplify");
199  ApplyResult res = t.apply(this, p);
200 
201  if (res.getNumSubgoals() == 0)
202  throw new Z3Exception("No subgoals");
203  else
204  return res.getSubgoals()[0];
205  }
206 
212  public String toString() {
213  return Native.goalToString(getContext().nCtx(), getNativeObject());
214  }
215 
221  public BoolExpr AsBoolExpr() {
222  int n = size();
223  if (n == 0) {
224  return getContext().mkTrue();
225  } else if (n == 1) {
226  return getFormulas()[0];
227  } else {
228  return getContext().mkAnd(getFormulas());
229  }
230  }
231 
232  Goal(Context ctx, long obj)
233  {
234  super(ctx, obj);
235  }
236 
237  Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) {
238  super(ctx, Native.mkGoal(ctx.nCtx(), (models),
239  (unsatCores), (proofs)));
240  }
241 
250  {
251  return new Model(getContext(),
252  Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject()));
253  }
254 
255 
256 
257  @Override
258  void incRef() {
259  Native.goalIncRef(getContext().nCtx(), getNativeObject());
260  }
261 
262  @Override
263  void addToReferenceQueue() {
264  getContext().getGoalDRQ().storeReference(getContext(), this);
265  }
266 }
com.microsoft.z3.Goal.translate
Goal translate(Context ctx)
Definition: Goal.java:169
com.microsoft.z3.Goal.convertModel
Model convertModel(Model m)
Definition: Goal.java:249
com.microsoft.z3.Goal.add
void add(BoolExpr ... constraints)
Definition: Goal.java:79
com.microsoft.z3.enumerations.Z3_goal_prec.Z3_GOAL_OVER
Z3_GOAL_OVER
Definition: Z3_goal_prec.java:16
com.microsoft.z3.Tactic.apply
ApplyResult apply(Goal g)
Definition: Tactic.java:50
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.Goal.simplify
Goal simplify(Params p)
Definition: Goal.java:196
com.microsoft.z3.Goal.AsBoolExpr
BoolExpr AsBoolExpr()
Definition: Goal.java:221
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.Goal.size
int size()
Definition: Goal.java:118
com.microsoft.z3.Native.goalFormula
static long goalFormula(long a0, long a1, int a2)
Definition: Native.java:4032
com.microsoft.z3.Native.goalReset
static void goalReset(long a0, long a1)
Definition: Native.java:4015
com.microsoft.z3.Native.goalPrecision
static int goalPrecision(long a0, long a1)
Definition: Native.java:3980
com.microsoft.z3.Goal.inconsistent
boolean inconsistent()
Definition: Goal.java:92
com.microsoft.z3.Native.goalIsDecidedUnsat
static boolean goalIsDecidedUnsat(long a0, long a1)
Definition: Native.java:4059
com.microsoft.z3.Goal.isOverApproximation
boolean isOverApproximation()
Definition: Goal.java:60
com.microsoft.z3.Context.mkTactic
Tactic mkTactic(String name)
Definition: Context.java:2715
com.microsoft.z3.Context.mkAnd
BoolExpr mkAnd(BoolExpr... t)
Definition: Context.java:780
com.microsoft.z3.Goal.isDecidedSat
boolean isDecidedSat()
Definition: Goal.java:149
com.microsoft
com.microsoft.z3.Goal.isGarbage
boolean isGarbage()
Definition: Goal.java:69
com.microsoft.z3.Native.goalIncRef
static void goalIncRef(long a0, long a1)
Definition: Native.java:3964
com.microsoft.z3.Goal.isDecidedUnsat
boolean isDecidedUnsat()
Definition: Goal.java:158
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Goal.isPrecise
boolean isPrecise()
Definition: Goal.java:44
com.microsoft.z3.Native.goalConvertModel
static long goalConvertModel(long a0, long a1, long a2)
Definition: Native.java:4077
com.microsoft.z3.Context.getGoalDRQ
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:4058
com.microsoft.z3.enumerations.Z3_goal_prec.Z3_GOAL_UNDER_OVER
Z3_GOAL_UNDER_OVER
Definition: Z3_goal_prec.java:17
com.microsoft.z3.Goal.simplify
Goal simplify()
Definition: Goal.java:180
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6236
com.microsoft.z3.Native.goalToString
static String goalToString(long a0, long a1)
Definition: Native.java:4086
com.microsoft.z3.Model
Definition: Model.java:25
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Goal.toString
String toString()
Definition: Goal.java:212
com.microsoft.z3.ApplyResult.getNumSubgoals
int getNumSubgoals()
Definition: ApplyResult.java:28
com.microsoft.z3.Native.goalSize
static int goalSize(long a0, long a1)
Definition: Native.java:4023
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.ApplyResult
Definition: ApplyResult.java:24
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Goal.isUnderApproximation
boolean isUnderApproximation()
Definition: Goal.java:52
com.microsoft.z3.ApplyResult.getSubgoals
Goal[] getSubgoals()
Definition: ApplyResult.java:39
com.microsoft.z3.enumerations.Z3_goal_prec.Z3_GOAL_PRECISE
Z3_GOAL_PRECISE
Definition: Z3_goal_prec.java:14
com.microsoft.z3.Goal
Definition: Goal.java:26
com.microsoft.z3.Goal.reset
void reset()
Definition: Goal.java:110
com.microsoft.z3.Native.goalTranslate
static long goalTranslate(long a0, long a1, long a2)
Definition: Native.java:4068
com.microsoft.z3.Expr
Definition: Expr.java:30
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:25
com.microsoft.z3.enumerations.Z3_goal_prec
Definition: Z3_goal_prec.java:13
com.microsoft.z3.Goal.getNumExprs
int getNumExprs()
Definition: Goal.java:140
com.microsoft.z3.Native.goalIsDecidedSat
static boolean goalIsDecidedSat(long a0, long a1)
Definition: Native.java:4050
com.microsoft.z3.Goal.getFormulas
BoolExpr[] getFormulas()
Definition: Goal.java:128
com.microsoft.z3.Goal.getPrecision
Z3_goal_prec getPrecision()
Definition: Goal.java:35
com
com.microsoft.z3.Native.goalDepth
static int goalDepth(long a0, long a1)
Definition: Native.java:4006
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Native.goalAssert
static void goalAssert(long a0, long a1, long a2)
Definition: Native.java:3989
com.microsoft.z3.Native.goalNumExprs
static int goalNumExprs(long a0, long a1)
Definition: Native.java:4041
com.microsoft.z3.Context.mkTrue
BoolExpr mkTrue()
Definition: Context.java:677
com.microsoft.z3.enumerations.Z3_goal_prec.fromInt
static final Z3_goal_prec fromInt(int v)
Definition: Z3_goal_prec.java:35
com.microsoft.z3.enumerations.Z3_goal_prec.Z3_GOAL_UNDER
Z3_GOAL_UNDER
Definition: Z3_goal_prec.java:15
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
com.microsoft.z3.Native.goalInconsistent
static boolean goalInconsistent(long a0, long a1)
Definition: Native.java:3997
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10085
com.microsoft.z3.Tactic
Definition: Tactic.java:27
com.microsoft.z3.Goal.getDepth
int getDepth()
Definition: Goal.java:102