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                 GETELEMENTPARENTS(_inputs[i])->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         if (map->boolean.contains(this)) {
  48                 return map->boolean.get(this);
  49         } else {
  50                 Boolean * bvar=solver->getBooleanVar(type);
  51                 map->boolean.put(this, bvar);
  52                 return bvar;
  53         }
  54 }
  55
  56 Boolean * BooleanOrder::clone(CSolver * solver, CloneMap *map) {
  57         Order * ordercopy=order->clone(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(map);
  75         Boolean * defstatus=(undefStatus != NULL) ? undefStatus->clone(solver, map) : NULL;
  76
  77         return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus);
  78 }