在使用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添加斷言

回答

相關問題