Effect of option [+-]dnfConstraints

[qOEJXOT4]

I am unsure about what [+-]dnfConstraints exactly does. In the manual it states that this option turns ground constraints into DNF (for me ground constraints are formulae without any (free) variables).

The following shows an example output of Princess where I cannot follow what the option does (I am using it together with +mostGeneralConstraint):

1. ((((x₁-x₀) ≠ 1 ∨ 1 ≤ x₀ ≤ 2) ∧ (x₁ ≠ 0 ∨ 0 ≥ x₀)) ∧ ((x₁-x₀) = 1 ∨ 0 ≥ x₁)) (+dnfConstraints)
2. (((x₁-x₀) = 1 ∧ 1 ≤ x₀ ≤ 2) ∨ (x₁ = 0 ∧ x₀ = 0)) (-dnfConstraints)

Both of the mostGeneralConstraints do not contain any ground constraints so I would not expect [+-]dnfConstraints to change the result.

Can someone maybe explain to me what [+-]dnfConstraints exactly does? We are aiming for a DNF as seen in example 2. When dnfConstraints is disabled Princess seems to be tending more towards our desired result. Maybe there is another option for some kind of DNF not just designed to consider ground terms?

[pruemmer]

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.

[qOEJXOT4]

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.

[uuverifiers]

I see. +dnfConstraints is probably not what you want to use then. Princess has some internal functionality for DNF conversion of arbitrary formulas, but this is not yet exposed (properly) through the interface.

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

[qOEJXOT4]

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.

[pruemmer]

Sounds good as well. I have now added options -mgcFormat=dnf and -mgcFormat=cnf for outputting the constraint in those specific normal forms.

[qOEJXOT4]

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