Tutorial

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 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 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 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 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. 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 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 [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 enable by the proof_reduce option. proof_reduce [0] 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 [1] # Lowering unit clauses proof_red_trans [0] or more # Number of global iterations to execure proof_rec_piv 0 or [1] proof_struct_hash 0 or [1] proof_transf_trav 0 or [1]