theory_records.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_records.h
00004  * 
00005  * Author: Daniel Wichs
00006  * 
00007  * Created: 7/22/03
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 #ifndef _cvc3__include__theory_records_h_
00021 #define _cvc3__include__theory_records_h_
00022 
00023 #include "theory.h"
00024 
00025 namespace CVC3 {
00026 
00027   class RecordsProofRules;
00028 
00029  typedef enum {
00030    RECORD = 2500,
00031    RECORD_SELECT,
00032    RECORD_UPDATE,
00033    RECORD_TYPE,
00034    TUPLE,
00035    TUPLE_SELECT,
00036    TUPLE_UPDATE,
00037    TUPLE_TYPE
00038  } RecordKinds;
00039                                     
00040 /*****************************************************************************/
00041 /*!
00042  *\class TheoryRecords
00043  *\ingroup Theories
00044  *\brief This theory handles records.
00045  *
00046  * Author: Daniel Wichs
00047  *
00048  * Created: 7/22/03
00049  */
00050 /*****************************************************************************/
00051 class TheoryRecords :public Theory {
00052   RecordsProofRules* d_rules;
00053   //! Auxiliary rewrites: Processing of AND and OR of equations.  Returns e=e'.
00054   Theorem rewriteAux(const Expr& e);
00055   //! Takes Thm(e), returns Thm(e'), where e rewrites to e' by rewriteAux.
00056   Theorem rewriteAux(const Theorem& thm);
00057 
00058 public:
00059   TheoryRecords(TheoryCore* core); //!< Constructor
00060   ~TheoryRecords(); //!< Destructor
00061   //! creates a reference to the proof rules
00062   RecordsProofRules* createProofRules();
00063   
00064   // Theory interface
00065 
00066   //! assert a fact to the theory of records
00067   void assertFact(const Theorem& e);
00068   //! empty implementation to fit theory interface
00069   void checkSat(bool fullEffort) {}
00070   //! rewrites an expression e to one of several allowed forms
00071   Theorem rewrite(const Expr& e);
00072   //! check record or tuple type
00073   void checkType(const Expr& e);
00074   //! computes the type of a record or a tuple
00075   void computeType(const Expr& e);
00076   Type computeBaseType(const Type& t);
00077   
00078   Expr computeTypePred(const Type& t, const Expr& e);
00079   void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00080   void computeModel(const Expr& e, std::vector<Expr>& vars);
00081 
00082   Expr computeTCC(const Expr& e);
00083   virtual Expr parseExprOp(const Expr& e);
00084   void setup(const Expr& e);
00085   void update(const Theorem& e, const Expr& d);
00086   //! pretty printing
00087   ExprStream& print(ExprStream& os, const Expr& e);
00088   //! Test whether expr is a record literal
00089   bool isRecord(const Expr& e) {
00090     return e.isApply() && e.getOpKind() == RECORD;
00091   }
00092   //! Test whether expr is a record type
00093   bool isRecordType(const Expr& e) {
00094     return e.isApply() && e.getOpKind() == RECORD_TYPE;
00095   }
00096   //! Test whether expr is a record type
00097   bool isRecordType(const Type& t) {
00098     return isRecordType(t.getExpr());
00099   }
00100   //! Test whether expr is a record select/update subclass
00101   bool isRecordAccess(const Expr& e)
00102   { return e.isApply() &&
00103       (e.getOpKind() == RECORD_SELECT || e.getOpKind() == RECORD_UPDATE); }
00104   //! Create a record literal
00105   Expr recordExpr(const std::vector<std::string>& fields,
00106       const std::vector<Expr>& kids);
00107   //! Create a record literal
00108   Expr recordExpr(const std::vector<Expr>& fields,
00109       const std::vector<Expr>& kids);
00110   //! Create a record type
00111   Type recordType(const std::vector<std::string>& fields,
00112       const std::vector<Type>& types);
00113   //! Create a record type (field types are given as a vector of Expr)
00114   Type recordType(const std::vector<std::string>& fields,
00115       const std::vector<Expr>& types);
00116   //! Create a record type (fields and types are given as a vector of Expr)
00117   Type recordType(const std::vector<Expr>& fields,
00118       const std::vector<Expr>& types);
00119   //! Create a record field select expression
00120   Expr recordSelect(const Expr& r, const std::string& field);
00121   //! Create a record field update expression
00122   Expr recordUpdate(const Expr& r, const std::string& field, const Expr& val);
00123   //! Get the list of fields from a record literal
00124   const std::vector<Expr>& getFields(const Expr& r);
00125   //! Get the i-th field name from the record literal or type
00126   const std::string& getField(const Expr& e, int i);
00127   //! Get the field index in the record literal or type
00128   /*! The field must be present in the record; otherwise it's an error. */
00129   int getFieldIndex(const Expr& e, const std::string& field);
00130   //! Get the field name from the record select and update expressions
00131   const std::string& getField(const Expr& e);
00132   //! Create a tuple literal
00133   Expr tupleExpr(const std::vector<Expr>& kids);
00134   //! Create a tuple type
00135   Type tupleType(const std::vector<Type>& types);
00136   //! Create a tuple type (types of components are given as Exprs)
00137   Type tupleType(const std::vector<Expr>& types);
00138   //! Create a tuple index selector expression
00139   Expr tupleSelect(const Expr& tup, int i);
00140   //! Create a tuple index update expression
00141   Expr tupleUpdate(const Expr& tup, int i, const Expr& val);
00142   //! Get the index from the tuple select and update expressions
00143   int getIndex(const Expr& e);
00144   //! Test whether expr is a tuple select/update subclass
00145   bool isTupleAccess(const Expr& e)
00146     { return e.isApply() &&
00147         (e.getOpKind() == TUPLE_SELECT || e.getOpKind() == TUPLE_UPDATE); }
00148   //! Test if expr is a tuple literal
00149   bool isTuple(const Expr& e) { return e.isApply() && e.getOpKind() == TUPLE; }
00150   //! Test if expr represents a tuple type
00151   bool isTupleType(const Expr& e)
00152     { return e.isApply() && e.getOpKind() == TUPLE_TYPE; }
00153   //! Test if 'tp' is a tuple type
00154   bool isTupleType(const Type& tp) { return isTupleType(tp.getExpr()); }
00155 };  // end of class TheoryRecords
00156 
00157 }
00158 
00159 #endif

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