Metadata-Version: 2.2
Name: infinite-models
Version: 2.0.1
Summary: Umbrella repository for all infinite-models-related research
License: BSD 3-Clause License
Requires-Python: >=3.12
Description-Content-Type: text/markdown
Requires-Dist: click==8.1.8
Requires-Dist: cvc5==1.2.0
Requires-Dist: z3-solver==4.13.3.0
Provides-Extra: dev
Requires-Dist: autoflake==2.3.1; extra == "dev"
Requires-Dist: black==24.10.0; extra == "dev"
Requires-Dist: build==1.2.2.post1; extra == "dev"
Requires-Dist: isort==5.13.2; extra == "dev"
Requires-Dist: mypy==1.14.1; extra == "dev"
Requires-Dist: pytest==8.3.4; extra == "dev"
Requires-Dist: z3-solver-stubs@ git+https://github.com/neta-elad/z3-solver-stubs@v4.13.3.0-11 ; extra == "dev"
Requires-Dist: cvc5-stubs@ git+https://github.com/neta-elad/cvc5-stubs@v1.2.0-1 ; extra == "dev"

# Infinite Models
Tools for finding, evaluating and using infinite models
in first-order logic.
The two main executables are `fest` (for finding infinite models)
and `axer` (for finding induction axioms).


## Requirements
- Python >= 3.12 (for local installation)
- Docker (for Docker image)


## Local Installation
Skip this section when using the Docker image.

Create a virtual environment by running:
```sh
make .venv
```
and activate it:
```shell
source .venv/bin/activate
```

Alternatively, you can create the virtual environment and activate it with a single command:
```shell
eval $(make -s env)
```

Install the Infinite Models tools locally with their dependencies:
```shell
make install
```

Or, for a development installation:
```shell
make install-dev
```

Run all fast tests (requires dev-installation / Docker image):
```shell
make test-fast
```


## Docker Installation
Skip this section when installing locally.

The Docker image is available in `dockerhub` under the name
`netaeladtau/infinite-models`:
```shell
docker pull netaeladtau/infinite-models:latest
```

You can run it interactively with:
```shell
docker run -it --rm netaeladtau/infinite-models bash
```

Or run a specific tool with:
```shell
docker run -i --rm netaeladtau/infinite-models <tool> [options]
```


## Usage
You can use `fest` to find a symbolic model by running (inside the virtual environment / Docker image):
```shell
fest -n echo_machine
```
and see that you get an infinite model for the `echo_machine` problem
(defined in `src/problems/distributed/echo_machine.py`).

Alternatively, you can supply an SMTLIB file:
```shell
fest my-smt-file.smt2
```

When using the Docker image, the easiest way to pass a file is through `stdin`:
```shell
docker run -i --rm netaeladtau/infinite-models fest - < /path/to/my-smt-file.smt2
```

Alternatively, you can mount a local directory:
```shell
docker run -v /path/to:/mnt/smt -i --rm netaeladtau/infinite-models fest /mnt/smt/my-smt-file.smt2
```

Similarly, you can use `axer` to find induction axioms and prove UNSAT:
```shell
axer -n echo_machine
```

By default, `axer` runs a bruteforce search, trying out many induction axioms.
You can run `axer` in a guided mode, which first constructs a symbolic model
and then uses it to produce induction axioms with the `-g` flag:
```shell
axer -g -n echo_machine
```

Like `fest`, `axer` also accepts SMTLIB files (by filename or through `stdin`).

## Configuration
The code uses a rudimentary configuration system with a few
knobs to allow some customization of the behavior of the `fest` and `axer` tools.
The defaults are defined in `default.config.toml` files:
```shell
find src -name default.config.toml
```
where further explanation about each config is provided.

The defaults are overridden by the user supplied `config.toml`, 
located at the root. 

## Code Overview
The code is split into several packages 
(under the `src` directory):
1. The `common` package, which includes shared utilities
  for working with Z3 and CVC5, 
  as well as the global config framework.
2. The `fest` package, which implements the model checking
  and model finding algorithms described
  in Sections 4-5 of the 
  [POPL'24 paper](https://arxiv.org/abs/2310.16762).
3. The `popl24` package, which runs the evaluation benchmark
  of the POPL '24 paper.
4. The `axer` package, which implements the semantics refinement,
  induction axioms finding procedure described
  in the [POPL '25 paper](https://arxiv.org/abs/2410.18671).
5. The `popl25` package, which runs the evaluation benchmark
  of the POPL '25 paper.

The easiest way to get into things is to pick a simple test
(e.g., `tests/test_fest/test_templates.py:test_client_server`)
and follow the function calls there.
