From 02ea63fb3e9cb4035ce3a2ccbf1a3ebf2c92a9b4 Mon Sep 17 00:00:00 2001 From: Bruno Andreotti Date: Fri, 23 Feb 2024 09:20:56 -0300 Subject: [PATCH] Correctly parse division terms as Real literals --- carcara/src/parser/mod.rs | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/carcara/src/parser/mod.rs b/carcara/src/parser/mod.rs index daeab83c..d13676e8 100644 --- a/carcara/src/parser/mod.rs +++ b/carcara/src/parser/mod.rs @@ -14,7 +14,7 @@ use crate::{ }; use error::assert_num_args; use indexmap::{IndexMap, IndexSet}; -use rug::Integer; +use rug::{Integer, Rational}; use std::{io::BufRead, str::FromStr}; use self::error::assert_indexed_op_args_value; @@ -257,6 +257,17 @@ impl<'a, R: BufRead> Parser<'a, R> { SortError::assert_eq(&Sort::Real, sorts[0])?; SortError::assert_all_eq(&sorts)?; } + + // If the term is a division between two positive integer constants, and their GCD + // is 1, then it should be interpreted as a rational literal. The only exception to + // this is the term '(/ 1 1)', which is still interpreted as a divison term. + if let Some(a) = args[0].as_integer() { + if let Some(b) = args[1].as_integer() { + if a > 0 && b > 0 && !(a == 1 && b == 1) && a.clone().gcd(&b) == 1 { + return Ok(self.pool.add(Term::new_real(Rational::from((a, b))))); + } + } + } } Operator::Mod => { assert_num_args(&args, 2)?;