diff options
Diffstat (limited to 'src/theory/arrays/array_proof_reconstruction.h')
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.h | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h new file mode 100644 index 000000000..ef3e09aed --- /dev/null +++ b/src/theory/arrays/array_proof_reconstruction.h @@ -0,0 +1,58 @@ +/********************* */ +/*! \file array_proof_reconstruction.h + ** \verbatim + ** Top contributors (to current version): + ** Guy Katz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Array-specific proof construction logic to be used during the + ** equality engine's path reconstruction + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H +#define __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H + +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +/** + * A callback class to be invoked whenever the equality engine traverses + * an "array-owned" edge during path reconstruction. + */ + +class ArrayProofReconstruction : public eq::PathReconstructionNotify { +public: + ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine); + + void notify(unsigned reasonType, Node reason, Node a, Node b, + std::vector<TNode>& equalities, eq::EqProof* proof) const; + + void setRowMergeTag(unsigned tag); + void setRow1MergeTag(unsigned tag); + void setExtMergeTag(unsigned tag); + +private: + /** Merge tag for ROW applications */ + unsigned d_reasonRow; + /** Merge tag for ROW1 applications */ + unsigned d_reasonRow1; + /** Merge tag for EXT applications */ + unsigned d_reasonExt; + + const eq::EqualityEngine* d_equalityEngine; +}; /* class ArrayProofReconstruction */ + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */ |