Adding table-based implementation of predicates and new config for encoding negation...

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 88868544ca2e01a19e020fca231492692a1aea8d..fa124a68f741e7044cd10c2b3cbe0ec0bdbdc494 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -72,7 +72,6 @@ Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value)
                                elemEnc->variables, i);
                }
        }
-       ASSERT(0);
        return NULL;
 }
 
@@ -297,6 +296,7 @@ Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
        switch(constraint->encoding.type){
                case ENUMERATEIMPLICATIONS:
+               case ENUMERATEIMPLICATIONSNEGATE:
                        return encodeEnumTablePredicateSATEncoder(This, constraint);
                case CIRCUIT:
                        ASSERT(0);
@@ -309,12 +309,26 @@ Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate
 
 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
        VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
+       FunctionEncodingType encType = constraint->encoding.type;
        uint size = getSizeVectorTableEntry(entries);
+       Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
        for(uint i=0; i<size; i++){
                TableEntry* entry = getVectorTableEntry(entries, i);
-               
+               if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
+                       continue;
+               else if(encType==ENUMERATEIMPLICATIONSNEGATE && entry->output !=false)
+                       continue;
+               ArrayElement* inputs = &constraint->inputs;
+               uint inputNum =getSizeArrayElement(inputs);
+               Constraint* carray[inputNum];
+               Element* el = getArrayElement(inputs, i);
+               for(uint j=0; j<inputNum; j++){
+                       carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
+               }
+               constraints[i]=allocArrayConstraint(AND, inputNum, carray);
        }
-       return NULL;
+       Constraint* result= allocArrayConstraint(OR, size, constraints);
+       return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result);
 }
 
 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){

diff --git a/src/Encoders/functionencoding.h b/src/Encoders/functionencoding.h
index a3521396f04abef9689b7371f4905e88b430dd14..41d99761e6958309e66f946e1e428c2e89639cbb 100644 (file)
--- a/src/Encoders/functionencoding.h
+++ b/src/Encoders/functionencoding.h
@@ -3,7 +3,7 @@
 #include "classlist.h"
 
 enum FunctionEncodingType {
-       FUNC_UNASSIGNED, ENUMERATEIMPLICATIONS, CIRCUIT
+       FUNC_UNASSIGNED, ENUMERATEIMPLICATIONS, ENUMERATEIMPLICATIONSNEGATE, CIRCUIT
 };
 
 typedef enum FunctionEncodingType FunctionEncodingType;