theory_uf.h

Go to the documentation of this file.
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

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