src/theory/sets/theory_sets_rewriter.cpp

   1 #include "theory/sets/theory_sets_rewriter.h"
   2
   3 namespace CVC4 {
   4 namespace theory {
   5 namespace sets {
   6
   7 bool checkConstantMembership(TNode elementTerm, TNode setTerm)
   8 {
   9   switch(setTerm.getKind()) {
  10   case kind::EMPTYSET:
  11     return false;
  12   case kind::SET_SINGLETON:
  13     return elementTerm == setTerm[0];
  14   case kind::UNION:
  15     return checkConstantMembership(elementTerm, setTerm[0]) ||
  16       checkConstantMembership(elementTerm, setTerm[1]);
  17   case kind::INTERSECTION:
  18     return checkConstantMembership(elementTerm, setTerm[0]) &&
  19       checkConstantMembership(elementTerm, setTerm[1]);
  20   case kind::SETMINUS:
  21     return checkConstantMembership(elementTerm, setTerm[0]) &&
  22       !checkConstantMembership(elementTerm, setTerm[1]);
  23   default:
  24     Unhandled();
  25   }
  26 }
  27
  28 // static
  29 RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
  30   NodeManager* nm = NodeManager::currentNM();
  31
  32   switch(node.getKind()) {
  33
  34   case kind::IN: {
  35     if(!node[0].isConst() || !node[1].isConst())
  36       break;
  37
  38     // both are constants
  39     bool isMember = checkConstantMembership(node[0], node[1]);
  40     return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
  41   }
  42
  43   case kind::SUBSET: {
  44     // rewrite (A subset-or-equal B) as (A union B = B)
  45     TNode A = node[0];
  46     TNode B = node[1];
  47     return RewriteResponse(REWRITE_AGAIN,
  48                            nm->mkNode(kind::EQUAL,
  49                                       nm->mkNode(kind::UNION, A, B),
  50                                       B) );
  51   }//kind::SUBSET
  52
  53   case kind::EQUAL:
  54   case kind::IFF: {
  55     //rewrite: t = t with true (t term)
  56     //rewrite: c = c' with c different from c' false (c, c' constants)
  57     //otherwise: sort them
  58     if(node[0] == node[1]) {
  59       Trace("sets-postrewrite") << "Sets::postRewrite returning true" << std::endl;
  60       return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
  61     }
  62     else if (node[0].isConst() && node[1].isConst()) {
  63       Trace("sets-postrewrite") << "Sets::postRewrite returning false" << std::endl;
  64       return RewriteResponse(REWRITE_DONE, nm->mkConst(false));
  65     }
  66     else if (node[0] > node[1]) {
  67       Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
  68       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
  69       return RewriteResponse(REWRITE_DONE, newNode);
  70     }
  71     break;
  72   }
  73
  74   case kind::UNION:
  75   case kind::INTERSECTION: {
  76     if(node[0] == node[1]) {
  77       Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
  78       return RewriteResponse(REWRITE_DONE, node[0]);
  79     } else if (node[0] > node[1]) {
  80       Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
  81       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
  82       return RewriteResponse(REWRITE_DONE, newNode);
  83     }
  84     break;
  85   }
  86
  87   default:
  88     break;
  89
  90   }//switch(node.getKind())
  91
  92   // This default implementation
  93   return RewriteResponse(REWRITE_DONE, node);
  94 }
  95
  96 // static
  97 RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
  98   NodeManager* nm = NodeManager::currentNM();
  99
 100   // do nothing
 101   if(node.getKind() == kind::EQUAL && node[0] == node[1])
 102     return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
 103   // Further optimization, if constants but differing ones
 104
 105   return RewriteResponse(REWRITE_DONE, node);
 106 }
 107
 108 }/* CVC4::theory::sets namespace */
 109 }/* CVC4::theory namespace */
 110 }/* CVC4 namespace */