SMT-LIB 수식 추출

Question

모든 선언, 정의 및 제약 조건을 포함하여 SMT-LIB 수식을 C++ API의 solver/model/context 클래스에서 .smt2 파일로 추출 할 수있는 방법이 있습니까? 나는. 함수 "Z3_parse_smtlib2_string"의 반대입니다.

Answer 1

좋은 점. C++에는이 기능이 없습니다. 파이썬 바인딩에는 이제 솔버 클래스를위한 바인딩이 있습니다.

std::string to_smt2() { 
     expr_vector es = assertions(); 
     ast* const* fmls = es.ptr(); 
     unsigned sz = es.size(); 
     if (sz > 0) { 
      --sz; 
      fml = fmls[sz]; 
     } 
     else { 
      fml = ctx().bool_val(true); 
     } 
     std::string result; 
     result = Z3_benchmark_to_smtlib_string(ctx(), 
               "", "", "", "", 
               sz, 
               fmls, 
               fml); 
     return result; 
    }