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)

(get-proof) These commands are needed to be able to print and manipulate (reduce) proofs. (set-option :produce-interpolants true) plus (sat-check)

(get-interpolants) The commands above are needed to be able to manipulate proofs and generate 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]