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

我正尝试使用C++/C API for z3（v4.5.1）加载smt2文件，然后使用API添加断言，数据类型以及在smt2文件中声明的函数。在使用C++ API加载smt2文件后向Z3添加断言

这里是我做的一个文件加载到求解一个例子：

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; 
}

因此，我怎么用什么在SMT2文件中定义，使用C或C++ API？（如果可能的话）。我想做更多的断言，得到一个模型，然后使用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))))

来源

2017-04-04 Codi Burley

这是一个非常“z3实现特定”的问题。如果您向开发商提交了一张门票，您可能会收到更好的回复：https://github.com/Z3Prover/z3/issues

来源

2017-04-05 18:05:49

谢谢，我收到了关于问题的回复。 https://github.com/Z3Prover/z3/issues/966#issuecomment-292287734 –

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

回答

相关问题