how to evaluate/simplify a term contain if-then-else's?

Thanks, that is helpful!
For our applications (where we don't have complicated terms)
the facilities of that package might be good enough.

Oliver


On Tue, Apr 13, 2010 at 09:25:54AM -0600, Robert Dodier wrote:
> On 4/13/10, Oliver Kullmann <O.Kullmann at swansea.ac.uk> wrote:
> 
> > exactf_tau_arithprog(k,n) :=
> >  if n < k then 0
> >  elseif k=1 then n
> >  elseif k=2 then n-1
> >  elseif n <= 2*k-1 and evenp(k) then
> >    if n = 2*k-1 then 2 else 1
> >  elseif n <= 2*k and oddp(k) then
> >    if n = 2*k then 2 else 1
> >  else unknown$
> >
> > which yields
> >
> > exactf_tau_arithprog(1,n);
> >  if n < 1 then 0 elseif 1 = 1 then n elseif 1 = 2 then n-1 elseif n <= 1 and
> > evenp(1)
> >            then (if n = 1 then 2 else 1) elseif n <= 2 and oddp(1) then (if
> > n = 2 then 2 else 1)
> >            else unknown
> >
> > however this should yield "if n < 1 then 0 else n" --- how to achieve this?
> 
> Since the first condition doesn't evaluate to true or false,
> none of the following conditions are evaluated either.
> This is probably justified by the desideratum of preventing
> side effects.
> 
> There is an experimental share package boolsimp which
> attempts some half-hearted simplifications of conditional
> expressions:
> 
> load (boolsimp);
> exactf_tau_arithprog (1, n);
>  =>  if n < 1 then 0 else n
> 
> I guess that's enough in this case. boolsimp is pretty simple-minded,
> and possibly out of date; don't expect much from it. There are some
> comments in boolsimp.lisp if you care to read them.
> 
> Incidentally, part of the problem is that 1=1 and 1=2 don't simplify
> to true and false, respectively. There has been some discussion
> about simplifying boolean expressions; I don't remember where we
> ended up last time the topic arose.
> 
> best
> 
> Robert Dodier

-- 
Dr. Oliver Kullmann
Computer Science Department
Swansea University
Faraday Building, Singleton Park
Swansea SA2 8PP, UK
http://cs.swan.ac.uk/~csoliver/