Skip to content

Using the API

Jump to bottom
Henri Nagel edited this page Jun 3, 2026 · 1 revision

Using the AProVE Programmatic API

The aprove.api package lets you construct and analyze problems entirely in Java, without writing or parsing .ari files. It is the recommended integration point for embedding AProVE in other tools.

Overview

The API follows a fluent builder pipeline:

AproveApi
  └─ newTrsInput() / newPtrsInput(goal)      → input builder
       └─ .add(rule) ... .name(...) .build() → AnalyzableProblemInput
            └─ .newProofTreeBuilder()         → ProofTreeBuilder
                 └─ .timeout(...) ...
                    .construct()             → ProofTree
                         └─ .run(handler)    → async result via ProofResultHandler

All types are in the aprove.api package (and sub-packages aprove.api.impl, aprove.api.prooftree).

Entry point

AproveApi api = AproveApi.newInstance();

AproveApi is an interface; newInstance() returns the default implementation.

Analyzing a TRS (Term Rewrite System)

Build rules using FunctionSymbol, TRSVariable, TRSTerm, and Rule:

import aprove.api.*;
import aprove.api.prooftree.*;
import aprove.verification.dpframework.BasicStructures.*;
import aprove.verification.oldframework.BasicStructures.*;

FunctionSymbol f    = FunctionSymbol.create("f", 1);
FunctionSymbol succ = FunctionSymbol.create("s", 1);
FunctionSymbol zero = FunctionSymbol.create("0", 0);
TRSVariable    x    = TRSVariable.createVariable("x");

// f(s(x)) -> f(x)
TRSFunctionApplication lhs1 = TRSTerm.createFunctionApplication(f,
    TRSTerm.createFunctionApplication(succ, x));
TRSFunctionApplication rhs1 = TRSTerm.createFunctionApplication(f, x);
Rule stepRule = Rule.create(lhs1, rhs1);

// f(0) -> 0
TRSFunctionApplication zeroTerm = TRSTerm.createFunctionApplication(zero);
TRSFunctionApplication lhs2     = TRSTerm.createFunctionApplication(f, zeroTerm);
Rule baseRule = Rule.create(lhs2, zeroTerm);

Then build the AnalyzableProblemInput and run the analysis:

AnalyzableProblemInput input = AproveApi.newInstance()
    .newTrsInput()
    .add(stepRule)
    .add(baseRule)
    .name("looped minus one")
    .build();

ProofTree tree = input.newProofTreeBuilder()
    .onlineCertificationPath(Optional.empty())
    .onlyCertifiableTechniquesIfPossible(false)
    .strategy(Optional.empty())
    .timeout(Timeout.positiveOrInfinite(60_000))
    .construct();

CountDownLatch done = new CountDownLatch(1);
String[] result = { "?" };

tree.run(new ProofResultHandler() {
    @Override public void onSuccess (ProofTreeOperationManager m, String msg) { 
        result[0] = msg;
        done.countDown(); }
    @Override public void onTimeout (ProofTreeOperationManager m) { 
        result[0] = "MAYBE (timeout)";
        done.countDown(); }
    @Override public void onError (ProofTreeOperationManager m, Exception e) {
        result[0] = "ERROR: " + e.getMessage();
        done.countDown(); }
    @Override public void onRun (ProofTreeOperationManager m) { }
});

done.await();
System.out.println(result[0]); // e.g. "YES"

The full runnable example is in src/aprove/api/examples/ApiExampleTRS.java.

Analyzing a PTRS (Probabilistic Term Rewrite System)

Choose a goal via the Goal enum (AST, SAST, or TERMINATION) and build ProbabilisticRule objects using MultiDistribution:

import aprove.api.*;
import aprove.api.prooftree.*;
import aprove.verification.dpframework.BasicStructures.*;
import aprove.verification.oldframework.BasicStructures.*;
import aprove.verification.probabilistic.BasicStructures.*;

FunctionSymbol zero = FunctionSymbol.create("0", 0);
FunctionSymbol rw   = FunctionSymbol.create("rw", 1);
FunctionSymbol succ = FunctionSymbol.create("s", 1);
TRSVariable    x    = TRSVariable.createVariable("x");

// rw(0) -> { 1 : 0 }
TRSFunctionApplication zeroTerm = TRSTerm.createFunctionApplication(zero);
TRSFunctionApplication lhs0     = TRSTerm.createFunctionApplication(rw, zeroTerm);
MultiDistribution.Builder<TRSTerm> d0 = new MultiDistribution.Builder<>();
d0.add(zeroTerm, 1);
ProbabilisticRule baseCase = ProbabilisticRule.create(lhs0, d0.build());

// rw(s(x)) -> { 1 : rw(s(s(x))), 1 : rw(x) }   
TRSFunctionApplication sx   = TRSTerm.createFunctionApplication(succ, x);
TRSFunctionApplication ssx  = TRSTerm.createFunctionApplication(succ, sx);
TRSFunctionApplication lhs1 = TRSTerm.createFunctionApplication(rw, sx);
MultiDistribution.Builder<TRSTerm> d1 = new MultiDistribution.Builder<>();
d1.add(TRSTerm.createFunctionApplication(rw, ssx), 1);
d1.add(TRSTerm.createFunctionApplication(rw, x),   1);
ProbabilisticRule step = ProbabilisticRule.create(lhs1, d1.build());

Build and run:

AnalyzableProblemInput input = AproveApi.newInstance()
    .newPtrsInput(Goal.AST)
    .add(baseCase)
    .add(step)
    .name("Random Walk")
    .build();

// ... same ProofTree / ProofResultHandler pattern as TRS above ...

The full runnable example is in src/aprove/api/examples/ApiExamplePTRS.java.

API reference

AproveApi

Method Returns Description
AproveApi.newInstance() AproveApi Factory — call once to get the API object
newTrsInput() TrsInputBuilder Start building a TRS problem
newPtrsInput(Goal) PtrsInputBuilder Start building a PTRS problem
newProblemInput(Path) ProblemInput Load a problem from an .ari/.xml file

TrsInputBuilder

Method Description
add(Rule) Add a rewrite rule
name(String) Human-readable problem name (used in proof output)
build() Produce an AnalyzableProblemInput

PtrsInputBuilder

Method Description
add(ProbabilisticRule) Add a probabilistic rewrite rule
name(String) Human-readable problem name
build() Produce an AnalyzableProblemInput

Goal (enum, aprove.api)

Constant Meaning
AST Almost-sure termination
SAST Sure almost-sure termination
TERMINATION Termination

ProofTreeBuilder

All setters return this (fluent). Call construct() to create the ProofTree.

Method Description
timeout(Timeout) Timeout.positiveOrInfinite(milliseconds)
strategy(Optional<Strategy>) Optional.empty() uses the default strategy
onlineCertificationPath(Optional<Path>) Optional.empty() to skip certification
onlyCertifiableTechniquesIfPossible(boolean) Restrict to certifiable processors
listener(ProofTreeListener) Receive live proof-tree events
construct() Build the ProofTree (does not start analysis yet)

Running the analysis

The recommended way is runAsync(), which wraps run(ProofResultHandler) and returns a CompletableFuture<String>:

String result = tree.runAsync().get();           // blocks until done
// or with timeout:
String result = tree.runAsync().get(60, TimeUnit.SECONDS);
// result is "YES", "NO", or "MAYBE"

ProofResultHandler (lower-level)

Implement this interface and pass it to tree.run(handler) for more control. The analysis runs asynchronously on internal threads; exactly one of onSuccess, onTimeout, or onError will be called.

Method When called
onRun(manager) Analysis has started
onSuccess(manager, message) A definitive result was found; message is e.g. "YES"
onTimeout(manager) The timeout elapsed before a result was found
onError(manager, exception) An unexpected exception occurred

ProofTreeListener

Optional live callbacks as the proof tree is built. Pass via ProofTreeBuilder.listener(...).

Method When called
createRoot(node) The root proof node is created
createChild(node) A child node is added
createProof(node) A proof is attached to a node
setTruth(node, truth) A truth value (e.g. "YES") is assigned to a node

Building terms

Terms are built using static factory methods on TRSTerm (aprove.verification.dpframework.BasicStructures):

// Constant (arity 0):
TRSFunctionApplication zero = TRSTerm.createFunctionApplication(FunctionSymbol.create("0", 0));

// Unary application:
TRSFunctionApplication sx = TRSTerm.createFunctionApplication(succ, x);

// Binary application:
TRSFunctionApplication plus_xy = TRSTerm.createFunctionApplication(plus, x, y);

FunctionSymbol.create(name, arity) and TRSVariable.createVariable(name) are also from aprove.verification.dpframework.BasicStructures and aprove.verification.oldframework.BasicStructures respectively.

Proof details

ProofTreeNode.getDetail(Capability) and ProofTreeProof.getDetail(Capability) return a Detail whose getDetailString() yields Optional<String>.

Capability Description
PLAIN Plain text — best for terminal/API output
HTML HTML markup
LATEX LaTeX markup
SOURCE ExternUsable text (only works for proofs that implement ExternUsable)
DOT Graphviz DOT format

Use Capability.PLAIN for terminal output — it works for all proof and obligation objects.

Suppressing internal logging

AProVE uses java.util.logging internally and produces verbose INFO output by default. Suppress it at the start of main():

Logger root = Logger.getLogger("");
root.setLevel(Level.SEVERE);
for (Handler h : root.getHandlers()) h.setLevel(Level.SEVERE);

Running the examples

Two runnable examples are in aprove.api.examples:

  • ApiExampleTRS — proves termination of f(s(x)) → f(x), f(0) → 0
  • ApiExamplePTRS — proves AST of a random walk PTRS

Adding support for a new problem type

The pattern for adding a new problem type (e.g. FooTRS) is:

  1. FooInputBuilder.java (in aprove.api) — fluent builder that collects rules/options and calls build(). The build() method constructs the problem-specific BasicObligation and returns a DirectAnalyzableProblemInput.
  2. DirectAnalyzableProblemInput (aprove.api.impl) — the shared AnalyzableProblemInput implementation used by all programmatic builders. Its newProofTreeBuilder() passes a lambda to ProofTreeBuilderImpl that calls AproveBuilder.createAproveFromObligation(obligation, language, name, ...).
  3. Wire up the new factory method in AproveApi (interface) and AproveApiImpl (implementation).

The AProVE(BasicObligation, Language, String) constructor in aprove.runtime.AProVE bypasses file parsing and directly injects a pre-built obligation into the analysis pipeline.

Clone this wiki locally