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
const bool & d_liftReadIte
Flag to lift ite's over reads.
Definition: theory_array.h:60
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Expr getBaseArray(const Expr &e) const
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
CDO< unsigned > d_index
Used in checkSat.
Definition: theory_array.h:67
Expr arrayLiteral(const Expr &ind, const Expr &body)
CDO< size_t > d_sharedIdx1
Definition: theory_array.h:69
void computeType(const Expr &e)
Compute and store the type of e.
ExprMap< Theorem > d_renameThms
Set of renaming theorems indexed by t.
Definition: theory_array.h:56
bool isWrite(const Expr &e)
Definition: theory_array.h:111
Type arrayType(const Type &type1, const Type &type2)
Definition: theory_array.h:116
MS C++ specific settings.
Definition: type.h:42
Base class for theories.
Definition: theory.h:64
TheoryArray(TheoryCore *core)
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
CDO< size_t > d_sharedIdx2
Definition: theory_array.h:69
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
bool isArrayLiteral(const Expr &e)
Definition: theory_array.h:112
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
ArrayKinds
Definition: theory_array.h:30
ArrayProofRules * createProofRules()
const Expr & getExpr() const
Definition: type.h:52
bool isClosure() const
Definition: expr.h:1007
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Theorem solve(const Theorem &e)
An optional solver.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
bool isArray(const Type &t)
Definition: theory_array.h:109
CDMap< Expr, Expr > d_sharedSubterms
Backtracking database of subterms of shared terms.
Definition: theory_array.h:63
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
CDList< Expr > d_sharedSubtermsList
Backtracking database of subterms of shared terms.
Definition: theory_array.h:65
Theorem pullIndex(const Expr &e, const Expr &index)
Derived rule.
This theory handles arrays.
Definition: theory_array.h:50
CDList< Expr > d_reads
Backtracking list of array reads, for building concrete models.
Definition: theory_array.h:54
ArrayProofRules * d_rules
Definition: theory_array.h:51
bool isRead(const Expr &e)
Definition: theory_array.h:110
void checkType(const Expr &e)
Check that e is a valid Type expr.
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
Definition: expr.cpp:35
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
int d_inCheckSat
Flag for use in checkSat.
Definition: theory_array.h:72
const bool & d_applicationsInModel
Flag to include array reads to the concrete model.
Definition: theory_array.h:58