Prototype of a Decision Procedure Over Sophisticated Fractional Permissions

This is in support for the "Decision Procedures Over Sophisticated Fractional Permissions" submission

  • Share prover prototype executable download: ( share-prover )
    The archive contains:
    • The share-prover excutable for Ubuntu 10.04.1 LTS (standalone mode)
    • The a testsuite for the standalone mode
  • Instalation only requires that the minisat is placed in /usr/local/bin/
  • Input format:
    query := SAT eq_syst | IMPL eq_syst eq_syst
    eq_syst:=
        exist_var* . non_zero_var* . var_equality* . var_instantiation* . equation* .
    exist_vars:= var
    non_zero_vars:= var
    var_equality := var '=' var
    var_instantiation := var '=' tree_const
    equation := vc vc EQ vc
    vc := var | tree_const
    var := IDENTIFIER
    tree_const :=
        '#' | '('   ')'
        |  '('  tree_const  ','  ')'  |  '('  ','  tree_const  ')'
        |  '('  tree_const  ','  tree_const  ')'
    The full tree constant is encoded as "#", the empty constant is "()", the left share is "(#, )" and so on.
    Equation systems are given as five lists each terminating with '.': existential variables, strictly positive variables, variable equalities, pairs of variables, variable instantiations, equations. Elements in the lists are separated by commas.