From cda29bc03b8e0e64099a4f7b95792fc181471a46 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Apr 2013 15:29:52 -0700 Subject: [PATCH] add abstraction and instantiation Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 9207fbe61..44852a52f 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -47,6 +47,7 @@ Revision History: #include"dl_mk_array_blast.h" #include"dl_mk_karr_invariants.h" #include"dl_mk_quantifier_abstraction.h" +#include"dl_mk_quantifier_instantiation.h" #include"datatype_decl_plugin.h" #include"expr_abstract.h" @@ -908,6 +909,7 @@ namespace datalog { m_transf.register_plugin(alloc(datalog::mk_quantifier_abstraction, *this, 33000)); + m_transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, *this, 32000)); m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000));