Re: Where is the LIA-Solver?

[Roberto]

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!