Merge pull request #341 from yushan87/prover-theorem-utils

Prover Immutable Theorem Representation

Author: yushan87

src/main/java/edu/clemson/cs/rsrg/prover/utilities/ImmutableVC.java

@@ -145,6 +145,15 @@ public final ConjunctionOfNormalizedAtomicExpressions getConjunct() {
         return myConjunction;
     }
 
+    /**
+     * <p>This method returns the current registry of symbols.</p>
+     *
+     * @return A {@link Registry}.
+     */
+    public final Registry getRegistry() {
+        return myRegistry;
+    }
+
     /**
      * <p>This method returns the current proving status for
      * this VC.</p>
@@ -287,6 +296,10 @@ private void seedDefaultTheorems() {
         myConjunction.addExpression(fandfeqf);
     }
 
+    // ===========================================================
+    // Helper Constructs
+    // ===========================================================
+
     /**
      * <p>When building an {@link ImmutableVC}, both Mike and Hampton did a bunch of
      * conversions. This class allows us to keep the same logic, but not have a separate

src/main/java/edu/clemson/cs/rsrg/prover/utilities/PExpWithScore.java

@@ -0,0 +1,105 @@
+/*
+ * PExpWithScore.java
+ * ---------------------------------
+ * Copyright (c) 2019
+ * RESOLVE Software Research Group
+ * School of Computing
+ * Clemson University
+ * All rights reserved.
+ * ---------------------------------
+ * This file is subject to the terms and conditions defined in
+ * file 'LICENSE.txt', which is part of this source code package.
+ */
+package edu.clemson.cs.rsrg.prover.utilities;
+
+import edu.clemson.cs.rsrg.prover.absyn.PExp;
+import java.util.Map;
+
+/**
+ * <p>This class allows us to create a comparable theorem with a score.</p>
+ *
+ * @author Mike Kabbani
+ * @version 2.0
+ */
+public class PExpWithScore implements Comparable<PExpWithScore> {
+
+    // ===========================================================
+    // Member Fields
+    // ===========================================================
+
+    /** <p>A theorem expression</p> */
+    private final PExp myTheorem;
+
+    /** <p>The theorem's definition.</p> */
+    private final String myTheoremDefinitionString;
+
+    /** <p>A comparison score.</p> */
+    private final Integer myScore;
+
+    /** <p>A map of symbols in this theorem.</p> */
+    private final Map<String, String> myBMap;
+
+    // ===========================================================
+    // Constructors
+    // ===========================================================
+
+    /**
+     * <p>This constructs a new expression that includes a score.</p>
+     *
+     * @param theorem A theorem represented as a {@link PExp}.
+     * @param bMap A map of symbols in this theorem.
+     * @param justification The theorem definition expressed as a string.
+     */
+    public PExpWithScore(PExp theorem, Map<String, String> bMap,
+            String justification) {
+        myBMap = bMap;
+        myScore = 1;
+        myTheorem = theorem;
+        myTheoremDefinitionString = justification;
+    }
+
+    // ===========================================================
+    // Public Methods
+    // ===========================================================
+
+    /**
+     * <p>Compares <code>this<code> and <code>o</code>.</p>
+     *
+     * @param o Another {@link PExpWithScore}.
+     *
+     * @return Comparison results expressed as an integer.
+     */
+    @Override
+    public final int compareTo(PExpWithScore o) {
+        return myScore - o.myScore;
+    }
+
+    /**
+     * <p>This method returns a theorem expression.</p>
+     *
+     * @return A {@link PExp}.
+     */
+    public final PExp getTheorem() {
+        return myTheorem;
+    }
+
+    /**
+     * <p>This method returns the theorem definition.</p>
+     *
+     * @return A string.
+     */
+    public final String getTheoremDefinitionString() {
+        return myTheoremDefinitionString;
+    }
+
+    /**
+     * <p>This method returns this expression in string format.</p>
+     *
+     * @return A string.
+     */
+    @Override
+    public final String toString() {
+        return myTheoremDefinitionString + "\n" + "\t[" + myScore + "]" + " "
+                + myTheorem.toString() + "\t" + myBMap + "\n";
+    }
+}

src/main/java/edu/clemson/cs/rsrg/prover/utilities/Registry.java

@@ -246,8 +246,6 @@ public final int findAndCompress(int index) {
         return index;
     }
 
-    //
-
     /**
      * <p>This method gets the set of children symbol names.</p>
      *

src/main/java/edu/clemson/cs/rsrg/prover/utilities/expressions/ConjunctionOfNormalizedAtomicExpressions.java

@@ -313,6 +313,16 @@ public final Set<Map<String, String>> getMatchesForOverrideSet(NormalizedAtomicE
         return rSet;
     }
 
+    /**
+     * <p>This method returns the set of normalized atomic expressions
+     * used as keys in this conjunction.</p>
+     *
+     * @return A set of {@link NormalizedAtomicExpression}.
+     */
+    public final Set<NormalizedAtomicExpression> getNormalizedAtomicExpressionKeys() {
+        return myExpressionSet.keySet();
+    }
+
     /**
      * <p>This method returns the set of expressions based on the
      * symbol number.</p>