Skip to content

UnderstandingProcessors

Jump to bottom
Kassing edited this page Mar 30, 2026 · 1 revision

Processors

A Processor is a class that implements the Processor interface. It is responsible for performing computations on a BasicObligation and producing a Result. There are two main methods: process() and isApplicable(BasicObligation obl). Most of the time, we have further refined subclasses of that implement new processTRS() and isTRSApplicable(TRSProblem problem) to handle certain problem classes, but the general idea remains the same.

  • isApplicable(BasicObligation obl) checks whether the processor is applicable for the given problem class (BasicObligation-Object). Here, we can check for certain properties of the problem class or even certain general options like which certifier to generate certificates we are currently using. Most of the new processors should not be applicable with a given certifier (like ceta in the following).

    Example:

    @Override
public boolean isQTRSApplicable(final QTRSProblem qtrs) {
    //Check Certifier
    if (Options.certifier.isCeta()) {
        return false;
    }
    
    //Check Problem Properties
    final ImmutableSet<Rule> r = qtrs.getR();
    if (! (qtrs.getQ().isEmpty() && r.size() == 1
            && qtrs.getMaxArity() == 1)) {
        return false;
    }

    return true;
}

  • process() performs the actual processor and returns a Result. The result can contain several components, typically for termination:

    • ObligationNode: This becomes the child of the input BasicObligationNode.
    • Proof: The justification for why the transformation is valid, see Understanding Proofs'.
    • Implication: Describes how truth values can be propagated upwards (e.g., EQUIVALENT, ANTIVALENT, COMPLETE, SOUND).
    • Strategy: Directs the Machine on the next steps.

    For different analysis like complexity analysis, we can even additionally include an upper bound on the proven complexity of the removed component.

Using ResultFactory

Typically, you should use the ResultFactory to create your Result objects, as it handles filling in the fields in a sensible way. It also assists in creating AND/OR junctors. However, it's important to understand the basic flow.

return ResultFactory.proved(newProblem, YNMImplication.EQUIVALENT, proof);

will result in a new BasicObligationNode for newProblem.

Proof Structure

The Result will have that node in its obligationChild, and will have a strategy of Success(basicOblNode) on that node.

return ResultFactory.provedAndFromOblNodes(listOfProblemNodes, YNMImplication.SOUND, proof);

will create a JunctorObligationNode with AND over the problem nodes.

Proof Structure

The result will have that junctor in its obligationChild, its Success(...) will contain all the problemNodes: The junctor will become the direct child in the proof tree, and the problem nodes (all BasicObligationNodes) are where more work is needed.

Most processors do not require a specific strategy to be applied after their execution. This feature exists mainly to support heuristic processors. When no specific strategy is needed, the Strategy in the Result will default to an instance of the Success class. This class tracks all BasicObligationNodes that require further work.

The basic strategy primitives, such as Any, Repeat, Maybe, First, and :, use this Success strategy to take the appropriate action, see Understanding Strategy Evaluation and 'the Machine'.

Example 1: Proving a new problem

The following example demonstrates how to create a new BasicObligationNode for a new problem.

return ResultFactory.proved(newProblem, YNMImplication.EQUIVALENT, proof);

This will generate a new BasicObligationNode for the new problem. The Result will contain this node in its obligationChild, and the strategy will be set to Success(basicOblNode) for further work on that node.

Example 2: Creating a junctor node

If you have a list of problem nodes, you can create a junctor obligation node using the ResultFactory.

return ResultFactory.provedAndFromOblNodes(listOfProblemNodes, YNMImplication.SOUND, proof);

This creates a JunctorObligationNode with an AND operation over the problem nodes. The Result will contain the junctor in its obligationChild, and the Success will hold all the problem nodes. The junctor becomes the direct child in the proof tree, while the problem nodes are marked as requiring more work.

Thread Safety!

Processors are required to be thread-safe. This means that they must not have any attributes that are obligation-dependent. However, attributes that store information regarding the processor configuration are allowed.

This can be accomplished in several ways:

  1. Do not use global attributes to store obligation-dependent information, but use local variables instead.
  2. If local variables would cause too many problems, you can wrap the actual computation inside objects of an inner class instead. Then, the inner class can hold such global information.

Reason: There are processors that output several obligations that all have to be fulfilled (e.g. the one that computes the Dependency Graph). Then, there is only one instance of the next Processor for all obligations (the same config is used for all obligations at this point of execution, so it was decided that only a single instance be created instead of several ones that would have held the same config info). This instance can then be accessed by several threads, possibly concurrently.



Advanced Concepts

Let us also dive deeper in some more advanced concepts that may be of interest

Invoking Other Processors

If you need to call a different processor from within your own processor, you have two options:

  1. Refactor the processor: Move the main calculation into a "solve" method that returns the result. In this case, your process() method will call that solve() method.
  2. Call process() directly: You can also invoke the process() method of another processor directly.

In most cases, the external processor will produce a single BasicObligationNode that you want to work with further. You can retrieve this node via Result.getSuccessPosition(). This method will throw an error if the processor produces an unexpected result. It’s recommended to avoid using result.getObligationChild().x as it’s less reliable. Always cast it explicitly to a BasicObligationNode if needed.

Common Scenarios

1. Invoking a Different Processor

To invoke a different processor, create the processor with the desired settings and call its process() method. Alternatively, refactor its logic into a solve() method and have the process() method invoke that.

2. Invoking a Different Strategy

For invoking a different strategy, refer to processors like OldNonTermHeuristic. While not the most elegant solution, it works: you can piece together your strategy as a string, parse it, and return it as a new strategy result.

3. Invoking a Strategy and Picking Through Results

In cases like SemLabProc, you can invoke the new strategy within a submachine. This approach gives you full control over the execution and lets you examine the results afterward. Be cautious, though, and ensure you're only passing a copy of your ObligationNode to the submachine, or you may inadvertently modify the proof tree.

4. Determining if a Problem Resolves to YES or NO

For problems that can be solved into a YES or NO outcome, it's best to use a junctor. We already have AND, OR, and COND junctors, which fit nicely into the model and include the necessary proofs in the proof tree.

If you can't express the logic with a junctor, you can use a submachine. However, don't rely on handle.getResult() as it only returns the result at the strategy level. Instead, inspect oblNode.getTruthValue() (where oblNode is the node you passed in). After the machine finishes, this will reflect the final result. You might also want to use Solve around the strategy running in the submachine.



Strategy Parameters

Before a processor can be used in a strategy file, its name must be declared in aprove/predefinedstrategies/Modules/std.strategy. Once declared, the framework needs to know how to instantiate the processor when that name is used. This is controlled by annotations on the processor class or its constructor (defined in aprove.strategies.Annotations).

@NoParams

Annotate the class with @NoParams if the processor takes no parameters from the strategy. The framework will call the public no-args constructor.

@NoParams
public class MySimpleProcessor implements Processor {
    public MySimpleProcessor() { ... }
}

@ParamsViaArguments

Annotate a constructor with @ParamsViaArguments({"name1", "name2", ...}), providing one string per constructor parameter. Those strings become the (case-insensitive) parameter names in the strategy. All listed parameters are required — omitting one is an error (unless -F is passed on the CLI to disable strategy checking).

public class MyProcessor implements Processor {
    @ParamsViaArguments({"maxIterations", "strict"})
    public MyProcessor(int maxIterations, boolean strict) { ... }
}

Usage in a strategy file:

MyProc[maxIterations = 5, strict = True]

@ParamsViaArgumentObject

Annotate a constructor that takes a single inner Arguments class. The framework instantiates the Arguments class via its no-args constructor, then populates its public non-final fields (and any setFoo(...) setter methods) from the strategy. Fields retain their default values if not specified in the strategy — making all parameters optional.

public class MyProcessor implements Processor {
    @ParamsViaArgumentObject
    public MyProcessor(Arguments args) { ... }

    public static class Arguments {
        public int maxIterations = 10;  // optional, defaults to 10
        public boolean strict = false;  // optional, defaults to false
    }
}

Subclasses should subclass Arguments as well, call super(args), and inherit all parent parameters automatically.

If both a public field and a setFoo(...) method exist for the same name, the setter takes precedence. Defining two setters with the same (case-insensitive) name is an error.

Clone this wiki locally