c++ - Z3:创建枚举类型，其中包含动态已知的项目数

我试图在Z3中创建枚举数据类型，其中的项目数仅在运行时才知道。我已经将其与Python API配合使用，但是我正在尝试同时使用C和C++ API进行相同的操作。以下是程序。

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


}

我正在做的是创建函数“create_enum”，该函数的名称为
我要创建的新数据类型，项目数和前缀(例如，如果项目数为3，且前缀为“p”，则项目将命名为p0，p1，p2)。该程序不断提高SIGSEGV，但由于极少出现这种情况，我得到了一些非常奇怪的结果。我从以下帖子中使用了很多代码:

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

谁能告诉我出了什么问题？一些相关的查询:是否可以使用C++ API创建枚举数据类型？似乎expr，func_decl等没有默认的构造函数，因此我需要创建一个exprs数组。使用malloc()是出路吗？

最佳答案

问题似乎是， call 者未在
Z3_mk_enumeration_sort返回的声明。我对您的代码做了一些修改
使用z3 ++。h中的某些实用程序。特别是，我将“consts”存储到func_decl对象的C++ vector 中。这些都是正确的参考计数，因此它们仍然有效
以后再使用。

我知道我们可以并且真的应该将这些添加为实用程序
C++ API，使每个人的生活变得更加简单。
感谢您报告这一问题。

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