Probleam in Rust version "mul" and "mul_towards_zero" function

[FoxMakarov]

Hello, everyone.

I am using the z3 solver with Rust language version v 0.10.0.

I encountered some issues while using the z3:: ast:: Float struction. I noticed that Float only has two functions related to multiplication, namely "mul" and "mul_towards_zero". In my scenario, I would like to multiply two Float type variables with actual values ranging from 0 to 1, similar to 0.35.
Here is my test code.

        let mut config = z3::Config::new();
        config.set_bool_param_value("auto_config", false);
        config.set_model_generation(true);
        let context = z3::Context::new(&config);

        let solver2 = z3::Solver::new(context);
        let f1 = Float::from_f64(&context, 1.0);
        let f2 = Float::from_f64(&context, 2.5);
        let f3 = Float::from_f64(&context, 3.5);
       
        let f4 = Float::fresh_const_double(&context, "test_res");
        let f5 = f1.mul(&f2, &f3);// thread 'main' panicked at /home/lzr/.cargo/registry/src/rsproxy.cn-0dccff568467c15b/z3-0.10.0/src/ast.rs:480:1:
                                  // assertion failed: !ast.is_null()
        let q = f4._eq(&Float::mul_towards_zero( &f2, &f3));
        solver2.assert(&q);

        match solver2.check() {
            z3::SatResult::Sat => {
                let model = solver2.get_model();
                let r1 = Option::as_ref(&model).unwrap().eval(&f4).unwrap().to_string();
                println!("{:?}", r1);  // fp # b0 # b10000000010 # x1800000000
            }
            z3::SatResult::Unsat => {
                println!("unsat");
            }
            z3::SatResult::Unknown => {
                println!("unknown");
            }
        }

When I use the "mul" function, which is f5 mentioned above, the program will report an error. I don't know if it's a problem with the parameter settings of my mul, or if there's a problem with the context, because after opening the source code, I realized that there might be a need for a field called RoundingMode? But there is no RoundingMode parameter in the function signature "pub fn mul(&self, a: &Self, b: &Self) -> Self". And must this function only multiply three numbers continuously, "f1 * f2 * f3"? I'm confused.

So I can only use the "mul_towards_zero" function. From its name, this function should ignore the decimal part after multiplication? I tried using a value as the output for 2.5 and 3.5. After the operation is completed, I noticed that the base representation of the operation result is "fp # b0 # b10000000010 # x1800000000" converted to float64, which is 8.75 when converted to decimal. This result doesn't been convert to 8? (And I also noticed that Float doesn't have a similar function Int::as_u32 which can be directly converted into the data structure of Rust). So does this function really not ignore decimals? If I want to use 0.35 * 0.064, i can get the right answer which means the result will not be converted to 0?

Please help me!

[wintersteiger]

Yes, that crate looks very incomplete and I would not be surprised if you were the first user of their float functions. They have known issues with mul and other functions, e.g. prove-rs/z3.rs#291. AFAIK, this create is not maintained by the Z3 team, so I think it's best to interact with them via their issue tracker.

[FoxMakarov]

Ok， Thanks！