CVC3  2.4.1
theory_array.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_array.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Wed Feb 26 18:32:06 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__theory_array_h_
22 #define _cvc3__include__theory_array_h_
23 
24 #include "theory_core.h"
25 
26 namespace CVC3 {
27 
28 class ArrayProofRules;
29 
30  typedef enum {
31  ARRAY = 2000,
34  // Array literal [ [type] e ]; creates a constant array holding 'e'
35  // in all elements: (CONST_ARRAY type e)
37  } ArrayKinds;
38 
39 /*****************************************************************************/
40 /*!
41  *\class TheoryArray
42  *\ingroup Theories
43  *\brief This theory handles arrays.
44  *
45  * Author: Clark Barrett
46  *
47  * Created: Thu Feb 27 00:38:20 2003
48  */
49 /*****************************************************************************/
50 class TheoryArray :public Theory {
52 
53  //! Backtracking list of array reads, for building concrete models.
55  //! Set of renaming theorems \f$\exists x. t = x\f$ indexed by t
57  //! Flag to include array reads to the concrete model
58  const bool& d_applicationsInModel;
59  //! Flag to lift ite's over reads
60  const bool& d_liftReadIte;
61 
62  //! Backtracking database of subterms of shared terms
64  //! Backtracking database of subterms of shared terms
66  //! Used in checkSat
68 
70 
71  //! Flag for use in checkSat
73 
74  //! Derived rule
75  // w(...,i,v1,...,) => w(......,i,v1')
76  // Returns Null Theorem if index does not appear
77  Theorem pullIndex(const Expr& e, const Expr& index);
78 
79 public:
80  TheoryArray(TheoryCore* core);
81  ~TheoryArray();
82 
83  // Trusted method that creates the proof rules class (used in constructor).
84  // Implemented in array_theorem_producer.cpp
86 
87  // Theory interface
88  void addSharedTerm(const Expr& e);
89  void assertFact(const Theorem& e);
90  void checkSat(bool fullEffort);
91  Theorem rewrite(const Expr& e);
92  void setup(const Expr& e);
93  void update(const Theorem& e, const Expr& d);
94  Theorem solve(const Theorem& e);
95  void checkType(const Expr& e);
97  bool enumerate, bool computeSize);
98  void computeType(const Expr& e);
99  Type computeBaseType(const Type& t);
100  void computeModelTerm(const Expr& e, std::vector<Expr>& v);
101  void computeModel(const Expr& e, std::vector<Expr>& vars);
102  Expr computeTCC(const Expr& e);
103  virtual Expr parseExprOp(const Expr& e);
104  ExprStream& print(ExprStream& os, const Expr& e);
105  Expr getBaseArray(const Expr& e) const;
106 };
107 
108 // Array testers
109 inline bool isArray(const Type& t) { return t.getExpr().getKind() == ARRAY; }
110 inline bool isRead(const Expr& e) { return e.getKind() == READ; }
111 inline bool isWrite(const Expr& e) { return e.getKind() == WRITE; }
112 inline bool isArrayLiteral(const Expr& e)
113  { return (e.isClosure() && e.getKind() == ARRAY_LITERAL); }
114 
115 // Array constructors
116 inline Type arrayType(const Type& type1, const Type& type2)
117  { return Type(Expr(ARRAY, type1.getExpr(), type2.getExpr())); }
118 
119 // Expr read(const Expr& arr, const Expr& index);
120 // Expr write(const Expr& arr, const Expr& index, const Expr& value);
121 Expr arrayLiteral(const Expr& ind, const Expr& body);
122 } // end of namespace CVC3
123 
124 #endif