c++ - Z3:创建具有动态已知项数的枚举类型

Question

我正在尝试在 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 等没有默认构造函数，我需要创建一个 expr 数组。使用 malloc() 是出路吗？

Answer 1

问题似乎是调用者没有对Z3_mk_enumeration_sort 返回的声明。我稍微修改了你的代码使用 z3++.h 中的一些实用程序。特别是，我将“常量”存储到 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;
}