Z3
Tactic.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
27 public class Tactic extends Z3Object
28 {
32  public String getHelp()
33  {
34  return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
35  }
36 
42  {
43  return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
44  .nCtx(), getNativeObject()));
45  }
46 
52  {
53  return apply(g, null);
54  }
55 
61  {
62  getContext().checkContextMatch(g);
63  if (p == null)
64  return new ApplyResult(getContext(), Native.tacticApply(getContext()
65  .nCtx(), getNativeObject(), g.getNativeObject()));
66  else
67  {
68  getContext().checkContextMatch(p);
69  return new ApplyResult(getContext(),
70  Native.tacticApplyEx(getContext().nCtx(), getNativeObject(),
71  g.getNativeObject(), p.getNativeObject()));
72  }
73  }
74 
80  public Solver getSolver()
81  {
82  return getContext().mkSolver(this);
83  }
84 
85  Tactic(Context ctx, long obj)
86  {
87  super(ctx, obj);
88  }
89 
90  Tactic(Context ctx, String name)
91  {
92  super(ctx, Native.mkTactic(ctx.nCtx(), name));
93  }
94 
95  void incRef(long o)
96  {
97  getContext().getTacticDRQ().incAndClear(getContext(), o);
98  super.incRef(o);
99  }
100 
101  void decRef(long o)
102  {
103  getContext().getTacticDRQ().add(o);
104  super.decRef(o);
105  }
106 }
static String tacticGetHelp(long a0, long a1)
Definition: Native.java:4325
static long mkTactic(long a0, String a1)
Definition: Native.java:4041
static long tacticApplyEx(long a0, long a1, long a2, long a3)
Definition: Native.java:4379
IDecRefQueue getTacticDRQ()
Definition: Context.java:3749
ApplyResult apply(Goal g, Params p)
Definition: Tactic.java:60
ApplyResult apply(Goal g)
Definition: Tactic.java:51
void incAndClear(Context ctx, long o)
static long tacticGetParamDescrs(long a0, long a1)
Definition: Native.java:4334
static long tacticApply(long a0, long a1, long a2)
Definition: Native.java:4370
ParamDescrs getParameterDescriptions()
Definition: Tactic.java:41