[SMT-LIB] Concerning enumerated types theory

[Tinelli, Cesare]

Mohammad,

On 30 Jul 2011, at 15:03, Mohammad Abdul Aziz wrote:

> Hey all,
> Is there an SMTlib equivilant of the Enumerated types theory used in CVC3??

Unfortunately not (yet). You must encode them in one of the existing logics for now.

> If not, I would like to know what is the most effecient way to deal with an
> enumerated user defined sort.

I do not know if there are more efficient ways, but one is to encode the enumeration type as a finite integer range in one of the logics with integers.

For instance, suppose you have a Color type with values red, yellow and green. You can define them as synonyms for 1,2,3 respectively, and add a predicate isColor that you must assert for each free constant or variable of type Color in your original problem, as in the following sample script.

----------------------
(set-logic QF_LIA)

(define-fun red () Int 1)
(define-fun yellow () Int 2)
(define-fun green () Int 3)

(define-fun isColor ( (x Int) ) Bool (<= 1 x 3))

(declare-fun c1 () Int)
(declare-fun c2 () Int)

(assert (isColor c1))
(assert (isColor c2))

...
------------------

Cheers,


Cesare




> Thanks in advance.
> Yours,
> Mohammad Abdul Aziz
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib