Determine variable IDs correctly

src/problem.rs

@@ -289,7 +289,7 @@ impl Problem
 
 	fn prove_unproven_statements(&self) -> Result<ProofResult, crate::Error>
 	{
-		let display_statement = |statement: &Statement| -> Result<(), crate::Error>
+		let display_statement = |statement: &mut Statement| -> Result<(), crate::Error>
 		{
 			let step_title = match statement.proof_status
 			{
@@ -319,6 +319,14 @@ impl Problem
 			self.shell.borrow_mut().print(&format!("{}: ", statement.kind),
 				&termcolor::ColorSpec::new())?;
 
+			match statement.kind
+			{
+				StatementKind::CompletedDefinition(_)
+				| StatementKind::IntegrityConstraint =>
+					crate::autoname_variables(&mut statement.formula),
+				_ => (),
+			}
+
 			print!("{}", statement.formula);
 
 			Ok(())
@@ -508,7 +516,7 @@ impl<'p> std::fmt::Display for ProblemTPTPDisplay<'p>
 			last_symbolic_constant = Some(std::rc::Rc::clone(symbolic_constant));
 		}
 
-		for (section_kind, statements) in self.0.statements.borrow().iter()
+		for (section_kind, statements) in self.0.statements.borrow_mut().iter_mut()
 		{
 			if statements.is_empty()
 			{
@@ -530,7 +538,7 @@ impl<'p> std::fmt::Display for ProblemTPTPDisplay<'p>
 
 			let mut i = 0;
 
-			for statement in statements.iter()
+			for statement in statements.iter_mut()
 			{
 				if let StatementKind::CompletedDefinition(_) = statement.kind
 				{
@@ -561,6 +569,15 @@ impl<'p> std::fmt::Display for ProblemTPTPDisplay<'p>
 					ProofStatus::Ignored => continue,
 				};
 
+				// TODO: avoid doing this twice
+				match statement.kind
+				{
+					StatementKind::CompletedDefinition(_)
+					| StatementKind::IntegrityConstraint =>
+						crate::autoname_variables(&mut statement.formula),
+					_ => (),
+				}
+
 				// TODO: add proper statement type
 				writeln!(formatter, "tff({}, {}, {}).", name, statement_type,
 					crate::output::tptp::display_formula(&statement.formula))?;

src/translate/verify_properties.rs

@@ -149,8 +149,6 @@ impl<'p> Translator<'p>
 			let mut completed_definition = completed_definition(predicate_declaration,
 				&mut self.definitions);
 
-			crate::autoname_variables(&mut completed_definition);
-
 			//crate::simplify(&mut completed_definition);
 
 			let statement_name =