records_proof_rules.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file records_proof_rules.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_proof_rules_h_
00021 #define _cvc3__records_proof_rules_h_
00022 
00023 namespace CVC3 {
00024 
00025   class Expr;
00026   class Theorem;
00027 
00028   class RecordsProofRules {
00029   public:
00030     //!< Destructor
00031     virtual ~RecordsProofRules() { }
00032     
00033     //! ==> (REC_LITERAL (f1 v1) ... (fi vi) ...).fi = vi
00034     virtual Theorem rewriteLitSelect(const Expr &e)  = 0;
00035     
00036     //! ==> (REC_SELECT (REC_UPDATE e fi vi) fi) = vi
00037     virtual Theorem rewriteUpdateSelect(const Expr& e) = 0;
00038     
00039     
00040     //! ==> (REC_UPDATE (REC_LITERAL (f1 v1) ... (fi vi) ...) fi v') =(REC_LITERAL (f1 v1) ... (fi v') ...)
00041     virtual Theorem rewriteLitUpdate(const Expr& e) = 0;
00042     //! From T|- e = e' return T|- AND (e.i = e'.i) for all i
00043     virtual Theorem expandEq(const Theorem& eqThrm) = 0;
00044     //! From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i
00045     virtual Theorem expandNeq(const Theorem& neqThrm) = 0;
00046     //! Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #)
00047     virtual Theorem expandRecord(const Expr& e) = 0;
00048     //! Expand a tuple into a literal: |- e = (e.0, ..., e.n-1)
00049     virtual Theorem expandTuple(const Expr& e) = 0;
00050   };
00051 }
00052 #endif

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2