+void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
+ uint numParents = elem->parents.getSize();
+ uint posPolarity = 0;
+ uint negPolarity = 0;
+ memo = false;
+ if (elem->type == ELEMFUNCRETURN) {
+ memo = true;
+ }
+ for (uint i = 0; i < numParents; i++) {
+ ASTNode *node = elem->parents.get(i);
+ if (node->type == PREDICATEOP) {
+ BooleanPredicate *pred = (BooleanPredicate *) node;
+ Polarity polarity = pred->polarity;
+ FunctionEncodingType encType = pred->encoding.type;
+ bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+ if (pred->predicate->type == TABLEPRED) {
+ //Could be smarter, but just do default thing for now
+
+ UndefinedBehavior undefStatus = ((PredicateTable *)pred->predicate)->undefinedbehavior;
+
+ Polarity tpolarity = polarity;
+ if (generateNegation)
+ tpolarity = negatePolarity(tpolarity);
+ if (undefStatus == SATC_FLAGFORCEUNDEFINED)
+ tpolarity = P_BOTHTRUEFALSE;
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+ memo = true;
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+ memo = true;
+ } else if (pred->predicate->type == OPERATORPRED) {
+ if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) {
+ Polarity tpolarity = polarity;
+ if (generateNegation)
+ tpolarity = negatePolarity(tpolarity);
+ PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
+ uint numDomains = pred->inputs.getSize();
+ bool isConstant = true;
+ for (uint i = 0; i < numDomains; i++) {
+ Element *e = pred->inputs.get(i);
+ if (elem != e && e->type != ELEMCONST) {
+ isConstant = false;
+ }
+ }
+ if (predicate->getOp() == SATC_EQUALS) {
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+ posPolarity++;
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+ negPolarity++;
+ } else {
+ if (isConstant) {
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+ posPolarity++;
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+ negPolarity++;
+ } else {
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+ memo = true;
+ if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+ memo = true;
+ }
+ }
+ }
+ } else {
+ ASSERT(0);
+ }
+ } else if (node->type == ELEMFUNCRETURN) {
+ //we are input to function, so memoize negative case
+ memo = true;
+ } else {
+ ASSERT(0);
+ }
+ }
+ if (posPolarity > 1)
+ memo = true;
+ if (negPolarity > 1)
+ memo = true;
+}
+
+
+Edge SATEncoder::getElementValueConstraint(Element *elem, Polarity p, uint64_t value) {
+ switch (elem->getElementEncoding()->type) {