[SMT-LIB] Sublogics mixing reals, ints and quantifiers
Cesare Tinelli
tinelli at cs.uiowa.edu
Sat Jul 25 06:13:47 EDT 2009
Dear Jochen,
On Jun 23, 2009, at 11:02 PM, Jochen Eisinger wrote:
> Hi,
>
> if the Real/Integer theory is changed, I would suggest to add the
> function "integer part" and the relations "congruence modulo n", since
> together with these additions, the Real/Integer theory would allow for
> quantifier elimination:
>
Thanks for your suggestion. We are going to overhaul all current SMT-
LIB theories and logics as we move to Version 2 of the SMT-LIB
language (more on Version 2 soon). We will take this addition into
account as well.
Cesare
> @inproceedings{Weispfenning99,
> author = {Volker Weispfenning},
> title = {Mixed real-integer linear quantifier elimination},
> booktitle = {Proceedings of the 1999 international symposium on
> Symbolic and algebraic computation},
> year = {1999},
> pages = {129--136},
> publisher = {ACM},
> }
>
> The congruences could also be added to the Integer theory which would
> then allow for quantifier elimination as well.
>
> kind regards
> -- jochen
>
> Cesare Tinelli wrote:
>> Hi Paul,
>>
>> thanks for your question and your request.
>>
>> I agree with you that it would be useful to have a built-in symbol in
>> AUFLIRA and AUFNIRA (or better their theory) that injects the
>> integers into the reals. I do not see any problems in doing that from
>> the SMT-LIB point of view.
>>
>> The only objections could come in principle from authors of solvers
>> that support one of these two logics but use separate solvers for the
>> integers and the reals. However, to my knowledge too, all solvers
>> that support integers and reals in fact use a mixed real and integer
>> arithmetic solver, so they would have no trouble in adding an int-to-
>> real function symbol.
>>
>> Does anybody in this list object to Paul's proposal?
>>
>> It is understood that any changes would be applied only after SMT-
>> COMP'09 :)
>>
>>
>> Cesare
>>
>>
>>
>> On Jun 9, 2009, at 1:18 PM, Paul Jackson wrote:
>>
>>> Hi,
>>>
>>> the currently-advertised sublogics that support quantifiers and both
>>> real and int types are AUFLIRA and AUFNIRA. Looking at the
>>> underlying
>>> theory, Int_Int_Real_Array_ArraysEx, I was suprised to see that no
>>> function is provided for the standard injection of the integers
>>> into the
>>> reals. As far as I gather, SMT solvers that support reals, ints and
>>> quantifiers (e.g. CVC3, Yices, Z3) allow one to mix real and int
>>> valued
>>> expressions, and so it would be natural to have a sublogic that
>>> allows
>>> this too.
>>>
>>> Yes, it is easy enough to introduce a new function for this
>>> injection
>>> and add axioms that characterise it precisely (e.g. that state it
>>> is a
>>> homomorphism on the respective additive groups and that it maps 1 to
>>> 1.0). This seems to work after a fashion, e.g: I experimented with:
>>>
>>> (benchmark int_to_real
>>> :logic AUFLIRA
>>> :extrafuns ((i2r Int Real))
>>> :assumption (= (i2r 0) 0.0)
>>> :assumption (= (i2r 1) 1.0)
>>> :assumption (forall (?i Int) (= (i2r (~ ?i))
>>> (~ (i2r ?i)) ))
>>> :assumption (forall (?i Int) (?j Int) (= (i2r (+ ?i ?j))
>>> (+ (i2r ?i) (i2r ?j))))
>>> ; :formula (not (= (i2r 3) 3.0))
>>> :formula (not (= (i2r 100) 100.0))
>>>
>>> :status unknown
>>> )
>>>
>>> CVC3, Yices and Z3 all find the benchmark with the 1st formula
>>> unsat in
>>> under 0.1sec, but Yices and Z3 take more than a few seconds with the
>>> 2nd, I assume because of a growing number of quantifier
>>> instantiations.
>>> (CVC3 quickly returns `unknown' on the 2nd.) But the solvers via
>>> their
>>> native interfaces can handle such goals trivially and there should
>>> be no
>>> need to resort to quantifier instantiation.
>>>
>>> I saw there is a Reals_Ints theory on the SMT-LIB website that takes
>>> the approach of just having a type Real and using a IsInt()
>>> predicate,
>>> but no logic seems to be defined that makes use of this, with or
>>> without
>>> quantifiers.
>>>
>>> Could an Int to Real injection be added to the AUFLIRA and AUFNIRA
>>> logics?
>>>
>>> Thanks,
>>>
>>> Paul.
>>>
>
More information about the SMT-LIB
mailing list