-
Notifications
You must be signed in to change notification settings - Fork 2
/
backend-lib.maude
103 lines (86 loc) · 5.23 KB
/
backend-lib.maude
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
--- name: backend-lib.maude
--- info: collects all modules used by backend tools
load prelude-aux.maude --- library of extensions to Maude's prelude
load meta-aux.maude --- library of extensions to Maude's META-LEVEL module
load unsortify.maude --- code to send ordersorted terms to unsorted and back
load renaming.maude --- next-gen renaming library
load sort-ops.maude --- empty and finite sort constructions
load mgci.maude --- most general constructor instance operation
load ctor-var-unif.maude --- computing constructor variants and unifiers
load foform.maude --- formula data structure
load cstrterm.maude --- constrained term data structure
load reachform.maude --- defines reach formulas
load confluence.maude --- critical pair generation and utilities
load config.maude --- set of config flags that can affect proofs
load proofstate.maude --- models the state of our proofs
fmod RLTOOL-BACKEND is
pr FOFORM .
pr FOFORM-FILTER .
pr MAYBE-BOOL .
pr REACH-PROOF-STATE .
pr TRANSITION-OPERATIONS . --- wellFormed
var SR : ScopedRegistry .
var D : ProofMetadata .
var F : QFForm? .
var SM : ScopedMap .
var MQL : ScopedMapList .
var B : Bool .
var MB : MaybeBool .
var MK : [Bool] .
op checkVal : ProofMetadata QFForm? -> MaybeBool .
op checkValInit : ScopedMapList ProofMetadata QFForm? -> MaybeBool .
op checkValFindTool : ScopedMapList ProofMetadata QFForm? -> MaybeBool .
op checkVal : ScopedMap ScopedMapList ProofMetadata QFForm? -> MaybeBool .
eq checkVal((reg(SR) ; D),F) = checkValInit(SR['validity,(nil).ScopedMapList],(reg(SR) ; D),F) .
eq checkValInit(nil,D,F) = errb('No 'validity 'checkers 'loaded; 'did 'you 'forget 'to 'load 'one 'and/or 'mistype 'the 'loading 'directive?) .
eq checkValInit(MQL,D,F) = checkValFindTool(MQL,D,F) [owise] .
eq checkValFindTool(SM MQL,D,F) = if wellFormed(getmodules(SM),F) then beDebugPrint(false,"VAL",checkVal(SM,MQL,D,F),F) else checkValFindTool(MQL,D,F) fi .
eq checkValFindTool(nil,D,F) = errb('No 'acceptable 'validity 'checker 'loaded) .
op checkUnsat : ProofMetadata QFForm? -> MaybeBool .
op checkUnsatInit : ScopedMapList ProofMetadata QFForm? -> MaybeBool .
op checkUnsatFindTool : ScopedMapList ProofMetadata QFForm? -> MaybeBool .
op checkUnsat : ScopedMap ScopedMapList ProofMetadata QFForm? -> MaybeBool .
eq checkUnsat((reg(SR) ; D),F) = checkUnsatInit(SR['unsatisfiability,(nil).ScopedMapList],(reg(SR) ; D),F) .
eq checkUnsatInit(nil,D,F) = errb('No 'unsatisfiability 'checkers 'loaded; 'did 'you 'forget 'to 'load 'one 'and/or 'mistype 'the 'loading 'directive?) .
eq checkUnsatInit(MQL,D,F) = checkUnsatFindTool(MQL,D,F) [owise] .
eq checkUnsatFindTool(SM MQL,D,F) =
if formOrConjFrag(getmodules(SM),F) :: QFForm?
then beDebugPrint(true,"UNSAT",checkUnsat(SM,MQL,D,formOrConjFrag(getmodules(SM),F)),formOrConjFrag(getmodules(SM),F))
else nobool
fi defined-or-else checkUnsatFindTool(MQL,D,F) .
eq checkUnsatFindTool(nil,D,F) = errb('No 'acceptable 'unsatisfiability 'checker 'loaded) .
op performSimp : ProofMetadata QFForm? -> MaybeBool .
op performSimpInit : ScopedMapList ProofMetadata QFForm? -> MaybeBool .
op performSimpFindTool : ScopedMapList ProofMetadata QFForm? -> MaybeBool .
op performSimp : ScopedMap ScopedMapList ProofMetadata QFForm? -> MaybeBool .
eq performSimp((reg(SR) ; D),F) = performSimpInit(SR['simplification,(nil).ScopedMapList],(reg(SR) ; D),F) .
eq performSimpInit(nil,D,F) = errb('No 'simplifiers 'loaded; 'did 'you 'forget 'to 'load 'one 'and/or 'mistype 'the 'loading 'directive?) .
eq performSimpInit(MQL,D,F) = performSimpFindTool(MQL,D,F) [owise] .
eq performSimpFindTool(SM MQL,D,F) = if wellFormed(getmodules(SM),F) then performSimp(SM,MQL,D,F) else performSimpFindTool(MQL,D,F) fi .
eq performSimpFindTool(nil,D,F) = errb('No 'acceptable 'simplifier 'loaded) .
op beDebugPrint : Bool String MaybeBool QFForm? -> MaybeBool .
eq beDebugPrint(true, "UNSAT", true, F) = true [print "UNSAT: " F] .
eq beDebugPrint(true, "UNSAT", false, F) = false [print "NOT UNSAT: " F] .
eq beDebugPrint(true, "VAL", true, F) = true [print "VAL: " F] .
eq beDebugPrint(true, "VAL", false, F) = false [print "NOT VAL: " F] .
eq beDebugPrint(true, S:String,nobool, F) = nobool .
eq beDebugPrint(false,S:String,MB, F) = MB:MaybeBool .
ceq beDebugPrint(B, S:String,MK, F) = MK if not (MK :: MaybeBool) [print S:String " ERROR: " MK] .
endfm
--- a backend implementation for testing purposes
fmod DUMB-BACKEND-IMPL is
pr RLTOOL-BACKEND .
var D : ProofMetadata .
var MQL : ScopedMapList .
var F : QFForm? .
var M : Module .
var ModArgs : ModuleList .
eq checkVal ((M,'return-false,ModArgs),MQL,D,F) = false .
eq checkUnsat((M,'return-false,ModArgs),MQL,D,F) = false .
eq checkVal ((M,'return-nobool,ModArgs),MQL,D,F) = nobool .
eq checkUnsat((M,'return-nobool,ModArgs),MQL,D,F) = nobool .
eq checkVal ((M,'return-true,ModArgs),MQL,D,F) = true .
eq checkUnsat((M,'return-true,ModArgs),MQL,D,F) = true .
eq checkVal ((M,'return-err,ModArgs),MQL,D,F) = errb('this 'error 'is 'expected) .
eq checkUnsat((M,'return-err,ModArgs),MQL,D,F) = errb('this 'error 'is 'expected) .
endfm