src/AST/boolean.cc

   1 #include "boolean.h"
   2 #include "structs.h"
   3 #include "csolver.h"
   4 #include "element.h"
   5 #include "order.h"
   6 #include "predicate.h"
   7
   8 Boolean::Boolean(ASTNodeType _type) :
   9         ASTNode(_type),
  10         polarity(P_UNDEFINED),
  11         boolVal(BV_UNDEFINED),
  12         parents() {
  13 }
  14
  15 BooleanVar::BooleanVar(VarType t) :
  16         Boolean(BOOLEANVAR),
  17         vtype(t),
  18         var(E_NULL) {
  19 }
  20
  21 BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) :
  22         Boolean(ORDERCONST),
  23         order(_order),
  24         first(_first),
  25         second(_second) {
  26         order->constraints.push(this);
  27 }
  28
  29 BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) :
  30         Boolean(PREDICATEOP),
  31         predicate(_predicate),
  32         encoding(this),
  33         inputs(_inputs, _numInputs),
  34         undefStatus(_undefinedStatus) {
  35         for (uint i = 0; i < _numInputs; i++) {
  36                 _inputs[i]->parents.push(this);
  37         }
  38 }
  39
  40 BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize) :
  41         Boolean(LOGICOP),
  42         op(_op),
  43         inputs(array, asize) {
  44 }
  45
  46 Boolean *BooleanVar::clone(CSolver *solver, CloneMap *map) {
  47         Boolean *b = (Boolean *) map->get(this);
  48         if (b != NULL)
  49                 return b;
  50         Boolean *bvar = solver->getBooleanVar(type);
  51         map->put(this, bvar);
  52         return bvar;
  53 }
  54
  55 Boolean *BooleanOrder::clone(CSolver *solver, CloneMap *map) {
  56         Order *ordercopy = order->clone(solver, map);
  57         return solver->orderConstraint(ordercopy, first, second);
  58 }
  59
  60 Boolean *BooleanLogic::clone(CSolver *solver, CloneMap *map) {
  61         Boolean *array[inputs.getSize()];
  62         for (uint i = 0; i < inputs.getSize(); i++) {
  63                 array[i] = inputs.get(i)->clone(solver, map);
  64         }
  65         return solver->applyLogicalOperation(op, array, inputs.getSize());
  66 }
  67
  68 Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
  69         Element *array[inputs.getSize()];
  70         for (uint i = 0; i < inputs.getSize(); i++) {
  71                 array[i] = inputs.get(i)->clone(solver, map);
  72         }
  73         Predicate *pred = predicate->clone(solver, map);
  74         Boolean *defstatus = (undefStatus != NULL) ? undefStatus->clone(solver, map) : NULL;
  75
  76         return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus);
  77 }