FazBrowse GitHub Viewer
|
Trending
|
URL:
|
Home
Tools:
[Download Repo ZIP]
[View Raw Code]
[Original HTTPS Page]
JavaRes/src/atp/Signature.java at master · eprover/JavaRes · GitHub
Uh oh!
There was an error while loading.
Please reload this page
.
eprover
/
JavaRes
Public
Notifications
You must be signed in to change notification settings
Fork
1
Star
1
Code
Issues
0
Pull requests
0
Actions
Projects
Security and quality
0
Insights
Additional navigation options
Code
Issues
Pull requests
Actions
Projects
Security and quality
Insights
Expand file tree
Breadcrumbs
JavaRes
/
src
/
atp
/
Signature.java
Copy path
More file actions
More file actions
Latest commit
History
History
History
135 lines (111 loc) · 4.04 KB
Breadcrumbs
JavaRes
/
src
/
atp
/
Signature.java
Copy path
File metadata and controls
135 lines (111 loc) · 4.04 KB
Raw
Copy raw file
Download raw file
Open symbols panel
Edit and raw actions
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
127
128
129
130
131
132
133
134
135
package
atp
;
import
java
.
io
.*;
import
java
.
util
.*;
public
class
Signature
{
/*
First-order signatures describe which names (for functions, including
constants, and predicates) are available in a given first-order
language. Very often, signatures are given implicitly. In other words,
the symbols used in terms and formulas implictly make up the
formula. For implementations of standard untyped predicate logic, we
can always extract the necessary information directly from the
formulae.
However, for certain operations it is much easier to have an explicit
data object providing signature information.
A signature is a triple (F,P,ar), with the following properties:
- F is a finite set of function symbols (including constants).
- P is a finite set of predicate symbols.
- F and P are disjunct, i.e. they don't share any symbols.
- ar:F \cup P ->N_0 is the arity function that associates a natural
number (the "arity") with each function symbol and predicate
symbols.
*/
public
ArrayList
<
String
>
funs
=
new
ArrayList
<
String
>();
public
ArrayList
<
String
>
preds
=
new
ArrayList
<
String
>();
public
HashMap
<
String
,
Integer
>
arity
=
new
HashMap
<
String
,
Integer
>();
/** ***************************************************************
* Return a printable representation of the signature.
*/
public
String
toString
() {
StringBuffer
res
=
new
StringBuffer
();
res
.
append
(
"Predicates:
\n
"
);
res
.
append
(
preds
.
toString
() +
"
\n
"
);
res
.
append
(
"Functions:
\n
"
);
res
.
append
(
funs
.
toString
() +
"
\n
"
);
return
res
.
toString
();
}
/** ***************************************************************
* Add a new function
*/
public
void
addFun
(
String
f
,
int
a
) {
if
(!
funs
.
contains
(
f
)) {
funs
.
add
(
f
);
arity
.
put
(
f
,
new
Integer
(
a
));
}
}
/** ***************************************************************
* Add a new predicate
*/
public
void
addPred
(
String
p
,
int
a
) {
if
(!
preds
.
contains
(
p
)) {
preds
.
add
(
p
);
arity
.
put
(
p
,
new
Integer
(
a
));
}
}
/** ***************************************************************
* Return True if p is a known predicate symbol.
*/
public
boolean
isPred
(
String
p
) {
return
preds
.
contains
(
p
);
}
/** ***************************************************************
* Return True if f is a known function symbol.
*/
public
boolean
isFun
(
String
f
) {
return
funs
.
contains
(
f
);
}
/** ***************************************************************
* Return True if f is a constant function symbol.
*/
public
boolean
isConstant
(
String
f
) {
return
isFun
(
f
) &&
arity
.
get
(
f
).
intValue
() ==
0
;
}
/** ***************************************************************
*/
public
int
getArity
(
String
f
) {
if
(
arity
.
containsKey
(
f
))
return
arity
.
get
(
f
).
intValue
();
else
return
0
;
}
/** ***************************************************************
* Test signature object.
*/
public
static
void
test
() {
String
s
=
"cnf(qg1_2,negated_conjecture,~product(X1, Y1, Z1)|~product(X2, Y2, Z1)|~product(Z2, Y1, X1)|~product(Z2, Y2, X2)|equalish(Y1, Y2))."
;
Clause
c
=
Clause
.
string2Clause
(
s
);
Signature
sig
=
new
Signature
();
c
.
collectSig
(
sig
);
System
.
out
.
println
(
"result: "
+
sig
);
sig
=
new
Signature
();
sig
.
addFun
(
"mult"
,
2
);
sig
.
addFun
(
"a"
,
0
);
sig
.
addPred
(
"weird"
,
4
);
System
.
out
.
println
(
sig
+
" should be preds[wierd] and funs[mult,a]"
);
System
.
out
.
println
(
"all should be true:"
);
System
.
out
.
println
(
sig
.
isPred
(
"weird"
));
System
.
out
.
println
(!
sig
.
isPred
(
"unknown"
));
System
.
out
.
println
(!
sig
.
isPred
(
"a"
));
System
.
out
.
println
(
sig
.
isFun
(
"a"
));
System
.
out
.
println
(
sig
.
isConstant
(
"a"
));
System
.
out
.
println
(!
sig
.
isFun
(
"unknown"
));
System
.
out
.
println
(!
sig
.
isFun
(
"weird"
));
System
.
out
.
println
(
sig
.
getArity
(
"a"
)==
0
);
System
.
out
.
println
(
sig
.
getArity
(
"weird"
)==
4
);
}
/** ***************************************************************
*/
public
static
void
main
(
String
[]
args
) {
test
();
}
}
Back
|
FazBrowse Home
|
New Git URL