diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-17 14:42:50 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 07:42:50 -0600 |
commit | 2d6de44a51fed47a625ae73181efbcc3dac0c751 (patch) | |
tree | 50ebd370468514d15b71a1d5f7d8993c24116fc0 /src/theory/quantifiers/cegqi | |
parent | a1a2d9389730ed46ab246865e320108db07c30ff (diff) |
Add InferenceId to buffered inference manager (#5911)
This PR collects the InferenceId in the InferenceManagerBuffered class.
Diffstat (limited to 'src/theory/quantifiers/cegqi')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 208933456..c37054fdd 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -394,7 +394,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) { Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i] << std::endl; - d_qim.addPendingLemma(auxLems[i]); + d_qim.addPendingLemma(auxLems[i], InferenceId::UNKNOWN); } } @@ -495,7 +495,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { bool InstStrategyCegqi::addPendingLemma(Node lem) const { - return d_qim.addPendingLemma(lem); + return d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); } CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { @@ -536,7 +536,7 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister) // add lemmas to process for (const Node& lem : lems) { - d_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); } // don't need to process this, since it has been reduced return true; |