src/theory/arrays/proof_checker.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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 arrays proof checker.
  14  */
  15
  16 #include "theory/arrays/proof_checker.h"
  17 #include "expr/skolem_manager.h"
  18 #include "theory/arrays/skolem_cache.h"
  19 #include "theory/rewriter.h"
  20
  21 namespace cvc5 {
  22 namespace theory {
  23 namespace arrays {
  24
  25 void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
  26 {
  27   pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE, this);
  28   pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_CONTRA, this);
  29   pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this);
  30   pc->registerChecker(PfRule::ARRAYS_EXT, this);
  31   // trusted rules
  32   pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2);
  33 }
  34
  35 Node ArraysProofRuleChecker::checkInternal(PfRule id,
  36                                            const std::vector<Node>& children,
  37                                            const std::vector<Node>& args)
  38 {
  39   NodeManager* nm = NodeManager::currentNM();
  40   if (id == PfRule::ARRAYS_READ_OVER_WRITE)
  41   {
  42     Assert(children.size() == 1);
  43     Assert(args.size() == 1);
  44     Node ideq = children[0];
  45     if (ideq.getKind() != kind::NOT || ideq[0].getKind() != kind::EQUAL)
  46     {
  47       return Node::null();
  48     }
  49     Node lhs = args[0];
  50     if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
  51         || lhs[0][1] != ideq[0][0])
  52     {
  53       return Node::null();
  54     }
  55     Node rhs = nm->mkNode(kind::SELECT, lhs[0][0], ideq[0][1]);
  56     return lhs.eqNode(rhs);
  57   }
  58   else if (id == PfRule::ARRAYS_READ_OVER_WRITE_CONTRA)
  59   {
  60     Assert(children.size() == 1);
  61     Assert(args.empty());
  62     Node adeq = children[0];
  63     if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL)
  64     {
  65       return Node::null();
  66     }
  67     Node lhs = adeq[0][0];
  68     Node rhs = adeq[0][1];
  69     if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
  70         || rhs.getKind() != kind::SELECT || lhs[1] != rhs[1])
  71     {
  72       return Node::null();
  73     }
  74     return lhs[1].eqNode(lhs[0][1]);
  75   }
  76   if (id == PfRule::ARRAYS_READ_OVER_WRITE_1)
  77   {
  78     Assert(children.empty());
  79     Assert(args.size() == 1);
  80     Node lhs = args[0];
  81     if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
  82         || lhs[0][1] != lhs[1])
  83     {
  84       return Node::null();
  85     }
  86     Node rhs = lhs[0][2];
  87     return lhs.eqNode(rhs);
  88   }
  89   if (id == PfRule::ARRAYS_EXT)
  90   {
  91     Assert(children.size() == 1);
  92     Assert(args.empty());
  93     Node adeq = children[0];
  94     if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL
  95         || !adeq[0][0].getType().isArray())
  96     {
  97       return Node::null();
  98     }
  99     Node k = SkolemCache::getExtIndexSkolem(adeq);
 100     Node a = adeq[0][0];
 101     Node b = adeq[0][1];
 102     Node as = nm->mkNode(kind::SELECT, a, k);
 103     Node bs = nm->mkNode(kind::SELECT, b, k);
 104     return as.eqNode(bs).notNode();
 105   }
 106   if (id == PfRule::ARRAYS_TRUST)
 107   {
 108     // "trusted" rules
 109     Assert(!args.empty());
 110     Assert(args[0].getType().isBoolean());
 111     return args[0];
 112   }
 113   // no rule
 114   return Node::null();
 115 }
 116
 117 }  // namespace arrays
 118 }  // namespace theory
 119 }  // namespace cvc5