[PCover] Minor improvements

p-org · Nov 7, 2023 · abb3387 · abb3387
1 parent 7528d06
commit abb3387
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 7 deletions.
diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/Guard.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/Guard.java
@@ -9,6 +9,9 @@
  * Currently, the guards are implemented using BDDs.
  */
 public class Guard implements Serializable {
+  private static Guard trueGuard = null;
+  private static Guard falseGuard = null;
+
   /** Represents the boolean formula for the restrict */
   private final SolverGuard guard;
 
@@ -17,12 +20,11 @@ public Guard(SolverGuard guard) {
   }
 
   /**
-   * Create a constant false restrict
-   *
-   * @return Guard representing constant false
+   * Initialize true/false guards
    */
-  public static Guard constFalse() {
-    return new Guard(SolverGuard.constFalse());
+  public static void initialize() {
+    trueGuard = new Guard(SolverGuard.constTrue());
+    falseGuard = new Guard(SolverGuard.constFalse());
   }
 
   /**
@@ -31,7 +33,16 @@ public static Guard constFalse() {
    * @return Guard representing constant true
    */
   public static Guard constTrue() {
-    return new Guard(SolverGuard.constTrue());
+    return trueGuard;
+  }
+
+  /**
+   * Create a constant false restrict
+   *
+   * @return Guard representing constant false
+   */
+  public static Guard constFalse() {
+    return falseGuard;
   }
 
   /**

diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/PrimitiveVS.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/PrimitiveVS.java
@@ -122,7 +122,15 @@ public List<GuardedValue<T>> getGuardedValues() {
 
   @Override
   public Guard getUniverse() {
-    if (universe == null) universe = Guard.orMany(new ArrayList<>(guardedValues.values()));
+    if (universe == null) {
+      universe = Guard.constFalse();
+      for (Guard g : guardedValues.values()) {
+        universe = universe.or(g);
+        if (universe.isTrue()) {
+          break;
+        }
+      }
+    }
     return universe;
   }
 

diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/solvers/SolverEngine.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/solvers/SolverEngine.java
@@ -4,6 +4,7 @@
 import lombok.Getter;
 import lombok.Setter;
 import psym.runtime.logger.SearchLogger;
+import psym.valuesummary.Guard;
 import psym.valuesummary.solvers.bdd.PJBDDImpl;
 import psym.valuesummary.solvers.sat.expr.ExprLibType;
 
@@ -21,6 +22,7 @@ public static void resumeEngine() {
     }
     setSolver(getSolverType(), getExprLibType());
     SolverGuard.resumeSolverGuard();
+    Guard.initialize();
   }
 
   public static void resetEngine(SolverType type, ExprLibType etype) {
@@ -29,6 +31,7 @@ public static void resetEngine(SolverType type, ExprLibType etype) {
     }
     setSolver(type, etype);
     SolverGuard.reset();
+    Guard.initialize();
   }
 
   public static void cleanupEngine() {