38 d_commonRules(tm->getRules()),
43 d_statistics(statistics),
45 d_nullExpr(tm->getEM()->getNullExpr()),
52 if (flags[
"minimizeClauses"].getBool()) {
53 CLFlags flags = ValidityChecker::createFlags();
54 flags.
setFlag(
"minimizeClauses",
false);
55 d_vc = ValidityChecker::create(flags);
81 bool foundInCache =
false;
101 vector<Theorem> thms;
102 vector<unsigned> changed;
106 for(i = e.
begin(), iend = e.
end(); i!=iend; ++i, ++index) {
111 for(i = e.
begin(), iend = e.
end(); i!=iend; ++i, ++index) {
115 changed.push_back(index);
118 if(changed.size() > 0) {
126 if (!foundInCache)
d_iteMap[e] = thm;
157 return Lit((*iMap).second);
162 bool translateOnly =
false;
166 translateOnly =
true;
184 for (i = e.
begin(), iend = e.
end(); i != iend; ++i) {
188 vector<Expr> new_chls;
189 vector<Theorem> thms;
190 for (idx = 0; idx < lits.size(); ++idx) {
195 Expr after = (isAnd ?
Expr(
AND,new_chls) : Expr(
OR,new_chls)) ;
199 for (idx = 0; idx < lits.size(); ++idx) {
206 std::string reasonStr = (isAnd ?
"and_mid" :
"or_mid");
213 for (idx = 0; idx < lits.size(); ++idx) {
217 std::string reasonStr = (isAnd ?
"and_final" :
"or_final") ;
220 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
227 vector<Theorem> thms;
258 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
268 vector<Theorem> thms;
304 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
316 vector<Theorem> thms;
352 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
368 after.push_back(aftere0);
369 after.push_back(aftere1);
370 after.push_back(aftere2);
384 vector<Theorem> thms ;
385 thms.push_back(e0thm);
386 thms.push_back(e1thm);
387 thms.push_back(e2thm);
432 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
438 "Corrupted Varinfo");
444 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
463 "Expected existing literal");
475 if (!translateOnly) {
501 for (i = e.
begin(), iend = e.
end(); i != iend; ++i) {
504 if (!translateOnly)
d_varInfo[v].fanins.push_back(l);
543 if (!translateOnly)
d_varInfo[v].fanins.push_back(l);
553 newLits.push_back(lb);
556 unsigned new_lb = (ub-lb+1)/2 + lb;
560 for (index = new_lb; index <= ub; ++index) {
566 cons(new_lb, ub, e2, newLits);
570 unsigned new_ub = new_lb-1;
572 for (index = lb; index <= new_ub; ++index) {
578 cons(lb, new_ub, e2, newLits);
582 cons(new_lb, ub, e2, newLits);
585 for (index = 0; index < newLits.size(); ++index) {
588 cons(lb, new_ub, e2, newLits);
596 vector<Theorem> clauses;
600 vector<Theorem>::iterator i = clauses.begin(), iend = clauses.end();
601 for (; i < iend; ++i) {
604 Expr e = (*i).getExpr();
625 if (
d_flags[
"cnf-formula"].getBool()) {
630 "expr:" + e.
toString() +
" is not an OR Expr or Ture or False" );
633 for (
int i = 0; i < e.
arity(); i++){
677 vector<Theorem> clauses;
679 DebugAssert(clauses.size() == 1,
"expected single clause");