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.
To get the resolution proof or interpolants, the following SMT-LIB2 commands have to be included in input file.
(sat-check) These commands are needed to be able to print and manipulate (reduce) proofs.
(set-option :produce-interpolants true) plus
(sat-check) The commands above are needed to be able to to manipulate proofs and generate interpolants.
We extended the SMT-LIB2 command
get-interpolant to specify variable assignment to compute interpolant(s). The command bellow will use 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 file containing default values generated automatically if the PVAIR is execute with
--config= pointing to non-existent file.
2.1 General options
Specification of standard and error output channels. Into the standard output the interpolants are printer whereas various statistics are dumped into diagnostic channel.
diagnostic_output_channel [stderr] Verbosity level influence how many details are printed into diagnostics channel.
verbosity  or 1 more SAT preprocessing in MiniSAT 2.2.0.
sat_preprocess_booleans  or 1
2.2 Interpolant properties
proof_set_inter_algo specifies interpolation algorithm used to compute interpolants
proof_set_inter_algo  or 1 or 2 Meaning of the values:
- 0 - McMillan interpolants
- 1 - Pudlák's interpolation system
- 2 - McMillan dual interpolation system
The labelling suggestions can be used only via C++ API. Option
proof_multiple_inter additional properties of a sequence of interpolants. Currently only path-interpolantion property (value 0) is supported in PVAIR.
proof_multiple_inter  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 enable by the
proof_reduce  or 1 Once enabled, it is possible to precisely tune the reduction algorithm using 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  # Lowering unit clauses
proof_red_trans  or more # Number of global iterations to execure
proof_rec_piv 0 or 
proof_struct_hash 0 or 
proof_transf_trav 0 or