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