div int int theories

27 views
Skip to first unread message

Luis Renato Santos

unread,
Apr 2, 2012, 7:32:42 AM4/2/12
to ope...@googlegroups.com

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

unread,
Apr 2, 2012, 8:02:23 PM4/2/12
to ope...@googlegroups.com


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

unread,
Apr 3, 2012, 7:47:42 AM4/3/12
to ope...@googlegroups.com
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

Message has been deleted

Roberto

unread,
Apr 7, 2012, 6:20:45 PM4/7/12
to ope...@googlegroups.com
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.

Reply all
Reply to author
Forward
0 new messages