Project Layout

Project Layout

This page contains a short list on all important folders within the main AProVE folder. Moreover, we list all modules and packages within the src-folder.

Source Folders within aprove

The main project AProVE contains multiple folders:

• build contains the complied Java classes as usual
• buildEcl contains more complied Java classes
• bench contains scripts to benchmark AProVE inside a docker container or locally
• eclipsePreferences contains the preference files for eclipse (e.g., how to format code, what is considered as an error or a warning, etc.)
• examples contains some examples on different programming languages and can be used for testing
• gen contains generated code and resources (mostly the generated code from the input grammars)
• lib contains all the necessary jar files AProVE uses as library
• licenses contains all the licenses of the jars used within AProVe as library
• res-classes contains .class files that are used as a resource
• src contains Java code and other non-generated resource
• test may contain tests in future releases

Note on GlobalSettings.java

aprove/src/aprove/GlobalSettings.java is intentionally excluded from version control (listed in .gitignore). It contains static final configuration flags that control compile-time feature toggles (e.g. certification output, external solver options). Because the compiler inlines static final boolean fields, changing these values requires a full rebuild.

After cloning, you will not have this file. The initialSetup ant target (next step) generates a default version for you. If you need to change a flag locally, edit your copy — your changes will not be committed accidentally. Be aware that whenever a new flag is added to GlobalSettings.java in the repository's default template, you may need to manually add it to your local copy if your build starts failing.

Packages within the source code of aprove

Name	Justification of Existence
api	The api for AProve, e.g., used in the Eclipse plugin
cli	The interface for AProVE as a command line tool
exit	Additionally needed code to kill AProVE appropriately (as Eclipse-Plugin and as commandline tool)
input	All classes concerning the input of AProVE, e.g., program syntax, parser, etc. including the input for the solver for diophantine equations in AProVE, e.g., polynomials, etc.
loggin	Some sort of logging
predefinedstrategies	Predefined strategies when to use which processor within AProVE
prooftree	All stuff regarding the general proof structure within AProVE
runtime	central implementation of parsing and solving of input problems. (Runtime stuff)
strategies	All stuff regarding the general structure of a strategie within AProVE
solver	Contains solver factory classes (e.g., KBO, LPO, RPOS, EMB, POLO, etc.) that are used throughout the rest of the codebase. Moreover, it contains all the engine classes for the SAT and SMT Solver we use as blackbox tools within many processors.
verification	All the different frameworks with all the problems and processors (the core logic of AProVE)
xml	All stuff for formatting the output of proofs, e.g., for HTML, Ceta, etc.

The Verification Package

The most important package in AProVE is the verification package. Here, all the different problems and processors are defined and implemented. The verification package contains the following subpackages:

Name	Justification of Existence
complexity	All stuff regarding complexity analysis within AProVE
diophantine	A standalone solver that solves diophantine equations (most likely using bit-blasting)
dpframework	All stuff regarding termination analysis within AProVE
idpframework	All stuff regarding termination of integer term rewriting. There are supposedly two different implementations of ITRSs, and only one of the works while the other is a more abstract version that was never finished. This might be either one of them.
oldframework	Old implementations of terms, orders, rules, etc. used by the theorem proving part of AProVE
probabilistic	All stuff regarding termination of probabilistic term rewriting.
relative	All stuff regarding termination of relative term rewriting via ADPs.
theoremprover	An outdated theorem prover that was used decades ago

dpframework vs. oldframework

Many important classes of AProVE (terms, orders, rules, ...) used to be stored in the package aprove.verification.oldframework. Due to some major refactoring started in spring 2005, these were reimplemented in the package aprove.verification.dpframework. However, e.g. the "old" terms are deprecated only for termination analysis, since they are still in use for theorem proving.

So, unless you are working on theorem proving, in case of doubt always use the common classes found in verification.dpframework and not those in verification.oldframework.

Regarding the introduction of new packages/classes into one of the two aforementioned packages:

• If the new code makes use of the verification.dpframework terms, putting it below aprove.verification.dpframework is probably a good idea. Example: The LPO implementation that uses SAT solving.
• If the new code is used for theorem proving, putting it below aprove.verification.oldframework is likely to be appropriate. Example: The PropositionalLogic package.