SMT-LIB: Initial proposal for a common format

[Silvio.Ranise@loria.fr]

Dear Greg,

I would like to thank you and the members of the Sparta 
group for commenting about the proposal.  Here follows 
some comments in replay to your comments about our proposal
for a common format of SMT-LIB:

- P1.F1 about "unsorted".  I agree with your proposal
  of not being able to prove non-trivial properties 
  about formulae containing "strangely" typed terms.
  However, we should make some efforts to define 
  what "non-trivial properties" means.  But this is
  not obvious to me.

- P1.F2 about preventing symbols with variable arity
  in any given problem of the library.  I agree with
  the choice of not allowing varyadic symbols and that
  the signature associated with each problem should be 
  derived while parsing the formulae (this will 
  simplify the statement of the problem and also shrink
  its size).

- P1.F3 about the strict distinction between terms and
  formulae.  I agree with enforcing this distinction
  (this will also simplify the parsing tools which
  will translate from the common format to the formats
  of the various satisfiability/validity checkers).

- P1.F4 about including an IF-THEN-ELSE construct.
  I think that the IF-THEN-ELSE construct is---for certain
  verification efforts---the key to write down formulae in 
  a compact way which otherwise would blow up in size once 
  expressed with the "standard" boolean connectives 
  (like implication, conjunction, etc...).  
  I think that we should also consider to include a LET 
  construct to name subterms and/or subformulae so to be
  able to write down more compact formuale.

- P2 about a normal form for problems.  I think that we 
  should allow formulae with arbitrary structure and 
  envisage tools to put the formulae into some normal
  forms.  Notice that if we allow IF-THEN-ELSE construct
  in the formulae, then translating formulae containing
  such a construct can cause an exponential blow-up in
  the size, which could prevent tools to handle formulae
  that can be otherwise handled if the input language of
  the tools contains the IF-THEN-ELSE construct.

- P3 about how specifying theories.  I agree with your
  proposal of using any technique which is most suited 
  to the theory to be characterized.

- P4 about adding a tag for the status of the problem.
  I agree that we should allows four tags: valid, invalid,
  satisfiable, and unsatisfiable.

- P5 about which theories should be contained in SMT-LIB.
  Here I have a question about the theory of arrays.
  I think this theory highlights the problems of working
  in a sorted or an unsorted framework.  For example, if we
  work in an unsorted framework, what can we say about
  intuitively ill-formed terms of the form 
      select(a, store(a,i,e))
  (where select is the function to read elements and store is
  the function to write elements in an array)?  Obviously,
  we espect an index as the second argument of the select
  above but we get an array (namely store(a,i,e)).  If 
  we use a sorted framework (with sorts for arrays, indexes, and
  elements) then ill-formed terms (such as the one above) are 
  ruled out.  For this theory, I think that the sorted framework
  is more natural than the unsorted one since it is obvious to interpret 
  select and store as distinct operators w.r.t. the remaining function 
  symbols: arrays are function from simple elements to simple elements with
  store modifying such function for a given input and select returning the 
  result of applying the function to a given value.  I do not see how to 
  adapt easly this interpretation to the unsorted case in which we cannot 
  distinguish the elements in the domain of the interpretation between 
  arrays and simple values.  
  Futhermore, if we allow the following extensionality axiom
  in the theory of arrays:

    forall A,B.((forall I.select(A,I)=select(B,I))) ==> A=B)

  then the question is: do you have any evidence that the unsorted 
  theory is consistent?  I can easly build a model for the 
  sorted theory, but I do not succeed in building a model for the
  unsorted case.

I hope the above comments will furtherly stimulate the discussion.

Best regards,

 Silvio.

PS: I would like to point out---once more---the importance of
    setting up the local web pages containing the benchmarks
    in your favorite format.  In fact, this activity can be
    done in parallel with the discussion, it allows to focus
    the discussion about the common format on the "real" 
    problems, and it gives us visibility to the rest of the 
    community.