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 proof rule checker.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "proof/proof_rule_checker.h"
      14                 :            : 
      15                 :            : #include "proof/proof_node.h"
      16                 :            : #include "util/rational.h"
      17                 :            : 
      18                 :            : using namespace cvc5::internal::kind;
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : 
      22                 :   12750282 : Node ProofRuleChecker::check(ProofRule id,
      23                 :            :                              const std::vector<Node>& children,
      24                 :            :                              const std::vector<Node>& args)
      25                 :            : {
      26                 :            :   // call instance-specific checkInternal method
      27                 :   12750282 :   return checkInternal(id, children, args);
      28                 :            : }
      29                 :            : 
      30                 :   43379817 : bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
      31                 :            : {
      32                 :            :   // must be a non-negative integer constant that fits an unsigned int
      33         [ +  - ]:   43264567 :   if (n.getKind() == Kind::CONST_INTEGER && n.getConst<Rational>().sgn() >= 0
      34 [ +  + ][ +  - ]:   86644384 :       && n.getConst<Rational>().getNumerator().fitsUnsignedInt())
         [ +  + ][ +  + ]
                 [ -  - ]
      35                 :            :   {
      36                 :   43264567 :     i = n.getConst<Rational>().getNumerator().toUnsignedInt();
      37                 :   43264567 :     return true;
      38                 :            :   }
      39                 :     115250 :   return false;
      40                 :            : }
      41                 :            : 
      42                 :       9654 : bool ProofRuleChecker::getBool(TNode n, bool& b)
      43                 :            : {
      44 [ +  - ][ +  - ]:       9654 :   if (n.isConst() && n.getType().isBoolean())
         [ +  - ][ +  - ]
                 [ -  - ]
      45                 :            :   {
      46                 :       9654 :     b = n.getConst<bool>();
      47                 :       9654 :     return true;
      48                 :            :   }
      49                 :          0 :   return false;
      50                 :            : }
      51                 :            : 
      52                 :        821 : bool ProofRuleChecker::getKind(TNode n, Kind& k)
      53                 :            : {
      54                 :            :   uint32_t i;
      55         [ -  + ]:        821 :   if (!getUInt32(n, i))
      56                 :            :   {
      57                 :          0 :     return false;
      58                 :            :   }
      59                 :        821 :   k = static_cast<Kind>(i);
      60                 :        821 :   return true;
      61                 :            : }
      62                 :            : 
      63                 :      12088 : Node ProofRuleChecker::mkKindNode(NodeManager* nm, Kind k)
      64                 :            : {
      65         [ -  + ]:      12088 :   if (k == Kind::UNDEFINED_KIND)
      66                 :            :   {
      67                 :            :     // UNDEFINED_KIND is negative, hence return null to avoid cast
      68                 :          0 :     return Node::null();
      69                 :            :   }
      70                 :      24176 :   return nm->mkConstInt(Rational(static_cast<uint32_t>(k)));
      71                 :            : }
      72                 :            : 
      73                 :    7639296 : NodeManager* ProofRuleChecker::nodeManager() const { return d_nm; }
      74                 :            : 
      75                 :            : }  // namespace cvc5::internal