00001 /*****************************************************************************/ 00002 /*! 00003 * \file theory_uf.h 00004 * 00005 * Author: Clark Barrett 00006 * 00007 * Created: Fri Jan 17 18:25:40 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 00021 #ifndef _cvc3__include__theory_uf_h_ 00022 #define _cvc3__include__theory_uf_h_ 00023 00024 #include "theory.h" 00025 00026 namespace CVC3 { 00027 00028 class UFProofRules; 00029 00030 //! Local kinds for transitive closure of binary relations 00031 typedef enum { 00032 TRANS_CLOSURE = 500, 00033 OLD_ARROW, // for backward compatibility with old function declarations 00034 } UFKinds; 00035 00036 /*****************************************************************************/ 00037 /*! 00038 *\class TheoryUF 00039 *\ingroup Theories 00040 *\brief This theory handles uninterpreted functions. 00041 * 00042 * Author: Clark Barrett 00043 * 00044 * Created: Sat Feb 8 14:51:19 2003 00045 */ 00046 /*****************************************************************************/ 00047 class TheoryUF :public Theory { 00048 UFProofRules* d_rules; 00049 //! Flag to include function applications to the concrete model 00050 const bool& d_applicationsInModel; 00051 00052 // For computing transitive closure of binary relations 00053 typedef struct TCMapPair { 00054 ExprMap<CDList<Theorem>*> appearsFirstMap; 00055 ExprMap<CDList<Theorem>*> appearsSecondMap; 00056 } TCMapPair; 00057 00058 ExprMap<TCMapPair*> d_transClosureMap; 00059 00060 //! Backtracking list of function applications 00061 /*! Used for building concrete models and beta-reducing 00062 * lambda-expressions. */ 00063 CDList<Expr> d_funApplications; 00064 //! Pointer to the last unprocessed element (for lambda expansions) 00065 CDO<size_t> d_funApplicationsIdx; 00066 00067 public: 00068 TheoryUF(TheoryCore* core); 00069 ~TheoryUF(); 00070 00071 // Trusted method that creates the proof rules class (used in constructor). 00072 // Implemented in uf_theorem_producer.cpp 00073 UFProofRules* createProofRules(); 00074 00075 // Theory interface 00076 void addSharedTerm(const Expr& e) {} 00077 void assertFact(const Theorem& e); 00078 void checkSat(bool fullEffort); 00079 Theorem rewrite(const Expr& e); 00080 void setup(const Expr& e); 00081 void update(const Theorem& e, const Expr& d); 00082 void checkType(const Expr& e); 00083 void computeType(const Expr& e); 00084 Type computeBaseType(const Type& t); 00085 void computeModelTerm(const Expr& e, std::vector<Expr>& v); 00086 void computeModel(const Expr& e, std::vector<Expr>& vars); 00087 Expr computeTCC(const Expr& e); 00088 virtual Expr parseExprOp(const Expr& e); 00089 ExprStream& print(ExprStream& os, const Expr& e); 00090 00091 //! Create a new LAMBDA-abstraction 00092 Expr lambdaExpr(const std::vector<Expr>& vars, const Expr& body); 00093 //! Create a transitive closure expression 00094 Expr transClosureExpr(const std::string& name, 00095 const Expr& e1, const Expr& e2); 00096 }; 00097 00098 } 00099 00100 #endif