如何在 C++ 中将字符串类型的约束转移到 z3 求解器 expr？

Question

例如，我有一个约束：“(number

context c;
expr number= c.int_const(number);
expr name = c->string_val(name.c_str());
expr constrain = ***procedure***("(number < 10) && (name == \"hello\")");

我该如何实现这个procedure()？

Use a C++ string in z3::expr? 中有一个不完整且未经验证的答案，我仍然不知道如何实现它？

我非常渴望并感谢您的帮助！谢谢！

Answer 1

试试：

#include <z3++.h>

using namespace z3;
using namespace std;

int main ()
{
  context c;
  expr number = c.int_const("number");
  expr name   = c.constant(c.str_symbol("name"), c.string_sort());
  expr hello  = c.string_val("hello");

  expr constraint = number < 10 && name == hello;

  solver s(c);
  s.add(constraint);
  cout << s.check() << "\n";
  cout << s.get_model() << "\n";

  return 0;
};

假设您将上述内容放在名为a.cpp 的文件中，您可以像这样编译它：

$ g++ -std=c++11 a.cpp -l z3

当运行时，它会产生：

sat
(define-fun number () Int
  9)
(define-fun name () String
  "hello")

使用更高级别的 API

您无疑已经注意到，使用 C/C++ 对 z3 进行编程非常冗长且极易出错。除非您有其他使用 C/C++ 的理由，否则我建议您使用更高级别的 API，例如 Python 或 Haskell，这在很大程度上简化了 z3 中的编程。

Python

例如，您可以像这样在 Python 中编写问题代码：

from z3 import *

number = Int('number')
name   = String('name')

s = Solver()
s.add(number < 10, name == "hello")
print(s.check())
print(s.model())

制作：

sat
[number = 9, name = "hello"]

哈斯克尔

在 Haskell 中，它看起来像：

import Data.SBV

ex :: IO SatResult
ex = sat $ do number <- sInteger "number"
              name   <- sString  "name"

              constrain $ number .< 10 .&& name .== literal "hello"

制作：

*Main> ex
Satisfiable. Model:
  number =       9 :: Integer
  name   = "hello" :: String

总结

长话短说，如果您可以使用更高级别的接口，最好避免使用 C/C++ 对 z3 进行编程（尽管完全有可能）。如果一定要坚持C/C++，一定要学习API：https://z3prover.github.io/api/html/namespacez3.html