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

[Jochen Eisinger]

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:

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