-
Notifications
You must be signed in to change notification settings - Fork 18
/
testExpansionImport.scala
59 lines (53 loc) · 2.36 KB
/
testExpansionImport.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
package gapt.testing
import ammonite.ops.FilePath
import gapt.expr.formula.hol.lcomp
import gapt.expr.Const
import gapt.expr.util.expressionSize
import gapt.formats.tptp.TptpImporter
import gapt.proofs.context.mutable.MutableContext
import gapt.proofs.expansion.eliminateCutsET
import gapt.proofs.expansion.eliminateDefsET
import gapt.proofs.resolution._
import gapt.provers.eprover.EProver
import gapt.utils.{ LogHandler, Logger, MetricsPrinter }
object testExpansionImport extends scala.App {
val logger = Logger( "testExpansionImport" )
import logger._
val metricsPrinter = new MetricsPrinter
LogHandler.current.value = metricsPrinter
val Seq( tptpFileName ) = args.toSeq
metric( "file", tptpFileName )
try time( "total" ) {
val tptp = time( "tptpparser" ) { TptpImporter.loadWithIncludes( FilePath( tptpFileName ) ) }
val problem = tptp.toSequent
metric( "problem_lcomp", lcomp( problem ) )
metric( "problem_scomp", expressionSize( problem.toImplication ) )
implicit val ctx = MutableContext.guess( problem )
val cnf = time( "clausifier" ) { structuralCNF( problem ) }
time( "prover" ) { new EProver( Seq( "--auto-schedule", "--soft-cpu-limit=60", "--memory-limit=2048" ) ).getResolutionProof( cnf ) } match {
case Some( resolution ) =>
metric( "size_res_dag", resolution.dagLike.size )
metric( "size_res_tree", resolution.treeLike.size )
val equational = containsEquationalReasoning( resolution )
metric( "equational", equational )
val expansionWithDefs = time( "withdefs" ) {
ResolutionToExpansionProof.withDefs(
resolution,
ResolutionToExpansionProof.inputsAsExpansionSequent )
}
metric( "size_withdefs", expansionWithDefs.size )
val defConsts = resolution.subProofs collect { case d: DefIntro => d.defConst: Const }
val withDefsCE = time( "cutelim1" ) { eliminateCutsET( expansionWithDefs ) }
val withoutDefs = time( "defelim" ) { eliminateDefsET( withDefsCE, !equational, defConsts ) }
val expansion = time( "cutelim2" ) { eliminateCutsET( withoutDefs ) }
metric( "size_exp", expansion.size )
metric( "status", "unsat" )
case None =>
metric( "status", "sat" )
}
} catch {
case t: Throwable =>
metric( "status", "exception" )
metric( "exception", t.getMessage.take( 100 ) )
}
}