Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Yoni Zohar, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Implementation of global_negate.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "preprocessing/passes/global_negate.h"
      17                 :            : 
      18                 :            : #include <vector>
      19                 :            : 
      20                 :            : #include "expr/node.h"
      21                 :            : #include "preprocessing/assertion_pipeline.h"
      22                 :            : #include "expr/node_algorithm.h"
      23                 :            : #include "theory/rewriter.h"
      24                 :            : 
      25                 :            : using namespace std;
      26                 :            : using namespace cvc5::internal::kind;
      27                 :            : using namespace cvc5::internal::theory;
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : namespace preprocessing {
      31                 :            : namespace passes {
      32                 :            : 
      33                 :          8 : Node GlobalNegate::simplify(const std::vector<Node>& assertions,
      34                 :            :                             NodeManager* nm)
      35                 :            : {
      36 [ -  + ][ -  + ]:          8 :   Assert(!assertions.empty());
                 [ -  - ]
      37         [ +  - ]:          8 :   Trace("cegqi-gn") << "Global negate : " << std::endl;
      38                 :            :   // collect free variables in all assertions
      39                 :         16 :   std::unordered_set<Node> syms;
      40                 :         16 :   std::unordered_set<TNode> visited;
      41         [ +  + ]:         24 :   for (const Node& as : assertions)
      42                 :            :   {
      43         [ +  - ]:         16 :     Trace("cegqi-gn") << "  " << as << std::endl;
      44                 :         16 :     expr::getSymbols(as, syms, visited);
      45                 :            :   }
      46         [ +  + ]:         10 :   for (const Node& s : syms)
      47                 :            :   {
      48         [ +  + ]:          8 :     if (s.getType().isFirstClass())
      49                 :            :     {
      50                 :            :       // We have a symbol whose type is not first class. For example, a
      51                 :            :       // datatype selector. In such cases, this preprocessing pass cannot be
      52                 :            :       // applied.
      53                 :          6 :       return Node::null();
      54                 :            :     }
      55                 :            :   }
      56                 :          4 :   std::vector<Node> fvs(syms.begin(), syms.end());
      57                 :            : 
      58                 :          4 :   Node body;
      59         [ -  + ]:          2 :   if (assertions.size() == 1)
      60                 :            :   {
      61                 :          0 :     body = assertions[0];
      62                 :            :   }
      63                 :            :   else
      64                 :            :   {
      65                 :          2 :     body = nm->mkNode(Kind::AND, assertions);
      66                 :            :   }
      67                 :            : 
      68                 :            :   // do the negation
      69                 :          2 :   body = body.negate();
      70                 :            : 
      71         [ -  + ]:          2 :   if (!fvs.empty())
      72                 :            :   {
      73                 :          0 :     std::vector<Node> bvs;
      74         [ -  - ]:          0 :     for (const Node& v : fvs)
      75                 :            :     {
      76                 :          0 :       Node bv = nm->mkBoundVar(v.getType());
      77                 :          0 :       bvs.push_back(bv);
      78                 :            :     }
      79                 :            : 
      80                 :          0 :     body = body.substitute(
      81                 :          0 :         fvs.begin(), fvs.end(), bvs.begin(), bvs.end());
      82                 :            : 
      83                 :          0 :     Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, bvs);
      84                 :            : 
      85                 :          0 :     body = nm->mkNode(Kind::FORALL, bvl, body);
      86                 :            :   }
      87                 :            : 
      88         [ +  - ]:          2 :   Trace("cegqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
      89                 :          2 :   body = rewrite(body);
      90         [ +  - ]:          2 :   Trace("cegqi-gn") << "...got (post-rewrite) : " << body << std::endl;
      91                 :          2 :   return body;
      92                 :            : }
      93                 :            : 
      94                 :      50369 : GlobalNegate::GlobalNegate(PreprocessingPassContext* preprocContext)
      95                 :      50369 :     : PreprocessingPass(preprocContext, "global-negate"){};
      96                 :            : 
      97                 :          8 : PreprocessingPassResult GlobalNegate::applyInternal(
      98                 :            :     AssertionPipeline* assertionsToPreprocess)
      99                 :            : {
     100                 :          8 :   NodeManager* nm = nodeManager();
     101                 :         16 :   Node simplifiedNode = simplify(assertionsToPreprocess->ref(), nm);
     102         [ +  + ]:          8 :   if (simplifiedNode.isNull())
     103                 :            :   {
     104                 :            :     // failed to convert, possibly due to an unhandled symbol
     105                 :          6 :     return PreprocessingPassResult::NO_CONFLICT;
     106                 :            :   }
     107                 :          4 :   Node trueNode = nm->mkConst(true);
     108                 :            :   // mark as negated
     109                 :          2 :   assertionsToPreprocess->markNegated();
     110         [ +  - ]:          2 :   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
     111                 :            :   {
     112         [ +  - ]:          2 :     if (i == 0)
     113                 :            :     {
     114                 :          2 :       assertionsToPreprocess->replace(i, simplifiedNode);
     115         [ +  - ]:          2 :       if (assertionsToPreprocess->isInConflict())
     116                 :            :       {
     117                 :          2 :         return PreprocessingPassResult::CONFLICT;
     118                 :            :       }
     119                 :            :     }
     120                 :            :     else
     121                 :            :     {
     122                 :          0 :       assertionsToPreprocess->replace(i, trueNode);
     123                 :            :     }
     124                 :            :   }
     125                 :          0 :   return PreprocessingPassResult::NO_CONFLICT;
     126                 :            : }
     127                 :            : 
     128                 :            : 
     129                 :            : }  // namespace passes
     130                 :            : }  // namespace preprocessing
     131                 :            : }  // namespace cvc5::internal