LCOV - code coverage report
Current view: top level - buildbot/coverage/build/src/theory/quantifiers - extended_rewrite.h (source / functions) Hit Total Coverage
Test: coverage.info Lines: 1 1 100.0 %
Date: 2025-02-09 13:32:29 Functions: 1 1 100.0 %
Branches: 0 0 -

           Branch data     Line data    Source code
       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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                 :            :  * extended rewriting class
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
      19                 :            : #define CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
      20                 :            : 
      21                 :            : #include <unordered_map>
      22                 :            : 
      23                 :            : #include "expr/node.h"
      24                 :            : #include "expr/subs.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace theory {
      28                 :            : 
      29                 :            : class Rewriter;
      30                 :            : 
      31                 :            : namespace quantifiers {
      32                 :            : 
      33                 :            : /** Extended rewriter
      34                 :            :  *
      35                 :            :  * This class is used for all rewriting that is not necessarily
      36                 :            :  * helpful for quantifier-free solving, but is helpful
      37                 :            :  * in other use cases. An example of this is SyGuS, where rewriting
      38                 :            :  * can be used for generalizing refinement lemmas, and hence
      39                 :            :  * should be highly aggressive.
      40                 :            :  *
      41                 :            :  * This class extended the standard techniques for rewriting
      42                 :            :  * with techniques, including but not limited to:
      43                 :            :  * - Redundant child elimination,
      44                 :            :  * - Sorting children of commutative operators,
      45                 :            :  * - Boolean constraint propagation,
      46                 :            :  * - Equality chain normalization,
      47                 :            :  * - Negation normal form,
      48                 :            :  * - Simple ITE pulling,
      49                 :            :  * - ITE conditional variable elimination,
      50                 :            :  * - ITE condition subsumption.
      51                 :            :  */
      52                 :            : class ExtendedRewriter
      53                 :            : {
      54                 :            :  public:
      55                 :            :   ExtendedRewriter(NodeManager* nm, Rewriter& rew, bool aggr = true);
      56                 :     592763 :   ~ExtendedRewriter() {}
      57                 :            :   /** return the extended rewritten form of n */
      58                 :            :   Node extendedRewrite(Node n) const;
      59                 :            : 
      60                 :            :  private:
      61                 :            :   /** Pointer to the underlying node manager */
      62                 :            :   NodeManager* d_nm;
      63                 :            :   /** The underlying rewriter that we are extending  */
      64                 :            :   Rewriter& d_rew;
      65                 :            :   /** cache that the extended rewritten form of n is ret */
      66                 :            :   void setCache(Node n, Node ret) const;
      67                 :            :   /** get the cache for n */
      68                 :            :   Node getCache(Node n) const;
      69                 :            :   /** add to children
      70                 :            :    *
      71                 :            :    * Adds nc to the vector of children, if dropDup is true, we do not add
      72                 :            :    * nc if it already occurs in children. This method returns false in this
      73                 :            :    * case, otherwise it returns true.
      74                 :            :    */
      75                 :            :   bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup) const;
      76                 :            : 
      77                 :            :   //--------------------------------------generic utilities
      78                 :            :   /** Rewrite ITE, for example:
      79                 :            :    *
      80                 :            :    * ite( ~C, s, t ) ---> ite( C, t, s )
      81                 :            :    * ite( A or B, s, t ) ---> ite( ~A and ~B, t, s )
      82                 :            :    * ite( x = c, x, t ) --> ite( x = c, c, t )
      83                 :            :    * t * { x -> c } = s => ite( x = c, s, t ) ---> t
      84                 :            :    *
      85                 :            :    * The parameter "full" indicates an effort level that this rewrite will
      86                 :            :    * take. If full is false, then we do only perform rewrites that
      87                 :            :    * strictly decrease the term size of n.
      88                 :            :    */
      89                 :            :   Node extendedRewriteIte(Kind itek, Node n, bool full = true) const;
      90                 :            :   /** Rewrite AND/OR
      91                 :            :    *
      92                 :            :    * This implements BCP, factoring, and equality resolution for the Boolean
      93                 :            :    * term n whose top symbolic is AND/OR.
      94                 :            :    */
      95                 :            :   Node extendedRewriteAndOr(Node n) const;
      96                 :            :   /** Pull ITE, for example:
      97                 :            :    *
      98                 :            :    *   D=C2 ---> false
      99                 :            :    *     implies
     100                 :            :    *   D=ite( C, C1, C2 ) --->  C ^ D=C1
     101                 :            :    *
     102                 :            :    *   f(t,t1) --> s  and  f(t,t2)---> s
     103                 :            :    *     implies
     104                 :            :    *   f(t,ite(C,t1,t2)) ---> s
     105                 :            :    *
     106                 :            :    * If this function returns a non-null node ret, then n ---> ret.
     107                 :            :    */
     108                 :            :   Node extendedRewritePullIte(Kind itek, Node n) const;
     109                 :            :   /** Negation Normal Form (NNF), for example:
     110                 :            :    *
     111                 :            :    *   ~( A & B ) ---> ( ~ A | ~B )
     112                 :            :    *   ~( ite( A, B, C ) ---> ite( A, ~B, ~C )
     113                 :            :    *
     114                 :            :    * If this function returns a non-null node ret, then n ---> ret.
     115                 :            :    */
     116                 :            :   Node extendedRewriteNnf(Node n) const;
     117                 :            :   /** (type-independent) Boolean constraint propagation, for example:
     118                 :            :    *
     119                 :            :    *   ~A & ( B V A ) ---> ~A & B
     120                 :            :    *   A & ( B = ( A V C ) ) ---> A & B
     121                 :            :    *
     122                 :            :    * This function takes as arguments the kinds that specify AND, OR, and NOT.
     123                 :            :    * It additionally takes as argument a map bcp_kinds. If this map is
     124                 :            :    * non-empty, then all terms that have a Kind that is *not* in this map should
     125                 :            :    * be treated as immutable. This is for instance to prevent propagation
     126                 :            :    * beneath illegal terms. As an example:
     127                 :            :    *   (bvand A (bvor A B)) is equivalent to (bvand A (bvor 1...1 B)), but
     128                 :            :    *   (bvand A (bvadd A B)) is not equivalent to (bvand A (bvadd 1..1 B)),
     129                 :            :    * hence, when using this function to do BCP for bit-vectors, we have that
     130                 :            :    * BITVECTOR_AND is a bcp_kind, but BITVECTOR_ADD is not.
     131                 :            :    *
     132                 :            :    * If this function returns a non-null node ret, then n ---> ret.
     133                 :            :    */
     134                 :            :   Node extendedRewriteBcp(Kind andk,
     135                 :            :                           Kind ork,
     136                 :            :                           Kind notk,
     137                 :            :                           std::map<Kind, bool>& bcp_kinds,
     138                 :            :                           Node n) const;
     139                 :            :   /** (type-independent) factoring, for example:
     140                 :            :    *
     141                 :            :    *   ( A V B ) ^ ( A V C ) ----> A V ( B ^ C )
     142                 :            :    *   ( A ^ B ) V ( A ^ C ) ----> A ^ ( B V C )
     143                 :            :    *
     144                 :            :    * This function takes as arguments the kinds that specify AND, OR, NOT.
     145                 :            :    * We assume that the children of n do not contain duplicates.
     146                 :            :    */
     147                 :            :   Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n) const;
     148                 :            :   /** (type-independent) equality resolution, for example:
     149                 :            :    *
     150                 :            :    *   ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B )
     151                 :            :    *   ( A V ~B ) & ( A = B ) ----> ( A = B )
     152                 :            :    *   ( A V B ) & ( A xor B ) ----> ( A xor B )
     153                 :            :    *   ( A & B ) V ( A xor B ) ----> B V ( A xor B )
     154                 :            :    *
     155                 :            :    * This function takes as arguments the kinds that specify AND, OR, EQUAL,
     156                 :            :    * and NOT. The equal kind eqk is interpreted as XOR if isXor is true.
     157                 :            :    * It additionally takes as argument a map bcp_kinds, which
     158                 :            :    * serves the same purpose as the above function.
     159                 :            :    * If this function returns a non-null node ret, then n ---> ret.
     160                 :            :    */
     161                 :            :   Node extendedRewriteEqRes(Kind andk,
     162                 :            :                             Kind ork,
     163                 :            :                             Kind eqk,
     164                 :            :                             Kind notk,
     165                 :            :                             std::map<Kind, bool>& bcp_kinds,
     166                 :            :                             Node n,
     167                 :            :                             bool isXor = false) const;
     168                 :            :   /** (type-independent) Equality chain rewriting, for example:
     169                 :            :    *
     170                 :            :    *   A = ( A = B ) ---> B
     171                 :            :    *   ( A = D ) = ( C = B ) ---> A = ( B = ( C = D ) )
     172                 :            :    *   A = ( A & B ) ---> ~A | B
     173                 :            :    *
     174                 :            :    * If this function returns a non-null node ret, then n ---> ret.
     175                 :            :    * This function takes as arguments the kinds that specify EQUAL, AND, OR,
     176                 :            :    * and NOT. If the flag isXor is true, the eqk is treated as XOR.
     177                 :            :    */
     178                 :            :   Node extendedRewriteEqChain(Kind eqk,
     179                 :            :                               Kind andk,
     180                 :            :                               Kind ork,
     181                 :            :                               Kind notk,
     182                 :            :                               Node n,
     183                 :            :                               bool isXor = false) const;
     184                 :            :   /** extended rewrite aggressive
     185                 :            :    *
     186                 :            :    * All aggressive rewriting techniques (those that should be prioritized
     187                 :            :    * at a lower level) go in this function.
     188                 :            :    */
     189                 :            :   Node extendedRewriteAggr(Node n) const;
     190                 :            :   /** Decompose right associative chain
     191                 :            :    *
     192                 :            :    * For term f( ... f( f( base, tn ), t{n-1} ) ... t1 ), returns term base, and
     193                 :            :    * appends t1...tn to children.
     194                 :            :    */
     195                 :            :   Node decomposeRightAssocChain(Kind k,
     196                 :            :                                 Node n,
     197                 :            :                                 std::vector<Node>& children) const;
     198                 :            :   /** Make right associative chain
     199                 :            :    *
     200                 :            :    * Sorts children to obtain list { tn...t1 }, and returns the term
     201                 :            :    * f( ... f( f( base, tn ), t{n-1} ) ... t1 ).
     202                 :            :    */
     203                 :            :   Node mkRightAssocChain(Kind k, Node base, std::vector<Node>& children) const;
     204                 :            :   /** Partial substitute
     205                 :            :    *
     206                 :            :    * Applies the substitution specified by assign to n, recursing only beneath
     207                 :            :    * terms whose Kind appears in rkinds (when rkinds is empty), and additionally
     208                 :            :    * never recursing beneath WITNESS.
     209                 :            :    */
     210                 :            :   Node partialSubstitute(Node n,
     211                 :            :                          const std::map<Node, Node>& assign,
     212                 :            :                          const std::map<Kind, bool>& rkinds) const;
     213                 :            :   /** same as above, with the subs utility */
     214                 :            :   Node partialSubstitute(Node n,
     215                 :            :                          const Subs& subs,
     216                 :            :                          const std::map<Kind, bool>& rkinds) const;
     217                 :            :   /** solve equality
     218                 :            :    *
     219                 :            :    * If this function returns a non-null node n', then n' is equivalent to n
     220                 :            :    * and is of the form that can be used by inferSubstitution below.
     221                 :            :    */
     222                 :            :   Node solveEquality(Node n) const;
     223                 :            :   /** infer substitution
     224                 :            :    *
     225                 :            :    * If n is an equality of the form x = t, where t is either:
     226                 :            :    * (1) a constant, or
     227                 :            :    * (2) a variable y such that x < y based on an ordering,
     228                 :            :    * then this method adds {x -> y} to subs and return true, otherwise
     229                 :            :    * it returns false.
     230                 :            :    * If usePred is true, we may additionally add n -> true, or n[0] -> false
     231                 :            :    * is n is a negation.
     232                 :            :    */
     233                 :            :   bool inferSubstitution(Node n, Subs& subs, bool usePred = false) const;
     234                 :            :   /** extended rewrite
     235                 :            :    *
     236                 :            :    * Prints debug information, indicating the rewrite n ---> ret was found.
     237                 :            :    */
     238                 :            :   void debugExtendedRewrite(Node n, Node ret, const char* c) const;
     239                 :            :   //--------------------------------------end generic utilities
     240                 :            : 
     241                 :            :   //--------------------------------------theory-specific top-level calls
     242                 :            :   /**
     243                 :            :    * If these methods return a non-null node ret', then ret is equivalent to
     244                 :            :    * ret'.
     245                 :            :    */
     246                 :            :   Node extendedRewriteStrings(const Node& ret) const;
     247                 :            :   Node extendedRewriteSets(const Node& ret) const;
     248                 :            :   //--------------------------------------end theory-specific top-level calls
     249                 :            : 
     250                 :            :   /**
     251                 :            :    * Whether this extended rewriter applies aggressive rewriting techniques,
     252                 :            :    * which are more expensive. Examples of aggressive rewriting include:
     253                 :            :    * - conditional rewriting,
     254                 :            :    * - condition merging,
     255                 :            :    * - sorting childing of commutative operators with more than 5 children.
     256                 :            :    *
     257                 :            :    * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting
     258                 :            :    * may be applied as a preprocessing step.
     259                 :            :    */
     260                 :            :   bool d_aggr;
     261                 :            :   /** Common constant nodes */
     262                 :            :   Node d_true;
     263                 :            :   Node d_false;
     264                 :            :   Node d_intZero;
     265                 :            : };
     266                 :            : 
     267                 :            : }  // namespace quantifiers
     268                 :            : }  // namespace theory
     269                 :            : }  // namespace cvc5::internal
     270                 :            : 
     271                 :            : #endif /* CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */

Generated by: LCOV version 1.14