src/theory/arrays/skolem_cache.h

   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  * Arrays skolem cache.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H
  19 #define CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H
  20
  21 #include "expr/node.h"
  22
  23 namespace cvc5 {
  24 namespace theory {
  25 namespace arrays {
  26
  27 /**
  28  * The arrays skolem cache, which provides static methods for constructing
  29  * skolems with witness forms.
  30  */
  31 class SkolemCache
  32 {
  33  public:
  34   SkolemCache();
  35   ~SkolemCache() {}
  36
  37   /**
  38    * Get the skolem correspoding to the index that witnesses the disequality
  39    * deq between arrays a and b. The witness form of this skolem is:
  40    * (witness ((x T)) (=> (not (= a b)) (not (= (select a x) (select b x)))))
  41    * This skolem is unique for deq, calling this method will always return the
  42    * same skolem over the lifetime of deq.
  43    */
  44   static Node getExtIndexSkolem(Node deq);
  45
  46  private:
  47   /**
  48    * Get the bound variable x of the witness term above for disequality deq
  49    * between arrays.
  50    */
  51   static Node getExtIndexVar(Node deq);
  52 };
  53
  54 }  // namespace arrays
  55 }  // namespace theory
  56 }  // namespace cvc5
  57
  58 #endif