Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
- uint numDomains = getSizeArraySet(&predicate->domains);
+ uint numDomains = predicate->domains.getSize();
FunctionEncodingType encType = constraint->encoding.type;
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
/* Call base encoders for children */
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement( &constraint->inputs, i);
+ Element *elem = constraint->inputs.get(i);
encodeElementSATEncoder(This, elem);
}
VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = getArraySet(&predicate->domains, i);
+ Set *set = predicate->domains.get(i);
vals[i] = set->getElement(indices[i]);
}
if (predicate->evalPredicateOperator(vals) ^ generateNegation) {
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement(&constraint->inputs, i);
+ Element *elem = constraint->inputs.get(i);
carray[i] = getElementValueConstraint(This, elem, vals[i]);
}
Edge term = constraintAND(This->cnf, numDomains, carray);
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = getArraySet(&predicate->domains, i);
+ Set *set = predicate->domains.get(i);
if (index < set->getSize()) {
vals[i] = set->getElement(index);
model_print("Operator Function ...\n");
#endif
FunctionOperator *function = (FunctionOperator *) func->function;
- uint numDomains = getSizeArrayElement(&func->inputs);
+ uint numDomains = func->inputs.getSize();
/* Call base encoders for children */
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement( &func->inputs, i);
+ Element *elem = func->inputs.get(i);
encodeElementSATEncoder(This, elem);
}
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = getElementSet(getArrayElement(&func->inputs, i));
+ Set *set = getElementSet(func->inputs.get(i));
vals[i] = set->getElement(indices[i]);
}
if (needClause) {
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement(&func->inputs, i);
+ Element *elem = func->inputs.get(i);
carray[i] = getElementValueConstraint(This, elem, vals[i]);
}
if (isInRange) {
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = getElementSet(getArrayElement(&func->inputs, i));
+ Set *set = getElementSet(func->inputs.get(i));
if (index < set->getSize()) {
vals[i] = set->getElement(index);
Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
- ASSERT(getSizeArraySet(&predicate->domains) == 2);
- Element *elem0 = getArrayElement( &constraint->inputs, 0);
+ Element *elem0 = constraint->inputs.get(0);
encodeElementSATEncoder(This, elem0);
- Element *elem1 = getArrayElement( &constraint->inputs, 1);
+ Element *elem1 = constraint->inputs.get(1);
encodeElementSATEncoder(This, elem1);
ElementEncoding *ee0 = getElementEncoding(elem0);
ElementEncoding *ee1 = getElementEncoding(elem1);