From 7d22e47ba12cac6d54a78a84f809e2ca5a1301bb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Mon, 13 Apr 2020 22:05:09 +0200
Subject: [PATCH] Represent quantified formulas consistently

Existential and universal quantification used redundant data
representations, while they actually share the same structure. This
unifies both into a single QuantifiedFormula type.
---
 src/ast.rs | 30 ++++++------------------------
 1 file changed, 6 insertions(+), 24 deletions(-)

diff --git a/src/ast.rs b/src/ast.rs
index 08c9cd2..b0e53e3 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -246,31 +246,13 @@ impl Compare
 	}
 }
 
-pub struct Exists
+pub struct QuantifiedFormula
 {
 	pub parameters: std::rc::Rc<VariableDeclarations>,
 	pub argument: Box<Formula>,
 }
 
-impl Exists
-{
-	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
-	{
-		Self
-		{
-			parameters,
-			argument,
-		}
-	}
-}
-
-pub struct ForAll
-{
-	pub parameters: std::rc::Rc<VariableDeclarations>,
-	pub argument: Box<Formula>,
-}
-
-impl ForAll
+impl QuantifiedFormula
 {
 	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
@@ -449,8 +431,8 @@ pub enum Formula
 	And(Formulas),
 	Boolean(bool),
 	Compare(Compare),
-	Exists(Exists),
-	ForAll(ForAll),
+	Exists(QuantifiedFormula),
+	ForAll(QuantifiedFormula),
 	IfAndOnlyIf(Formulas),
 	Implies(Implies),
 	Not(Box<Formula>),
@@ -483,7 +465,7 @@ impl Formula
 	{
 		assert!(!parameters.is_empty());
 
-		Self::Exists(Exists::new(parameters, argument))
+		Self::Exists(QuantifiedFormula::new(parameters, argument))
 	}
 
 	pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
@@ -500,7 +482,7 @@ impl Formula
 	{
 		assert!(!parameters.is_empty());
 
-		Self::ForAll(ForAll::new(parameters, argument))
+		Self::ForAll(QuantifiedFormula::new(parameters, argument))
 	}
 
 	pub fn greater(left: Box<Term>, right: Box<Term>) -> Self