src/AST/predicate.cc

   1 #include "predicate.h"
   2 #include "boolean.h"
   3 #include "set.h"
   4 #include "table.h"
   5 #include "csolver.h"
   6
   7 PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), domains(domain, numDomain), op(_op) {
   8 }
   9
  10 PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) {
  11 }
  12
  13 bool PredicateOperator::evalPredicateOperator(uint64_t *inputs) {
  14         switch (op) {
  15         case SATC_EQUALS:
  16                 return inputs[0] == inputs[1];
  17         case SATC_LT:
  18                 return inputs[0] < inputs[1];
  19         case SATC_GT:
  20                 return inputs[0] > inputs[1];
  21         case SATC_LTE:
  22                 return inputs[0] <= inputs[1];
  23         case SATC_GTE:
  24                 return inputs[0] >= inputs[1];
  25         }
  26         ASSERT(0);
  27         return false;
  28 }
  29
  30 Predicate *PredicateOperator::clone(CSolver *solver, CloneMap *map) {
  31         Predicate *p = (Predicate *) map->get(this);
  32         if (p != NULL)
  33                 return p;
  34
  35         Set *array[domains.getSize()];
  36         for (uint i = 0; i < domains.getSize(); i++)
  37                 array[i] = domains.get(i)->clone(solver, map);
  38
  39         p = solver->createPredicateOperator(op, array, domains.getSize());
  40         map->put(this, p);
  41         return p;
  42 }
  43
  44 Predicate *PredicateTable::clone(CSolver *solver, CloneMap *map) {
  45         Predicate *p = (Predicate *) map->get(this);
  46         if (p != NULL)
  47                 return p;
  48
  49         p = solver->createPredicateTable(table->clone(solver, map), undefinedbehavior);
  50         map->put(this, p);
  51         return p;
  52 }
  53
  54 void PredicateTable::serialize(Serializer* serializer){
  55         if(serializer->isSerialized(this))
  56                 return;
  57         serializer->addObject(this);
  58
  59         table->serialize(serializer);
  60
  61         ASTNodeType type = PREDTABLETYPE;
  62         serializer->mywrite(&type, sizeof(ASTNodeType));
  63         PredicateTable* This = this;
  64         serializer->mywrite(&This, sizeof(PredicateTable*));
  65         serializer->mywrite(&table, sizeof(Table *));
  66         serializer->mywrite(&undefinedbehavior, sizeof(UndefinedBehavior));
  67 }
  68
  69 void PredicateTable::print(){
  70         model_println("{PredicateTable:");
  71         table->print();
  72         model_println("}\n");
  73 }
  74
  75 void PredicateOperator::serialize(Serializer* serializer){
  76         if(serializer->isSerialized(this))
  77                 return;
  78         serializer->addObject(this);
  79
  80         uint size = domains.getSize();
  81         for(uint i=0; i<size; i++){
  82                 Set* domain = domains.get(i);
  83                 domain->serialize(serializer);
  84         }
  85
  86         ASTNodeType type = PREDOPERTYPE;
  87         serializer->mywrite(&type, sizeof(ASTNodeType));
  88         PredicateOperator* This = this;
  89         serializer->mywrite(&This, sizeof(PredicateOperator*));
  90         serializer->mywrite(&op, sizeof(CompOp));
  91         serializer->mywrite(&size, sizeof(uint));
  92         for(uint i=0; i<size; i++){
  93                 Set* domain = domains.get(i);
  94                 serializer->mywrite(&domain, sizeof(Set*));
  95         }
  96 }
  97
  98 void PredicateOperator::print(){
  99         model_println("{PredicateOperator: %s }", op ==SATC_EQUALS? "EQUAL": "NOT-EQUAL");
 100 }
 101
 102
 103