Branch data     Line data    Source code

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