In order to use PVAIR you need:

- An executable of PVAIR and

- An example configuration file pvai.conf and

- An example input battleship-5-8-unsat.smt2.

## Example

PVAIR can be executed as follows: ` ./pvair --config=pvai.conf battleship-5-8-unsat.smt2`

It will produce various statistics and since the input formula is unsatisfiable it will print PVAI interpolant.

## Obtaining interpolants

To get the resolution proof or interpolants, the following SMT-LIB2 commands have to be included in the input file. `(sat-check)`

These commands are needed to be able to print and manipulate (reduce) proofs.

(get-proof)`(set-option :produce-interpolants true)`

plus `(sat-check)`

The commands above are needed to be able to manipulate proofs and generate interpolants.

(get-interpolants)

## Variable assignments

We extended the SMT-LIB2 command `get-interpolant`

to specify variable assignment to compute interpolant(s). The command bellow will use an assignment where variables v2 and v28 as assigned to True and v1 is assigned to False. `(get-interpolants v28 (not v1) v2)`

It is also possible to specify assignment via C++ API.

## Configuration files

Configuration file containing default values generated automatically if the PVAIR is executed with `--config=`

pointing to a non-existent file.

### 2.1 General options

Specification of standard and error output channels. Into the standard output, the interpolants are printers whereas various statistics are dumped into the diagnostic channel. ` regular_output_channel [stdout] `

` diagnostic_output_channel [stderr] `

Verbosity level influence how many details are printed into diagnostics channel. ` verbosity [0] or 1 more `

SAT preprocessing in MiniSAT 2.2.0. ` sat_preprocess_booleans [0] or 1 `

### 2.2 Interpolant properties

Option `proof_set_inter_algo`

specifies interpolation algorithm used to compute interpolants ` proof_set_inter_algo [0] or 1 or 2 `

Meaning of the values:

- 0 - McMillan interpolants
- 1 - Pudlák's interpolation system
- 2 - McMillan dual interpolation system

The labeling suggestions can be used only via C++ API. Option `proof_multiple_inter`

additional properties of a sequence of interpolants. Currently only path-interpolation property (value 0) is supported in PVAIR. ` proof_multiple_inter [0] `

Note that PVAIR currently supports only path interpolants using McMillan algorithm. Using different options mean that generated interpolants may not satisfy expected properties.

### 2.3 Proof reductions

Proof reductions can be enabled by the `proof_reduce`

option. ` proof_reduce [0] or 1 `

Once enabled, it is possible to precisely tune the reduction algorithm using the following options. The proof reduction is based on a single run of LowerUnits followed by a number of global iterations. Each global iteration consists of running in order RecyclePivots, StructuralHashing, TransformationTraversals. Each technique can be independently enabled or disabled. ` proof_push_units 0 or [1] # Lowering unit clauses `

` proof_red_trans [0] or more # Number of global iterations to execute `

` proof_rec_piv 0 or [1] `

` proof_struct_hash 0 or [1] `

` proof_transf_trav 0 or [1] `