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