Simplify Constant methods in Absy.cs.

Addresses review comments in PR #767.
boogie-org · Aug 4, 2023 · e059d8e · e059d8e
1 parent 89643d8
commit e059d8e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 20 deletions.
diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
@@ -1429,23 +1429,7 @@ public class Constant : Variable
     // from all other constants.
     public readonly bool Unique;
 
-    public IList<Axiom> DefinitionAxioms => definitionAxioms;
-
-    private IList<Axiom> definitionAxioms = new List<Axiom>();
-
-    public bool RemoveDefinitionAxiom(Axiom axiom)
-    {
-      Contract.Requires(axiom != null);
-
-      return definitionAxioms.Remove(axiom);
-    }
-
-    public void AddDefinitionAxiom(Axiom axiom)
-    {
-      Contract.Requires(axiom != null);
-
-      DefinitionAxioms.Add(axiom);
-    }
+    public IList<Axiom> DefinitionAxioms { get; set; }
 
     public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent)
       : this(tok, typedIdent, true)
@@ -1468,7 +1452,7 @@ public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent,
       Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);
       Contract.Requires(typedIdent.WhereExpr == null);
       this.Unique = unique;
-      this.definitionAxioms = definitionAxioms ?? new List<Axiom>();
+      this.DefinitionAxioms = definitionAxioms ?? new List<Axiom>();
     }
 
     public override bool IsMutable => false;

diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs
@@ -1522,9 +1522,9 @@ void UpdateConstantDependencies(HashSet<Constant> constants)
             {
               foreach (var newAxiom in newAxioms.Where(ax => newAxiomConstants[ax].Contains(constant)))
               {
-                constant.AddDefinitionAxiom(newAxiom);
+                constant.DefinitionAxioms.Add(newAxiom);
               }
-              constant.RemoveDefinitionAxiom(oldAxiom);
+              constant.DefinitionAxioms.Remove(oldAxiom);
             }
           }
         }