diff options
author | Guy <katz911@gmail.com> | 2016-07-01 16:49:02 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-01 16:49:02 -0700 |
commit | a58abbe71fb1fc07129ff9c7568ac544145fb57c (patch) | |
tree | bbca6289fad9fdd3ea21b27bee9f6be82b1c5685 /src | |
parent | 1d4ad74ca90641bd9165f9a2c019c54cde6e80c1 (diff) |
When proving a lemma, ignore literals that don't belong to the theory in question, except for equalties
Diffstat (limited to 'src')
-rw-r--r-- | src/proof/theory_proof.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
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; |