Adding support for Reals

[pleich]

This PR would add support for Real values. In more detail:

• It adds the type real, with the helper method real_sort
• It adds the method con_to_real for converting Int values to reals
• It adds the method rdiv which corresponds to division for reals (i.e. /)
• It adds support for parsing real valued solutions (see below)

On Parsing Real Solutions

As it turns out, parsing the satisfying assignment for solutions to real values is not as straightforward. In many cases, the SMT solver will represent a solution as a fraction, e.g. if it assigns the value 2.5 to a variable, when asked for the solution, it will return it as the expression / 5.0 2.0.

For my project, I am fine with the loss of precision when evaluating this expression to an f32 or f64. The get_f32 and get_f64 methods in this PR will evaluate this expression and return the result. However, if this is not desired, the next section discusses possible alternatives.

I have written a small test that should check all possible variations of solutions that can be returned by the SMT solver:

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

    let x = ctx.declare_const("x", ctx.real_sort()).unwrap();
    // x == 2.0
    ctx.assert(ctx.eq(x, ctx.decimal(2.0))).unwrap();
    assert_eq!(ctx.check().unwrap(), Response::Sat);
    let solution = ctx.get_value(vec![x]).unwrap();
    let sol = ctx.get_f64(solution[0].1).unwrap();
    // Z3 returns `2.0`
    assert!(sol == 2.0, "Expected solution to be 2.5, got {}", sol);

    let y = ctx.declare_const("y", ctx.real_sort()).unwrap();
    // y == -2.0
    ctx.assert(ctx.eq(y, ctx.decimal(-2.0))).unwrap();
    assert_eq!(ctx.check().unwrap(), Response::Sat);
    let solution = ctx.get_value(vec![y]).unwrap();
    let sol = ctx.get_f64(solution[0].1).unwrap();
    // Z3 returns `- 2.0`
    assert!(sol == -2.0, "Expected solution to be 2.5, got {}", sol);

    let z = ctx.declare_const("z", ctx.real_sort()).unwrap();
    // z == 2.5 / 1.0
    ctx.assert(ctx.eq(z, ctx.rdiv(ctx.decimal(2.5), ctx.decimal(1.0))))
        .unwrap();
    assert_eq!(ctx.check().unwrap(), Response::Sat);
    let solution = ctx.get_value(vec![z]).unwrap();
    let sol = ctx.get_f64(solution[0].1).unwrap();
    // Z3 returns `(/ 5.0 2.0)`
    assert!(sol == 2.5, "Expected solution to be 2.5, got {}", sol);

    let a = ctx.declare_const("a", ctx.real_sort()).unwrap();
    // a == 2.5 / -1.0
    ctx.assert(ctx.eq(a, ctx.rdiv(ctx.decimal(2.5), ctx.decimal(-1.0))))
        .unwrap();
    assert_eq!(ctx.check().unwrap(), Response::Sat);
    let solution = ctx.get_value(vec![a]).unwrap();
    let sol = ctx.get_f64(solution[0].1).unwrap();
    // Z3 returns `(- (/ 5.0 2.0))`
    assert!(sol == -2.5, "Expected solution to be -2.5, got {}", sol);
}

Possible Alternatives

If the loss of precision that occurs when parsing the solution is not desired, I see two alternatives:

• Explicitly have functions like get_numerator and get_denominator
• Defining / importing a fractional type (possibly hidden behind a feature flag)

Let me know your thoughts!

[elliottt]

I'll do a more detailed review tonight, but I think that only supporting f32 and f64 is fine for now. Thank you for the contribution!

[elliottt]

I think this is looking good, thank you for fixing this!

Would you mind adding the test you wrote in a way that we can check it in CI?

[pleich]

@elliottt I forgot to add the test. I added in 604ebe2 as a separate file in the tests folder

[elliottt]

The test you added looks good, thank you! An alternative to fixing the assertion messages would be to use assert_eq!; the only thing I'm really worried about is making sure that the test failures are meaningful.

[elliottt]

Suggested change

	assert!(sol == 2.0, "Expected solution to be 2.5, got {}", sol);
	assert!(sol == 2.0, "Expected solution to be 2.0, got {}", sol);

[pleich]

Great that you caught that, I never properly updated the messages after using them for debugging.
Since I already used assert_eq! for checking the response, I changed all assertions assert_eq! in 4390749

[elliottt]

Suggested change

	assert!(sol == -2.0, "Expected solution to be 2.5, got {}", sol);
	assert!(sol == -2.0, "Expected solution to be -2.0, got {}", sol);

[pleich]

Great that you caught that, I never properly updated the messages after using them for debugging.
Since I already used assert_eq! for checking the response, I changed all assertions assert_eq! in 4390749

[elliottt]

Thank you!