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 arrays proof checker.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/arrays/proof_checker.h"
      14                 :            : 
      15                 :            : #include "expr/skolem_manager.h"
      16                 :            : #include "theory/arrays/skolem_cache.h"
      17                 :            : #include "theory/arrays/theory_arrays_rewriter.h"
      18                 :            : #include "theory/rewriter.h"
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : namespace theory {
      22                 :            : namespace arrays {
      23                 :            : 
      24                 :      51241 : ArraysProofRuleChecker::ArraysProofRuleChecker(NodeManager* nm)
      25                 :      51241 :     : ProofRuleChecker(nm)
      26                 :            : {
      27                 :      51241 : }
      28                 :      19955 : void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
      29                 :            : {
      30                 :      19955 :   pc->registerChecker(ProofRule::ARRAYS_READ_OVER_WRITE, this);
      31                 :      19955 :   pc->registerChecker(ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA, this);
      32                 :      19955 :   pc->registerChecker(ProofRule::ARRAYS_READ_OVER_WRITE_1, this);
      33                 :      19955 :   pc->registerChecker(ProofRule::ARRAYS_EXT, this);
      34                 :      19955 : }
      35                 :            : 
      36                 :       2076 : Node ArraysProofRuleChecker::checkInternal(ProofRule id,
      37                 :            :                                            const std::vector<Node>& children,
      38                 :            :                                            const std::vector<Node>& args)
      39                 :            : {
      40                 :       2076 :   NodeManager* nm = nodeManager();
      41         [ +  + ]:       2076 :   if (id == ProofRule::ARRAYS_READ_OVER_WRITE)
      42                 :            :   {
      43 [ -  + ][ -  + ]:        849 :     Assert(children.size() == 1);
                 [ -  - ]
      44 [ -  + ][ -  + ]:        849 :     Assert(args.size() == 1);
                 [ -  - ]
      45                 :        849 :     Node ideq = children[0];
      46 [ +  - ][ -  + ]:        849 :     if (ideq.getKind() != Kind::NOT || ideq[0].getKind() != Kind::EQUAL)
         [ +  - ][ -  + ]
                 [ -  - ]
      47                 :            :     {
      48                 :          0 :       return Node::null();
      49                 :            :     }
      50                 :        849 :     Node lhs = args[0];
      51 [ +  - ][ -  + ]:       1698 :     if (lhs.getKind() != Kind::SELECT || lhs[0].getKind() != Kind::STORE
                 [ -  - ]
      52                 :       1698 :         || lhs[0][1] != ideq[0][0])
      53                 :            :     {
      54                 :          0 :       return Node::null();
      55                 :            :     }
      56                 :       1698 :     Node rhs = nm->mkNode(Kind::SELECT, lhs[0][0], ideq[0][1]);
      57                 :        849 :     return lhs.eqNode(rhs);
      58                 :        849 :   }
      59         [ +  + ]:       1227 :   else if (id == ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA)
      60                 :            :   {
      61 [ -  + ][ -  + ]:          5 :     Assert(children.size() == 1);
                 [ -  - ]
      62 [ -  + ][ -  + ]:          5 :     Assert(args.empty());
                 [ -  - ]
      63                 :          5 :     Node adeq = children[0];
      64 [ +  - ][ -  + ]:          5 :     if (adeq.getKind() != Kind::NOT || adeq[0].getKind() != Kind::EQUAL)
         [ +  - ][ -  + ]
                 [ -  - ]
      65                 :            :     {
      66                 :          0 :       return Node::null();
      67                 :            :     }
      68                 :          5 :     Node lhs = adeq[0][0];
      69                 :          5 :     Node rhs = adeq[0][1];
      70 [ +  - ][ -  + ]:         10 :     if (lhs.getKind() != Kind::SELECT || lhs[0].getKind() != Kind::STORE
                 [ -  - ]
      71                 :         10 :         || rhs.getKind() != Kind::SELECT || lhs[1] != rhs[1])
      72                 :            :     {
      73                 :          0 :       return Node::null();
      74                 :            :     }
      75                 :          5 :     return lhs[1].eqNode(lhs[0][1]);
      76                 :          5 :   }
      77         [ +  + ]:       1222 :   if (id == ProofRule::ARRAYS_READ_OVER_WRITE_1)
      78                 :            :   {
      79 [ -  + ][ -  + ]:        730 :     Assert(children.empty());
                 [ -  - ]
      80 [ -  + ][ -  + ]:        730 :     Assert(args.size() == 1);
                 [ -  - ]
      81                 :        730 :     Node lhs = args[0];
      82 [ +  - ][ -  + ]:       1460 :     if (lhs.getKind() != Kind::SELECT || lhs[0].getKind() != Kind::STORE
                 [ -  - ]
      83                 :       1460 :         || lhs[0][1] != lhs[1])
      84                 :            :     {
      85                 :          0 :       return Node::null();
      86                 :            :     }
      87                 :        730 :     Node rhs = lhs[0][2];
      88                 :        730 :     return lhs.eqNode(rhs);
      89                 :        730 :   }
      90         [ +  - ]:        492 :   if (id == ProofRule::ARRAYS_EXT)
      91                 :            :   {
      92 [ -  + ][ -  + ]:        492 :     Assert(children.size() == 1);
                 [ -  - ]
      93 [ -  + ][ -  + ]:        492 :     Assert(args.empty());
                 [ -  - ]
      94                 :        492 :     Node adeq = children[0];
      95 [ +  - ][ -  + ]:        984 :     if (adeq.getKind() != Kind::NOT || adeq[0].getKind() != Kind::EQUAL
                 [ -  - ]
      96                 :        984 :         || !adeq[0][0].getType().isArray())
      97                 :            :     {
      98                 :          0 :       return Node::null();
      99                 :            :     }
     100                 :        492 :     Node k = SkolemCache::getExtIndexSkolem(nm, adeq);
     101                 :        492 :     Node a = adeq[0][0];
     102                 :        492 :     Node b = adeq[0][1];
     103                 :        984 :     Node as = nm->mkNode(Kind::SELECT, a, k);
     104                 :        984 :     Node bs = nm->mkNode(Kind::SELECT, b, k);
     105                 :        984 :     return as.eqNode(bs).notNode();
     106                 :        492 :   }
     107                 :            :   // no rule
     108                 :          0 :   return Node::null();
     109                 :            : }
     110                 :            : 
     111                 :            : }  // namespace arrays
     112                 :            : }  // namespace theory
     113                 :            : }  // namespace cvc5::internal