Effect of option [+-]dnfConstraints about princess HOT 6 CLOSED

from princess.

The description for this option is rather confusing indeed. While constructing proofs, Princess will repeatedly add quantifiers for some of the variables in the constraints, then eliminate those quantifiers. Sometimes the disjunction or conjunction of multiple constraints is formed. The option controls whether the constraints are fully expanded to either DNF or CNF in between those quantifier elimination steps. What are you trying to achieve when playing with this option? In most cases, you should get better performance with -dnfConstraints.

We are aiming for a DNF where we consider the relation atoms and quantified subformulae for divisibility as variables. Of course DNF is used in the context of propositional logic and not predicate logic but when you consider them that way it should hopefully be clear what we mean.

from princess.

from princess.

A simple and clean solution would be to add an SMT-LIB command for DNF conversion; would that be helpful in your application?

We are using the native language of Princess. It would be much appreciated if we could trigger the internal conversion to DNF for the most general constraint. We implemented a conversion to DNF ourselves but using your internal conversion might be more efficient.

Thank you very much.

from princess.

from princess.

Thank you very much for the help and the quick introduction of the new feature.

from princess.