@@ -50,48 +50,58 @@ Setup
50
50
The latest stable release for Scala 2.11 is available on Sonatype, simply add
51
51
the following to your ` build.sbt ` :
52
52
53
- libraryDependencies += "com.regblanc" %% "scala-smtlib" % "0.2.2"
53
+ ``` scala
54
+ libraryDependencies += " com.regblanc" %% " scala-smtlib" % " 0.2.2"
55
+ ```
54
56
55
57
Getting Started with Examples
56
58
-----------------------------
57
59
58
60
To construct a parser, you will need a java.io.Reader and a lexer:
59
61
60
- val is = new java.io.FileReader("INPUT")
61
- val lexer = new smtlib.lexer.Lexer(is)
62
- val parser = new smtlib.parser.Parser(lexer)
62
+ ``` scala
63
+ val is = new java.io.FileReader (" INPUT" )
64
+ val lexer = new smtlib.lexer.Lexer (is)
65
+ val parser = new smtlib.parser.Parser (lexer)
66
+ ```
63
67
64
68
The parser then provides a ` parseCommand ` functions that will consume the input
65
69
until the end of command:
66
70
67
- val script: List[Command] = {
68
- var cmds = new ListBuffer[Command]
69
- var cmd = parser.parseCommand
70
- while(cmd != null)
71
- cmds.append(cmd)
72
- cmds.toList
73
- }
71
+ ``` scala
72
+ val script : List [Command ] = {
73
+ var cmds = new ListBuffer [Command ]
74
+ var cmd = parser.parseCommand
75
+ while (cmd != null )
76
+ cmds.append(cmd)
77
+ cmds.toList
78
+ }
79
+ ```
74
80
75
81
` parseCommand ` returns ` null ` when the end of file is reached.
76
82
77
83
You can decompose a command using pattern matching:
78
84
79
- import smtlib.parser.Commands._
80
- cmd match {
81
- case Assert(term) => ???
82
- case CheckSat() => ???
83
- case Pop(1) => ???
84
- }
85
+ ``` scala
86
+ import smtlib .parser .Commands ._
87
+ cmd match {
88
+ case Assert (term) => ???
89
+ case CheckSat () => ???
90
+ case Pop (1 ) => ???
91
+ }
92
+ ```
85
93
86
94
If you want to generate a script to feed to a solver, you can build the AST
87
95
explicitly, and use the pretty printers:
88
96
89
- import smtlib.parser.Commands._
90
- import smtlib.parser.theories.Ints._
91
- val x = QualifiedIdentifier(SimpleIdentifier(SSymbol("x")))
92
- val y = QualifiedIdentifier(SimpleIdentifier(SSymbol("y")))
93
- val formula = Assert(LessThan(NumeralLit(0), Plus(x, y)))
94
- smtlib.printer.RecursivePrinter.toString(formula) //(assert (< 0 (+ x y)))
97
+ ``` scala
98
+ import smtlib .parser .Commands ._
99
+ import smtlib .parser .theories .Ints ._
100
+ val x = QualifiedIdentifier (SimpleIdentifier (SSymbol (" x" )))
101
+ val y = QualifiedIdentifier (SimpleIdentifier (SSymbol (" y" )))
102
+ val formula = Assert (LessThan (NumeralLit (0 ), Plus (x, y)))
103
+ smtlib.printer.RecursivePrinter .toString(formula) // (assert (< 0 (+ x y)))
104
+ ```
95
105
96
106
The above is a little bit verbose due to the objective of supporting all of
97
107
SMT-LIB. We are hoping to provide a nicer API in the future to build SMT-LIB
@@ -116,9 +126,11 @@ parsing of [`Tokens`](/src/main/scala/smtlib/lexer/Tokens.scala), The
116
126
tokens. It reads lazily from a ` java.io.Reader ` , on invocation of the ` nextToken `
117
127
method:
118
128
119
- class Lexer(reader: java.io.Reader) {
120
- def nextToken: Token = { ... }
121
- }
129
+ ``` scala
130
+ class Lexer (reader : java.io.Reader ) {
131
+ def nextToken : Token = { ... }
132
+ }
133
+ ```
122
134
123
135
One call to ` nextToken ` will only consume the input until the end of the
124
136
current token. It will read one character at a time from the input ` Reader `
@@ -147,10 +159,12 @@ interested in fully formated SMT-LIB expressions. The
147
159
expressions. The [ ` Parser ` ] ( /src/main/scala/smtlib/parser/Parser.scala ) consumes
148
160
tokens generated by the above lexer:
149
161
150
- class Parser(lexer: smtlib.lexer.Lexer) {
151
- def nextCommand: Command = { ... }
152
- def nextTerm: Term = { ... }
153
- }
162
+ ``` scala
163
+ class Parser (lexer : smtlib.lexer.Lexer ) {
164
+ def nextCommand : Command = { ... }
165
+ def nextTerm : Term = { ... }
166
+ }
167
+ ```
154
168
155
169
It provides many ` nextX ` methods (more than shown above) to parse any expressions
156
170
defined by the SMT-LIB standard grammar. The more common are the ` nextCommand `
0 commit comments