Installing CUDD, Fast Downward and the verifier
-----------------------------------------------
(In what follows <path-to-cudd> is the path where you want CUDD to be
installed to)
1. Download CUDD 3.0.0 from here: http://vlsi.colorado.edu/~fabio/
2. unpack the archive
3. In folder cudd-3.0.0 call the following steps to get the 32-bit library
   with dddmp and c++-wrapper (if you do not want 32 bit, omit "CFLAGS=-m32"
   "CXXFLAGS=-m32" "LDFLAGS=-m32"):
  - ./configure --prefix=<path-to-cudd> --enable-shared --enable-dddmp --enable-obj --enable-static "CFLAGS=-m32" "CXXFLAGS=-m32" "LDFLAGS=-m32"
  - make
  - make install
4. Move the following two header files to <path-to-cudd>/include:
  - config.h
  - util/util.h
  (I don't know why this is necessary, but else the dddmp library complains...)
5. In your .bashrc export the path to the CUDD library:
   "export DOWNWARD_CUDD_ROOT=<path-to-cudd>$
   (DOWNWARD_CUDD_ROOT is used both in Fast Downward in the file FindCUDD
   under src/cmake_modules and in the verifier MAKE file)
7. Compile Fast Downward with ./build.py (choose a 32 bit compilation if you
   compiled the library in 32 bit)
8. Compile the verifier by calling make in the verifier directory
   (you need to change the Makefile if you want a 64 bit compilation)


Generating and verifying proofs
-------------------------------------
The script "test" can be used to test your installation. In
it you can specify a PDDL file and a Fast Downward configuration, and the
script will then first run Fast Downward in order to generate a proof,
and then call the verifier which verifies the proof. It contains all
configurations used in the ICAPS 2018 paper "A Proof System for Unsolvable
Planning Tasks".

The verifier takes two arguments which specify the locations of
 - the task file
 - the proof file
and an optional third argument setting a time limit.

The verifier directory also contains an example certificate for testing
purposes (containing of the files testbdd.bdd, testcertificate.txt
and testtask.txt). You can call it with "./verify testtask.txt
testcertificate.txt".


Formats
-------

The task description (task.txt) has the following format:
________________________________________________________________________________
begin_atoms:<#atoms>
<atom 1>
<atom 2>
... (list all atoms (by name), one each row)
end_atoms
begin_init
<initital state atom index 1>
<initital state atom index 2>
... (lists atoms (by index) that are true in initial state, one each row)
end_init
begin_goal
<goal atom index 1>
<goal atom index 2>
... (lists atoms (by index) that are true in goal, one each row)
end_goal
begin_actions:<#actions>
begin_action
<action_name>
cost: <action_cost>
PRE:<precondition atom index 1>
... (more PRE)
ADD:<added atom index 1>
... (more ADD)
DEL:<deleted atom index 1>
... (more DEL)
end_action
... (lists all actions)
end_actions
________________________________________________________________________________


In the proof (by default named "certificate.txt"), each line describes either
a set expression or a new knowledge about set expressions.

Set expressions can either be constant sets, "basic" sets (which are defined
in a concrete language), or "compound" sets (negation, intersection, union,
progression, regression). Each set expression has a unique identifier.
The following tree represents the delcaration syntax for set expressions:

              /- e                                     (constant empty set)
         /- c -- i                                     (constant initstate set)
        /     \- g                                     (constant goal set)
       /--- b <bdd_filename> <bdd_index> ;             (BDD set)
      /---- h <description in DIMACS> ;                (Horn formula set)
     /----- t <description in DIMACS> ;                (2CNF set)
    /------ e <list of STRIPS states encoded in hex> ; (explicit set)
e # ------- n #                                        (negation)
    \------ i # #                                      (intersection)
     \----- u # #                                      (union)
      \---- p #                                        (progression)
       \--- r #                                        (regression)

(the different parts of the description are separated by space characters) 

The first number is the unique identifier of the new set expression.
For compound sets, the numbers at the end are the identifiers of the respective
subsets (for example "e 10 u 3 5" means "set expression #10 is the union of
set expression #3 and #5).

The description for BDDs must be stored in a different file called
<bdd_filename> (created by the dddmp library). It stores an array of bdds,
thus the <bdd_index> refers to the concrete BDD.
IMPORTANT: each BDD in the file can only be referred to by *ONE* setid,
since the BDD will be deleted when this setid is no longer needed!

Horn and 2CNF formulas are described in the DIMACS format (without comments
or using newline characters). The structure is as follows: "p cnf <#var>
<#clauses> <clause> 0 ... 0 <clause>", where each clause is a list of positive
or negative integers separated by space characters. A positive integer
x refers to variable (x-1) (DIMACS starts counting at 1), and a negative
integer -y to the negation of variable (y-1).
(Example: "p cnf 3 2 2 -1 0 3" represents the formula ((b \lor ¬a) \land (c)) )

Explicit sets are described by a list of STRIPS states, separated by
comma. The state is encoded in hex, meaning that 4 STRIPS variables are
combined to one hex digit. When the number of variables is not divisible by
4 the last hex digit assumes 0 for the missing bits.
(Example: for a task with 9 variables, "5e8" represents state 010111101 (5 =
0101, e = 1110, 8 = 1000)


Knowledge comes in 3 forms:
 - a set expression is dead
 - a set expression is a subset of another set expression
 - the task is unsolvable

The following tree represents the declaration syntax for knowledge:

                      /- b1
                     /-- b2
                    /--- b3
        /---- s # # ---- b4
       /            \--- b5
      /              \-- d10 #
     /                \- d11 #
k # -              /- d1
     \            /-- d2 # #
      \          /--- d3 # #
       \----- d # ---- d6 # # #
        \        \--- d7 # # #
         \        \-- d8 # # #
          \        \- d9 # # #
           \- u -- d4 #
                \- d5 #

(the different parts of the description are separated by space characters) 

The first number is the unique identifier for the knowledge.
The the number behind d (dead) as well as the two numbers behind s (subset)
are set expression identifiers.
(Example: "s 3 5") means set expression #3 is a subset of set expression #5,
and "d 6" means set expression #6 is dead)

Knowledge gained with basic statements do not have any additional
parameters. However the 2 set expressions behind s must match the structure
needed for the corresponding basic statements. Let x_i be sets of type constant
or basic, and l_i sets of type constant, basic or negation of constant or
basic, and si_1 and si_2 be the first and second set expression identifier
after "s":
 - b1: si_1 and si_2 represent sets l_1 and l_2
 - b2: si_1 represents x_1 and si_2 represents the union of x_2 and x_3
 - b3: si_1 represents an intersection between l_1 and the constant goal, and
   si_2 represents l_2
 - b4: si_1 represents the progression of x_1, and si_2 represents the union
   of x_1 and l_1
 - b5: si_1 represents the regression of x_1, and si_2 represents the union
   of x_1 and l_1

For knowledge gained with derivation stepts, the numbers behind dx are
knowledge identifiers pointing to the knowledge needed for deriving the
new knowledge (in the same order as they are mentioned in the paper). Again,
the knowledge must match the structure. Let ki_i be a knowledge identifier: 
 - k # s si_1 si_2 d10 ki_1: si_1 represents the progression of the negation
   of set expression s_1, si_2 represents the negation of a set expression
   s_2 and ki_1 says that the regression of s_2 is a subset of s_1.
 - k # s si_1 si_2 d11 ki_1: si_1 represents the regression of the negation
   of set expression s_1, si_2 represents the negation of a set expression
   s_2 and ki_1 says that the progression of s_2 is a subset of s_1.
 - k # d si d1: si_1 must be the constant empty set
 - k # d si d2 ki_1 ki_2: si must be a union of two set expressions s_1 and
   s_2, ki_1 says that s_1 is dead and ki_2 says that s_2 is dead.
 - k # d si d3 ki_1 ki_2: si represents set expression s_1, ki_1 says that
   s_1 is a subset of set expression s_2 and ki_2 says that s_2 is dead.
 - k # d si d6 ki_1 ki_2 ki_3: si represents set expression s_1, ki_1 says
   that the progression of s_1 is a subset of s_1 \cup s_2, ki_2 says that s_2
   is dead and ki_3 says that the intersection between s_1 and the constant
   goal is dead.
 - k # d si d7 ki_1 ki_2 ki_3: si represents the negation of a set expression
   s_1, ki_1 says that the progression of s_1 is a subset of s_1 \cup s_2,
   ki_2 says that s_2 is dead and ki_3 says that the constant initial state
   set is a subset of s_1.
 - k # d si d8 ki_1 ki_2 ki_3: si represents the negation of a set expression
   s_1, ki_1 says that the regression of s_1 is a subset of s_1 \cup s_2, ki_2
   says that s_2 is dead and ki_3 says that the negation of s_1 intersected
   with the constant goal is dead.
 - k # d si d9 ki_1 ki_2 ki_3: si represents set expression s_1, ki_1 says
   that the regression of s_1 is a subset of s_1 \cup s_2, ki_2 says that s_2
   is dead and ki_3 says that the constant initial state set is a subset of
   the negation of s_1
 - u d4 ki: ki must state that the constant initial state set is dead
 - u d5 ki: ki must state that the constant goal is dead

________________________________________________________________________________




