C++环境下如何将字符串格式约束转换为Z3求解器的expr表达式

前置修正 #

原有代码存在两处Z3 C++ API使用错误，先修正为可运行的基础定义：

z3::context c;
// 创建int类型变量常量
z3::expr number = c.int_const("number");
// 创建string类型变量常量（注意：string_val是字符串字面量，不是可绑定变量）
z3::expr name = c.string_const("name");

核心实现逻辑 #

要实现字符串约束转Z3 expr，需要完成三个核心步骤：

• 维护变量名到已定义Z3常量的映射表，避免重复创建变量
• 实现递归下降解析器，按运算符优先级拆解中缀表达式
• 遇到字面量时调用Z3对应接口创建节点，遇到变量时从映射表取已定义的expr

完整代码实现 #

#include <z3++.h>
#include <unordered_map>
#include <string>
#include <cctype>
#include <stdexcept>

using namespace z3;

// 工具函数：跳过字符串中的空白字符
void skip_whitespace(const std::string& s, size_t& pos) {
    while (pos < s.size() && std::isspace(s[pos])) pos++;
}

// 前置声明：解析整个表达式的入口函数
expr parse_expr(const std::string& s, size_t& pos, context& ctx, const std::unordered_map<std::string, expr>& var_map);

// 解析原子表达式：变量、字面量、括号包裹的子表达式
expr parse_atom(const std::string& s, size_t& pos, context& ctx, const std::unordered_map<std::string, expr>& var_map) {
    skip_whitespace(s, pos);
    if (pos >= s.size()) throw std::runtime_error("输入意外结束");

    // 处理括号包裹的子表达式
    if (s[pos] == '(') {
        pos++; // 跳过左括号
        expr sub_expr = parse_expr(s, pos, ctx, var_map);
        skip_whitespace(s, pos);
        if (pos >= s.size() || s[pos] != ')') throw std::runtime_error("缺少右括号");
        pos++; // 跳过右括号
        return sub_expr;
    }

    // 处理带双引号的字符串字面量
    if (s[pos] == '"') {
        pos++; // 跳过开头双引号
        size_t start = pos;
        while (pos < s.size() && s[pos] != '"') pos++;
        if (pos >= s.size()) throw std::runtime_error("字符串字面量未闭合");
        std::string str_val = s.substr(start, pos - start);
        pos++; // 跳过结尾双引号
        return ctx.string_val(str_val);
    }

    // 处理数字字面量
    if (std::isdigit(s[pos])) {
        size_t start = pos;
        while (pos < s.size() && std::isdigit(s[pos])) pos++;
        int num = std::stoi(s.substr(start, pos - start));
        return ctx.int_val(num);
    }

    // 处理变量标识符
    if (std::isalpha(s[pos]) || s[pos] == '_') {
        size_t start = pos;
        while (pos < s.size() && (std::isalnum(s[pos]) || s[pos] == '_')) pos++;
        std::string var_name = s.substr(start, pos - start);
        if (!var_map.count(var_name)) throw std::runtime_error("未定义的变量: " + var_name);
        return var_map.at(var_name);
    }

    throw std::runtime_error("非法字符: " + std::string(1, s[pos]));
}

// 处理一元非运算 !
expr parse_unary(const std::string& s, size_t& pos, context& ctx, const std::unordered_map<std::string, expr>& var_map) {
    skip_whitespace(s, pos);
    if (pos < s.size() && s[pos] == '!') {
        pos++;
        return !parse_unary(s, pos, ctx, var_map);
    }
    return parse_atom(s, pos, ctx, var_map);
}

// 处理比较运算: < > <= >= == !=
expr parse_cmp(const std::string& s, size_t& pos, context& ctx, const std::unordered_map<std::string, expr>& var_map) {
    expr left = parse_unary(s, pos, ctx, var_map);
    skip_whitespace(s, pos);
    while (pos + 1 < s.size()) {
        if (s[pos] == '=' && s[pos+1] == '=') {
            pos += 2;
            expr right = parse_unary(s, pos, ctx, var_map);
            left = (left == right);
        } else if (s[pos] == '!' && s[pos+1] == '=') {
            pos += 2;
            expr right = parse_unary(s, pos, ctx, var_map);
            left = (left != right);
        } else if (s[pos] == '<' && s[pos+1] == '=') {
            pos += 2;
            expr right = parse_unary(s, pos, ctx, var_map);
            left = (left <= right);
        } else if (s[pos] == '>' && s[pos+1] == '=') {
            pos += 2;
            expr right = parse_unary(s, pos, ctx, var_map);
            left = (left >= right);
        } else if (s[pos] == '<') {
            pos += 1;
            expr right = parse_unary(s, pos, ctx, var_map);
            left = (left < right);
        } else if (s[pos] == '>') {
            pos += 1;
            expr right = parse_unary(s, pos, ctx, var_map);
            left = (left > right);
        } else {
            break;
        }
        skip_whitespace(s, pos);
    }
    return left;
}

// 处理逻辑与 &&
expr parse_and(const std::string& s, size_t& pos, context& ctx, const std::unordered_map<std::string, expr>& var_map) {
    expr left = parse_cmp(s, pos, ctx, var_map);
    skip_whitespace(s, pos);
    while (pos + 1 < s.size() && s[pos] == '&' && s[pos+1] == '&') {
        pos += 2;
        expr right = parse_cmp(s, pos, ctx, var_map);
        left = left && right;
        skip_whitespace(s, pos);
    }
    return left;
}

// 处理逻辑或 ||（最低优先级）
expr parse_expr(const std::string& s, size_t& pos, context& ctx, const std::unordered_map<std::string, expr>& var_map) {
    expr left = parse_and(s, pos, ctx, var_map);
    skip_whitespace(s, pos);
    while (pos + 1 < s.size() && s[pos] == '|' && s[pos+1] == '|') {
        pos += 2;
        expr right = parse_and(s, pos, ctx, var_map);
        left = left || right;
        skip_whitespace(s, pos);
    }
    return left;
}

// 对外暴露的procedure函数：传入约束字符串、Z3上下文、变量映射表
expr procedure(const std::string& constraint_str, context& ctx, const std::unordered_map<std::string, expr>& var_map) {
    size_t pos = 0;
    expr res = parse_expr(constraint_str, pos, ctx, var_map);
    if (pos != constraint_str.size()) {
        throw std::runtime_error("输入存在尾部多余字符: " + constraint_str.substr(pos));
    }
    return res;
}

使用示例 #

int main() {
    context c;
    // 定义所需的变量常量
    expr number = c.int_const("number");
    expr name = c.string_const("name");
    // 构建变量名到Z3常量的映射表
    std::unordered_map<std::string, expr> var_map = {
        {"number", number},
        {"name", name}
    };
    // 解析约束字符串
    expr constrain = procedure("(number < 10) && (name == \"hello\")", c, var_map);
    // 可直接传入Z3 solver验证
    solver s(c);
    s.add(constrain);
    // 输出sat，证明约束解析正确
    std::cout << s.check() << std::endl;
    return 0;
}

扩展说明 #

• 该实现支持括号、比较运算、逻辑与/或/非，可按需扩展算术运算（+ - * /）等语法规则
• 变量映射表必须传入已经初始化的Z3常量，避免解析时新建变量导致符号不匹配
• 解析错误可根据业务需求调整抛出逻辑，当前实现的错误信息便于调试

内容的提问来源于stack exchange，提问作者Jocelyn