1 /*----------------------------------------------------------------------- 2 3 File : che_axiomscan.h 4 5 Author: Stephan Schulz 6 7 Contents 8 9 Declarations for functions recognizing certain axioms (e.g. AC 10 axioms). 11 12 Copyright 1998, 1999 by the author. 13 This code is released under the GNU General Public Licence and 14 the GNU Lesser General Public License. 15 See the file COPYING in the main E directory for details.. 16 Run "eprover -h" for contact information. 17 18 Changes 19 20 <1> New 21 22 -----------------------------------------------------------------------*/ 23 24 #ifndef CHE_AXIOMSCAN_H 25 26 #define CHE_AXIOMSCAN_H 27 28 #include <ccl_clausesets.h> 29 #include <cle_indexfunctions.h> 30 31 32 33 /*---------------------------------------------------------------------*/ 34 /* Data type declarations */ 35 /*---------------------------------------------------------------------*/ 36 37 38 39 40 /*---------------------------------------------------------------------*/ 41 /* Exported Functions and Variables */ 42 /*---------------------------------------------------------------------*/ 43 44 45 FunCode DetectCommutativity(Clause_p clause); 46 FunCode DetectAssociativity(Clause_p clause); 47 bool ClauseScanAC(Sig_p sig, Clause_p clause); 48 bool ClauseSetScanAC(Sig_p sig, ClauseSet_p set); 49 50 51 #endif 52 53 /*---------------------------------------------------------------------*/ 54 /* End of File */ 55 /*---------------------------------------------------------------------*/ 56 57 58 59 60 61 62