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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
/* This file is part of the FaCT++ DL reasoner
Copyright (C) 2003-2015 Dmitry Tsarkov and The University of Manchester
Copyright (C) 2015-2016 Dmitry Tsarkov
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 2.1 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
*/
#ifndef PRIORITYMATRIX_H
#define PRIORITYMATRIX_H
#include "eFaCTPlusPlus.h"
#include "dlVertex.h" // DagTag
#include "logging.h"
typedef unsigned short int ToDoListIndex;
/// number of regular options (o- and NN-rules are not included)
const ToDoListIndex nRegularOps = 7;
/// priority index for o- and ID operations (note that these ops have the highest priority)
const ToDoListIndex iId = nRegularOps+1;
/// priority index for <= operation in nominal node
const ToDoListIndex iNN = nRegularOps+2;
/// Auxiliary class to get priorities on operations
class ToDoPriorMatrix
{
protected: // members
// regular operation indexes
ToDoListIndex iAnd,
iOr,
iExists,
iForall,
iLE,
iGE;
public: // interface
/// empty c'tor
ToDoPriorMatrix ( void ) {}
/// empty d'tor
~ToDoPriorMatrix ( void ) {}
/// init priorities via given string OPTIONS
void initPriorities ( const std::string& options, const char* optionName );
/// get an index corresponding given Op, Sign and NominalNode
ToDoListIndex getIndex ( DagTag Op, bool Sign, bool NominalNode ) const;
}; // ToDoPriorMatrix
inline void ToDoPriorMatrix :: initPriorities ( const std::string& options, const char* optionName )
{
// check for correctness
if ( options.size () != 7 )
throw EFaCTPlusPlus ( "ToDo List option string should have length 7" );
// init values by symbols loaded
iAnd = options[1] - '0';
iOr = options[2] - '0';
iExists = options[3] - '0';
iForall = options[4] - '0';
iLE = options[5] - '0';
iGE = options[6] - '0';
// correctness checking
if ( iAnd >= nRegularOps ||
iOr >= nRegularOps ||
iExists >= nRegularOps ||
iForall >= nRegularOps ||
iGE >= nRegularOps ||
iLE >= nRegularOps )
throw EFaCTPlusPlus ( "ToDo List option out of range" );
// inform about used rules order
if ( LLM.isWritable(llAlways) )
LL << "\nInit " << optionName << " = " << iAnd << iOr << iExists << iForall << iLE << iGE;
}
inline ToDoListIndex ToDoPriorMatrix :: getIndex ( DagTag Op, bool Sign, bool NominalNode ) const
{
switch ( Op )
{
case dtAnd:
return (Sign?iAnd:iOr);
case dtForall:
case dtIrr: // process local (ir-)reflexivity as a FORALL
return (Sign?iForall:iExists);
case dtProj: // it should be the lowest priority but now just OR's one
case dtChoose: // probably should be highest branching one
return iOr;
case dtLE:
return (Sign?(NominalNode?iNN:iLE):iGE);
case dtDataType:
case dtDataValue:
case dtDataExpr:
case dtNN:
case dtTop: // no need to process these ops
return nRegularOps;
case dtPSingleton:
case dtPConcept: // no need to process neg of PC
return (Sign?iId:nRegularOps);
case dtNSingleton:
case dtNConcept: // both NC and neg NC are processed
return iId;
default: // safety check
fpp_unreachable();
}
}
#endif
|
