details

I have a requirement,which is solve all feasible result,and the expression have only unknown.I use rust z3 to do that,but efficiency too slow!

my thinking

For example,I have a expression like “param < 123456789”.

In my code:

1. I will solve a mid_value first
2. I will gradually add assertions,this assertions like “param != mid_value”.
3. Repeatedly,maybe i can get all feasible values.

my code

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))
}

questions

1. effiency too slow
2. how to parallel to solve
3. Is better way to solve it ?