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 
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 
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 }
static String tacticGetHelp(long a0, long a1)
Definition: Native.java:4017
static long mkTactic(long a0, String a1)
Definition: Native.java:3733
static long tacticApplyEx(long a0, long a1, long a2, long a3)
Definition: Native.java:4071
static void tacticIncRef(long a0, long a1)
Definition: Native.java:3742
IDecRefQueue< Tactic > getTacticDRQ()
Definition: Context.java:3999
void storeReference(Context ctx, T obj)
ApplyResult apply(Goal g, Params p)
Definition: Tactic.java:59
ApplyResult apply(Goal g)
Definition: Tactic.java:50
static long tacticGetParamDescrs(long a0, long a1)
Definition: Native.java:4026
static long tacticApply(long a0, long a1, long a2)
Definition: Native.java:4062
ParamDescrs getParameterDescriptions()
Definition: Tactic.java:40
def String(name, ctx=None)
Definition: z3py.py:9443