Add support for parsing negative solution values

[pleich]

Description

This PR would add support for solutions that contain negative integers.

Currently, the problem with negative solutions is that the SMT solver will return for example (x (- 2)) a solution to x < 0 . When calling get, this solution will be parsed into an SExprData::List . Calling try_from_int will then return always return the error NotAnAtom.

This PR introduces a new variant of SExprData, which is a special case of SExprData::List, which is returned for lists that contain exactly two atoms , where the first one is either + or -.

Additionally it fixes typos in comments.

Minimal Test

use easy_smt::{ContextBuilder, Response};

#[test]
fn test_negative_integers() {
    let mut ctx = ContextBuilder::new()
        .solver("z3")
        .solver_args(["-smt2", "-in"])
        .build()
        .unwrap();

    let x = ctx.declare_const("x", ctx.int_sort()).unwrap();

    ctx.assert(ctx.lt(x, ctx.numeral(0))).unwrap();

    assert_eq!(ctx.check().unwrap(), Response::Sat);

    let solution = ctx.get_value(vec![x]).unwrap();
    let sol_x = ctx.get(solution[0].1);

    let sol = i64::try_from(sol_x).expect("Failed to parse");
    assert!(sol < 0)
}

[fitzgen]

Thanks for opening the issue and draft PR.

I think I'd prefer adding methods to extract {u,i}{8,16,32,64,128,size} to Context that explicitly check for and handle this case, rather than a whole new variant to SExprData and the underlying arena representation.

Something like

impl Context {
    // Existing

    pub fn get(&self, expr: SExpr) -> SExprData { ... }

    // New

    pub fn get_atom(&self, expr: SExpr) -> Option<&str> { ... }
    pub fn get_str(&self, expr: SExpr) -> Option<&str> { ... }
    pub fn get_list(&self, expr: SExpr) -> Option<&[SExpr]> { ... }

    pub fn get_u8(&self, expr: SExpr) -> Option<u8> { ... }
    pub fn get_u16(&self, expr: SExpr) -> Option<u16> { ... }
    // etc...

    pub fn get_i8(&self, expr: SExpr) -> Option<i8> { ... }
    pub fn get_i16(&self, expr: SExpr) -> Option<i16> { ... }
    // etc...
}

And maybe also is_* variants of all those things

[pleich]

Thanks for opening the issue and draft PR.

I think I'd prefer adding methods to extract {u,i}{8,16,32,64,128,size} to Context that explicitly check for and handle this case, rather than a whole new variant to SExprData and the underlying arena representation.

Something like

impl Context {
    // Existing

    pub fn get(&self, expr: SExpr) -> SExprData { ... }

    // New

    pub fn get_atom(&self, expr: SExpr) -> Option<&str> { ... }
    pub fn get_str(&self, expr: SExpr) -> Option<&str> { ... }
    pub fn get_list(&self, expr: SExpr) -> Option<&[SExpr]> { ... }

    pub fn get_u8(&self, expr: SExpr) -> Option<u8> { ... }
    pub fn get_u16(&self, expr: SExpr) -> Option<u16> { ... }
    // etc...

    pub fn get_i8(&self, expr: SExpr) -> Option<i8> { ... }
    pub fn get_i16(&self, expr: SExpr) -> Option<i16> { ... }
    // etc...
}

And maybe also is_* variants of all those things

I implemented your proposed interface in daa988e.

I have chosen not to implement is_* methods, since this would involve trying to parse the integers from the strings returned by the SMT solver. Otherwise, the check using is_* might succeed but subsequent get call might not, which in my opinion would be confusing. Therefore I decided to only implement the get_* methods.

Let me know what you think about the implementation

[fitzgen]

Thanks!

One nitpick below before we can merge this plus another optional thing that you can take or leave

[fitzgen]

I think this is fine to land as-is, but ideally we would avoid the .to_owned() here and the allocation it implies, and instead always parse the integer as the unsigned version at that width and then negate it if necessary.

Something like

fn try_parse_t(a: &str, radix: u32, negative: bool) -> Option<Self> {
    let unsigned = <$unsigned_ty>::from_str_radix(a, radix).ok()?;
    let signed = <$signed_ty>::try_from(unsigned).ok()?;
    if negative {
        signed.checked_neg()
    } else {
        Some(signed)
    }
}

If you don't feel up for tackling that in this PR, would you mind filing a follow-up issue for this change?

[pleich]

I agree that the allocation is unnecessary here. But maybe this is a more compact version:

fn try_parse_t(a: &str, negate: bool) -> Option<Self> {
  let x = if let Some(a) = a.strip_prefix("#x") {
       <$ty>::from_str_radix(a, 16).ok()?
  } else if let Some(a) = a.strip_prefix("#b") {
       <$ty>::from_str_radix(a , 2).ok()?
  } else {
       a.parse::<$ty>().ok()?
   };

   if negate {
       return x.checked_neg();
   }

   Some(x)
}

Added in 9b1ca34

[fitzgen]

Looks great modulo one final nitpick

[pleich]

Fixed it :)

[fitzgen]

Thanks! And thanks for going through multiple iterations of this PR