[YICES-HELP] set-arith-only! prevents set-evidence! from working
(in some cases)?
bruno at csl.sri.com
Tue Sep 4 15:44:02 PDT 2007
Johannes Waldmann wrote:
> for the following program,
> (define-type foo (record bar :: nat))
> (define a :: foo)
> (define b :: foo)
> (define gt :: (-> foo foo bool)
> (lambda (x :: foo y :: foo) (> (select x foo) (select y foo))))
> (assert (gt a b))
> yices correctly finds a model,
> and it is output after "-e" on the command line
> resp. (set-evidence! true) in the source.
> now, if I switch on (set-arith-only! true) in the source,
> yices still says "sat", but it will not print the model
> (via either of the above methods).
> I am not sure whether "arith-only" is applicable here
> but if I change the assertion to (gt a a) yices says "unsat",
> so the engine seems to be working fine.
> I am asking because I have a larger program
> where arith-only gives a noticeable speedup
> but it is not much use if I don't see the model afterwards.
> Best regards, Johannes Waldmann.
A model is generated but nothing is displayed because there are no
arithmetic variables in your specifications.
In any case, you should not use (set-arith-only! true) on this
example. As the name indicates that's reserved for specifications that
contain only arithmetic. Records are not part of the arithmetic
fragment. It's a lucky coincidence that you get the right
answer in two cases.
More information about the YICES-HELP