From 959f5e77f96b406a498c3b67ce22d25e39d7bd2d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 1 Dec 2012 02:57:59 +0000 Subject: 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 --- src/theory/quantifiers/model_builder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/quantifiers/model_builder.cpp') diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index c7e68acb1..2f44140c2 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -17,7 +17,6 @@ #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_model.h" -#include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" @@ -25,6 +24,7 @@ #include "theory/quantifiers/model_builder.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/inst_gen.h" +#include "theory/quantifiers/trigger.h" using namespace std; using namespace CVC4; -- cgit v1.2.3