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?

One note of caution: Z3's raw C API requires callers to manage reference counts. You should increase a reference count on any object, such as Z3_sort, Z3_func_decl, Z3_ast, that is created by the API functions. The C++ wrapper does this for you, but as you here mix C and C++ abstractions not all reference counts are handled for you. — Nikolaj Bjorner, Jan 06 '14 at 01:45
Hi, thanks for the comment. I read about that in the question that I quoted (http://stackoverflow.com/questions/15085232/how-to-use-enumerated-constants-after-calling-of-some-tactic-in-z3), and so, I went for the "corrected" version of the code that was given in the answer. I imagined that the reference count issue was taken care of by the C++ API. Could you kindly give some insight into why I keep getting SIGSEGV? — SPMP, Jan 06 '14 at 02:06

score 1 · Accepted Answer · answered Jan 07 '14 at 04:24

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

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

1 Answers1