z3 提取 Seq Int 作为 std：：vector<int>

z3 extracting Seq Int as std::vector<int>

本文关键字：lt 提取 int gt Seq vector 作为 std z3 Int      更新时间：2023-10-16

我正在尝试将Seq Int从model提取到std::vector<int>。 我可以用<<打印它，但我该如何进行提取？

void oren_example()
{
// context + solver
context ctx;
solver solver(ctx);
// sorts
sort int_sort     = ctx.int_sort();
sort seq_int_sort = ctx.seq_sort(int_sort);
sort bool_sort    = ctx.bool_sort();
// constants
expr two   = ctx.int_val(2);
expr five  = ctx.int_val(5);
expr four  = ctx.int_val(4);
expr three = ctx.int_val(3);
// define State sort
const char *names[4]={"x","A","b","n"};
sort sorts[4]={int_sort,seq_int_sort,bool_sort,int_sort};
func_decl_vector projs(ctx);
sort state_sort = ctx.tuple_sort("State",4,names,sorts,projs).range();
// define an arbitrary state sigma
expr sigma = ctx.constant("sigma",state_sort);
// define some predicate on the state
func_decl init = function("init",state_sort,bool_sort);
solver.add(forall(sigma,
init(sigma) == (
((projs[0](sigma))          == two  ) &&
((projs[1](sigma).length()) == three) &&
((projs[1](sigma).nth(two)) == five ) &&
((projs[3](sigma))          == five ))));
// find an initial state
solver.add(init(sigma));
// check sat + get model
if (solver.check() == sat)
{
model m = solver.get_model();
std::cout << "x = " << m.eval(projs[0](sigma)) << "n";
std::cout << "A = " << m.eval(projs[1](sigma)) << "n";
std::cout << "b = " << m.eval(projs[2](sigma)) << "n";
std::cout << "n = " << m.eval(projs[3](sigma)) << "n";
}
}

一切都按预期打印出来：

x = 2
A = (seq.++ (seq.unit 6) (seq.unit 7) (seq.unit 5))
b = false
n = 5

尝试：

std::vector<int> output;
int size = m.eval(projs[1](sigma).length()).get_numeral_int();
std::cout << "size = " << size << std::endl;
for(int i = 0; i < size; ++i)
output.push_back(m.eval(projs[1](sigma).nth(ctx.int_val(i))).get_numeral_int());
for(int i = 0; i < size; ++i)
std::cout << "output[" << i << "] = " << output[i] << std::endl;

当我将其添加到您的程序中并运行它时，我得到：

x = 2
A = (seq.++ (seq.unit 4) (seq.unit 6) (seq.unit 5))
b = false
n = 5
size = 3
output[0] = 4
output[1] = 6
output[2] = 5
相关文章：