Microsoft Z3 C# API中策略组合子（Tactical）的使用方法咨询

Great question! I’ve run into this exact scenario when working with Z3’s C# API too. The tactical combinators like then and or-else you’re looking for aren’t named exactly as they appear in the tutorial, but the C# API provides equivalent methods to compose tactics in the same way. Let me break this down with concrete examples:

Sequential Composition (Equivalent to then) #

To chain tactics so they run one after another (the then tactical), use the Then() method on a Tactic instance. This combines two tactics: the first runs on the goal, then the second runs on any resulting subgoals.

Here’s a quick example:

using Microsoft.Z3;

class Z3TacticChainExample
{
    static void Main()
    {
        using (Context ctx = new Context())
        {
            // Create base tactics
            Tactic simplify = ctx.MkTactic("simplify");
            Tactic satSolver = ctx.MkTactic("sat");

            // Combine them sequentially: simplify first, then run sat solver
            Tactic combinedTactic = simplify.Then(satSolver);

            // Create a sample goal with constraints
            Goal goal = ctx.MkGoal();
            Expr x = ctx.MkIntConst("x");
            goal.Add(ctx.MkGt(x, ctx.MkInt(3)));
            goal.Add(ctx.MkLt(x, ctx.MkInt(8)));

            // Apply the combined tactic
            Subgoal[] subgoals = combinedTactic.Apply(goal);

            // Inspect results
            foreach (var subgoal in subgoals)
            {
                Console.WriteLine($"Subgoal status: {subgoal.Status}");
            }
        }
    }
}

Alternative Composition (Equivalent to or-else) #

For the or-else tactical (try the first tactic, if it doesn’t fully solve the goal, fall back to the second), use the OrElse() method. This lets you define a fallback strategy when your primary tactic doesn’t work as expected.

Example:

using Microsoft.Z3;

class Z3TacticOrElseExample
{
    static void Main()
    {
        using (Context ctx = new Context())
        {
            Tactic simplify = ctx.MkTactic("simplify");
            Tactic qfliaSolver = ctx.MkTactic("qflia"); // Specialized for linear integer arithmetic

            // Try simplifying first; if that doesn't resolve the goal, use the QFLIA solver
            Tactic orElseTactic = simplify.OrElse(qfliaSolver);

            // Apply to a goal
            Goal goal = ctx.MkGoal();
            Expr x = ctx.MkIntConst("x");
            goal.Add(ctx.MkGt(x, ctx.MkInt(3)));
            goal.Add(ctx.MkLt(x, ctx.MkInt(8)));

            Subgoal[] subgoals = orElseTactic.Apply(goal);
        }
    }
}

Other Useful Tactical Combinations #

The C# API supports more common tacticals through additional Tactic methods:

• Repeat: Use Repeat() to apply a tactic repeatedly until no further progress is made (equivalent to the repeat tactical).

  Tactic repeatedSimplify = ctx.MkTactic("simplify").Repeat();
  

• If-Then-Else: Use IfThenElse() to apply a tactic conditionally based on a filter (equivalent to if-then-else).
• Par: Use Par() to run tactics in parallel (equivalent to par).

You can also nest these combinators to build complex strategies, like chaining an or-else combination inside a then sequence:

Tactic complexStrategy = simplify.Then(qfliaSolver.OrElse(satSolver));

Key Note #

All these methods are part of the Microsoft.Z3.Tactic class in the C# API. If you’re ever unsure about a tactical’s equivalent method, check the Tactic class documentation—most core tacticals from the tutorial have direct counterparts here, just with slightly adjusted naming (using PascalCase instead of hyphenated names).

内容的提问来源于stack exchange，提问作者Amarjit Datta