diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-28 13:27:27 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-28 13:27:27 -0600 |
| commit | 3234db430074e278258e6d687c07146a59769a92 (patch) | |
| tree | 17db55e1ff335c3998e1c4e172d174dc9f6e3b21 /src/theory/quantifiers/fmf | |
| parent | 4cd2d73366aba081a38900ddc2f4f172ce9ed2f8 (diff) | |
Use standard equality engine information in quantifiers state (#5824)
This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.
This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
Diffstat (limited to 'src/theory/quantifiers/fmf')
| -rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index b2c7bf704..053174d07 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -358,7 +358,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ Node r = fm->getRepresentative( it->second[a] ); if( Trace.isOn("fmc-model-debug") ){ std::vector< Node > eqc; - d_qe->getEqualityQuery()->getEquivalenceClass( r, eqc ); + d_qstate.getEquivalenceClass(r, eqc); Trace("fmc-model-debug") << " " << (it->second[a]==r); Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 4d74c1697..427d82e7c 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -279,14 +279,13 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ if( !riter.isIncomplete() ){ int triedLemmas = 0; int addedLemmas = 0; - EqualityQuery* qy = d_quantEngine->getEqualityQuery(); Instantiate* inst = d_quantEngine->getInstantiate(); while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match InstMatch m( f ); for (unsigned i = 0; i < riter.getNumTerms(); i++) { - m.set(qy, i, riter.getCurrentTerm(i)); + m.set(d_qstate, i, riter.getCurrentTerm(i)); } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; |