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

[Cesare Tinelli]

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.
>
> -- 
> Paul Jackson, School of Informatics, University of Edinburgh
> http://homepages.inf.ed.ac.uk/pbj/
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib