more

proofs/alf/rules/drat/sat-lemmas-prove.sh

@@ -4,12 +4,14 @@
 # true if it is as expected:
 # (
 # "name of CNF file"
+# "name of SMT-LIB file"
 # "name of original SMT-LIB problem"
 # t
 # )
 
 count=0
 cnfFile=""
+smtFile=""
 lemmas=""
 while read -r line
     do
@@ -19,9 +21,12 @@ while read -r line
         cnfFile="$line"
         count=$((count+1))
     elif (( count == 2 )); then
+        smtFile="$line"
+        count=$((count+1))
+    elif (( count == 3 )); then
         lemmas="$line"
         count=$((count+1))
-    elif (( count == 3 )) && [[ "$line" == ")" ]]; then
+    elif (( count == 4 )) && [[ "$line" == ")" ]]; then
         break
     else
         echo "false"
@@ -30,7 +35,13 @@ while read -r line
 done < /dev/stdin
 
 # >&2 echo "File with CNF: $cnfFile"
+# >&2 echo "File with CNF: $smtFile"
 # >&2 echo "Lemmas to prove: $lemmas"
 
+## TODO:
+# 1. ensure $cnfFile is unsat
+# 2. minimize the lemmas necessary to refute $cnfFile
+# 3. check the corresponding lemmas in $lemmas that were in the minimized lemma set
+
 echo "true"
 exit 0

src/prop/cnf_stream.cpp

@@ -848,7 +848,7 @@ void CnfStream::dumpDimacs(std::ostream& out,
       lits.push_back(n);
     }
     Trace("dimacs-debug") << "Print " << n << std::endl;
-    // dclauses << "@l" << lemmaId++ << " ";
+    dclauses << "@l" << lemmaId++ << " ";
     for (const Node& l : lits)
     {
       SatLiteral lit = getLiteral(l);