records_theorem_producer.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file records_theorem_producer.h
00004  * 
00005  * Author: Daniel Wichs
00006  * 
00007  * Created: Jul 22 22:59:07 GMT 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 #ifndef _cvc3__records_theorem_producer_h_
00021 #define _cvc3__records_theorem_producer_h_
00022 
00023 #include "records_proof_rules.h"
00024 #include "theorem_producer.h"
00025 #include "theory_records.h"
00026 
00027 namespace CVC3 {
00028   
00029   class RecordsTheoremProducer: public RecordsProofRules,
00030     public TheoremProducer {
00031       TheoryRecords* d_theoryRecords;
00032 
00033     public:
00034     // Constructor
00035       RecordsTheoremProducer(TheoremManager* tm, TheoryRecords* t):
00036   TheoremProducer(tm), d_theoryRecords(t) { }
00037       Theorem rewriteLitSelect(const Expr &e);
00038       Theorem rewriteUpdateSelect(const Expr& e);
00039       Theorem rewriteLitUpdate(const Expr& e);
00040       Theorem expandEq(const Theorem& eqThrm);
00041       Theorem expandNeq(const Theorem& neqThrm);
00042       Theorem expandRecord(const Expr& e);
00043       Theorem expandTuple(const Expr& e);
00044 
00045       // Expr creation functions
00046       //! Test whether expr is a record type
00047       bool isRecordType(const Expr& e)
00048   { return d_theoryRecords->isRecordType(e); }
00049       //! Test whether Type is a record type
00050       bool isRecordType(const Type& t)
00051   { return d_theoryRecords->isRecordType(t); }
00052       //! Test whether expr is a record select/update subclass
00053       bool isRecordAccess(const Expr& e)
00054   { return d_theoryRecords->isRecordAccess(e); }
00055       //! Create a record literal
00056       Expr recordExpr(const std::vector<std::string>& fields,
00057           const std::vector<Expr>& kids)
00058   { return d_theoryRecords->recordExpr(fields, kids); }
00059       //! Create a record literal
00060       Expr recordExpr(const std::vector<Expr>& fields,
00061           const std::vector<Expr>& kids)
00062   { return d_theoryRecords->recordExpr(fields, kids); }
00063       //! Create a record type
00064       Type recordType(const std::vector<std::string>& fields,
00065           const std::vector<Type>& types)
00066   { return d_theoryRecords->recordType(fields, types); }
00067       //! Create a record type (field types are given as a vector of Expr)
00068       Type recordType(const std::vector<std::string>& fields,
00069           const std::vector<Expr>& types)
00070   { return d_theoryRecords->recordType(fields, types); }
00071       //! Create a record field select expression
00072       Expr recordSelect(const Expr& r, const std::string& field)
00073   { return d_theoryRecords->recordSelect(r, field); }
00074       //! Create a record field update expression
00075       Expr recordUpdate(const Expr& r, const std::string& field,
00076       const Expr& val)
00077   { return d_theoryRecords->recordUpdate(r, field, val); }
00078       //! Get the list of fields from a record literal
00079       const std::vector<Expr>& getFields(const Expr& r)
00080   { return d_theoryRecords->getFields(r); }
00081       //! Get the i-th field name from the record literal or type
00082       const std::string& getField(const Expr& e, int i)
00083   { return d_theoryRecords->getField(e, i); }
00084       //! Get the field index in the record literal or type
00085       /*! The field must be present in the record; otherwise it's an error. */
00086       int getFieldIndex(const Expr& e, const std::string& field)
00087   { return d_theoryRecords->getFieldIndex(e, field); }
00088       //! Get the field name from the record select and update expressions
00089       const std::string& getField(const Expr& e)
00090   { return d_theoryRecords->getField(e); }
00091       //! Create a tuple literal
00092       Expr tupleExpr(const std::vector<Expr>& kids)
00093   { return d_theoryRecords->tupleExpr(kids); }
00094       //! Create a tuple type
00095       Type tupleType(const std::vector<Type>& types)
00096   { return d_theoryRecords->tupleType(types); }
00097       //! Create a tuple type (types of components are given as Exprs)
00098       Type tupleType(const std::vector<Expr>& types)
00099   { return d_theoryRecords->tupleType(types); }
00100       //! Create a tuple index selector expression
00101       Expr tupleSelect(const Expr& tup, int i)
00102   { return d_theoryRecords->tupleSelect(tup, i); }
00103       //! Create a tuple index update expression
00104       Expr tupleUpdate(const Expr& tup, int i, const Expr& val)
00105   { return d_theoryRecords->tupleUpdate(tup, i, val); }
00106       //! Get the index from the tuple select and update expressions
00107       int getIndex(const Expr& e)
00108   { return d_theoryRecords->getIndex(e); }
00109       //! Test whether expr is a tuple select/update subclass
00110       bool isTupleAccess(const Expr& e)
00111   { return d_theoryRecords->isTupleAccess(e); }
00112     };
00113 
00114 } 
00115 
00116 #endif

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