Change formatting of negative numbers from -x to (- x) to be SMTL…

…IB2 compliant

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 {

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

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))

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"))),
+  ]))),
+])))

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

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")]

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));
-    }
-}

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"),
+    }
+}

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 {