Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Implementation of dynamic_rewriter.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/dynamic_rewrite.h"
      14                 :            : 
      15                 :            : #include "expr/skolem_manager.h"
      16                 :            : #include "smt/env.h"
      17                 :            : #include "theory/rewriter.h"
      18                 :            : 
      19                 :            : using namespace std;
      20                 :            : using namespace cvc5::internal::kind;
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace theory {
      24                 :            : namespace quantifiers {
      25                 :            : 
      26                 :         39 : DynamicRewriter::DynamicRewriter(Env& env,
      27                 :            :                                  context::Context* c,
      28                 :         39 :                                  const std::string& name)
      29                 :         39 :     : d_equalityEngine(env, c, "DynamicRewriter::" + name, true), d_rewrites(c)
      30                 :            : {
      31                 :         39 :   d_equalityEngine.addFunctionKind(Kind::APPLY_UF);
      32                 :         39 : }
      33                 :            : 
      34                 :          3 : void DynamicRewriter::addRewrite(Node a, Node b)
      35                 :            : {
      36         [ +  - ]:          3 :   Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl;
      37         [ -  + ]:          3 :   if (a == b)
      38                 :            :   {
      39         [ -  - ]:          0 :     Trace("dyn-rewrite") << "...equal." << std::endl;
      40                 :          0 :     return;
      41                 :            :   }
      42                 :            : 
      43                 :            :   // add to the equality engine
      44                 :          3 :   Node ai = toInternal(a);
      45                 :          3 :   Node bi = toInternal(b);
      46 [ +  - ][ -  + ]:          3 :   if (ai.isNull() || bi.isNull())
                 [ -  + ]
      47                 :            :   {
      48         [ -  - ]:          0 :     Trace("dyn-rewrite") << "...not internalizable." << std::endl;
      49                 :          0 :     return;
      50                 :            :   }
      51         [ +  - ]:          3 :   Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl;
      52                 :            : 
      53         [ +  - ]:          3 :   Trace("dyn-rewrite-debug") << "assert eq..." << std::endl;
      54                 :          3 :   Node eq = ai.eqNode(bi);
      55                 :          3 :   d_rewrites.push_back(eq);
      56                 :          3 :   d_equalityEngine.assertEquality(eq, true, eq);
      57 [ -  + ][ -  + ]:          3 :   Assert(d_equalityEngine.consistent());
                 [ -  - ]
      58         [ +  - ]:          3 :   Trace("dyn-rewrite-debug") << "Finished" << std::endl;
      59 [ +  - ][ +  - ]:          3 : }
      60                 :            : 
      61                 :          6 : bool DynamicRewriter::areEqual(Node a, Node b)
      62                 :            : {
      63         [ -  + ]:          6 :   if (a == b)
      64                 :            :   {
      65                 :          0 :     return true;
      66                 :            :   }
      67         [ +  - ]:          6 :   Trace("dyn-rewrite-debug") << "areEqual? : " << a << " " << b << std::endl;
      68                 :            :   // add to the equality engine
      69                 :          6 :   Node ai = toInternal(a);
      70                 :          6 :   Node bi = toInternal(b);
      71 [ +  - ][ -  + ]:          6 :   if (ai.isNull() || bi.isNull())
                 [ -  + ]
      72                 :            :   {
      73         [ -  - ]:          0 :     Trace("dyn-rewrite") << "...not internalizable." << std::endl;
      74                 :          0 :     return false;
      75                 :            :   }
      76         [ +  - ]:          6 :   Trace("dyn-rewrite-debug") << "internal : " << ai << " " << bi << std::endl;
      77                 :          6 :   d_equalityEngine.addTerm(ai);
      78                 :          6 :   d_equalityEngine.addTerm(bi);
      79         [ +  - ]:          6 :   Trace("dyn-rewrite-debug") << "...added terms" << std::endl;
      80                 :          6 :   return d_equalityEngine.areEqual(ai, bi);
      81                 :          6 : }
      82                 :            : 
      83                 :         33 : Node DynamicRewriter::toInternal(Node a)
      84                 :            : {
      85                 :         33 :   std::map<Node, Node>::iterator it = d_term_to_internal.find(a);
      86         [ +  + ]:         33 :   if (it != d_term_to_internal.end())
      87                 :            :   {
      88                 :         24 :     return it->second;
      89                 :            :   }
      90                 :          9 :   Node ret = a;
      91                 :            : 
      92         [ +  + ]:          9 :   if (!a.isVar())
      93                 :            :   {
      94                 :          4 :     std::vector<Node> children;
      95         [ +  + ]:          4 :     if (a.hasOperator())
      96                 :            :     {
      97                 :          3 :       Node op = a.getOperator();
      98         [ +  - ]:          3 :       if (a.getKind() != Kind::APPLY_UF)
      99                 :            :       {
     100                 :          3 :         op = d_ois_trie[op].getSymbol(a);
     101                 :            :         // if this term involves an argument that is not of first class type,
     102                 :            :         // we cannot reason about it. This includes operators like str.in-re.
     103         [ -  + ]:          3 :         if (op.isNull())
     104                 :            :         {
     105                 :          0 :           return Node::null();
     106                 :            :         }
     107                 :            :       }
     108                 :          3 :       children.push_back(op);
     109         [ +  - ]:          3 :     }
     110         [ +  + ]:         10 :     for (const Node& ca : a)
     111                 :            :     {
     112                 :          6 :       Node cai = toInternal(ca);
     113         [ -  + ]:          6 :       if (cai.isNull())
     114                 :            :       {
     115                 :          0 :         return Node::null();
     116                 :            :       }
     117                 :          6 :       children.push_back(cai);
     118 [ +  - ][ +  - ]:          6 :     }
     119         [ +  + ]:          4 :     if (!children.empty())
     120                 :            :     {
     121         [ -  + ]:          3 :       if (children.size() == 1)
     122                 :            :       {
     123                 :          0 :         ret = children[0];
     124                 :            :       }
     125                 :            :       else
     126                 :            :       {
     127                 :          3 :         ret = a.getNodeManager()->mkNode(Kind::APPLY_UF, children);
     128                 :            :       }
     129                 :            :     }
     130         [ +  - ]:          4 :   }
     131                 :          9 :   d_term_to_internal[a] = ret;
     132                 :          9 :   d_internal_to_term[ret] = a;
     133                 :          9 :   return ret;
     134                 :          9 : }
     135                 :            : 
     136                 :          0 : Node DynamicRewriter::toExternal(Node ai)
     137                 :            : {
     138                 :          0 :   std::map<Node, Node>::iterator it = d_internal_to_term.find(ai);
     139         [ -  - ]:          0 :   if (it != d_internal_to_term.end())
     140                 :            :   {
     141                 :          0 :     return it->second;
     142                 :            :   }
     143                 :          0 :   return Node::null();
     144                 :            : }
     145                 :            : 
     146                 :          3 : Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
     147                 :            : {
     148                 :          3 :   NodeManager* nm = n.getNodeManager();
     149                 :          3 :   std::vector<TypeNode> ctypes;
     150         [ +  + ]:          9 :   for (const Node& cn : n)
     151                 :            :   {
     152                 :          6 :     ctypes.push_back(cn.getType());
     153                 :          6 :   }
     154                 :          3 :   ctypes.push_back(n.getType());
     155                 :            : 
     156                 :          3 :   OpInternalSymTrie* curr = this;
     157         [ +  + ]:         12 :   for (unsigned i = 0, size = ctypes.size(); i < size; i++)
     158                 :            :   {
     159                 :            :     // cannot handle certain types (e.g. regular expressions or functions)
     160         [ -  + ]:          9 :     if (!ctypes[i].isFirstClass())
     161                 :            :     {
     162                 :          0 :       return Node::null();
     163                 :            :     }
     164                 :          9 :     curr = &(curr->d_children[ctypes[i]]);
     165                 :            :   }
     166         [ +  + ]:          3 :   if (!curr->d_sym.isNull())
     167                 :            :   {
     168                 :          1 :     return curr->d_sym;
     169                 :            :   }
     170                 :            :   // make UF operator
     171                 :          2 :   TypeNode utype;
     172         [ -  + ]:          2 :   if (ctypes.size() == 1)
     173                 :            :   {
     174                 :          0 :     utype = ctypes[0];
     175                 :            :   }
     176                 :            :   else
     177                 :            :   {
     178                 :          2 :     utype = nm->mkFunctionType(ctypes);
     179                 :            :   }
     180                 :          4 :   Node f = NodeManager::mkDummySkolem("ufd", utype);
     181                 :          2 :   curr->d_sym = f;
     182                 :          2 :   return f;
     183                 :          3 : }
     184                 :            : 
     185                 :            : }  // namespace quantifiers
     186                 :            : }  // namespace theory
     187                 :            : }  // namespace cvc5::internal