[YICES-HELP] unbounded loop

[Bruno Dutertre]

Jean-Francois Couchot wrote:
> Hi.
> 
> I've some difficulties to understand why Yices does not discharge the
> proof obligation joined in attachement in smtlib formalism.
> 
> More precisely, the command
> 
> $yices -smt -v 10 sstrat.smt
> 
> returns
> Yices (version 1.0.2). Copyright 2005, 2006 SRI International.
> GMP (version 4.1.4). Copyright Free Software Foundation, Inc.
> Build date: Mon Nov 13 09:58:33 PST 2006
> simplifying...
> hash consing...
> eliminating term ite...
> searching...
> ssiIssssiI.s...........s...........s...r.........s.......s
> .......s........s.........s.......s......s.......s....r....s
> ......s...........s............s..........s.............s......s
> ............s........s......s........s.......s.....................
> .........s........s.......s.............s..........s..............s.
> 
> Well, it seems that the case spliting rule of the SAT solver is widely
> activated.
> 
> However, in the proof obligation, when I comment the two quantified axioms
> 
> ;; Why axiom ite_true
>  :assumption
>    (forall (?t_5_200_144 c_type)
>    (forall (?x_75_145 c_unique)
>    (forall (?y_74_146 c_unique)
>    (= (smtlib__ite c_Boolean_true  (c_sort ?t_5_200_144 ?x_75_145)
>       (c_sort ?t_5_200_144 ?y_74_146))
>    ?x_75_145))))
> 
> ;; Why axiom ite_false
>  :assumption
>    (forall (?t_6_201_147 c_type)
>    (forall (?x_77_148 c_unique)
>    (forall (?y_76_149 c_unique)
>    (= (smtlib__ite c_Boolean_false  (c_sort ?t_6_201_147 ?x_77_148)
>       (c_sort ?t_6_201_147 ?y_76_149))
>    ?y_76_149))))
> 
> the proof is discharged. It makes me think that the instantiation
> process which diverges.
> 
> Where is the really origin ?
> 
> Thanks
> 
> 

Hi,

The instantiation process does not loop. Yices does not terminate in
reasonable time on your example, because it instantiates the axioms too
much. This causes an explosion in the number of new terms and atoms, and
the SAT solver is lost doing irrelevant case-splits. The ite_true and
ite_false axioms are particularly bad because they create case splits.

You should get better results by using command line option -pc 2, which
selects a less aggressive instantiation heurisitics.

If you want better results from Yices, you should consider translating
the proof obligations to Yices's own input language rather than SMT LIB.
By doing that, you could avoid most of the axioms or write them as definitions,
which is much better for Yices to process. Using Yices's built-in booleans,
array updates, etc., is much more efficient that using your own axiomatized versions.

Best regards,

Bruno