diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-24 17:44:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-24 22:44:52 +0000 |
| commit | 77b75a69e51b742e1448d754b6886c10ef76e79f (patch) | |
| tree | b3c4f9793fc0db34494e1d914286e32a1bd4c04c /src/theory/quantifiers/conjecture_generator.cpp | |
| parent | cfe207563479a1e9e13d52bdd93446a8c816636a (diff) | |
Use inference manager to access intantiate utility instead of quantifiers engine (#6198)
Towards breaking dependencies on quantifers engine.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index f1ed9fe00..04ab464f8 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" @@ -602,7 +603,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) //check each skolem variable bool disproven = true; std::vector<Node> skolems; - d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems); + d_qim.getSkolemize()->getSkolemConstants(q, skolems); Trace("sg-conjecture") << " CONJECTURE : "; std::vector< Node > ce; for (unsigned j = 0; j < skolems.size(); j++) @@ -1102,7 +1103,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< if( n.getNumChildren()>0 ){ Trace("sg-gt-enum-debug") << "Get enumerate uf terms " << n << " (" << num << ")" << std::endl; - TermEnumeration* te = d_quantEngine->getTermEnumeration(); + TermEnumeration* te = d_quantEngine->getTermRegistry().getTermEnumeration(); // below, we do a fair enumeration of vectors vec of indices whose sum is // 1,2,3, ... std::vector< int > vec; |