Implement property generalization

[CyanoKobalamyne]

This adds a flag that enables the generalization of the property by adding quantifiers for all variables that don't have a next state assigned (input variables and state variables without an update function).

This should always be a sound transformation, but we check whether the new property implies the old one anyway.

Such generalization should help k-induction with solving simple array problems that otherwise cannot be proven with the current engines we have.

[ahmed-irfan]

You can use this method instead:

pono/modifiers/prophecy_modifier.h

Line 41 in 2451303

std::pair<smt::Term, smt::Term> get_proph(const smt::Term & target,

to modify the transition system.

[ahmed-irfan]

get_proph(target_var, 0)

[CyanoKobalamyne]

Would that work? Doesn't this just add a new frozen state variable to the system that then I would need to replace with a parameter inside the property anyway to be able to put it in a quantifier? Just having the property be var = proph_var ==> prop wouldn't be strong enough to prove it, I think.

[ahmed-irfan]

You are right about the updated property not strong enough. So, get_proph is not what you want.

However, the get_proph method is not exactly doing what you mentioned.
Let me explain a bit.
get_proph(var, 0) is performing two steps:

1. introduce the quantifier to the property: \forall x. x = target -> property

2. remove the quantifier from the property by introducing a frozen variable y. Frozen variable has the constraint y' = y in the TRANS. The property becomes: y = target -> property.

Additional improvement: You can apply step 2 to remove the quantifier. This will allow to use a quantifier free solver in a model checking algorithm. However, you will still be needing a quantifier handling solver to check this query in your code: https://github.com/stanford-centaur/pono/pull/346/files#diff-6bd9034d0d17559c7dab57996b6d59016614b054e009c26b00e6792460d7a6ffR177