div int int theories

[Luis Renato Santos]

Hello,

The SMTLib 2.0 said that in Int theories we can use div when we can use division. But I try it in OpenSMT like this:

(set-logic QF_LIA)
(declare-fun t () Int)
(assert (< 0 t))
(assert (> 79 t))
(assert (distinct (div t 20) 0))
(assert (distinct (div t 20) 1))
(assert (distinct (div t 20) 2))
(assert (distinct (div t 20) 3))
(check-sat)
(exit)

And the OpenSMT return:

# Error: undeclared function symbol  div Int Int (triggered at EgraphStore.C, 583)

Did I do anything wrong?

Thanks,
Luis Renato

[Luis Renato Santos]

Em segunda-feira, 2 de abril de 2012 08h32min42s UTC-3, Luis Renato Santos escreveu:

Hello,

The SMTLib 2.0 said that in Int theories we can use div when we can use division. But I try it in OpenSMT like this:

(set-logic QF_IDL)

[Roberto Bruttomesso]

Dear Luis Renato,

opensmt does not support the div operator, as well as other constructs
defined inside the SMT-LIB. It only supports the logics QF_IDL/RDL,
QF_UF, QF_LRA and some combinations.

Cheers,
R

> --
> You received this message because you are subscribed to the Google Groups
> "opensmt" group.
> To view this discussion on the web visit
> https://groups.google.com/d/msg/opensmt/-/ZZRwkmBRtNQJ.
>
> To post to this group, send email to ope...@googlegroups.com.
> To unsubscribe from this group, send email to
> opensmt+u...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/opensmt?hl=en.

--
Roberto Bruttomesso, PhD - http://tinyurl.com/r0b3r70

[Roberto]

Hi,

On Wednesday, April 4, 2012 2:40:42 PM UTC+2, Luis Renato Santos wrote:

Dear Roberto,

Thank you for the answer. So, it's have another way to do division between two integer?

no there is no way to divide integers in opensmt. you may try your luck with more complete solvers

Cheers,

Roberto

 

Cheers,
Luis Renato

> opensmt+unsubscribe@googlegroups.com.

> For more options, visit this group at
> http://groups.google.com/group/opensmt?hl=en.