Merge pull request #129 from sanctuuary/fix_119_empty_clause_creation

Implement non-empty clause counting which fixes an empty clause error when having only one tool in the workflow

Author: eladrion

src/main/java/nl/uu/cs/ape/models/templateFormulas/SLTLxTemplateFormula.java

@@ -545,6 +545,7 @@ public static String connectedModules(TaxonomyPredicate firstPredicate, Taxonomy
         for (Integer currComb : allCombinations) {
             constraints.append(currComb + " ");
         }
+
         constraints.append("0\n");
 
         // each combination enforces usage of the corresponding tools and output/inputs

src/main/java/nl/uu/cs/ape/solver/minisat/SATSynthesisEngine.java

@@ -278,7 +278,7 @@ public boolean synthesisEncoding() throws IOException {
          * counted again.
          */
         int variables = mappings.getSize();
-        int clauses = APEUtils.countLines(cnfEncoding);
+        int clauses = APEUtils.countCNFClauses(new FileInputStream(cnfEncoding));
         String satInputHeader = "p cnf " + variables + " " + clauses + "\n";
         APEUtils.timerRestartAndPrint(currLengthTimer, "Reading rows");
         satInputFile = APEFiles.prependToFile(satInputHeader, cnfEncoding);

src/main/java/nl/uu/cs/ape/solver/minisat/SatEncodingUtils.java

@@ -74,7 +74,7 @@ public static String encodeAPEConstraints(SATSynthesisEngine synthesisEngine, AP
     }
 
     /**
-     * Function used to provide SAT encoding of a constrain based on the constraint
+     * Function used to provide SAT encoding of a constraint based on the constraint
      * ID specified and provided parameters.
      *
      * @param constraintID    ID of the constraint.

src/main/java/nl/uu/cs/ape/utils/APEUtils.java

@@ -469,6 +469,59 @@ public static void timerPrintText(String timerID, String text) {
 		log.info(text + " Running time: " + (printTime / 1000F) + " sec.");
 	}
 
+    /**
+     * This function counts the CNF clauses in a stream, assuming correct CNF syntax.
+     *
+     * @param cnfEncoding the CNF encoding
+     * @return the count of non-empty clauses
+     */
+    public static int countCNFClauses(InputStream cnfEncoding) {
+
+        int count = 0;
+        try (BufferedReader b = new BufferedReader(new InputStreamReader(cnfEncoding))) {
+            String line = null;
+            while ((line = b.readLine()) != null) {
+                if (line.endsWith(" 0")) count++;
+            }
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+
+        return count;
+    }
+
+    /**
+     * This function counts the non-empty CNF clauses in a stream and
+     * while also checking the CNF syntax and warns if a clause is empty.
+     *
+     * @param cnfEncoding the CNF encoding
+     * @return the count of non-empty clauses
+     */
+    public static int checkCNFClauses(InputStream cnfEncoding) {
+
+        int clauseCount = 0;
+        int litCount    = 0;
+
+        Scanner scanner = new Scanner(cnfEncoding);
+        while (scanner.hasNextInt()) {
+            int intAtom = scanner.nextInt();
+
+            if (intAtom == 0) {
+                if (litCount == 0) {
+                    log.warn("Found empty clause (" + (clauseCount + 1) + ") after in CNF input, will not count for DIMACS.");
+                } else {
+                    clauseCount++;
+                }
+                litCount = 0;
+            } else {
+                litCount++;
+            }
+        }
+        scanner.close();
+
+        return clauseCount;
+    }
+
 	/**
 	 * Convert cnf 2 human readable string.
 	 *