[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Simplify boolean formulas

Hi Brian,

Could you send me some examples, so that we can look into this in detail?
It's rather hard to answer your questions otherwise.

Sam Owre

Brian J. Cardiff <bcardiff@gmail.com> wrote:

> Hi,
> I am a member of the Relational Formal Methods Research Group of the
> Universidad de Buenos Aires, headed by Marcelo Frias.
> Currently we are trying to simplify a formula (mainly boolean variables) using
> PVS 4.0. The formulas are not theorems, but we expect that redundant
> information is removed and some automated deduction be performed. Other than
> booleans, there are some (not many) enum variables that are not useful in the
> simplification process.
> Despite some of the experiments are quite long, we were expecting better
> results.
> For example:
>  * Theory size: 16 Kb, 140 booleans constants. 3 minutes were needed by grind
> to return a result.
>  * Theory size: 18 Kb, 170 booleans constants. We waited more than 40 minutes
> and cut the execution.
> The main questions we have are:
>  * Are there any limitation we should know about using pvs for simplifying
> formulas with booleans variables?
>  * Is there any detailed information about how bddsimp is implemented that we
> could take advantage of?
> If someone has any kind of feedback it would be great.
> --
> Brian J. Cardiff
> bcardiff(?)gmail.com
> .