diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
| commit | 304404e3709ff7e95156c87f65a3e2647d9f3441 (patch) | |
| tree | 10fd1c4cc42567c3fac5fd91ad76aef3d49975b5 /src/theory/uf | |
| parent | 697dd317af39a896865c99b922e80baac2bb4b23 (diff) | |
more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_instantiator.cpp | 3 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_instantiator.h | 1 |
2 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index 24da83786..eceb4715b 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/options.h" #include "theory/rewriterules/options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/candidate_generator.h" using namespace std; using namespace CVC4; @@ -771,7 +772,7 @@ void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler& handler, //take all terms from the uf term db and add to candidate generator if( pats[0].getKind() == kind::INST_CONSTANT ){ TypeNode ty = pats[0].getType(); - rrinst::CandidateGenerator* cg = d_quantEngine->getRRCanGenClasses(ty); + rrinst::CandidateGenerator* cg = new GenericCandidateGeneratorClasses(d_quantEngine); cg->reset(Node::null()); TNode c; SetNode ele; diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index 13a35d8a3..501ef9a6d 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -26,6 +26,7 @@ #include "util/statistics_registry.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/inst_match_generator.h" #include "util/ntuple.h" #include "context/cdqueue.h" |