src/theory/sets/theory_sets_rewriter.cpp

   1 /*********************                                                        */
   2 /*! \file theory_sets_rewriter.cpp
   3  ** \verbatim
   4  ** Original author: Kshitij Bansal
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2013-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Sets theory rewriter.
  13  **
  14  ** Sets theory rewriter.
  15  **/
  16
  17 #include "theory/sets/theory_sets_rewriter.h"
  18
  19 namespace CVC4 {
  20 namespace theory {
  21 namespace sets {
  22
  23 bool checkConstantMembership(TNode elementTerm, TNode setTerm)
  24 {
  25   switch(setTerm.getKind()) {
  26   case kind::EMPTYSET:
  27     return false;
  28   case kind::SET_SINGLETON:
  29     return elementTerm == setTerm[0];
  30   case kind::UNION:
  31     return checkConstantMembership(elementTerm, setTerm[0]) ||
  32       checkConstantMembership(elementTerm, setTerm[1]);
  33   case kind::INTERSECTION:
  34     return checkConstantMembership(elementTerm, setTerm[0]) &&
  35       checkConstantMembership(elementTerm, setTerm[1]);
  36   case kind::SETMINUS:
  37     return checkConstantMembership(elementTerm, setTerm[0]) &&
  38       !checkConstantMembership(elementTerm, setTerm[1]);
  39   default:
  40     Unhandled();
  41   }
  42 }
  43
  44 // static
  45 RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
  46   NodeManager* nm = NodeManager::currentNM();
  47
  48   switch(node.getKind()) {
  49
  50   case kind::MEMBER: {
  51     if(!node[0].isConst() || !node[1].isConst())
  52       break;
  53
  54     // both are constants
  55     bool isMember = checkConstantMembership(node[0], node[1]);
  56     return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
  57   }
  58
  59   case kind::SUBSET: {
  60     // rewrite (A subset-or-equal B) as (A union B = B)
  61     TNode A = node[0];
  62     TNode B = node[1];
  63     return RewriteResponse(REWRITE_AGAIN,
  64                            nm->mkNode(kind::EQUAL,
  65                                       nm->mkNode(kind::UNION, A, B),
  66                                       B) );
  67   }//kind::SUBSET
  68
  69   case kind::EQUAL:
  70   case kind::IFF: {
  71     //rewrite: t = t with true (t term)
  72     //rewrite: c = c' with c different from c' false (c, c' constants)
  73     //otherwise: sort them
  74     if(node[0] == node[1]) {
  75       Trace("sets-postrewrite") << "Sets::postRewrite returning true" << std::endl;
  76       return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
  77     }
  78     else if (node[0].isConst() && node[1].isConst()) {
  79       Trace("sets-postrewrite") << "Sets::postRewrite returning false" << std::endl;
  80       return RewriteResponse(REWRITE_DONE, nm->mkConst(false));
  81     }
  82     else if (node[0] > node[1]) {
  83       Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
  84       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
  85       return RewriteResponse(REWRITE_DONE, newNode);
  86     }
  87     break;
  88   }
  89
  90   case kind::UNION:
  91   case kind::INTERSECTION: {
  92     if(node[0] == node[1]) {
  93       Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
  94       return RewriteResponse(REWRITE_DONE, node[0]);
  95     } else if (node[0] > node[1]) {
  96       Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
  97       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
  98       return RewriteResponse(REWRITE_DONE, newNode);
  99     }
 100     break;
 101   }
 102
 103   default:
 104     break;
 105
 106   }//switch(node.getKind())
 107
 108   // This default implementation
 109   return RewriteResponse(REWRITE_DONE, node);
 110 }
 111
 112 // static
 113 RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
 114   NodeManager* nm = NodeManager::currentNM();
 115
 116   // do nothing
 117   if(node.getKind() == kind::EQUAL && node[0] == node[1])
 118     return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
 119   // Further optimization, if constants but differing ones
 120
 121   return RewriteResponse(REWRITE_DONE, node);
 122 }
 123
 124 }/* CVC4::theory::sets namespace */
 125 }/* CVC4::theory namespace */
 126 }/* CVC4 namespace */