[SMT-LIB] Sublogics mixing reals, ints and quantifiers

[Cesare Tinelli]

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.
>>>
>