Z3Python API需要比Z3 Rust API更长的时间更长的时间 - 为什么？ 我一直在测试使用Z3 API时的性能增益，以切换为生锈。我测试了以下用例，在那里建立了一个长公式。考虑以下生锈代码和以下python Co ...

Question

Time to find the model: 0.554883247

当与python一起奔跑时，实际上是solving

（呼叫

solver.check()

），该模型需要更长的7倍

Time to find the model: 4.0679099559783936 我对这个结果感到惊讶 - 在求解模型时，python Z3 API是否不对低级二进制代码进行调用，因此，实际求解应大致相同的时间？我在这里错过了什么？

rust代码：

use z3;
use z3::ast::Ast;
use z3::Solver;
use std::time::Instant;


fn tester() -> () {
    let cfg = z3::Config::new();
    let ctx = z3::Context::new(&cfg);
    let solver = Solver::new(&ctx);

    let x = z3::ast::BV::new_const(&ctx, "x", 32);
    let mut this_formula = Vec::new();
    for i in 0..10000 {
        let y = z3::ast::BV::from_u64(&ctx, i, 32);
        this_formula.push(x._eq(&y));
    }
    let binding = this_formula.iter().map(|x| x).collect::<Vec<_>>();
    let slice = binding.as_slice();
    let formula = z3::ast::Bool::or(&ctx, slice);
    solver.assert(&formula);

    let start = Instant::now();
    let res = solver.check();
    let end = std::time::Instant::now();
    let time_difference = end.duration_since(start);
    let took_time = time_difference.as_secs_f64();
    println!("Time to find the model: {}", took_time);
    if res == z3::SatResult::Sat {
        let model = solver.get_model().unwrap();
        println!("model:");
    }
}

fn main() {
    tester();
}

Python代码：

import z3
import time

def tester():
  x = z3.BitVec("x", 32)
  this_formula = []
  for i in range(10000):  # Assuming a loop to make profiling meaningful
      y = z3.BitVecVal(i, 32)
      this_formula.append(x == y)
  formula = z3.Or(this_formula)
  solver = z3.Solver()
  solver.add(formula)
  start_time = time.time()
  res = solver.check()
  end_time = time.time()
  elasped_time = end_time - start_time
  print("Time to find the model: ", elasped_time)
  print("Res", res)

tester()

您的直觉是正确的：实际的求解过程和时间应该相似，因为Rust和Python都称为同一Z3求解器。

问题是，Python是一种更效率的语言，但比Rust更容易编写它，而生锈以其在内存管理方面掌握效率而闻名。

python记忆管理和数据结构

函数呼叫高架 这些是我能想到为什么Python在效率方面可怕的三个原因。

Answer 1