theory_array.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_array.h
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Wed Feb 26 18:32:06 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 #ifndef _cvc3__include__theory_array_h_
00022 #define _cvc3__include__theory_array_h_
00023 
00024 #include "theory.h"
00025 
00026 namespace CVC3 {
00027 
00028 class ArrayProofRules;
00029 
00030  typedef enum {
00031    ARRAY = 2000,
00032    READ,
00033    WRITE,
00034    // Array literal [ [type] e ]; creates a constant array holding 'e'
00035    // in all elements: (CONST_ARRAY type e)
00036    ARRAY_LITERAL
00037  } ArrayKinds;
00038 
00039 /*****************************************************************************/
00040 /*!
00041  *\class TheoryArray
00042  *\ingroup Theories
00043  *\brief This theory handles arrays.
00044  *
00045  * Author: Clark Barrett
00046  *
00047  * Created: Thu Feb 27 00:38:20 2003
00048  */
00049 /*****************************************************************************/
00050 class TheoryArray :public Theory {
00051   ArrayProofRules* d_rules;
00052 
00053   //! Backtracking list of array reads, for building concrete models.
00054   CDList<Expr> d_reads;
00055   //! Set of renaming theorems \f$\exists x. t = x\f$ indexed by t
00056   ExprMap<Theorem> d_renameThms;
00057   //! Flag to include array reads to the concrete model
00058   const bool& d_applicationsInModel;
00059   //! Flag to lift ite's over reads
00060   const bool& d_liftReadIte;
00061 
00062   // Private methods
00063   Theorem renameExpr(const Expr& e);
00064 
00065 public:
00066   TheoryArray(TheoryCore* core);
00067   ~TheoryArray();
00068 
00069   // Trusted method that creates the proof rules class (used in constructor).
00070   // Implemented in array_theorem_producer.cpp
00071   ArrayProofRules* createProofRules();
00072 
00073   // Theory interface
00074   void addSharedTerm(const Expr& e) {}
00075   void assertFact(const Theorem& e) {}
00076   void checkSat(bool fullEffort) {}
00077   Theorem rewrite(const Expr& e);
00078   void setup(const Expr& e);
00079   void update(const Theorem& e, const Expr& d);
00080   Theorem solve(const Theorem& e);
00081   void checkType(const Expr& e);
00082   void computeType(const Expr& e);
00083   Type computeBaseType(const Type& t);
00084   void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00085   void computeModel(const Expr& e, std::vector<Expr>& vars);
00086   Expr computeTCC(const Expr& e);
00087   virtual Expr parseExprOp(const Expr& e);
00088   ExprStream& print(ExprStream& os, const Expr& e);
00089 };
00090 
00091 // Array testers
00092 inline bool isArray(const Type& t) { return t.getExpr().getKind() == ARRAY; }
00093 inline bool isRead(const Expr& e) { return e.getKind() == READ; }
00094 inline bool isWrite(const Expr& e) { return e.getKind() == WRITE; }
00095 inline bool isArrayLiteral(const Expr& e)
00096   { return (e.isClosure() && e.getKind() == ARRAY_LITERAL); }
00097 
00098 // Array constructors
00099 inline Type arrayType(const Type& type1, const Type& type2)
00100   { return Type(Expr(ARRAY, type1.getExpr(), type2.getExpr())); }
00101 
00102 // Expr read(const Expr& arr, const Expr& index);
00103 // Expr write(const Expr& arr, const Expr& index, const Expr& value);
00104 Expr arrayLiteral(const Expr& ind, const Expr& body);
00105 } // end of namespace CVC3
00106 
00107 #endif

Generated on Tue Jul 3 14:33:40 2007 for CVC3 by  doxygen 1.5.1