diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-12-01 02:57:59 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-12-01 02:57:59 +0000 |
commit | 959f5e77f96b406a498c3b67ce22d25e39d7bd2d (patch) | |
tree | e3cb4518ff5156de8286f9351a827bf40636804e /src/theory/quantifiers/Makefile.am | |
parent | b66fc3eac2717e8a887f1d4603c15cbcb7460e98 (diff) |
drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine
Diffstat (limited to 'src/theory/quantifiers/Makefile.am')
-rw-r--r-- | src/theory/quantifiers/Makefile.am | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 371aa5543..316af7616 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -11,16 +11,12 @@ libquantifiers_la_SOURCES = \ quantifiers_rewriter.h \ quantifiers_rewriter.cpp \ theory_quantifiers.cpp \ - theory_quantifiers_instantiator.h \ - theory_quantifiers_instantiator.cpp \ instantiation_engine.h \ instantiation_engine.cpp \ trigger.h \ trigger.cpp \ candidate_generator.h \ candidate_generator.cpp \ - instantiator_default.h \ - instantiator_default.cpp \ inst_match.h \ inst_match.cpp \ model_engine.h \ @@ -44,7 +40,11 @@ libquantifiers_la_SOURCES = \ inst_match_generator.h \ inst_match_generator.cpp \ macros.h \ - macros.cpp + macros.cpp \ + inst_strategy_e_matching.h \ + inst_strategy_e_matching.cpp \ + inst_strategy_cbqi.h \ + inst_strategy_cbqi.cpp EXTRA_DIST = \ kinds \ |