Get interpolants

[Jorge]

I'm trying to figure out how to extract interpolants from an
unsatisfiable proof.
First, I made sure to compile opensmt with option --enable-proof.
Then, I wrote this trivial example:

(set-option :produce-proofs true)
(set-option :produce-interpolants true)
(set-logic QF_RDL)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
(assert (= x0 0))
(assert (= x1 (+ x0 2)))
(assert (> x1 10))
(check-sat)
(get-interpolants)
(exit)

I get the message:

# Warning: skipping option :produce-interpolants
# Warning: disabling SATElite preprocessing to track proof
# Warning: Skipping command (get-interpolants) as (produce-
interpolants) is not set
unsat

What I am missing?

Thanks!
Jorge

[Simone Fulvio Rollini]

Bueno, si la versión es la última del repository svn, la solución es simple.

Imagino que no estés usando un file de configuración para OpenSMT;

hay que ejecutar OpenSMT con la opción "--config=<config_file_name>" y un file de default será generado.

Entonces, tienes que poner el parámetro "produce_inter" a 1 para obtener los interpolantes.

Simone

2011/11/21 Simone Fulvio Rollini <roll...@usi.ch>

Hola Jorge,

que versión de OpenSMT estás usando?

Simone

 

2011/11/21 Jorge <jo...@clip.dia.fi.upm.es>

Jorge

--
You received this message because you are subscribed to the Google Groups "opensmt" group.
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.

[Jorge]

Thank you!

It works now.

Jorge

On Nov 22, 5:04 am, Simone Fulvio Rollini <rolli...@usi.ch> wrote:
> Bueno, si la versión es la última del repository svn, la solución es simple.
>
> Imagino que no estés usando un file de configuración para OpenSMT;
> hay que ejecutar OpenSMT con la opción "--config=<config_file_name>" y un
> file de default será generado.
> Entonces, tienes que poner el parámetro "produce_inter" a 1 para obtener
> los interpolantes.
>
> Simone
>

> 2011/11/21 Simone Fulvio Rollini <rolli...@usi.ch>