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