Z3: Creating an enumerated type with number of items known dynamically

Question

I am trying to create an enumerated datatype in Z3, where the number of items is known only at run time. I have it working with the Python API, but I am trying the same thing using the C and C++ APIs together. The following is the program.

#include<stdio.h>
#include<stdlib.h>
#include<string.h>
#include<stdarg.h>
#include<memory.h>
#include<z3++.h>
using namespace std;
using namespace z3;

expr get_expr(context &c,Z3_func_decl constant)//get expression from constant
{
    func_decl temp=to_func_decl(c, constant);
    return(to_expr(c, Z3_mk_app(c, temp, 0, 0)));
}

sort create_enum(context &c,char const *dtypename,int count,char const *prefix,Z3_func_decl consts[])
{
    int i;
    char itemname[10];
    Z3_symbol *names=new Z3_symbol[count];
    Z3_func_decl *testers=new Z3_func_decl[count];
    for(i=0;i<count;i++)
    {
        sprintf(itemname,"%s%d",prefix,i);
        names[i]=Z3_mk_string_symbol(c,itemname);
    }
    Z3_symbol enum_nm = Z3_mk_string_symbol(c,dtypename);
    sort s = to_sort(c, Z3_mk_enumeration_sort(c, enum_nm, 3, names, consts, testers));
    return(s);
}

int main()
{


    context c;

    int count=3,i;
    char itemname[10],prefix[]={"p"},dtypename[]={"phynodetype"};
    Z3_func_decl *phynodeconsts=new Z3_func_decl[count];
    sort phynodetype=create_enum(c,"phynodetype",count,"p",phynodeconsts);  
    func_decl g = function("g", phynodetype, phynodetype);
    solver s(c);
    expr tst1= get_expr(c,phynodeconsts[0])==g(get_expr(c,phynodeconsts[1]));
    expr tst2= get_expr(c,phynodeconsts[1])==g(get_expr(c,phynodeconsts[0]));
    cout<<tst1<<endl<<tst2<<endl;
    s.add(tst1);
    s.add(tst2);
    s.add(implies(a,b>=5));
    s.add(b<5);
    cout<<s.check();
    cout<<s.get_model();


}

What I am doing is, creating the function "create_enum", which will take the name of the new datatpye I wish to create, the number of items, and a prefix (For eg., if the number of items is 3, and the prefix is "p", the items will be named p0,p1,p2). The program keeps raising SIGSEGV, and on the rare ocassion that it doesn't, I get some very weird results. I have used a lot of code from the following post:

How to use enumerated constants after calling of some tactic in Z3?

Could anyone tell what is going wrong? Some related queries: Is there a way to create enumerated datatypes using the C++ API? It seems that expr, func_decl etc do not have a default constructor, and I need to create an array of exprs. Is using malloc() the way out?

Answer 1

The problem seems to be that the caller did not take reference counts on the declarations returned by Z3_mk_enumeration_sort. I have modified your code a little to use some of the utilities from z3++.h. In particular, I store the "consts" into a C++ vector of func_decl objects. These are properly reference counted so they are still live when they are later used.

I realize we could and really should add these as utilities to the C++ API to make life simpler for everybody. Thanks for reporting this problem.

#include<stdarg.h>
#include<memory.h>
#include"z3++.h"
using namespace std;
using namespace z3;

expr get_expr(context &c,Z3_func_decl constant)//get expression from constant
{
   func_decl temp=to_func_decl(c, constant);
   return(to_expr(c, Z3_mk_app(c, temp, 0, 0)));
}

sort create_enum(context &c,char const *dtypename,int count,char const *prefix, func_decl_vector& consts)
{
    int i;
    char itemname[10];
    array<Z3_symbol> names(count);
    array<Z3_func_decl> _testers(count);
    array<Z3_func_decl> _consts(count);

    for(i=0;i<count;i++)
    {
       sprintf(itemname,"%s%d",prefix,i);
       names[i] = Z3_mk_string_symbol(c,itemname);
    }
    Z3_symbol enum_nm = Z3_mk_string_symbol(c,dtypename);
    Z3_sort _s = Z3_mk_enumeration_sort(c, enum_nm, count, names.ptr(), _consts.ptr(), _testers.ptr());
    for (i = 0; i < count; ++i) {
        consts.push_back(to_func_decl(c, _consts[i]));
    }
    sort s = to_sort(c, _s);

    return(s);
}

int main()
{
    context c;

    int count=3,i;
    char itemname[10],prefix[]={"p"},dtypename[]={"phynodetype"};
    func_decl_vector phynodeconsts(c);
    sort phynodetype=create_enum(c,"phynodetype",count,"p",phynodeconsts);  
    func_decl g = function("g", phynodetype, phynodetype);
    solver s(c);
    expr tst1= get_expr(c,phynodeconsts[0])==g(get_expr(c,phynodeconsts[1]));
    expr tst2= get_expr(c,phynodeconsts[1])==g(get_expr(c,phynodeconsts[0]));
    cout<<tst1<<endl<<tst2<<endl;
    s.add(tst1);
    s.add(tst2);
    //s.add(implies(a,b>=5));
    //s.add(b<5);
     cout<<s.check() << endl;
    cout<<s.get_model() << endl;
}