prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

Can't convert dynamic coming from array into DataType #299

Closed CyrilFMoser closed 3 months ago

CyrilFMoser commented 3 months ago

In the following code:

let mut typ = DatatypeBuilder::new(&ctx, "Type")
            .variant(
                "Base",
                vec![
                    ("base_name", DatatypeAccessor::Sort(Sort::string(&ctx))),
                    (
                        "base_typargs",
                        DatatypeAccessor::Sort(Sort::array(
                            &ctx,
                            &Sort::int(&ctx),
                            &Sort::uninterpreted(&ctx, Symbol::String("Type".to_string())),
                        )),
                    ),
                ],
            ).finish();

let valid = RecFuncDecl::new(ctx, "valid", &[&typ.sort], &Sort::bool(ctx));
let t = Datatype::new_const(ctx, "t", &typ.sort);

let typarg_accessor = typ.variants.first().unwrap().accessors.get(1).unwrap();
let typarg_array = typarg_accessor.apply(&[&t]).as_array().unwrap();

let cur_typarg = typarg_array.select(&Int::from_u64(ctx, 0)); // cur_typarg.as_datatype() returns a None value
let appl = valid.apply(&[&cur_typarg]);

In the second last line, I can't convert the dynamic, and if I don't try to do any conversion and just pass the dynamic directly to valid.apply(), then I get: assertion failed: !ast.is_null()

Is this intended? If so what am I doing wrong?

Edit: might be related to https://github.com/prove-rs/z3.rs/issues/149