Z3
Tactic.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
27public class Tactic extends Z3Object {
31 public String getHelp()
32 {
33 return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
34 }
35
41 {
42 return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
43 .nCtx(), getNativeObject()));
44 }
45
51 {
52 return apply(g, null);
53 }
54
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
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}
IDecRefQueue< Tactic > getTacticDRQ()
Definition: Context.java:4135
void storeReference(Context ctx, T obj)
ParamDescrs getParameterDescriptions()
Definition: Tactic.java:40
ApplyResult apply(Goal g)
Definition: Tactic.java:50
ApplyResult apply(Goal g, Params p)
Definition: Tactic.java:59
def String(name, ctx=None)
Definition: z3py.py:10693