[PLE] Create DecidableRefinements when parsing NNF 'define'

[shingarov]

This fix belongs in the pure-z3 branch, not in reflect*, because it is in the "plumbing connecting Refinements and PLE" introduced in 629ab