rust z3 并行求解所有可行值

Question

详情

我有一个需求，就是求出所有可行的结果，而表达式只有未知。我用rust z3来做，但是效率太慢了！

我的想法

例如，我有一个像“param < 123456789".

在我的代码中：

1. 我会先解决一个 mid_value
2. 我会逐渐添加断言，这个断言就像“param != mid_value”。
3. 如此反复，也许我能得到所有可行的值。

我的代码

pub fn evaluate_exp_with_unknown(_expression: &str) -> Result<(u128, u128), ExpressionCaclError> {
    // z3上下文以及求解器
    let cfg = Config::new();
    let ctx = Context::new(&cfg);
    let solver = Solver::new(&ctx);
    // 去除空格
    let _expression = _expression.replace(" ", "");
    // 用&&分割表达式
    let _expressions = _expression.split("&&");

    // 得到变量，此时的exp应该只有一个未知数
    let temps = get_all_variables(&_expression);
    // 第一个即为未知数
    let param = temps.first().unwrap();
    // 创建z3未知数
    let x = Int::new_const(&ctx, param.as_str());
    // 添加基本约束，未知数>0
    solver.assert(&x.ge(&Int::from_i64(&ctx, 0)));

    // 遍历每个表达式，为求解器分别加上约束
    for _exp in _expressions {
        println!("now expression {:?}", _exp);
        // 得到中缀表达式
        let re = Regex::new(r"([a-zA-Z_][a-zA-Z0-9_]*|[0-9]+|[+\-*/()<>!=])").unwrap();
        let infix: Vec<String> = re
            .find_iter(_exp.as_bytes())
            .map(|mat| String::from_utf8(mat.as_bytes().to_vec()).unwrap())
            .collect();
        println!("infix {:?}", infix);

        // 中缀转后缀
        let y = infix_to_postfix(infix);
        println!("表达式 {:?}", y);
        // 计算后缀表达式，为求解器加上约束
        evaluate_postfix_with_unknown(&solver, y.clone(), x.clone());
        // println!("now constraint {:?}", &solver.get_assertions());
    }
    let mut _new_param: Vec<u128> = vec![];
    let context = solver.get_context();
    for ether in (1_000_000_000_000_000_000u64..=10_000_000_000_000_000_000)
        .step_by(1_000_000_000_000_000_000)
    {
        let ether_value = ast::Int::from_u64(context, ether);
        solver.push(); // 保留回退点
        solver.assert(&x._eq(&ether_value)); // 添加约束

        match solver.check() {
            SatResult::Sat => {
                println!("{:?} 是解", ether_value);
                // 如果 ether 是解，添加 param >= ether 的约束
                solver.pop(1); // 回退到之前的状态
                solver.push(); // 保存当前状态
                solver.assert(&x.gt(&ether_value));
            }
            SatResult::Unsat | SatResult::Unknown => {
                solver.pop(1); // 回退到之前的状态
                if !ether.eq(&1_000_000_000_000_000_000u64) {
                    _new_param.push((ether - 1_000_000_000_000_000_000u64) as u128);
                }
                break;
            }
        }
    }
    println!("经过初次筛选后的范围长度{:?}", _new_param[0]);
    println!("当前求解器的约束{:?}", solver.get_assertions());
    // todo 求解太慢了，需要进行并行计算，但是z3并不能在多线程中安全使用
    match solver.check() {
        SatResult::Sat => {
            // 找到第一个解
            let mut mid_value = solver.get_model().unwrap().eval(&x, true).unwrap();
            println!("第一个解 {:?}", mid_value);
            // 保留
            _new_param.push(mid_value.as_u64().unwrap().into());
            // 做循环，直到没有解情况
            loop {
                // 保留回退点
                solver.push();
                // 添加约束，需要当前解不重复
                solver.assert(&x._eq(&mid_value).not());
                // 检查是否有解
                match solver.check() {
                    SatResult::Sat => {
                        // 更新解
                        mid_value = solver.get_model().unwrap().eval(&x, true).unwrap();
                        println!("{:?}是解", mid_value);
                        // 插入解
                        _new_param.push(mid_value.as_u64().unwrap().into());
                    }
                    SatResult::Unsat | SatResult::Unknown => {
                        // 无解则break
                        solver.pop(1);
                        break;
                    }
                }
            }
        }
        SatResult::Unsat | SatResult::Unknown => {
            return Err(ExpressionCaclError::SyntaxError);
        }
    }
    // 返回值
    let (max, min) = find_max_min(&_new_param).unwrap();
    Ok((min, max))
}

问题

1. 效率太慢
2. 如何并行求解
3. 有更好的方法来解决吗？

Answer 1

听起来你想解决 all-sat 问题，即返回所有令人满意的假设。并行解决此类查询通常效果不佳，除非您尝试解决的确切问题相对简单。最著名的方法，尤其是对于位向量问题，是分而治之的方法，这里解释：https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-blocking-evaluations

这里提出的解决方案是用 Python 编写的。我不确定 rust-z3 人员是否在他们的绑定中实现了相同的功能。如果没有，您要么必须自己实施，要么要求他们这样做。或者，如果您不被迫使用 rust，您可以使用 Python，或者改用 Haskell，它附带了一个 allSat 实现，可以开箱即用地实现这个想法。