0

I am new to SMT solver and these topics. I need to convert a C++ code into an equivalent of SMT2 (I have a tool that needs .smt2 as input). I've already found this solution but it does not explain completely how to do that? Could you help me. Thanks

while (x<y)
{
x=5*x+3; 
y=3*y+5; 
w=3*z+w; 
z=z+6;
}

Is there any kind of tool for this conversion? or how should I learn about this topic?

user9137963
  • 105
  • 9

1 Answers1

1

If you're looking for a tool that can convert arbitrary C++ to SMTLib, then I don't believe such a tool exists, nor it would be feasible to do so for that would mean you'd need a very precise semantics of C++ encoded in SMTLib, a gargantuan task if not impossible.

If you care about a restricted subset, or just want to hand-translate one-or two specific examples, then the answer you found is as good as it's going to get. Start by studying SMTLib itself, and look up SSA (single static-assignment). Loops will be difficult, but there are ways to deal with them. Again, it all depends on what exactly you're trying to achieve. Once you look at these options, perhaps you can ask a more specific question.

alias
  • 28,120
  • 2
  • 23
  • 40