mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

add missing files

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-22 09:48:08 -08:00
parent 8540b379ad
commit fcdde59438
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/muz_qe/pdr_dl_interface.cpp
View file

@ -25,7 +25,7 @@ Revision History:
#include "dl_mk_rule_inliner.h"
#include "dl_rule.h"
#include "dl_rule_transformer.h"
//include "dl_mk_extract_quantifiers.h"
#include "dl_mk_extract_quantifiers.h"
#include "smt2parser.h"
#include "pdr_context.h"
#include "pdr_dl_interface.h"
@ -146,7 +146,6 @@ lbool dl_interface::query(expr * query) {
--num_unfolds;
}
}
#if 0
// remove universal quantifiers from body.
datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx);
datalog::rule_transformer extract_q_tr(m_ctx);
@ -186,8 +185,7 @@ lbool dl_interface::query(expr * query) {
return result;
}
}
#endif
return l_undef;
}
expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) {