Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Parse model values of the form 5e1 (no decimal) #861

Merged
merged 4 commits into from
Apr 11, 2024
+52 −4
Merged

Parse model values of the form 5e1 (no decimal) #861

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e2a462c
Parse model values of the form 5e1 (no decimal)
atomb Apr 4, 2024
01ca761
Different approach to recognizing reals
atomb Apr 5, 2024
44e2251
Merge branch 'master' into parse-exp-without-decimal
atomb Apr 9, 2024
25de4ac
Add unit tests for model parsing
atomb Apr 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 3 additions & 4 deletions Source/Model/Model.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -647,7 +647,7 @@ public override string ToString()

#region factory methods

Element ConstructElement(string name)
public Element ConstructElement(string name)
{
if (name.ToLower() == "true")
{
Expand Down Expand Up @@ -699,7 +699,6 @@ Element ConstructElement(string name)
}

var allDigits = new Regex(@"^-?[0-9]*$");
var real = new Regex(@"^-?[0-9]+\.[0-9]+$");
if (allDigits.IsMatch(name))
{
if (szi > 0)
Expand All @@ -711,7 +710,7 @@ Element ConstructElement(string name)
return new Integer(this, name);
}
}
else if (real.IsMatch(name))
else if (double.TryParse(name, out var _))
{
return new Real(this, name);
}
Expand Down Expand Up @@ -1077,4 +1076,4 @@ public static List<Model> ParseModels(System.IO.TextReader rd, Func<string, stri
return p.resModels;
}
}
}
}
49 changes: 49 additions & 0 deletions Source/UnitTests/CoreTests/Model.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
using Microsoft.Boogie;
using NUnit.Framework;

namespace ModelTests
{
[TestFixture()]
public class ModelTests
{
[Test]
public void ParseRealModelElements()
{
var m = new Model();
var e1 = m.ConstructElement("1e2");
Assert.AreEqual(e1.Kind, Model.ElementKind.Real);
Assert.AreEqual(e1.ToString(), "1e2");
var e2 = m.ConstructElement("-3e5");
Assert.AreEqual(e2.Kind, Model.ElementKind.Real);
Assert.AreEqual(e2.ToString(), "-3e5");
var e3 = m.ConstructElement("1.2e3");
Assert.AreEqual(e3.Kind, Model.ElementKind.Real);
Assert.AreEqual(e3.ToString(), "1.2e3");
var e4 = m.ConstructElement("-3.1e6");
Assert.AreEqual(e4.Kind, Model.ElementKind.Real);
Assert.AreEqual(e4.ToString(), "-3.1e6");
}

[Test]
public void ParseBoolModelElements()
{
var m = new Model();
var e1 = m.ConstructElement("true");
Assert.AreEqual(e1, m.True);
var e2 = m.ConstructElement("false");
Assert.AreEqual(e2, m.False);
}

[Test]
public void ParseIntModelElements()
{
var m = new Model();
var e1 = m.ConstructElement("3289");
Assert.AreEqual(e1.Kind, Model.ElementKind.Integer);
Assert.AreEqual(e1.ToString(), "3289");
var e2 = m.ConstructElement("-12389");
Assert.AreEqual(e2.Kind, Model.ElementKind.Integer);
Assert.AreEqual(e2.ToString(), "-12389");
}
}
}
Loading