Z3 |

Tactic.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
27 public class Tactic extends Z3Object {
31 public String getHelp()
32 {
33 return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
34 }
35
40 public ParamDescrs getParameterDescriptions()
41 {
42 return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
43 .nCtx(), getNativeObject()));
44 }
45
50 public ApplyResult apply(Goal g)
51 {
52 return apply(g, null);
53 }
54
59 public ApplyResult apply(Goal g, Params p)
60 {
61 getContext().checkContextMatch(g);
62 if (p == null)
63 return new ApplyResult(getContext(), Native.tacticApply(getContext()
64 .nCtx(), getNativeObject(), g.getNativeObject()));
65 else
66 {
67 getContext().checkContextMatch(p);
68 return new ApplyResult(getContext(),
69 Native.tacticApplyEx(getContext().nCtx(), getNativeObject(),
70 g.getNativeObject(), p.getNativeObject()));
71 }
72 }
73
79 public Solver getSolver()
80 {
81 return getContext().mkSolver(this);
82 }
83
84 Tactic(Context ctx, long obj)
85 {
86 super(ctx, obj);
87 }
88
89 Tactic(Context ctx, String name)
90 {
91 super(ctx, Native.mkTactic(ctx.nCtx(), name));
92 }
93
94 @Override
95 void incRef() {
96 Native.tacticIncRef(getContext().nCtx(), getNativeObject());
97 }
98
99 @Override
100 void addToReferenceQueue() {
101 getContext().getTacticDRQ().storeReference(getContext(), this);
102 }
103}
com.microsoft.z3.ApplyResult
Definition: ApplyResult.java:24
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.mkSolver
Solver mkSolver()
Definition: Context.java:3105
com.microsoft.z3.Context.getTacticDRQ
IDecRefQueue< Tactic > getTacticDRQ()
Definition: Context.java:4135
com.microsoft.z3.Goal
Definition: Goal.java:26
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.ParamDescrs
Definition: ParamDescrs.java:25
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.Solver
Definition: Solver.java:28
com.microsoft.z3.Tactic
Definition: Tactic.java:27
com.microsoft.z3.Tactic.getParameterDescriptions
ParamDescrs getParameterDescriptions()
Definition: Tactic.java:40
com.microsoft.z3.Tactic.getHelp
String getHelp()
Definition: Tactic.java:31
com.microsoft.z3.Tactic.apply
ApplyResult apply(Goal g)
Definition: Tactic.java:50
com.microsoft.z3.Tactic.getSolver
Solver getSolver()
Definition: Tactic.java:79
com.microsoft.z3.Tactic.apply
ApplyResult apply(Goal g, Params p)
Definition: Tactic.java:59
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693