The initial objective of this work has been to factor common (non-Horn) elements ouf of NNFParser to FixpointParser (so that the latter would serve as a common superclass for NNFParser and FQParser, see #363). As the work progressed, two other defects became evident: nomenclature inconsistent with LiquidFixpoint, and the use of (extremely broken) matchedParen even though we already have RefinementExpressionParser. This PR addresses all three issues.
The initial objective of this work has been to factor common (non-Horn) elements ouf of NNFParser to FixpointParser (so that the latter would serve as a common superclass for NNFParser and FQParser, see #363). As the work progressed, two other defects became evident: nomenclature inconsistent with LiquidFixpoint, and the use of (extremely broken) matchedParen even though we already have RefinementExpressionParser. This PR addresses all three issues.