-
Notifications
You must be signed in to change notification settings - Fork 18
/
testLKToND.scala
135 lines (110 loc) · 4.26 KB
/
testLKToND.scala
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 gapt.testing
import ammonite.ops.FilePath
import gapt.expr.formula.hol.containsQuantifierOnLogicalLevel
import gapt.formats.tptp.TptpImporter
import gapt.proofs.context.mutable.MutableContext
import gapt.proofs.expansion.ExpansionProofToLK
import gapt.proofs.expansion.deskolemizeET
import gapt.proofs.lk.LKProof
import gapt.proofs.lk.rules.OrRightRule
import gapt.proofs.lk.rules.WeakeningRightRule
import gapt.proofs.lk.transformations.LKToND
import gapt.proofs.lk.util.containsEqualityReasoning
import gapt.proofs.lk.util.isMaeharaMG3i
import gapt.proofs.loadExpansionProof
import gapt.proofs.nd.ExcludedMiddleRule
import gapt.proofs.nd.NDProof
import gapt.proofs.resolution.ResolutionToExpansionProof
import gapt.proofs.resolution.structuralCNF
import gapt.provers.eprover.EProver
import gapt.utils.LogHandler
import gapt.utils.Logger
import gapt.utils.MetricsPrinter
private object lkStats {
def apply( lk: LKProof, logger: Logger ): Unit = {
import logger._
metric( "size_lk", lk.treeLike.size )
metric( "equational", containsEqualityReasoning( lk ) )
metric( "lk_max_succ_size", lk.subProofs.map( _.endSequent.succedent.size ).max )
metric( "lk_max_succ_set_size", lk.subProofs.map( _.endSequent.succedent.toSet.size ).max )
metric( "lk_in_mg3i", isMaeharaMG3i( lk ) )
metric( "lk_disj_right", lk.subProofs.count( _.isInstanceOf[OrRightRule] ) )
metric( "lk_disj_right_after_weak", lk.subProofs.count {
case OrRightRule( WeakeningRightRule( _, _ ), _, _ ) => true
case _ => false
} )
}
}
private object ndStats {
def apply( nd: NDProof, logger: Logger ): Unit = {
import logger._
metric( "size_nd", nd.treeLike.size )
val emFormulas = nd.treeLike.postOrder.collect {
case em: ExcludedMiddleRule => em.formulaA
}
val qEmFormulas = emFormulas.filter( containsQuantifierOnLogicalLevel( _ ) )
metric( "num_excl_mid", emFormulas.size )
metric( "num_quant_excl_mid", qEmFormulas.size )
metric( "num_excl_mid_distinct", emFormulas.toSet.size )
metric( "num_quant_excl_mid_distinct", qEmFormulas.toSet.size )
}
}
object testLKToND extends scala.App {
val logger = Logger( "testLKToND" )
import logger._
val metricsPrinter = new MetricsPrinter
LogHandler.current.value = metricsPrinter
try time( "total" ) {
val Seq( fileName ) = args.toSeq
metric( "file", fileName )
val expansion = time( "import" ) { loadExpansionProof( FilePath( fileName ) ) }
metric( "size_exp", expansion.size )
val Right( lk ) = time( "exp2lk" ) { ExpansionProofToLK.withIntuitionisticHeuristics( expansion ) }
lkStats( lk, logger )
val nd = time( "lk2nd" ) { LKToND( lk ) }
ndStats( nd, logger )
metric( "status", "ok" )
} catch {
case t: Throwable =>
metric( "status", "exception" )
metric( "exception", t.toString )
}
}
object testLKToND2 extends scala.App {
val logger = Logger( "testLKToND2" )
import logger._
val metricsPrinter = new MetricsPrinter
LogHandler.current.value = metricsPrinter
try time( "total" ) {
val Seq( fileName ) = args.toSeq
metric( "file", fileName )
val tptp = time( "tptp" ) { TptpImporter.loadWithIncludes( FilePath( fileName ) ) }
val problem = tptp.toSequent
implicit val ctx = MutableContext.guess( problem )
val cnf = time( "clausifier" ) { structuralCNF( problem ) }
time( "prover" ) {
new EProver(
Seq( "--auto-schedule", "--soft-cpu-limit=120", "--memory-limit=2048" ) ).getResolutionProof( cnf )
} match {
case Some( resolution ) =>
val expansion = time( "res2exp" ) { ResolutionToExpansionProof( resolution ) }
metric( "size_exp", expansion.size )
val desk = time( "desk" ) { deskolemizeET( expansion ) }
time( "exp2lk" ) { ExpansionProofToLK.withIntuitionisticHeuristics( desk ) } match {
case Right( lk ) =>
lkStats( lk, logger )
val nd = time( "lk2nd" ) { LKToND( lk ) }
ndStats( nd, logger )
metric( "status", "ok" )
case Left( _ ) =>
metric( "status", "desk_wo_eq" )
}
case None =>
metric( "status", "unprovable" )
}
} catch {
case t: Throwable =>
metric( "status", "exception" )
metric( "exception", t.toString.take( 100 ) )
}
}