dreal / dreal4

Automated Reasoning in Nonlinear Theories of Reals
https://dreal.github.io
Apache License 2.0
150 stars 31 forks source link

Integer Division #304

Closed juliusbrehme closed 1 year ago

juliusbrehme commented 1 year ago

Hello everyone,

I have the following code:

  Expression exp1{10};
  Expression exp2{3};
  Expression result{exp1/exp2};

The expected result of the Expression is 3, because of Integer Division, but I get 3.3333. If I do the following:

Expression result{10/3};

I get the expected 3.

I don't know if that is intended or not.

Thanks in advance.

soonhokong commented 1 year ago
  Expression exp1{10};
  Expression exp2{3};
  Expression result{exp1/exp2};  // result = 3.3333

This is expected behavior. A constant expression holds a double value and division between expressions is handled not following the integer division rule.

  Expression result{10/3};

Here, 10/3 = 3 is computed before it is passed to the constructor of Expression class. There is nothing much we can do about it. This is how C++ works.