Possibility for Square Root in Kind 2 on Variables of Type Real

[Frontmaker1990]

Hello,

is there a possibility to express the (square) root operator in Kind2 so that SMT-Solvers get along with it? I tried implementing the square root operator using Heron algorithm with inductive array defintion and old fashioned simple variables. But SMT-Solvers do not get along with that. As far as i know Z3 supports root operators. Am i missing a operator for square root or is that not part of Kind2 like it is in Lustre?

Thanks for help.

[daniel-larraz]

The square root is not a built-in operator in Kind 2. However, you can easily define it using an imported function as follows:

function imported sqrt(n: real) returns (r: real);
(*@contract
  assume n >= 0.0;
  guarantee r >= 0.0 and r * r = n;
*)

If your model contains polynomial non-linearities, I recommend you to use Yices 2 as the back-end solver. In our experience Kind 2 with Yices 2 succeeds more often with these kind of problems. To use Yices 2 as the back-end solver, pass this argument --smt_solver Yices2. If the yices-smt2 binary is not in your PATH, you can provide the path with --yices2_bin /path/to/yices-smt2

[Frontmaker1990]

Hello Mr. Larraz,

thanks for your fast support. This is a really nice feature I have never thought about, because I am a bit new in this tool. This saved the day. Maybe the hole week. In the documentation this feature is introduced, but I have not understood the full power of this feature. This could be a nice example for future versions of the documentation, so that more people get familar with this feature.

Best regards

Andreas Vorwald