45 vector<Expr> operatorStack;
46 vector<int> childStack;
49 operatorStack.push_back(e);
50 childStack.push_back(0);
52 while (!operatorStack.empty()) {
53 DebugAssert(operatorStack.size() == childStack.size(),
"Invariant violated");
54 if (childStack.back() < operatorStack.back().arity()) {
55 e2 = operatorStack.back()[childStack.back()++];
59 if (operatorStack.size() >= 5000) {
64 operatorStack.push_back(e2);
65 childStack.push_back(0);
69 cache[operatorStack.back()] =
true;
70 operatorStack.pop_back();
71 childStack.pop_back();
74 DebugAssert(childStack.empty(),
"Invariant violated");
104 if (ppRes.
isRefl())
break;
142 TRACE(
"pushNegation",
"pushNegationRec(", e,
143 ", neg=" +
string(neg?
"true":
"false") +
") {");
147 TRACE(
"pushNegation",
"pushNegationRec [cached] => ", (*i).second,
"}");
153 switch(e.getKind()) {
166 vector<Theorem> thms;
186 vector<Theorem> thms;
196 switch(e.getKind()) {
203 vector<Theorem> thms;
219 TRACE(
"pushNegation",
"pushNegationRec => ", res,
"}");
231 "pushNegationRec(Theorem, neg = true): bad Theorem: "
240 TRACE(
"pushNegation1",
"pushNegation1(", e,
") {");
243 switch(e[0].getKind()) {
256 vector<Theorem> thms;
268 vector<Theorem> thms;
277 TRACE(
"pushNegation1",
"pushNegation1 => ", res.getExpr(),
" }");
301 if (it != cache.
end())
return (*it).second;
306 if (thm.getRHS().isBoolConst()) {
314 vector<Theorem> newChildrenThm;
315 vector<unsigned> changed;
317 for(
int k = 0; k < ar; ++k) {
321 newChildrenThm.push_back(thm2);
322 changed.push_back(k);
325 if(changed.size() > 0) {
358 vector<Theorem> newChildrenThm;
359 vector<unsigned> changed;
360 int ar = current.
arity();
361 for(
int k = 0; k < ar; ++k) {
365 newChildrenThm.push_back(thm);
366 changed.push_back(k);
369 if(changed.size() > 0) {
386 if ((newExpr[0].isLiteral() || newExpr[0].isAnd())) {
415 const set<Expr>& careSet)
421 set<Expr>* cs2 = (*it).second;
422 set<Expr>* csNew =
new set<Expr>;
423 set_intersection(careSet.begin(), careSet.end(), cs2->begin(), cs2->end(),
424 inserter(*csNew, csNew->begin()));
425 (*it).second = csNew;
429 queue[e] =
new set<Expr>(careSet);
449 it = substTable.
find(e);
450 iend = substTable.
end();
458 vector<Theorem> newChildrenThm;
459 vector<unsigned> changed;
460 for(
int k = 0; k < ar; ++k) {
463 newChildrenThm.push_back(thm);
464 changed.push_back(k);
467 if(changed.size() > 0) {
489 while (!queue.
empty()) {
530 set<Expr>::iterator iCare, iCareEnd = cs.end();
534 iCare = cs.find(v[0]);
535 if (iCare != iCareEnd) {
543 iCare = cs.find(v[0].negate());
544 if (iCare != iCareEnd) {
556 cs.insert(v[0].negate());
562 for (i = 0; i < v.
arity(); ++i) {
563 iCare = cs.find(v[i].negate());
564 if (iCare != iCareEnd) {
578 for (i = 1; i < v.
arity(); ++i) {
585 for (i = 0; i < v.
arity(); ++i) {
586 iCare = cs.find(v[i]);
587 if (iCare != iCareEnd) {
596 cs.insert(v[1].negate());
598 cs.erase(v[1].negate());
599 cs.insert(v[0].negate());
600 for (i = 1; i < v.
arity(); ++i) {
612 for (
int i = 0; i < v.
arity(); ++i) {