Skip to content

Commit

Permalink
Enabling string operations. (#131)
Browse files Browse the repository at this point in the history 
* Enabling string operations.

* Preparing for string literals.

* Added regex type.

* Added regex tests.

* Added string literal rule to parser.

* Shallow type for string literals.

* Added string literal test.

* Better regex test.

* Printing string literals.

* Parsing strings from model.
  • Loading branch information
@michael-emmi
michael-emmi authored Feb 18, 2020
1 parent fd500e1 commit a38904c
Show file tree
Hide file tree
Showing 16 changed files with 345 additions and 21 deletions.
41 changes: 41 additions & 0 deletions Source/Core/AbsyExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -373,6 +373,11 @@ public static LiteralExpr Literal(RoundingMode value)
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return new LiteralExpr(Token.NoToken, value);
}
public static LiteralExpr Literal(String value)
{
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return new LiteralExpr(Token.NoToken, value);
}

private static LiteralExpr/*!*/ true_ = Literal(true);
public static LiteralExpr/*!*/ True {
Expand Down Expand Up @@ -645,6 +650,21 @@ public LiteralExpr(IToken/*!*/ tok, RoundingMode v, bool immutable = false)
CachedHashCode = ComputeHashCode();
}

/// <summary>
/// Creates a literal expression for the string value "v".
/// </summary>
/// <param name="tok"></param>
/// <param name="v"></param>
public LiteralExpr(IToken/*!*/ tok, String v, bool immutable = false)
: base(tok, immutable)
{
Contract.Requires(tok != null);
Val = v;
Type = Type.String;
if (immutable)
CachedHashCode = ComputeHashCode();
}

[Pure]
[Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object obj) {
Expand Down Expand Up @@ -675,6 +695,8 @@ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bo
stream.SetToken(this);
if (this.Val is bool) {
stream.Write((bool)this.Val ? "true" : "false"); // correct capitalization
} else if (Type.IsString) {
stream.Write("\"" + cce.NonNull(this.Val.ToString()) + "\"");
} else {
stream.Write(cce.NonNull(this.Val.ToString()));
}
Expand Down Expand Up @@ -710,6 +732,8 @@ public override Type/*!*/ ShallowType {
return Type.GetBvType(((BvConst)Val).Bits);
} else if (Val is RoundingMode) {
return Type.RMode;
} else if (Val is String) {
return Type.String;
} else {
{
Contract.Assert(false);
Expand Down Expand Up @@ -821,6 +845,23 @@ public RoundingMode asRoundingMode
}
}

public bool isString
{
get
{
return Val is String;
}
}

public String asString
{
get
{
Contract.Assert(isString);
return (String)cce.NonNull(Val);
}
}

public override Absy StdDispatch(StandardVisitor visitor) {
//Contract.Requires(visitor != null);
Contract.Ensures(Contract.Result<Absy>() != null);
Expand Down
84 changes: 82 additions & 2 deletions Source/Core/AbsyType.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -259,6 +259,16 @@ public virtual bool IsRMode {
return false;
}
}
public virtual bool IsString {
get {
return false;
}
}
public virtual bool IsRegEx {
get {
return false;
}
}

public virtual bool IsVariable {
get {
Expand Down Expand Up @@ -371,6 +381,8 @@ public virtual int BvBits {
public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real);
public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool);
public static readonly Type/*!*/ RMode = new BasicType(SimpleType.RMode);
public static readonly Type/*!*/ String = new BasicType(SimpleType.String);
public static readonly Type/*!*/ RegEx = new BasicType(SimpleType.RegEx);
private static BvType[] bvtypeCache;

static public BvType GetBvType(int sz) {
Expand Down Expand Up @@ -917,6 +929,10 @@ public override string ToString() {
return "bool";
case SimpleType.RMode:
return "rmode";
case SimpleType.String:
return "string";
case SimpleType.RegEx:
return "regex";
}
Debug.Assert(false, "bad type " + T);
{
Expand Down Expand Up @@ -1054,6 +1070,20 @@ public override bool IsRMode
return this.T == SimpleType.RMode;
}
}
public override bool IsString
{
get
{
return this.T == SimpleType.String;
}
}
public override bool IsRegEx
{
get
{
return this.T == SimpleType.RegEx;
}
}

public override Absy StdDispatch(StandardVisitor visitor) {
//Contract.Requires(visitor != null);
Expand Down Expand Up @@ -1501,7 +1531,7 @@ public override int GetHashCode(List<TypeVariable> boundVariables) {
public override Type ResolveType(ResolutionContext rc) {
//Contract.Requires(rc != null);
Contract.Ensures(Contract.Result<Type>() != null);
// first case: the type name denotes a bitvector-type, float-type, or rmode-type
// first case: the type name denotes a bitvector-type, float-type, rmode-type, string-type, or regex-type

if (Name.StartsWith("bv") && Name.Length > 2) {
bool is_bv = true;
Expand Down Expand Up @@ -1554,6 +1584,28 @@ public override Type ResolveType(ResolutionContext rc) {
return Type.RMode;
}

if (Name.Equals("string"))
{
if (Arguments.Count > 0)
{
rc.Error(this,
"string type must not be applied to arguments: {0}",
Name);
}
return Type.String;
}

if (Name.Equals("regex"))
{
if (Arguments.Count > 0)
{
rc.Error(this,
"regex type must not be applied to arguments: {0}",
Name);
}
return Type.RegEx;
}

// second case: the identifier is resolved to a type variable
TypeVariable var = rc.LookUpTypeBinder(Name);
if (var != null) {
Expand Down Expand Up @@ -2186,6 +2238,22 @@ public override bool IsRMode
return p != null && p.IsRMode;
}
}
public override bool IsString
{
get
{
Type p = ProxyFor;
return p != null && p.IsString;
}
}
public override bool IsRegEx
{
get
{
Type p = ProxyFor;
return p != null && p.IsRegEx;
}
}

public override bool IsVariable {
get {
Expand Down Expand Up @@ -3068,6 +3136,16 @@ public override bool IsRMode {
return ExpandedType.IsRMode;
}
}
public override bool IsString {
get {
return ExpandedType.IsString;
}
}
public override bool IsRegEx {
get {
return ExpandedType.IsRegEx;
}
}
public override bool IsVariable {
get {
Expand Down Expand Up @@ -3843,7 +3921,9 @@ public enum SimpleType {
Int,
Real,
Bool,
RMode
RMode,
String,
RegEx
};


Expand Down
1 change: 1 addition & 0 deletions Source/Core/BoogiePL.atg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1284,6 +1284,7 @@ AtomExpression<out Expr/*!*/ e>
| Dec<out bd> (. e = new LiteralExpr(t, bd); .)
| Float<out bf> (. e = new LiteralExpr(t, bf); .)
| BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .)
| string (. e = new LiteralExpr(t, t.val.Trim('"')); .)

| Ident<out x> (. id = new IdentifierExpr(x, x.val); e = id; .)
[ "("
Expand Down
14 changes: 9 additions & 5 deletions Source/Core/Parser.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1811,6 +1811,11 @@ void AtomExpression(out Expr/*!*/ e) {
e = new LiteralExpr(t, bn, n);
break;
}
case 4: {
Get();
e = new LiteralExpr(t, t.val.Trim('"'));
break;
}
case 1: {
Ident(out x);
id = new IdentifierExpr(x, x.val); e = id;
Expand Down Expand Up @@ -2109,7 +2114,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
Get();
Expect(1);
key = t.val; parameters = new List<object/*!*/>();
if (StartOf(16)) {
if (StartOf(9)) {
AttributeParameter(out param);
parameters.Add(param);
while (la.kind == 13) {
Expand Down Expand Up @@ -2212,14 +2217,13 @@ public void Parse() {
{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _T,_T,_x,_T, _x,_x,_T,_T, _T,_T,_T,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_T,_T,_T, _x,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_T,_T,_T, _x,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_T,_T,_T, _x,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}
{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}

};
} // end Parser
Expand Down
32 changes: 23 additions & 9 deletions Source/Model/ModelParser.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ abstract internal class ModelParser
internal List<Model> resModels = new List<Model> ();
internal System.IO.TextReader rd;
string lastLine = "";
protected static char[] seps = new char[] { ' ' };
protected static Regex seps = new Regex("( |(?=\")|(?<=\"))");
protected static Regex bitVec = new Regex (@"\(_ BitVec (\d+)\)");
protected static Regex bv = new Regex (@"\(_ bv(\d+) (\d+)\)");

Expand Down Expand Up @@ -49,7 +49,7 @@ string[] GetWords (string line)
{
if (line == null)
return null;
var words = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
var words = Array.FindAll(seps.Split (line), word => word != "" && word != " ");
return words;
}

Expand Down Expand Up @@ -116,24 +116,38 @@ List<object> GetFunctionTokens (string newLine)

line = line.Replace ("(", " ( ");
line = line.Replace (")", " ) ");
var tuple = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
var tuple = seps.Split (line);

List<object> newTuple = new List<object> ();
Stack<List<object>> wordStack = new Stack<List<object>> ();
var wordStack = new Stack<Tuple<string,List<object>>> ();
for (int i = 0; i < tuple.Length; i++) {
string elem = tuple [i];
if (elem == "(") {
List<object> ls = new List<object> ();

if (elem == "" || elem == " ")
continue;

if (elem == "(" || elem == "\"" && (wordStack.Count == 0 || wordStack.Peek().Item1 != "\"")) {
var ls = Tuple.Create(elem, new List<object> ());
wordStack.Push (ls);
} else if (elem == ")") {
List<object> ls = wordStack.Pop ();
var tup = wordStack.Pop ();
if (tup.Item1 != "(")
BadModel("unmatched parentheses");
var ls = tup.Item2;
if (wordStack.Count > 0) {
wordStack.Peek ().Add (ls);
wordStack.Peek ().Item2.Add (ls);
} else {
newTuple.Add (ls);
}
} else if (elem == "\"") {
var words = "\"" + String.Join(" ", wordStack.Pop().Item2) + "\"";
if (wordStack.Count > 0)
wordStack.Peek().Item2.Add(String.Join(" ", words));
else
newTuple.Add(words);

} else if (wordStack.Count > 0) {
wordStack.Peek ().Add (elem);
wordStack.Peek ().Item2.Add (elem);
} else {
newTuple.Add (elem);
}
Expand Down
13 changes: 11 additions & 2 deletions Source/Provers/SMTLib/SMTLibLineariser.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ private static void TypeToStringHelper(Type t, StringBuilder sb)
}
sb.Append(']');
TypeToStringHelper(m.Result, sb);
} else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv || t.IsRMode) {
} else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv || t.IsRMode || t.IsString) {
sb.Append(TypeToString(t));
} else {
System.IO.StringWriter buffer = new System.IO.StringWriter();
Expand Down Expand Up @@ -149,8 +149,12 @@ public static string TypeToString(Type t)
return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatSignificand + ")";
else if (t.IsBv)
return "(_ BitVec " + t.BvBits + ")";
else if (t.IsRMode) {
else if (t.IsRMode)
return "RoundingMode";
else if (t.IsString)
return "String";
else if (t.IsRegEx) {
return "(RegEx String)";
} else {
StringBuilder sb = new StringBuilder();
TypeToStringHelper(t, sb);
Expand Down Expand Up @@ -218,6 +222,11 @@ public bool Visit(VCExprLiteral node, LineariserOptions options)
RoundingMode lit = ((VCExprRModeLit)node).Val;
wr.Write(lit.ToString());
}
else if (node is VCExprStringLit)
{
String lit = ((VCExprStringLit)node).Val;
wr.Write("\"" + lit.ToString() + "\"");
}
else {
Contract.Assert(false);
throw new cce.UnreachableException();
Expand Down
2 changes: 1 addition & 1 deletion Source/Provers/SMTLib/TypeDeclCollector.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -316,7 +316,7 @@ private void RegisterType(Type type)
return;
}

if (type.IsBool || type.IsInt || type.IsReal || type.IsBv || type.IsFloat || type.IsRMode)
if (type.IsBool || type.IsInt || type.IsReal || type.IsBv || type.IsFloat || type.IsRMode || type.IsString || type.IsRegEx)
return;

CtorType ctorType = type as CtorType;
Expand Down
2 changes: 2 additions & 0 deletions Source/VCExpr/Boogie2VCExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -338,6 +338,8 @@ private VCExpr TranslateLiteralExpr(LiteralExpr node) {
return Gen.Float(node.asBigFloat);
} else if (node.Val is RoundingMode) {
return Gen.RMode(node.asRoundingMode);
} else if (node.Val is String) {
return Gen.String(node.asString);
}
else if (node.Val is BvConst) {
return Gen.Bitvector((BvConst)node.Val);
Expand Down
Loading

0 comments on commit a38904c

Please sign in to comment.