DOMAINS :: SMT-LIB :: Some SMT-COMP/LIB issues

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. Some SMT-COMP/LIB issues

tinelli wrote at Nov 01, 2004 - 05:01 PM
---------------------------------------------------------------------
Hi everybody,

as a follow up to Aaron message about SMT-COMP, we would like to get 
more feedback from this community on a number of currently unresolved 
issues about SMT-COMP, and on some new issues about the SMT-LIB format 
that the SMT-COMP organization has brought up.
These issues have been preliminary discussed between among us (Silvio 
and Cesare), the SMT-COMP organizers (Arran, Clark and Leonardo) and the 
PDPAR'05 organizers (Alessandro Armando and Alessandro Cimatti). While 
we have reached a rough consensus on many of them, we would appreciate 
everybody's input before we go ahead.

Here follows a list of the issues with a few alternative solutions and 
their rationale. To better follow them it would be helpful to review 
first the current rules of the SMT-LIB competion 
(http://www.csl.sri.com/users/demoura/smt-comp/index.shtml) and the 
current SMT-LIB format (Version 1.0 at 
http://goedel.cs.uiowa.edu/smtlib/papers.html).

Again, your feedback on these matters is very important. We urge you to 
espress your opinion soon, in the interest of the SMT-LIB initiative ... 
and your own if you plan to participate to the competition :)

Thanks,


Silvio and Cesare


PS: Sorry is what follows is quite long. But note that it is
    divided into sections and subsections each of which can be
    read independently from the other ones.

-----------------------------------------------------------------

1) THE SMT-LIB FORMAT

The SMT-COMP organizers have asked if we could modify the SMT-LIB format 
in order to allow solvers to parse a single benchmark, as opposed to a 
benchmark set.
The problem with parsing a single benchmark now is that the benchmark 
may cointain function or predicate symbols that are not in the signature 
of the corresponding background theory.
The syntax of benchmark *sets* allows one to declare these extra symbols 
in the attributes :extrafuns and :extrapreds, with a scope that includes 
all the benchmarks in the set.
To allow single benchmarks to be parsed independently then we basically 
have 3 options:
a) leave the SMT-format as it is, and use for the competition "singleton 
benchsets", that is benchsets containing a single benchmark in them.
b) move the :extrafuns and :extrapreds attributes from benchsets to 
single benchmarks, allowing each benchmark to locally extend the 
signature of the theory. (For benchmarks in a benchset, the scope of 
each extra symbol declaration would then be limited to the single 
benchmark containing the declaration.)
c) add an :extrafuns and an :extrapreds attribute to benchmarks but 
leave those attributes in benchsets as well, and adopt the expected 
scoping rules for the declarations: declarations in a benchset are 
global to all of its benchmarks, the declarations in a benchmarks are 
local to the benchmark and override the global ones.

The current consensus is that option (b) would be a good compromise 
between the flexibility requested by the STM-COMP organizers and the 
SMT-LIB design goal of keeping the format simple. It might require in 
some cases to duplicate a declaration over very many benchmarks in a 
set. But this does not seem to be a big deal as the increase in size of 
a benchset is not going to be significant when compared to the size of 
the whole library.


2) THEORIES

There is an ongoing debate between some of us on what exactly we should 
call a theory in SMT-LIB and how we should define it. This impacts 
SMT-COMP for what concerns the definition of the competition's 
divisions. Since this is a relative big issue, we'll write about it in a 
separate post.


3) DIVISIONS

The SMT-COMP benchmarks will be partitioned in a number of divisions.
An initial description of these partitions can be found on the SMT-COMP 
website. But it is only a first approximation. Here are some comments 
about the current partitions.

Qffs:
SMT-LIB does not allow quantifier-free formulas unless they are ground.
But it gives one the choice to represent quantifier-free benchmarks
as ground formulas, by declaring all their variables as free constants
in the :extrafuns attribute, or as existential formulas, with all the 
originally free variables existentially quantified.
The current consensus is to represent quantifier-free benchmarks as 
ground formulas with free constants in all divisions.

EUF:
It turns out that it would be useful if a benchset, or a benchmark, 
could define extra (uninterpreted) sorts in addition to extra function 
and predicate symbol.
Our proposal is to extend the SMT-LIB format in this direction.
Correspondingly, the benchmark in the EUF division would now not have an 
implicity sort (as currently written in the SMT-COMP rules), but declare 
all needed sorts explicitly.

ARITH:
Some of us think that it might be best to put mixed real-integer 
problems in their own division, separately from the ARITH division. The 
reasons are that
1) the theories in question are different: one is the theory of the 
reals, the other is the theory of the reals + the integers
2) it is likely that some of the entrant solvers in the competition will 
be unsound for mixed real-integer problems; the split would give them a 
chance to excel on pure real arithmetic problems.
We have not reached a consensus on this. So your feedback is crucial here.

IsInteger predicate:
The following is not so much a proposal but an explanation of a decision 
currently with no alternatives.
In the mixed real-integer problems all free constants (the unkowns) will 
be formally of type Real. To express that a particular unknown x ranges 
over the integers only, the benchmark will contain a constraint of the 
form IsInteger(x).
The reason to do it this way is that, we do not really have the option 
in the current SMT-LIB format to declare integer variables of sort Int 
into a benchmark. In fact, since SMT-LIB's logic is not order-sorted, we 
cannot declare Int as a subsort of Real. But then a term like x + y is 
ill-sorted if y, say, is declared of sort Int, and + of type Real x Real 
-> Real (recall that SMT-LIB does not allow overloading of function or 
predicate symbols either).

DIFF
There seem to be two types of difference constraint in the literature.
One with real valued variables and one with integer valued variables.
Which one(s) should SMT-COMP include?
The answer to this question depends mostly on the community's wish (and 
the availability of benchmarks).

MIXED
For the Mixed division the exact sorts involved for the array and the
unintepreted symbols are still to be determined.
The SMT-COMP organizers currently propose, for simplicity, to have for 
arrays just a Real_real_arry sort (for real indexed, real valued arrays) 
and an Int_real_array sort (for integer indexed, real valued arrays).
Note that this will require to also have some theory of integers (say 
Presburger arithmetic) as one of the component theories. Because of the 
sorting limitations explained earlier, integer expressions will be used 
only for array indexes, not for array values.

JUDGING AND SCORING
The competition recognizes that some of the entrant solvers might be, by 
design, incomplete or even unsound (as stochastic solvers are) for 
certain divisions. (By soundness we mean that if a solver reports 
unsatisfiable then the input is unsatisfiable, and by completeness that 
if an input is unsatisfiable the solver will terminate and report 
unsatisfiable). So they devised a scoring scheme that favors correct 
anwers without drastically punishing incorrect solvers.
Our preliminary discussion has pointed out though that it would be not 
proper or fair to have solvers based on sound and complete methods 
compete against solvers based on unsound or incomplete methods.
While we all agree on this we have not reached a consensus on how to 
judge the two different kinds of solvers.
Some of us propose that the scoring for solvers in the 
unsound/incomplete category be as explained on the SMT-COMP website, 
while the scoring for solvers in the sound and complete category be more 
similar to what is done in the CASC competition for theorem provers. 
There, provers giving a wrong answer during the competition are 
immediate disqualified; provers may also be retroactively disqualified 
if the entered version is later discovered to be buggy.
In contrast, the SMT-LIB organizers propose to judge solvers in the 
sound and complete category as those in the other category with the only 
difference that the former get penalized more severily for wrong answers 
(instead of being disqualified).


---------------------------------------------------------------------

Reply to this message:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=54&forum=46

Browse thread:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=54

You are receiving this Email because you are subscribed to be notified of events in forums at: http://www.qpq.org/