Re: Where is the LIA-Solver?

23 views
Skip to first unread message

Roberto

unread,
Sep 10, 2012, 3:52:32 AM9/10/12
to ope...@googlegroups.com
Hello,

we had a preliminary implementation of QF_LIA on top of QF_LRA, but it was not fully functional. This is why you get the error message

Regards,
Roberto

On Monday, September 10, 2012 3:54:31 AM UTC+2, Mohamed SIALA wrote:
Hello,

I'm trying to use opensmt. The complilation was ok, but I couldn't test any LIA file. Seems like the LIA logic is not implemented! 

Here the example : 

(set-option :print-success false)
(set-logic QF_LIA)
(declare-fun x ( ) Int)
(declare-fun y ( ) Int)
(assert (<= (+ x y) 0))
(assert (= x 0))
(assert (or (= x 1) (>= y 0)))
(assert (not (= y 0)))
(check-sat)
(exit)


The error message is "  Error: (<= (* 1 y) 0)  cannot be handled by any TSolver. Did you disable some solver in the configure file ? (triggered at 
../../../src/egraph/EgraphSolver.C, 77)" 


Thanks!

P.S. There is no liasolver in the tsolvers directory!
Reply all
Reply to author
Forward
0 new messages