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