Adding assertions to Z3 after loading in smt2 file with C++ API

[CodiBurley]

I'm am trying to load in an smt2 file using the C++/C API for z3 (v4.5.1), and then add assertions using the API, with datatypes and functions that were declared in the smt2 file.

Here is an example of what I do to load a file into a solver:

solver loadBackgroundTheoryFile(context& c, string filename) {
  Z3_ast ast = Z3_parse_smtlib2_file(c, filename.c_str(), 0, 0, 0, 0, 0, 0);

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

So how do I use what was defined in the smt2 file, using the C or C++ API? (If possible). I would like to make more assertions, get a model, and then evaluate, using the functions and data types defined in the smt2 file. Here are the contents of the smt2 file if anyone is interested:

;(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))))

[wintersteiger]

Z3 does not keep a symbol or function table, but only an AST table. This is however not accessible from the outside. Instead I would recommend to simply walk the expression that was read from the SMT2 file to collect the function symbols that appear in it; technically, this is only a tiny bit less efficient than walking the internal AST table. For instance, something like the following function lets us find all the predicates (func_decls with Boolean range):

void collect_fds(expr & e, vector<func_decl> & fds) {
    if (e.is_app()) {
        func_decl fd = e.decl();

        if (fd.range().is_bool())
            fds.push_back(fd);

        for (unsigned i = 0; i < e.num_args(); i++)
            collect_fds(e.arg(i), fds);
    }
    else if (e.is_quantifier())
        collect_fds(e.body(), fds);
}

and we could use that like so:

Z3_ast ast = Z3_parse_smtlib2_file(c, filename.c_str(), 0, 0, 0, 0, 0, 0);
expr e(c, ast);
vector<func_decl> my_fds;
collect_fds(e, my_fds);

[NikolajBjorner]

We also recently added

      c.parse_file(filename.c_str())

to avoid the more awkward Z3_parse_smtlib2_file call.

[CodiBurley]

@wintersteiger Thank you, this describes how I could get function declarations and such very well. Is there an easy way you know of to utilize the constructors and accessors created by the declare-datatypes command?

(declare-datatypes () ((Person (person (name String)))))

[NikolajBjorner]

You can access all this information from the func_decl parameters, but it is very low level so essentially a nonstarter. The file datatype_decl_plugin describes the format and implements helper functions you would have to replicate.

[NikolajBjorner]

Is your issue resolved?

[CodiBurley]

Sorry for the delayed response.

@NikolajBjorner I took your advice and looked into reimplementing some of the helper functions in datatype_decl_plugin. In particular I looked into reimplementing func_decl * datatype_util::get_constructor(sort * ty, unsigned c_id).

Im running into issues with this call (func_decl * d = m_manager.mk_func_decl(m_family_id, OP_DT_CONSTRUCTOR, 2, p, domain.size(), domain.c_ptr());) inside get_constructor. I think that this function is what does the work in regards to getting a reference to the constructor function for the datatype that I declare in an smt2 and load in using the api. I'm having problems with it because I do not have access to the ast_manager m_manager or any ast manager that I know of, through the api. I tried replacing this in some way with just a call to Z3_mk_func_decl but that did not seem to get an actual reference to the function and instead just created a new function declaration.

I really appreciate your help so far, Thanks!

[NikolajBjorner]

I am so sorry for miss-leading you. There are in fact API methods for accessing constructors. You should be able to just use these to access the relevant information.

  unsigned Z3_API Z3_get_datatype_sort_num_constructors(
       Z3_context c, Z3_sort t);

   Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(
       Z3_context c, Z3_sort t, unsigned idx);

   Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c,
                                                              Z3_sort t,
                                                              unsigned idx_c,
                                                              unsigned idx_a);

They are a bit esotheric, so they havent' found their way into the C++ API, but it should be fairly straight-forward to write wrappers for them so they are convenient from C++.

[CodiBurley]

@NikolajBjorner No worries at all. These functions work great for me, does exactly what I was looking for. I'll go ahead and close this issue. Thanks for the help!