Add utilities for dumping DIMACS (cvc5#10447)

Towards proofs that rely on external SAT calls.

src/prop/cnf_stream.cpp

@@ -778,5 +778,51 @@ CnfStream::Statistics::Statistics(StatisticsRegistry& sr,
 {
 }
 
+void CnfStream::dumpDimacs(std::ostream& out, const std::vector<Node>& clauses)
+{
+  std::vector<Node> auxUnits;
+  dumpDimacs(out, clauses, auxUnits);
+}
+
+void CnfStream::dumpDimacs(std::ostream& out,
+                           const std::vector<Node>& clauses,
+                           const std::vector<Node>& auxUnits)
+{
+  std::stringstream dclauses;
+  SatVariable maxVar = 0;
+  for (size_t j = 0; j < 2; j++)
+  {
+    const std::vector<Node>& cls = j == 0 ? clauses : auxUnits;
+    for (const Node& i : cls)
+    {
+      std::vector<Node> lits;
+      if (j == 0 && i.getKind() == Kind::OR)
+      {
+        // print as clause if not an auxiliary unit
+        lits.insert(lits.end(), i.begin(), i.end());
+      }
+      else
+      {
+        lits.push_back(i);
+      }
+      Trace("dimacs-debug") << "Print " << i << std::endl;
+      for (const Node& l : lits)
+      {
+        bool negated = l.getKind() == Kind::NOT;
+        const Node& atom = negated ? l[0] : l;
+        SatLiteral lit = getLiteral(atom);
+        SatVariable v = lit.getSatVariable();
+        maxVar = v > maxVar ? v : maxVar;
+        dclauses << (negated ? "-" : "") << v << " ";
+      }
+      dclauses << "0" << std::endl;
+    }
+  }
+
+  out << "p cnf " << maxVar << " " << (clauses.size() + auxUnits.size())
+      << std::endl;
+  out << dclauses.str();
+}
+
 }  // namespace prop
 }  // namespace cvc5::internal

src/prop/cnf_stream.h

@@ -159,7 +159,54 @@ class CnfStream : protected EnvObj
   /** Retrieves map from literals to nodes. */
   const CnfStream::LiteralToNodeMap& getNodeCache() const;
 
+  /**
+   * Dump dimacs of the given clauses to the given output stream.
+   * We use the identifiers for literals computed by this class. All literals
+   * in clauses should be assigned by this class already.
+   *
+   * @param out The output stream.
+   * @param clauses The clauses to print.
+   */
+  void dumpDimacs(std::ostream& out, const std::vector<Node>& clauses);
+  /**
+   * Same as above, but additionally prints the clauses in auxUnits as unit
+   * clauses, after clause. In particular, say
+   * we pass the following clauses to this method:
+   *
+   * (or ~(or A B) ~C)
+   * (or A B)
+   * C
+   *
+   * And the auxilary units:
+   *
+   * (or A B)
+   *
+   * Here, we would print the DIMACS:
+   *
+   * p cnf 4 4
+   * -1 -2 0
+   * 3 4 0
+   * 2 0
+   * 1 0
+   *
+   * Note that the copy of (or A B) in clauses is printed as "3 4 0" whereas
+   * the copy of (or A B) in auxUnits is printed as "1 0".
+   *
+   * @param out The output stream.
+   * @param clauses The clauses to print.
+   * @param auxUnits The auxiliary units that were appended to the end of the
+   * DIMACS, after clauses were printed.
+   */
+  void dumpDimacs(std::ostream& out,
+                  const std::vector<Node>& clauses,
+                  const std::vector<Node>& auxUnits);
+
  protected:
+  /** Helper function */
+  void dumpDimacsInternal(std::ostream& out,
+                          const std::vector<Node>& clauses,
+                          std::vector<Node>& auxUnits,
+                          bool printAuxUnits);
   /**
    * Same as above, except that uses the saved d_removable flag. It calls the
    * dedicated converter for the possible formula kinds.

src/prop/proof_cnf_stream.cpp

@@ -953,5 +953,18 @@ SatLiteral ProofCnfStream::handleIte(TNode node)
   return lit;
 }
 
+void ProofCnfStream::dumpDimacs(std::ostream& out,
+                                const std::vector<Node>& clauses)
+{
+  d_cnfStream.dumpDimacs(out, clauses);
+}
+
+void ProofCnfStream::dumpDimacs(std::ostream& out,
+                                const std::vector<Node>& clauses,
+                                const std::vector<Node>& auxUnits)
+{
+  d_cnfStream.dumpDimacs(out, clauses, auxUnits);
+}
+
 }  // namespace prop
 }  // namespace cvc5::internal

src/prop/proof_cnf_stream.h

@@ -65,6 +65,7 @@ class ProofCnfStream : protected EnvObj
    */
   void convertAndAssert(
       TNode node, bool negated, bool removable, bool input, ProofGenerator* pg);
+
   /**
    * Ensure that the given node will have a designated SAT literal that is
    * definitionally equal to it.  The result of this function is that the Node
@@ -90,6 +91,19 @@ class ProofCnfStream : protected EnvObj
    */
   void getBooleanVariables(std::vector<TNode>& outputVariables) const;
 
+  /**
+   * Dump dimacs of the given clauses to the given output stream.
+   * For details, see cnf_stream.h.
+   */
+  void dumpDimacs(std::ostream& out, const std::vector<Node>& clauses);
+  /**
+   * Same as above, but also prints additional "auxiliary unit" clauses.
+   * For details, see cnf_stream.h.
+   */
+  void dumpDimacs(std::ostream& out,
+                  const std::vector<Node>& clauses,
+                  const std::vector<Node>& auxUnits);
+
  private:
   /**
    * Same as above, except that uses the saved d_removable flag. It calls the

src/prop/prop_proof_manager.cpp

@@ -270,6 +270,33 @@ Node PropPfManager::normalizeAndRegister(TNode clauseNode,
 
 LazyCDProof* PropPfManager::getCnfProof() { return &d_proof; }
 
+std::vector<Node> PropPfManager::computeAuxiliaryUnits(
+    const std::vector<Node>& clauses)
+{
+  std::vector<Node> auxUnits;
+  for (const Node& c : clauses)
+  {
+    if (c.getKind() != Kind::OR)
+    {
+      continue;
+    }
+    // Determine if any OR child occurs as a top level clause. If so, it may
+    // be relevant to include this as a unit clause.
+    for (const Node& l : c)
+    {
+      const Node& atom = l.getKind() == Kind::NOT ? l[0] : l;
+      if (atom.getKind() == Kind::OR
+          && std::find(clauses.begin(), clauses.end(), atom) != clauses.end()
+          && std::find(auxUnits.begin(), auxUnits.end(), atom)
+                 == auxUnits.end())
+      {
+        auxUnits.push_back(atom);
+      }
+    }
+  }
+  return auxUnits;
+}
+
 std::vector<Node> PropPfManager::getInputClauses()
 {
   std::vector<Node> cls;

src/prop/prop_proof_manager.h

@@ -163,6 +163,27 @@ class PropPfManager : protected EnvObj
   std::vector<Node> getInputClauses();
   /** Retrieve the clauses derived from lemmas */
   std::vector<Node> getLemmaClauses();
+  /**
+   * Get auxilary units. Computes top-level formulas in clauses that
+   * also occur as literals which we call "auxiliary units". In particular,
+   * consider the set of propositionally unsatisfiable clauses:
+   *
+   * (or ~(or A B) ~C)
+   * (or A B)
+   * C
+   *
+   * Here, we return (or A B) as an auxilary unit clause.
+   *
+   * Note that in the above example, it is ambiguous whether to interpret the
+   * second clause (or A B) as a unit clause or as a clause with literals
+   * A and B. To ensure that we generate an unsatisfiable DIMACS, we include
+   * both in a proof output. In particular, Any OR-term that occurs as a literal
+   * of another clause is included in the return vector.
+   *
+   * @param clauses The clauses
+   * @return the auxiliary units for the set of clauses.
+   */
+  std::vector<Node> computeAuxiliaryUnits(const std::vector<Node>& clauses);
   /** The proofs of this proof manager, which are saved once requested (note the
    * cache is for both the request of the full proof (true) or not (false)).
    *