expr_transform.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file expr_transform.h
00004  *\brief Generally Useful Expression Transformations
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Fri Aug  5 16:11:51 2005
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__expr_transform_h_
00023 #define _cvc3__include__expr_transform_h_
00024 
00025 #include "expr.h"
00026 
00027 namespace CVC3 {
00028 
00029   class VCL;
00030   class TheoryCore;
00031   class CommonProofRules;
00032   class CoreProofRules;
00033 
00034 class ExprTransform {
00035 
00036   TheoryCore* d_core;
00037   CommonProofRules* d_commonRules;
00038   CoreProofRules* d_rules;
00039 
00040   //! Cache for pushNegation()
00041   ExprMap<Theorem> d_pushNegCache;
00042 
00043 public:
00044   ExprTransform(TheoryCore* core);
00045   ~ExprTransform() {}
00046 
00047   //! Simplification that avoids stack overflow
00048   /*! Stack overflow is avoided by traversing the expression to depths that are
00049     multiples of 5000 until the bottom is reached.  Then, simplification is done
00050     bottom-up.
00051    */
00052   Theorem smartSimplify(const Expr& e, ExprMap<bool>& cache);
00053   Theorem preprocess(const Expr& e);
00054   Theorem preprocess(const Theorem& thm);
00055   //! Push all negations down to the leaves
00056   Theorem pushNegation(const Expr& e);
00057   //! Auxiliary recursive function for pushNegation().
00058   Theorem pushNegationRec(const Expr& e, bool neg);
00059   //! Its version for transitivity
00060   Theorem pushNegationRec(const Theorem& e, bool neg);
00061   //! Push negation one level down.  Takes 'e' which is 'NOT e[0]'
00062   Theorem pushNegation1(const Expr& e);
00063   /*@}*/ // end of preprocessor stuff
00064 
00065 };
00066 
00067 }
00068 
00069 #endif

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