1 /********************* */ 2 /*! \file array_proof_reconstruction.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Paul Meng, Tim King 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 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.\endverbatim 11 ** 12 ** \brief Array-specific proof construction logic to be used during the 13 ** equality engine's path reconstruction 14 **/ 15 16 #include "cvc4_private.h" 17 18 #ifndef __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H 19 #define __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H 20 21 #include "theory/uf/equality_engine.h" 22 23 namespace CVC4 { 24 namespace theory { 25 namespace arrays { 26 27 /** 28 * A callback class to be invoked whenever the equality engine traverses 29 * an "array-owned" edge during path reconstruction. 30 */ 31 32 class ArrayProofReconstruction : public eq::PathReconstructionNotify { 33 public: 34 ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine); 35 36 void notify(unsigned reasonType, Node reason, Node a, Node b, 37 std::vector<TNode>& equalities, 38 eq::EqProof* proof) const override; 39 40 void setRowMergeTag(unsigned tag); 41 void setRow1MergeTag(unsigned tag); 42 void setExtMergeTag(unsigned tag); 43 44 private: 45 /** Merge tag for ROW applications */ 46 unsigned d_reasonRow; 47 /** Merge tag for ROW1 applications */ 48 unsigned d_reasonRow1; 49 /** Merge tag for EXT applications */ 50 unsigned d_reasonExt; 51 52 const eq::EqualityEngine* d_equalityEngine; 53 }; /* class ArrayProofReconstruction */ 54 55 }/* CVC4::theory::arrays namespace */ 56 }/* CVC4::theory namespace */ 57 }/* CVC4 namespace */ 58 59 #endif /* __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */ 60