more

proofs/alf/rules/drat/Drat.smt3

@@ -68,9 +68,14 @@
   :conclusion false
 )
 
+(declare-oracle-fun run_sat_lemmas_prove (String Bool) Bool ./sat-lemmas-prove.sh)
 
-
-
+(declare-rule sat_lemmas_external_prove ((F Bool) (D String) (L Bool))
+  :premise-list F and
+  :args (D L)
+  :requires (((run_sat_lemmas_prove D L) true))
+  :conclusion false
+)
 
 ; run_sat_prove_dimacs takes:
 ; - A string corresponding to a DIMACS input.

src/prop/prop_proof_manager.cpp

@@ -325,24 +325,8 @@ std::shared_ptr<ProofNode> PropPfManager::getProof(
     std::fstream dout(dinputFile.str(), std::ios::out);
     d_proofCnfStream->dumpDimacs(dout, inputs, lemmas);
     dout.close();
-
-    // Build the equalities between the lemma ids and the lemmas. Note that we
-    // expect that the order in which the ids are assigned to lemma clauses is
-    // the same as the one in which they are converted to DIMACs.
-    std::vector<Node> namedLemmas;
-    for (size_t i = 0, size = lemmas.size(); i < size; ++i)
-    {
-      std::stringstream lemmaId;
-      lemmaId << "@l" << i;
-      Node lemmaIdNode = nm->mkRawSymbol(lemmaId.str(), bt);
-      namedLemmas.push_back(nm->mkNode(Kind::SEXPR,
-                                       {nm->mkRawSymbol("!", bt),
-                                        lemmas[i],
-                                        nm->mkRawSymbol(":named", bt),
-                                        lemmaIdNode}));
-    }
-    args.push_back(lemmas.size() > 1 ? nm->mkNode(Kind::AND, namedLemmas)
-                                     : namedLemmas[0]);
+    args.push_back(lemmas.size() > 1 ? nm->mkNode(Kind::AND, lemmas)
+                                     : lemmas[0]);
     // build the proof node
     CDProof cdp(d_env);
     Node falseNode = nm->mkConst(false);