# Just Launched: You can now import projects and releases from Google Code onto SourceForge

We are excited to release new functionality to enable a 1-click import from Google Code onto the Allura platform on SourceForge. You can import tickets, wikis, source, releases, and more with a few simple steps.

## [Reduce-algebra-developers] [Question] Weird behaviours of redcsl

 [Reduce-algebra-developers] [Question] Weird behaviours of redcsl From: Duy Khanh Le - 2013-03-23 11:07:27 Attachments: Message as HTML Hi, I am a newbie using Redlog to solve floating point constraints. I recently re-installed my machine and hence I also re-installed redcsl from SVN by following the instruction at http://sourceforge.net/apps/mediawiki/reduce-algebra/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(x-1\,\neq\, 0\,\vee\, y-1\,\neq\, 0\right)\,\vee\, x-1\,>\, 0\right)\,\vee\, x-y=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(x-1\,\neq\, 0\,\vee\, y-1\,\neq\, 0\right)\,\vee\, x-y=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) 1995-2009 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 error-prone? THank you so much for your help. Best regards, Khanh 

 [Reduce-algebra-developers] [Question] Weird behaviours of redcsl From: Duy Khanh Le - 2013-03-23 11:07:27 Attachments: Message as HTML Hi, I am a newbie using Redlog to solve floating point constraints. I recently re-installed my machine and hence I also re-installed redcsl from SVN by following the instruction at http://sourceforge.net/apps/mediawiki/reduce-algebra/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(x-1\,\neq\, 0\,\vee\, y-1\,\neq\, 0\right)\,\vee\, x-1\,>\, 0\right)\,\vee\, x-y=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(x-1\,\neq\, 0\,\vee\, y-1\,\neq\, 0\right)\,\vee\, x-y=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) 1995-2009 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 error-prone? THank you so much for your help. Best regards, Khanh