CVC3

theory_simulate.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file theory_simulate.h
00004  *\brief Implementation of a symbolic simulator
00005  *
00006  * Author: Sergey Berezin
00007  *
00008  * Created: Tue Oct  7 10:13:15 2003
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__include__theory_simulate_h_
00023 #define _cvc3__include__theory_simulate_h_
00024 
00025 #include "theory.h"
00026 
00027 namespace CVC3 {
00028 
00029 class SimulateProofRules;
00030 
00031 /*****************************************************************************/
00032 /*!
00033  * \class TheorySimulate
00034  * \ingroup Theories
00035  * \brief "Theory" of symbolic simulation.
00036  *
00037  * Author: Sergey Berezin
00038  *
00039  * Created: Tue Oct  7 10:13:15 2003
00040  *
00041  * This theory owns the SIMULATE operator.  It's job is to replace the above
00042  * expressions by their definitions using rewrite rules.
00043  */
00044 /*****************************************************************************/
00045 
00046 class TheorySimulate: public Theory {
00047 private:
00048   //! Our local proof rules
00049   SimulateProofRules* d_rules;
00050   //! Create proof rules for this theory
00051   SimulateProofRules* createProofRules();
00052 public:
00053   //! Constructor
00054   TheorySimulate(TheoryCore* core);
00055   //! Destructor
00056   ~TheorySimulate();
00057   // The required Theory API functions
00058   void assertFact(const Theorem& e) { }
00059   void checkSat(bool fullEffort) { }
00060   Theorem rewrite(const Expr& e);
00061   void computeType(const Expr& e);
00062   Expr computeTCC(const Expr& e);
00063   Expr parseExprOp(const Expr& e);
00064   ExprStream& print(ExprStream& os, const Expr& e);
00065 }; // end of class TheorySimulate
00066 
00067 } // end of namespace CVC3
00068 
00069 #endif