Support hashing domains

src/ast.rs

@@ -26,6 +26,13 @@ pub struct ForAll
 	pub argument: Box<Formula>,
 }
 
+#[derive(PartialEq)]
+pub enum ImplicationDirection
+{
+	LeftToRight,
+	RightToLeft,
+}
+
 #[derive(PartialEq)]
 pub enum Formula
 {
@@ -34,7 +41,7 @@ pub enum Formula
 	Not(Box<Formula>),
 	And(Vec<Box<Formula>>),
 	Or(Vec<Box<Formula>>),
-	Implies(Box<Formula>, Box<Formula>),
+	Implies(Box<Formula>, Box<Formula>, ImplicationDirection),
 	Biconditional(Box<Formula>, Box<Formula>),
 	Less(Term, Term),
 	LessOrEqual(Term, Term),
@@ -46,7 +53,7 @@ pub enum Formula
 	Predicate(Predicate),
 }
 
-#[derive(PartialEq)]
+#[derive(Eq, Hash, PartialEq)]
 pub enum Domain
 {
 	Program,

src/format.rs

@@ -75,7 +75,7 @@ fn formula_precedence(formula: &crate::Formula) -> u64
 		crate::Formula::Not(_) => 2,
 		crate::Formula::And(_) => 3,
 		crate::Formula::Or(_) => 4,
-		crate::Formula::Implies(_, _) => 5,
+		crate::Formula::Implies(_, _, _) => 5,
 		crate::Formula::Biconditional(_, _) => 6,
 	}
 }
@@ -98,7 +98,7 @@ fn formula_requires_parentheses(child: &crate::Formula, parent: Option<&crate::F
 			// Implications aren’t associative, so handle them separately
 			match parent
 			{
-				crate::Formula::Implies(_, _) => true,
+				crate::Formula::Implies(_, _, _) => true,
 				_ => false,
 			}
 		},
@@ -229,7 +229,11 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					separator = " or "
 				}
 			},
-			crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
+			crate::Formula::Implies(ref left, ref right, implication_direction) => match implication_direction
+			{
+				crate::ImplicationDirection::LeftToRight => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
+				crate::ImplicationDirection::RightToLeft => write!(format, "{:?} <- {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
+			},
 			crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
 			crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
 			crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,

src/lib.rs

@@ -2,5 +2,5 @@ mod ast;
 pub mod format;
 pub mod parse;
 
-pub use ast::{Domain, Exists, Formula, ForAll, Predicate, PredicateDeclaration, VariableDeclaration, Term};
+pub use ast::{Domain, Exists, Formula, ForAll, ImplicationDirection, Predicate, PredicateDeclaration, VariableDeclaration, Term};
 pub use parse::{formula, formulas, term};

src/parse.rs

@@ -100,7 +100,7 @@ fn is_uppercase_alphanumeric(c: char) -> bool
 	c.is_alphanumeric() && c.is_uppercase()
 }
 
-fn symbolic_identifier(i: &str) -> IResult<&str, String>
+pub fn symbolic_identifier(i: &str) -> IResult<&str, String>
 {
 	let (i, symbolic_identifier) = map
 	(
@@ -174,7 +174,7 @@ fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
 				let domain = match name.chars().next()
 				{
 					Some('X') | Some('Y') | Some('Z') => crate::Domain::Program,
-					Some('I') | Some('N') | Some('M') => crate::Domain::Integer,
+					Some('I') | Some('J') | Some('K') | Some('L') | Some('M') | Some('N') => crate::Domain::Integer,
 					Some(other) => panic!("variable “{}” starts with character “{}”, which is not allowed", name, other),
 					None => panic!("unexpected variable name, please report to bug tracker"),
 				};
@@ -518,7 +518,7 @@ fn exists(i: &str) -> IResult<&str, crate::Formula>
 						tag(","),
 						variable_declaration
 					),
-					formula_precedence_1
+					formula_precedence_2
 				)
 			),
 			whitespace0
@@ -553,7 +553,7 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula>
 						tag(","),
 						variable_declaration
 					),
-					formula_precedence_1
+					formula_precedence_2
 				)
 			),
 			whitespace0
@@ -647,8 +647,12 @@ fn formula_precedence_5(i: &str) -> IResult<&str, crate::Formula>
 
 	match preceded(tag("->"), formula_precedence_4)(i)
 	{
-		Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right)))),
-		Err(_) => Ok((i, left)),
+		Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right), crate::ImplicationDirection::LeftToRight))),
+		Err(_) => match preceded(tag("<-"), formula_precedence_4)(i)
+		{
+			Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right), crate::ImplicationDirection::RightToLeft))),
+			Err(_) => Ok((i, left)),
+		},
 	}
 }