From 787a671cd88f93253fbfdb4be70b35cd838f19ef Mon Sep 17 00:00:00 2001
From: oeb25 <oliverboving@gmail.com>
Date: Thu, 12 Sep 2024 10:26:01 +0200
Subject: [PATCH] Change formatting of negative numbers from `-x` to `(- x)` to
 be SMTLIB2 compliant

---
 lowlevel/src/lexicon.rs                       |  6 ++-
 ...wlevel__tests__z3__negative_numbers-2.snap |  5 +++
 ...wlevel__tests__z3__negative_numbers-3.snap |  5 +++
 ...wlevel__tests__z3__negative_numbers-4.snap |  9 +++++
 ...lowlevel__tests__z3__negative_numbers.snap |  5 +++
 lowlevel/src/tests.rs                         | 12 ++++++
 smtlib/src/lib.rs                             | 31 +---------------
 smtlib/src/tests.rs                           | 37 +++++++++++++++++++
 smtlib/src/theories/ints.rs                   |  7 +++-
 9 files changed, 85 insertions(+), 32 deletions(-)
 create mode 100644 lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-2.snap
 create mode 100644 lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-3.snap
 create mode 100644 lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-4.snap
 create mode 100644 lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers.snap
 create mode 100644 smtlib/src/tests.rs

diff --git a/lowlevel/src/lexicon.rs b/lowlevel/src/lexicon.rs
index 88bbdf6..be85971 100644
--- a/lowlevel/src/lexicon.rs
+++ b/lowlevel/src/lexicon.rs
@@ -5,7 +5,11 @@ use crate::parse::{ParseError, Parser, Token};
 pub struct Numeral(pub String);
 impl std::fmt::Display for Numeral {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "{}", self.0)
+        if let Some(rest) = self.0.strip_prefix('-') {
+            write!(f, "(- {rest})")
+        } else {
+            write!(f, "{}", self.0)
+        }
     }
 }
 impl SmtlibParse for Numeral {
diff --git a/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-2.snap b/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-2.snap
new file mode 100644
index 0000000..d940a9c
--- /dev/null
+++ b/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-2.snap
@@ -0,0 +1,5 @@
+---
+source: lowlevel/src/tests.rs
+expression: "d.exec(&Command::parse(r#\"(assert (< x 0))\"#)?)?"
+---
+Success
diff --git a/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-3.snap b/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-3.snap
new file mode 100644
index 0000000..968f83c
--- /dev/null
+++ b/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-3.snap
@@ -0,0 +1,5 @@
+---
+source: lowlevel/src/tests.rs
+expression: "d.exec(&Command::parse(r#\"(check-sat)\"#)?)?"
+---
+SpecificSuccessResponse(CheckSatResponse(Sat))
diff --git a/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-4.snap b/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-4.snap
new file mode 100644
index 0000000..6536c6f
--- /dev/null
+++ b/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers-4.snap
@@ -0,0 +1,9 @@
+---
+source: lowlevel/src/tests.rs
+expression: "d.exec(&Command::parse(r#\"(get-model)\"#)?)?"
+---
+SpecificSuccessResponse(GetModelResponse(GetModelResponse([
+  DefineFun(FunctionDef(Symbol("x"), [], Sort(Simple(Symbol("Int"))), Application(Identifier(Simple(Symbol("-"))), [
+    SpecConstant(Numeral(Numeral("2"))),
+  ]))),
+])))
diff --git a/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers.snap b/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers.snap
new file mode 100644
index 0000000..8722d80
--- /dev/null
+++ b/lowlevel/src/snapshots/smtlib_lowlevel__tests__z3__negative_numbers.snap
@@ -0,0 +1,5 @@
+---
+source: lowlevel/src/tests.rs
+expression: "d.exec(&Command::parse(r#\"(declare-const x Int)\"#)?)?"
+---
+Success
diff --git a/lowlevel/src/tests.rs b/lowlevel/src/tests.rs
index dc347a5..58146f1 100644
--- a/lowlevel/src/tests.rs
+++ b/lowlevel/src/tests.rs
@@ -30,6 +30,18 @@ mod z3 {
 
         Ok(())
     }
+
+    #[test]
+    fn negative_numbers() -> Result<(), Box<dyn std::error::Error>> {
+        let mut d = Driver::new(Z3Binary::new("z3")?)?;
+
+        cmd!(d, r#"(declare-const x Int)"#);
+        cmd!(d, r#"(assert (< x (- 1)))"#);
+        cmd!(d, r#"(check-sat)"#);
+        cmd!(d, r#"(get-model)"#);
+
+        Ok(())
+    }
 }
 
 #[cfg(feature = "z3-static")]
diff --git a/smtlib/src/lib.rs b/smtlib/src/lib.rs
index 50a08c5..135dd7b 100644
--- a/smtlib/src/lib.rs
+++ b/smtlib/src/lib.rs
@@ -22,6 +22,8 @@ pub mod funs;
 mod solver;
 pub mod sorts;
 pub mod terms;
+#[cfg(test)]
+mod tests;
 pub mod theories;
 
 pub use solver::Solver;
@@ -187,32 +189,3 @@ impl Model {
         Some(self.values.get(x.name().trim_matches('|'))?.clone().into())
     }
 }
-
-#[cfg(test)]
-mod tests {
-    use terms::StaticSorted;
-
-    use crate::terms::{forall, Sorted};
-
-    use super::*;
-
-    #[test]
-    fn int_math() {
-        let x = Int::new_const("x");
-        let y = Int::new_const("hello");
-        // let x_named = x.labeled();
-        let mut z = 12 + y * 4;
-        z += 3;
-        let w = x * x + z;
-        println!("{w}");
-    }
-
-    #[test]
-    fn quantifiers() {
-        let x = Int::new_const("x");
-        let y = Int::new_const("y");
-
-        let res = forall((x, y), (x + 2)._eq(y));
-        println!("{}", ast::Term::from(res));
-    }
-}
diff --git a/smtlib/src/tests.rs b/smtlib/src/tests.rs
new file mode 100644
index 0000000..94168a7
--- /dev/null
+++ b/smtlib/src/tests.rs
@@ -0,0 +1,37 @@
+use terms::StaticSorted;
+
+use crate::terms::{forall, Sorted};
+
+use super::*;
+
+#[test]
+fn int_math() {
+    let x = Int::new_const("x");
+    let y = Int::new_const("hello");
+    // let x_named = x.labeled();
+    let mut z = 12 + y * 4;
+    z += 3;
+    let w = x * x + z;
+    println!("{w}");
+}
+
+#[test]
+fn quantifiers() {
+    let x = Int::new_const("x");
+    let y = Int::new_const("y");
+
+    let res = forall((x, y), (x + 2)._eq(y));
+    println!("{}", ast::Term::from(res));
+}
+
+#[test]
+fn negative_numbers() {
+    let mut solver = Solver::new(crate::backend::z3_binary::Z3Binary::new("z3").unwrap()).unwrap();
+    let x = Int::new_const("x");
+    solver.assert(x.lt(-1)).unwrap();
+    let model = solver.check_sat_with_model().unwrap().expect_sat().unwrap();
+    match model.eval(x) {
+        Some(x) => println!("This is the value of x: {x}"),
+        None => panic!("Oh no! This should never happen, as x was part of an assert"),
+    }
+}
diff --git a/smtlib/src/theories/ints.rs b/smtlib/src/theories/ints.rs
index 5891fe7..3ff55ce 100644
--- a/smtlib/src/theories/ints.rs
+++ b/smtlib/src/theories/ints.rs
@@ -1,6 +1,6 @@
 #![doc = concat!("```ignore\n", include_str!("./Ints.smt2"), "```")]
 
-use smtlib_lowlevel::ast::Term;
+use smtlib_lowlevel::{ast::Term, lexicon::Numeral};
 
 use crate::{
     impl_op,
@@ -54,7 +54,10 @@ impl StaticSorted for Int {
 }
 impl From<i64> for Int {
     fn from(i: i64) -> Self {
-        Term::Identifier(qual_ident(i.to_string(), None)).into()
+        Term::SpecConstant(smtlib_lowlevel::ast::SpecConstant::Numeral(Numeral(
+            i.to_string(),
+        )))
+        .into()
     }
 }
 impl Int {