Microsoft Z3 の C++ API に、.NET API にある Context.ParseSMTLIB2String を追加する試み

ConsoleApplication43.cpp

// ConsoleApplication43.cpp : コンソール アプリケーションのエントリ ポイントを定義します。
//

#include "stdafx.h"


namespace z3 {
    
    class context_ex : 
        public context
    {
    public: 
        context_ex() : context() { }
        context_ex(config & c) : context(c) { }
        ~context_ex() { }

        expr parse_smtlib2_string(char const *str, unsigned num_sorts = 0, symbol const *sort_names = nullptr, sort const *sorts = nullptr, unsigned num_decls = 0, symbol const *decl_names = nullptr, func_decl const *decls = nullptr)
        {
            assert(num_sorts != 0 ? sort_names && sorts : true);
            assert(num_decls != 0 ? decl_names && decls : true);
            
            auto _sort_names = std::vector<Z3_symbol>(num_sorts);
            auto _sorts = std::vector<Z3_sort>(num_sorts);
            if (0u < num_sorts)
            {
                for (auto i = 0u; i < num_sorts; ++i)
                {
                    _sort_names[i] = static_cast<Z3_symbol>(sort_names[i]);
                    _sorts[i] = static_cast<Z3_sort>(sorts[i]);
                }
            }
            
            auto _decl_names = std::vector<Z3_symbol>();
            auto _decls = std::vector<Z3_func_decl>();
            if (0u < num_decls)
            {
                for (auto i = 0u; i < num_decls; ++i)
                {
                    _decl_names[i] = static_cast<Z3_symbol>(decl_names[i]);
                    _decls[i] = static_cast<Z3_func_decl>(decls[i]);
                }
            }

            auto ast = ::Z3_parse_smtlib2_string(static_cast<Z3_context>(*this), 
                                                 str, 
                                                 num_sorts, 
                                                 _sort_names.empty() ? nullptr : &_sort_names[0], 
                                                 _sorts.empty() ? nullptr : &_sorts[0], 
                                                 num_decls, 
                                                 _decl_names.empty() ? nullptr : &_decl_names[0], 
                                                 _decls.empty() ? nullptr : &_decls[0]);
            return to_expr(*this, ast);
        }
    };

}   // namespace z3 {

void demorgan_original_cpp_api()
{
    using std::cout;
    using z3::context_ex;
    using z3::expr;
    using z3::solver;
    using z3::unsat;
    using z3::sat;
    using z3::unknown;

    cout << "de-Morgan example\n";

    context_ex c;

    expr x = c.bool_const("x");
    expr y = c.bool_const("y");
    expr conjecture = !(x && y) == (!x || !y);
    
    solver s(c);
    s.add(!conjecture);
    cout << s << "\n";

    switch (s.check()) 
    {
        case unsat:   cout << "de-Morgan is valid\n"; break;
        case sat:     cout << "de-Morgan is not valid\n"; break;
        case unknown: cout << "unknown\n"; break;
    }
}

void demorgan_parse_smtlib2_string()
{
    using std::cout;
    using z3::context_ex;
    using z3::expr;
    using z3::solver;
    using z3::unsat;
    using z3::sat;
    using z3::unknown;

    cout << "de-Morgan example\n";

    auto c = context_ex();

    auto conjecture = c.parse_smtlib2_string("" 
"(declare-const x Bool)\n"
"(declare-const y Bool)\n"
"(assert (= (not (and x y)) (or (not x) (not y))))\n"
"");
    
    solver s(c);
    s.add(!conjecture);
    cout << s << "\n";

    switch (s.check()) 
    {
        case unsat:   cout << "de-Morgan is valid\n"; break;
        case sat:     cout << "de-Morgan is not valid\n"; break;
        case unknown: cout << "unknown\n"; break;
    }
}

int _tmain(int argc, _TCHAR* argv[])
{
    demorgan_original_cpp_api();
    // Output ---
    // de-Morgan example
    // (solver
    //   (not (= (not (and x y)) (or (not x) (not y)))))
    // de-Morgan is valid
    
    demorgan_parse_smtlib2_string();
    // Output ---
    // de-Morgan example
    // (solver
    //   (not (= (not (and x y)) (or (not x) (not y)))))
    // de-Morgan is valid

    std::string line;
    std::getline(std::cin, line);
    return 0;
}