Z3 |

Goal.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
20 import com.microsoft.z3.enumerations.Z3_goal_prec;
21
26 public class Goal extends Z3Object {
35 public Z3_goal_prec getPrecision()
36 {
37 return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
38 getNativeObject()));
39 }
40
44 public boolean isPrecise()
45 {
46 return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE;
47 }
48
52 public boolean isUnderApproximation()
53 {
54 return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER;
55 }
56
60 public boolean isOverApproximation()
61 {
62 return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER;
63 }
64
69 public boolean isGarbage()
70 {
71 return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER;
72 }
73
79 @SafeVarargs
80 public final void add(Expr<BoolSort>... constraints)
81 {
82 getContext().checkContextMatch(constraints);
83 for (Expr<BoolSort> 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
129 public BoolExpr[] getFormulas()
130 {
131 int n = size();
132 BoolExpr[] res = new BoolExpr[n];
133 for (int i = 0; i < n; i++)
134 res[i] = (BoolExpr) Expr.create(getContext(), Native.goalFormula(getContext().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
250 public Model convertModel(Model m)
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}
com.microsoft.z3.ApplyResult
Definition: ApplyResult.java:24
com.microsoft.z3.ApplyResult.getSubgoals
Goal[] getSubgoals()
Definition: ApplyResult.java:39
com.microsoft.z3.ApplyResult.getNumSubgoals
int getNumSubgoals()
Definition: ApplyResult.java:28
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.Context.getGoalDRQ
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:4100
com.microsoft.z3.Context.mkTactic
Tactic mkTactic(String name)
Definition: Context.java:2757
com.microsoft.z3.Context.mkTrue
BoolExpr mkTrue()
Definition: Context.java:702
com.microsoft.z3.Context.mkAnd
final BoolExpr mkAnd(Expr< BoolSort >... t)
Definition: Context.java:807
com.microsoft.z3.Expr< BoolSort >
com.microsoft.z3.Goal
Definition: Goal.java:26
com.microsoft.z3.Goal.isOverApproximation
boolean isOverApproximation()
Definition: Goal.java:60
com.microsoft.z3.Goal.isUnderApproximation
boolean isUnderApproximation()
Definition: Goal.java:52
com.microsoft.z3.Goal.isGarbage
boolean isGarbage()
Definition: Goal.java:69
com.microsoft.z3.Goal.isPrecise
boolean isPrecise()
Definition: Goal.java:44
com.microsoft.z3.Goal.getNumExprs
int getNumExprs()
Definition: Goal.java:141
com.microsoft.z3.Goal.getDepth
int getDepth()
Definition: Goal.java:103
com.microsoft.z3.Goal.AsBoolExpr
BoolExpr AsBoolExpr()
Definition: Goal.java:222
com.microsoft.z3.Goal.getPrecision
Z3_goal_prec getPrecision()
Definition: Goal.java:35
com.microsoft.z3.Goal.simplify
Goal simplify()
Definition: Goal.java:181
com.microsoft.z3.Goal.add
final void add(Expr< BoolSort >... constraints)
Definition: Goal.java:80
com.microsoft.z3.Goal.translate
Goal translate(Context ctx)
Definition: Goal.java:170
com.microsoft.z3.Goal.isDecidedUnsat
boolean isDecidedUnsat()
Definition: Goal.java:159
com.microsoft.z3.Goal.simplify
Goal simplify(Params p)
Definition: Goal.java:197
com.microsoft.z3.Goal.convertModel
Model convertModel(Model m)
Definition: Goal.java:250
com.microsoft.z3.Goal.toString
String toString()
Definition: Goal.java:213
com.microsoft.z3.Goal.getFormulas
BoolExpr[] getFormulas()
Definition: Goal.java:129
com.microsoft.z3.Goal.reset
void reset()
Definition: Goal.java:111
com.microsoft.z3.Goal.inconsistent
boolean inconsistent()
Definition: Goal.java:93
com.microsoft.z3.Goal.size
int size()
Definition: Goal.java:119
com.microsoft.z3.Goal.isDecidedSat
boolean isDecidedSat()
Definition: Goal.java:150
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Model
Definition: Model.java:26
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.Tactic
Definition: Tactic.java:27
com.microsoft.z3.Tactic.apply
ApplyResult apply(Goal g)
Definition: Tactic.java:50
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6579
Z3_goal_prec
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1408