Fortress is a command-line tool and library for manipulating many-sorted first order logic (MSFOL) (plus transitive closure and hopefully soon, set cardinality) formulas with SMT solvers. In particular, given scopes for all the sorts of the problem, Fortress can transform problems into formulas within the equality with uninterpreted functions decidable subset of MSFOL.
Fortress takes as input:
- a first-order logic theory specified in SMT-LIB 2.6 format, and
- (usually) a domain size ("scope") for each sort.
It answers whether the theory has a satisfying interpretation (a "model" or "solution") with the given domain sizes.
Fortress was originally described in the paper "Finite Model Finding Using the Logic of Equality with Uninterpreted Functions", available here, and has been re-implemented to create a powerful and general tool.
Details on using Fortress as the command line are available in this file. The fortress CLI take as input a file in an augmented SMT-LIB format.
Details on using Fortress as a library are available in UserGuide.md .
Details on the internal code organization and design decisions in Fortress can be found in DevelopersGuide.md .
The following are necessary to build Fortress:
- Java 10 or higher
- A command line installation of the
Z3
SMT solver, version 4.8.15 or higher.- Binaries are available here.
- If using MacOS, we recommend using Homebrew:
brew install z3
. - If on
Ubuntu
, do not useapt-get
, since its version of Z3 is out of date. - We have not successfully built fortress on Windows yet, however, if built elsewhere the jars should work on Windows.
- If using CVC4 or CVC5, a command line installation of the
CVC4/CVC5
SMT solver.- If using MacOS, we recommend using Homebrew:
brew tap cvc4/cvc4 && brew install cvc4
.
- If using MacOS, we recommend using Homebrew:
- The sbt build tool.
This repository contains a multi-project sbt build, with the following projects:
fortressCore
, the main functionality of Fortressfortress
, the command line interface of Fortress (depends onfortressCore
)fortressDebug
, a command line interface for debugging Fortress (depends onfortressCore
)root
, the root project which aggregatesfortress
andfortressDebug
Building the root
project (default) is the easiest way to build Fortress.
To use Fortress on the command line, you want the output from the fortress
project.
You can read more about how to use multi-project builds in the sbt reference manual.
sbt stage
This will compile the code and produce executables:
- For the
fortress
project, the executable is./cli/target/universal/stage/bin/fortress
- For the
fortressCore
project, there are 4 jars in./core/target/universal/stage/lib/
- For the
fortressDebug
project, the executable is./debug/target/universal/stage/bin/fortressdebug
Alternatively,
sbt dist
will compile the code produce universal zip archives:
- For the
fortress
project, the output zip is in thecli/target/universal/fortress-x.y.z.zip
directory. - For the
fortressCore
project, the output zip is in thecore/target/universal/fortresscore-x.y.z.zip
directory. - For the
fortressDebug
project, the output zip is in thedebug/target/universal/fortressdebug-x.y.z.zip
directory.
sbt compile
sbt test
Most often Fortress is used as a library. You can either:
- put
./core/target/universal/stage/lib
(built by sbt stage) in your class path or - copy
./core/target/universal/fortresscore-0.1.0.zip
(built by sbt dist) somewhere, uzip it, and put that location in your class path.
All 4 jars must be in the class path.
Instructions on using the Fortress API interface can be found in the API guide.
You can run the Fortress CLI, by either:
./cli/target/universal/stage/bin/fortress
(built by sbt stage) or- Unzipping
cli/target/universal/fortresscore-x.y.z.zip
and running./cli/target/universal/fortresscli-0.1.0/bin/fortress
(built by sbt dist)
The options to the Fortress CLI, can be found by running fortress --help
. In addition:
-
A filename is required of a file in an augmented smttc file format.
-
The lists of possible modelFinders, compilers, solvers, and transformers can be found in the Registry files within the code, e.g., ./core/src/main/scala/fortress/compilers/CompilersRegistry.scala contains the Compiler names. But good defaults are used if these options are not provided in the command-line.
-
A scope can be set with default values (
--scope
), individually on a sort by sort basis (-S
), and in the input file.- A scope is set for a sort using the default scope (
--scope {SCOPE}
if provided), which is overwritten by a scope for the sort provided in the file, which is overwritten by a scope provided in the command-line argument-S {SORT}={SCOPE}
.-S
can take a sequence of{SORT}={SCOPE}
s or it can be used multiple times in the command line.
- A scope is set for a sort using the default scope (
Example usage:
fortress --timeout 30 -S A=3 B=2 --generate function.smttc
This creates a theory using the function.smttc
file, and determines whether there is a satisfying interpretation for this theory where the scope of sort A
is 3 and the scope of sort B
is 2.
If a model exists, fortress outputs Sat
and writes out the model (because of the --generate
option).
Information on the architecture of Fortress is available in the Developer's Guide.
You can run the FortressDebug CLI, by either:
./debug/target/universal/stage/bin/fortressDebug
or- Unzipping
debug/target/universal/fortressdebug-x.y.z.zip
and running./debug/target/universal/fortressdebug-0.1.0/bin/fortressdebug
The options to the FortressDebug, can be found by running fortressDebug --help
. In particular:
-S {SORT}={SCOPE}
- Sets the scope of a sort. This option can be used multiple times (the-S
can be omitted after the first use).--scope {SCOPE}
- Sets the default scope to use when a sort has no specified scope. This is overriden by-S
for a specific sort.-T {transformer1} {transformer2} ...
- Specify exactly which transformers will be used, in order.--version {VERSION}
- Sets the model finder and compiler version. The options for versions can be found in the ./core/src/main/scala/fortress/modelFinders/ModelFindersRegistry.scala
Example usage:
fortressdebug --timeout 60 --mode count -S A=3 B=2 --version JoeONE function.smt2
You can increase the JVM stack size by setting option "-J-Xss", for example, "-J-Xss8m" sets the max stack size to 8 MB. You might want to increase stack size, because the antlr parser causes stack overflow errors when parsing large smt2 and tptp files.
If the gradle build is not working properly ensure that your JAVA_HOME
environment variable is correctly set (to the folder where the jdk that you are using is installed).
The original version of Fortress was created by Amirhossein Vakili and Nancy Day. Fortress was completely rewritten in Scala by Joseph Poremba and greatly enhanced by Ryan Dancy. Joe also greatly extended the symmetry breaking used in Fortress. Additional contributors to Fortress include: Ruomei Yan, Orson Baines, Callum Moseley, Yie Jin (James) Long, and Owen Zila.
Some TPTP files publicly available on the TPTP Problem Library(http://www.tptp.org/) are used for unit tests.