Parse datatypes and define-funs from string

[leonardoalt]

If I give the following file to z3 it parses it correctly: https://gist.github.com/leonardoalt/dd99670d70726b10367f0fd2df1e7d16 .
Is there a way that I can give this as string/file to z3 in the C++ API and somehow retrieve the exprs or func_decls for the dataypes and define-funs?
context::parse_string returns an expr_vector of the given assertions, but there are no assertions.

[NikolajBjorner]

This isn't a supported scenario at this point.

The pretty printer for the solver object will not even show you all declarations that were used in the string passed to solver::from_string(..).

The rationale for not going there is that you can call the C++ API directly to create datatypes.
There are maybe SMTLIB2 tools that can give you back an abstract syntax tree that can be used to then call C++ API functions that create Datatypes.

The following methods are available over the C API:

• expose a method on a DATATYPE_SORT to return set of constructors
• expose methods on a constructor to return accessors and testers

They are:

Z3_get_datatype_sort_num_constructors
Z3_get_datatype_sort_constructor
Z3_get_datatype_sort_recognizer
Z3_get_datatype_sort_constructor_accessors

and I added C++ versions of these functions to the C++ API.

They still require that you have some sorts to start out with, that is the sorts you declare are used somewhere (add dummy assertions).

Example usage:

#include "z3++.h"
#include <vector>
#include <unordered_set>

using namespace z3;

void main() {
    context c;
    solver s(c);
    s.from_file("leo.smt2");
    expr_vector es(c);
    std::cout << s << "\n";
    std::unordered_set<unsigned> seen_e, seen_s;
    for (auto& e : s.assertions())
        es.push_back(e);
    for (unsigned i = 0; i < es.size(); ++i) {
        expr e = es[i];
        if (seen_e.find(e) != seen_e.end())
            continue;
        seen_e.insert(e.id());
        for (auto& arg : e)
            es.push_back(arg);

        sort s = e.get_sort();
        if (seen_s.find(s) != seen_s.end())
            continue;
        seen_s.insert(s.id());
        if (s.sort_kind() == Z3_DATATYPE_SORT) { // or cleaner: s.is_datatype()
            std::cout << "datatype " << e.get_sort() << "\n";
            auto cs = s.constructors();
            for (auto & c : cs) {
                auto as = c.accessors();
                std::cout << "constructor: " << c << " " << as << "\n";
            }
        }
    }
}

where leo.smt2 contains:

...
(define-fun summary_constructor_2_C_13_0 ((A Int) (B Int) (C abi_type) (D crypto_type) (E tx_type) (F state_type) (G state_type) (H Int) (I Int)) Bool (and (= G F) (and (and (and (= A 0) (= H 0)) (= I 0)) (and (>= (select (balances F) B) (msg.value E)) (= (balances F) (balances F))))))

(declare-const c1 |crypto_type|)
(declare-fun p1 (|crypto_type|) Bool)
(assert (p1 c1))

[leonardoalt]

Alright, thanks @NikolajBjorner ! Yea I was going the direction of the dummy assertions already, so sounds good.