1 /* 2 3 This file is part of the Maude 2 interpreter. 4 5 Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. 6 7 This program is free software; you can redistribute it and/or modify 8 it under the terms of the GNU General Public License as published by 9 the Free Software Foundation; either version 2 of the License, or 10 (at your option) any later version. 11 12 This program is distributed in the hope that it will be useful, 13 but WITHOUT ANY WARRANTY; without even the implied warranty of 14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 15 GNU General Public License for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with this program; if not, write to the Free Software 19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA. 20 21 */ 22 23 // 24 // Abstract base class for terms in the NA theory. 25 // 26 #ifndef _NA_Term_hh_ 27 #define _NA_Term_hh_ 28 #include "term.hh" 29 30 class NA_Term : public Term 31 { 32 public: 33 NA_Term(NA_Symbol* symbol); 34 // 35 // Functions required by theory interface. 36 // 37 // The following functions are left to the derived class to handle: 38 // 39 // int compareArguments(const Term* other) const 40 // int compareArguments(const DagNode* other) const 41 // 42 RawArgumentIterator* arguments(); 43 void deepSelfDestruct(); 44 void findEagerVariables(bool atTop, NatSet& eagerVariables) const; 45 void analyseConstraintPropagation(NatSet& BoundUniquely) const; 46 LhsAutomaton* compileLhs2(bool matchAtTop, 47 const VariableInfo& variableInfo, 48 NatSet& boundUniquely, 49 bool& subproblemLikely); 50 void markEagerArguments(int nrVariables, 51 const NatSet& eagerVariables, 52 Vector<int>& problemVariables); 53 DagNode* dagify2(); 54 55 void findAvailableTerms(TermBag& availableTerms, bool eagerContext, bool atTop); 56 int compileRhs2(RhsBuilder& rhsBuilder, 57 VariableInfo& variableInfo, 58 TermBag& availableTerms, 59 bool eagerContext); 60 61 // 62 // The following pure virtual functions are particular to NA_Term 63 // and must be defined by the derived class. 64 // 65 virtual void overwriteWithDagNode(DagNode* old) const = 0; 66 virtual NA_DagNode* makeDagNode() const = 0; 67 }; 68 69 #endif 70