在 z3::expr 中使用 C++ 字符串? [英] Use a C++ string in z3::expr?
本文介绍了在 z3::expr 中使用 C++ 字符串?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
我在使用 Z3::expr 时遇到了困难.在 z3 中,expr conj 可以这样定义:
I got difficulties in using Z3::expr. In z3, the expr conj can be defined like:
expr x = c.bool_const("x");
expr y = c.bool_const("y");
expr conj = (!x || !y);
有没有办法使用字符串变量来定义conj?类似的东西:
Is there a way to use a string variable to define conj? Something like:
expr x = c.bool_const("x");
expr y = c.bool_const("y");
string str = "(!x || !y)";
expr conj = some_API(str);
我被这个问题困扰了好几天.
I got stuck on the problem for days.
谢谢
推荐答案
在示例中无法使用该特定字符串,但您可以使用 parse_string
,它可以理解 SMT2 格式的字符串.
There is no way to use that particular string in the example, but you can use parse_string
, which understands strings in SMT2 format.
这篇关于在 z3::expr 中使用 C++ 字符串?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文