From c198f374972e62db0cebc93d3977fd1e414f431b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 8 Feb 2021 16:50:16 -0600 Subject: Use quantifiers inference manager for lemma management (#5867) Towards eliminating dependencies on quantifiers engine. This replaces the custom implementation of lemma management in quantifiers engine with the standard one. It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers. Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact. --- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/cegqi/ceg_instantiator.cpp') diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 411ab36b9..b2fff012e 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1082,8 +1082,9 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector } Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl; bool ret = d_parent->doAddInstantiation(subs); - for( unsigned i=0; iaddLemma(lemmas[i]); + for (const Node& l : lemmas) + { + d_parent->addPendingLemma(l); } return ret; } -- cgit v1.2.3