在使用 C++ 加载 smt2 文件后向 Z3 添加断言 API

Question

我正在尝试使用 C++/C API 为 z3 (v4.5.1) 加载 smt2 文件，然后使用 API 添加断言以及数据类型和函数在 smt2 文件中声明。

这是我将文件加载到求解器中的示例：

solver loadBackgroundTheoryFile(context& c, string filename) {
  Z3_ast ast = Z3_parse_smtlib2_file(c, filename.c_str(), 0, 0, 0, 0, 0, 0);

  Z3_solver c_solver;

  expr e(c, ast);

  solver s(c);
  s.add(e);

  return s;
}

int main() {
  context g;

  solver s = loadBackgroundTheoryFile(g, "family.smt2");

  std::cout << s << std::endl;
  // Here it shows that the solver has all the contents of the family.smt2 file
  return 0;
}

那么如何使用 C 或 C++ API 使用 smt2 文件中定义的内容？（如果可能的话）。我想做更多的断言，得到一个模型，然后使用 smt2 文件中定义的函数和数据类型进行评估。如果有人感兴趣，这里是smt2文件的内容：

;(declare-sort Person)
(declare-datatypes () ((Person (person (name String)))))
(declare-fun related (Person Person) Bool)
(declare-fun father (Person Person) Bool)
(declare-fun sibling (Person Person) Bool)

; related symetric
(assert
  (forall ((p Person) (q Person))
    (=> (related p q)
        (related q p))))
; related transitive
(assert
  (forall ((p Person) (q Person) (j Person))
    (=> (and (related p q) (related q j))
        (related p j))))
; the father of a person is related to that person
(assert
  (forall ((p Person) (q Person))
    (=> (father p q)
        (related p q))))
; for all people, there exists another person that is their father
(assert
  (forall ((p Person))
    (exists ((q Person)) (father q p))))
; sibling symetric
(assert
  (forall ((p Person) (q Person))
    (=> (sibling p q) (sibling q p))))
; siblings have the same father
(assert
  (forall ((p Person) (q Person) (j Person))
    (=> (and (sibling p q) (father j p))
        (father j q))))

(declare-fun get-father (Person) Person)
; here we use a double implication to define the behavior of get-father
(assert
  (forall ((p Person) (q Person))
    (= (father q p) (= (get-father p) q))))

Answer 1

这是一个非常"z3 implementation specific"的问题。如果您在此处向开发人员提交工单，您可能会得到更好的回应：https://github.com/Z3Prover/z3/issues

在使用 C++ 加载 smt2 文件后向 Z3 添加断言 API

Adding assertions to Z3 after loading in smt2 file with C++ API

z3