[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Simplify boolean formulas
Could you send me some examples, so that we can look into this in detail?
It's rather hard to answer your questions otherwise.
Brian J. Cardiff <firstname.lastname@example.org> wrote:
> 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
> 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