请写一段c++代码完成以下工作：在调用z3求解器的c++API进行求解时，定义一个bitvector类型符号，对其添加一个位向量约束，然后将其转换为int型，在转换为float型，对其添加一个float型约束后求解该符号（不使用ast_manager

为了使用Z3求解器的C++ API，你需要先包含必要的头文件并设置好环境。以下是一个简化的示例，展示了如何定义一个位向量符号、添加位向量约束以及将其转换为整数和浮点数进行约束。请注意，这个例子假设你已经安装了Z3库并且知道如何初始化`context`和`solver`。

#include <z3++.h>

// 创建Z3上下文
using namespace z3;

int main() {
    // 初始化Z3上下文
    Context ctx;
    std::string solver_name = "boolector"; // 如果你想用 Boolector 解求器，替换为对应的名称
    Solver solver(ctx, solver_name);

    // 定义一个位向量符号，这里假设我们有8个位
    unsigned n_bits = 8;
    BitVec sort("x", n_bits); // 定义名为"x"的位向量符号，长度n_bits

    // 添加位向量约束，例如所有位都设为0或1
    Constraint all_ones = And(Extract(i, i, sort) == 1 for (unsigned i = 0; i < n_bits; ++i));
    solver.add(all_ones);

    // 将位向量转换为整数
    int_vector iv(sort.getSort());
    solver.add(iv == ToIntVector(sort));

    // 将整数转换为浮点数，并添加约束
    Real float_value = cast<Real>(iv[0]); // 假设我们只关心第一个元素
    Constraint float_constraint = float_value >= 0 && float_value <= 10; // 一个简单的浮点区间约束
    solver.add(float_constraint);

    // 求解
    if (solver.check() == sat) {
        Assignment assignment = solver.model();
        // 获取转换后的整数值
        int int_val = assignment.evaluate(iv[0]);
        // 获取转换后的浮点数值
        double float_val = assignment.evaluate(float_value);
        std::cout << "Int value: " << int_val << ", Float value: " << float_val << std::endl;
    } else {
        std::cout << "No solution found." << std::endl;
    }

    return 0;
}