tclbdd

Check-in [d459b6ae38]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Add a first whack at a Boolean expression parser
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:d459b6ae384036bbe0d787f5ae89cc66915a8de5
User & Date: kbk 2013-12-05 03:08:02
Context
2013-12-05
03:16
Fix several miscellaneous packaging and coding issues identified by dgp and aku check-in: a87110a479 user: kbk tags: trunk
03:08
Add a first whack at a Boolean expression parser check-in: d459b6ae38 user: kbk tags: trunk
2013-12-04
06:01
Gave up on the unique quantifier and expunged it from the code. Added hard tests for exists and forall; now need tests of the glue surrounding them. check-in: 232f5ceef1 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to library/tclbdd.tcl.

5
6
7
8
9
10
11



12
13
14
15
16
17
18
19

20
21
22
23
24
25
26





































































































































# Copyright (c) 2013 by Kevin B. Kenny
#
# See the file "license.terms" for information on usage and redistribution
# of this file, and for a DISCLAIMER OF ALL WARRANTIES.
#
#------------------------------------------------------------------------------




namespace eval bdd {
    namespace export system
}

oo::class create bdd::system {
    method === {exprName1 exprName2} {
	expr {[my beadindex $exprName1] == [my beadindex exprName2]}
    }

    method satisfiable {exprName} {
	expr {[my beadindex $exprName] != 0}
    }
    method tautology {exprName} {
	expr {[my beadindex $exprname] == 1}
    }
}












































































































































>
>
>








>






|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
# Copyright (c) 2013 by Kevin B. Kenny
#
# See the file "license.terms" for information on usage and redistribution
# of this file, and for a DISCLAIMER OF ALL WARRANTIES.
#
#------------------------------------------------------------------------------

package require grammar::aycock;	# TEMP - Build parser in advance!
package require grammar::aycock::runtime

namespace eval bdd {
    namespace export system
}

oo::class create bdd::system {
    method === {exprName1 exprName2} {
	expr {[my beadindex $exprName1] == [my beadindex exprName2]}
    }
    export ===
    method satisfiable {exprName} {
	expr {[my beadindex $exprName] != 0}
    }
    method tautology {exprName} {
	expr {[my beadindex $exprname] == 1}
    }

}

proc bdd::Lexer {script} {
    set lexvals {\n ; ; ; ( ( ) ) = = ? ? : : nor NOR < < <= <=
	== == != != ^ ^ > > >= >= -> <= <- >= <-> == & & | | ~ ~ - - ! ~
	0 constant 1 constant}
    set line 0
    set cpos -1
    set symbols {}
    set values {}
    set indx 0
    while {[regexp -expanded -indices -start $indx {
	\A(?:
	   \\\n
	   | \n
	   | \s
	   | ;
	   | \(
	   | \)
	   | =
	   | \?
	   | :
	   | nor
	   | <
	   | <=
	   | ==
	   | !=
	   | >
	   | >=
	   | ->
	   | <-
	   | <->
	   | &
	   | \|
	   | -
	   | \^
	   | ~
	   | !
	   | 0\M
	   | 1\M
	   | [A-Za-z_][A-Za-z0-9_]*
	   )} $script token]} {
	lassign $token start end
	set value [string range $script $start $end]
	if {[dict exists $lexvals $value]} {
	    lappend tokens [dict get $lexvals $value]
	    lappend values $value
	} elseif {![string is space $value]} {
	    lappend tokens variable
	    lappend values $value
	}
	if {$token eq "\n"} {
	    incr line
	    set cpos $start
	}
	set indx [expr {$end+1}]
    }
    if {$indx == [string length $script]} {
	return [list $tokens $values]
    } else {
	set lpos [expr {$indx - $cpos}]
	set ch 	 [string index $script $indx]
	return -code error \
	    -errorCode [list BDD LexError $line $lpos $ch] \
	    "Lexical error at $line:$lpos near character '$ch'"
    }
}

set bdd::Parser [grammar::aycock::parser {
    
    start ::= script {}

    script ::= stmt {set _}
    script ::= script ; stmt {linsert [lindex $_ 0] end [lindex $_ 2]}

    stmt ::= assignment {}

    assignment ::= variable = expression {
	list [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }

    expression ::= expression ? orexp : expression {
	list terop ?: [lindex $_ 2] [lindex $_ 0] [lindex $_ 4]
    }
    expression ::= orexp {}

    orexp ::= orexp | xorexp {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    orexp ::= xorexp {}

    xorexp ::= xorexp ^ andexp {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    xorexp ::= andexp {}

    andexp ::= andexp & eqvexp {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    andexp ::= eqvexp {}

    eqvexp ::= eqvexp == ineqexp {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    eqvexp ::= eqvexp != ineqexp {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    eqvexp ::= ineqexp {}

    ineqexp ::= ineqexp <= addexp {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    ineqexp ::= ineqexp < addexp {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    ineqexp ::= ineqexp > addexp {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    ineqexp ::= ineqexp >= addexp {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    ineqexp ::= addexp {}
    
    addexp ::= addexp - primary {
	list binop [lindex $_ 1] [lindex $_ 0] [lindex $_ 2]
    }
    addexp ::= primary {}

    primary ::= ( expression ) { lindex $_ 1 }
    primary ::= variable { list variable [lindex $_ 0] }
    primary ::= CONSTANT { list constant [lindex $_ 0] }

}]