From: Duy Khanh Le <le.duykhanh.cs@gm...>  20130323 11:07:27

Hi, I am a newbie using Redlog to solve floating point constraints. I recently reinstalled my machine and hence I also reinstalled redcsl from SVN by following the instruction at http://sourceforge.net/apps/mediawiki/reducealgebra/index.php?title=Installation However, after I was able to get redcsl installed, redcsl seems to work in an unexpected way. This is the command that I typed in redcsl IDE: 1: load redlog; 2: rlabout(); Redlog Development Version, Sat Mar 23 15:07:38 2013 (C) A. Dolzmann and T. Sturm http://www.redlog.eu/ 5: rlset R; 7: phi1:=rlall((((((x <> 1.)) or ((y <> 1.))) or ((x > 1.))) or ((x = y)))); \phi\mathrm{:=}\forall x\forall y\left(\left(\left(x1\,\neq\, 0\,\vee\, y1\,\neq\, 0\right)\,\vee\, x1\,>\, 0\right)\,\vee\, xy=0\right) 8: rlqe phi1; \mathrm{false} The PROBLEM is that redcsl returns FALSE (which is not correct). The formula phi I wanted to prove is: x=1.0 and y=1.0 and x<=1.0 imply x=y (which should be correct). Note that x<=1.0 is indeed redudant due to x=1.0. However, if we omit x<=1.0, the outcome is correct. 4: phi2:=rlall(((((x <> 1.)) or ((y <> 1.))) or ((x = y)))); \phi\mathrm{:=}\forall x\forall y\left(\left(x1\,\neq\, 0\,\vee\, y1\,\neq\, 0\right)\,\vee\, xy=0\right) 5: rlqe phi2; \mathrm{true} However, if I use the older version of redlog in another machine of mine, then the REDLOG DEVELOPMENT VERSION, Wed Jan 12 16:27:06 2011 (C) 19952009 A. Dolzmann and T. Sturm http://www.redlog.eu/ Then, I got the correct result for "rlqe phi1;" which is TRUE. Would it be the case that the latest version of redlog from SVN is errorprone? THank you so much for your help. Best regards, Khanh 