From: Guy <katz911@gmail.com>
Date: Fri, 1 Jul 2016 23:49:02 +0000 (-0700)
Subject: When proving a lemma, ignore literals that don't belong to the theory in question... 
X-Git-Tag: cvc5-1.0.0~6049^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a58abbe71fb1fc07129ff9c7568ac544145fb57c;p=cvc5.git

When proving a lemma, ignore literals that don't belong to the theory in question, except for equalties
---

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index e70cd60b9..d12b561a6 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -948,11 +948,15 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->ProduceProofs() DONE" << std::endl;
 
   MyPreRegisterVisitor preRegVisitor(th);
-  for( unsigned i=0; i<lemma.size(); i++ ){
-    Node lit = Node::fromExpr( lemma[i] ).negate();
-    Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl;
-    NodeVisitor<MyPreRegisterVisitor>::run(preRegVisitor, lit);
-    th->assertFact(lit, false);
+  for (unsigned i=0; i<lemma.size(); i++) {
+    Node strippedLit = (lemma[i].getKind() == kind::NOT) ? lemma[i][0] : lemma[i];
+    if (strippedLit.getKind() == kind::EQUAL ||
+        d_theory->getId() == theory::Theory::theoryOf(strippedLit)) {
+      Node lit = Node::fromExpr( lemma[i] ).negate();
+      Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl;
+      NodeVisitor<MyPreRegisterVisitor>::run(preRegVisitor, lit);
+      th->assertFact(lit, false);
+    }
   }
 
   Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->check()" << std::endl;