diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
| -rw-r--r-- | src/theory/arrays/theory_arrays.h | 30 |
1 files changed, 22 insertions, 8 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index eba6c000e..c1223474c 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_arrays.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic, Clark Barrett - ** Minor contributors (to current version): Tim King, Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Clark Barrett, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** 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 Theory of arrays ** @@ -23,6 +23,7 @@ #include "context/cdhashset.h" #include "context/cdqueue.h" #include "theory/arrays/array_info.h" +#include "theory/arrays/array_proof_reconstruction.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "util/statistics_registry.h" @@ -124,11 +125,20 @@ class TheoryArrays : public Theory { /** conflicts in setModelVal */ IntStat d_numSetModelValConflicts; + // Merge reason types + + /** Merge tag for ROW applications */ + unsigned d_reasonRow; + /** Merge tag for ROW1 applications */ + unsigned d_reasonRow1; + /** Merge tag for EXT applications */ + unsigned d_reasonExt; + public: TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - std::string instanceName = ""); + std::string name = ""); ~TheoryArrays(); void setMasterEqualityEngine(eq::EqualityEngine* eq); @@ -183,7 +193,7 @@ class TheoryArrays : public Theory { bool propagate(TNode literal); /** Explain why this literal is true by adding assumptions */ - void explain(TNode literal, std::vector<TNode>& assumptions); + void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof); /** For debugging only- checks invariants about when things are preregistered*/ context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered; @@ -195,6 +205,7 @@ class TheoryArrays : public Theory { void preRegisterTerm(TNode n); void propagate(Effort e); + Node explain(TNode n, eq::EqProof *proof); Node explain(TNode n); ///////////////////////////////////////////////////////////////////////////// @@ -429,6 +440,9 @@ class TheoryArrays : public Theory { bool d_inCheckModel; int d_topLevel; + /** An equality-engine callback for proof reconstruction */ + ArrayProofReconstruction d_proofReconstruction; + public: eq::EqualityEngine* getEqualityEngine() { |