Documentation ¶
Overview ¶
Package file takes an input stream and outputs an AST for the file. It also provides the types to interface with the generated tree.
The parser here is for a subset of SMT-LIB. It is more restrictive in most aspects, but more permissive in others. See grammar.go for more details about what is accepted. Most of the QF_IDL benchmarks parse correctly. It just doesn't support atoms of the form (op x (+ y c)).
Code generated by Participle. DO NOT EDIT.
Index ¶
- Constants
- Variables
- type BoolOp
- type BoolOpBuilder
- type CmpArguments
- type CmpDiff
- type CmpOp
- type CmpOpBuilder
- type CmpSym
- type Declaration
- type DiffAtom
- type DiffExpr
- type EquOp
- type EquOpBuilder
- type Expr
- type File
- type ITEBuilder
- type LetBinding
- type LetBuilder
- type Metadata
- type MetadataCategory
- type MetadataLicense
- type MetadataNotes
- type MetadataSource
- type MetadataStatus
- type NotBuilder
- type Number
- type NumberAtom
- type Sort
- type Status
- type StringLit
- type Symbol
- type SymbolAtom
- type Version
Constants ¶
const ( EquOpEQ EquOp = iota EquOpNE CmpOpLE CmpOp = iota CmpOpLT CmpOpGE CmpOpGT BoolOpIMP BoolOp = iota BoolOpAND BoolOpOR BoolOpXOR )
Enumeration constants for EquOp, CmpOp, and BoolOp. Not all the operations are present since some of them are handled with custom parse rules.
Variables ¶
var GenBackRefCache sync.Map
var GenLexer lexer.Definition = lexerGenDefinitionImpl{}
var Lexer = lexer.MustSimple([]lexer.SimpleRule{
{Name: "ParenOpen", Pattern: `\(`},
{Name: "ParenClose", Pattern: `\)`},
{Name: "Whitespace", Pattern: `[ \t\n\r]+`},
{Name: "Symbol", Pattern: `[A-Za-z~!@$%^&*_\-+=<>.?\/][A-Za-z0-9~!@$%^&*_\-+=<>.?\/]*|\|[^|\\]*\|`},
{Name: "Version", Pattern: `(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)`},
{Name: "Numeral", Pattern: `0|[1-9][0-9]*`},
{Name: "Attribute", Pattern: `:[A-Za-z~!@$%^&*_\-+=<>.?\/][A-Za-z0-9~!@$%^&*_\-+=<>.?\/]*`},
{Name: "StringLit", Pattern: `"([^"]|"")*"`},
})
This variable defines the lexer we use for QFIDL-LIB files. It is used to generate an optimized version.
var Parser = participle.MustBuild[File]( participle.UseLookahead(2), participle.Elide("Whitespace"), participle.Lexer(GenLexer), participle.Union[Metadata]( MetadataSource{}, MetadataLicense{}, MetadataCategory{}, MetadataStatus{}, MetadataNotes{}, ), participle.Union[Expr]( NumberAtom{}, DiffAtom{}, SymbolAtom{}, NotBuilder{}, ITEBuilder{}, EquOpBuilder{}, CmpOpBuilder{}, BoolOpBuilder{}, LetBuilder{}, ), participle.Union[CmpArguments]( CmpSym{}, CmpDiff{}, ), participle.Union[DiffExpr]( DiffAtom{}, SymbolAtom{}, ), )
This variable defines the parser we will use on QFIDL-LIB input streams. Note the unions. These have to be declared here and below.
Functions ¶
This section is empty.
Types ¶
type BoolOp ¶
type BoolOp int
The BoolOp type represents the the associative boolean operations. That is:
- Impliciation
- AND
- OR
- XOR
type BoolOpBuilder ¶
type BoolOpBuilder struct { Operation BoolOp `parser:"'(':ParenOpen @( '=>':Symbol | 'and':Symbol | 'or':Symbol | 'xor':Symbol )"` Arguments []Expr `parser:"@@ @@+ ')':ParenClose"` Pos lexer.Position }
BoolOpBuilder represents all of the formula building operators for associative boolean operations. It wraps a BoolOp and its arguments, of which there are at least two.
func (BoolOpBuilder) Position ¶
func (b BoolOpBuilder) Position() lexer.Position
type CmpArguments ¶
type CmpArguments interface {
// contains filtered or unexported methods
}
type CmpDiff ¶
type CmpDiff struct { Difference DiffExpr `parser:"@@"` Constant NumberAtom `parser:"@@"` }
type CmpOp ¶
type CmpOp int
CmpOp represents the different operations we can apply to difference atoms. Recall that difference atoms are of the form (op (- x y) n). However, it does not include equality operations. Those are handled separately.
type CmpOpBuilder ¶
type CmpOpBuilder struct { Operation CmpOp `parser:"'(':ParenOpen @( '<=':Symbol | '<':Symbol | '>=':Symbol | '>':Symbol )"` Arguments CmpArguments `parser:"@@ ')':ParenClose"` Pos lexer.Position }
CmpOpBuilder is the formula building operator for relational symbols, which are all the operations we can do on numbers except for equality. Its syntax is quite restrictive. Its arguments are described by CmpArguments, which can either be two symbols or a difference expression and a number.
func (CmpOpBuilder) Position ¶
func (b CmpOpBuilder) Position() lexer.Position
type Declaration ¶
type Declaration struct { Name Symbol `parser:"'(':ParenOpen ( 'declare-fun':Symbol @Symbol '(':ParenOpen ')':ParenClose | 'declare-const':Symbol @Symbol )"` Sort Sort `parser:"@Symbol ')':ParenClose"` }
The Declaration struct represents a variable declaration in a QFIDL-LIB file. It can be declares with declare-const or declare-fun, and it can have sort either Bool or Int.
type DiffAtom ¶
type DiffAtom struct { LHS Symbol `parser:"'(':ParenOpen '-':Symbol @Symbol"` RHS Symbol `parser:"@Symbol ')':ParenClose"` Pos lexer.Position }
A DiffAtom represents the difference of two symbols. Both of these symbols should have sort Int, but we'll check this later.
type DiffExpr ¶
The DiffExpr interface represents a difference expression - an expression of the form (- x y). It also includes symbols because of let bindings.
type EquOp ¶
type EquOp int
An EquOp represents the different operations we can apply to equalities or disequalities of two symbols. That is:
- Equals
- Distinct
type EquOpBuilder ¶
type EquOpBuilder struct { Operation EquOp `parser:"'(':ParenOpen @( '=':Symbol | 'distinct':Symbol )"` Arguments []Expr `parser:"@@ @@+ ')':ParenClose"` Pos lexer.Position }
EquOpBuilder represents the formula building operators for equalities and disequalities. That is, it wraps an EquOp and its arguments, of which there are at least two.
This is very similar in structure to BoolOpBuilder, but it has different semantics, so we separate it in the grammar. For example, it has to deal with both boolean arguments and difference arguments.
func (EquOpBuilder) Position ¶
func (b EquOpBuilder) Position() lexer.Position
type Expr ¶
type Expr interface { // The Position method returns the starting position of this expression. Position() lexer.Position // contains filtered or unexported methods }
The Expr interface expresses the set of expressions we will attempt to parse. Ideally, this approximates the set of well-formed-formulas in QF_IDL.
type File ¶
type File struct { // The Version field describes the version number declared in the file. This // is ignored, but it may be useful in the future. Version Version `parser:"'(':ParenOpen 'set-info':Symbol ':smt-lib-version':Attribute @Version ')':ParenClose"` // The Logic field gives the logic the file was written with. We only // support QF_IDL, and we will reject anything that doesn't declare that // type, even if it is otherwise valid. Logic Symbol `parser:"'(':ParenOpen 'set-logic':Symbol @Symbol ')':ParenClose"` // This holds all the metadata entries given in the file. These correspond // to all the attributes we declared in the lexer, minus the version. Metadata []Metadata `parser:"@@*"` // This array holds all of the variable delclarations Declarations []Declaration `parser:"@@*"` // This array holds all of the assertions for the solver, as they are given // in the AST. Assertions []Expr `parser:"( '(':ParenOpen 'assert':Symbol @@ ')':ParenClose )*"` // command followed by an exit command. The grammar requires that the footer // be present, so this will always be true. Footer bool `parser:"@('(':ParenOpen 'check-sat':Symbol ')':ParenClose '(':ParenOpen 'exit':Symbol ')':ParenClose)"` }
The File struct represents the root of the AST. It contains file metadata, along with all the declarations and assertions.
type ITEBuilder ¶
type ITEBuilder struct { If Expr `parser:"'(':ParenOpen 'ite':Symbol @@"` Then Expr `parser:"@@"` Else Expr `parser:"@@ ')':ParenClose"` Pos lexer.Position }
ITEBuilder is the formula building operator for if-then-else. It takes exactly three arguments because anything else doesn't really make sense.
func (ITEBuilder) Position ¶
func (b ITEBuilder) Position() lexer.Position
type LetBinding ¶
type LetBinding struct { Name Symbol `parser:"'(':ParenOpen @Symbol"` Bind Expr `parser:"@@ ')':ParenClose"` Pos lexer.Position }
A single binding for a LetBuilder expression. It has a name and what formula that is bound to.
type LetBuilder ¶
type LetBuilder struct { Bindings []LetBinding `parser:"'(':ParenOpen 'let':Symbol '(':ParenOpen @@+ ')':ParenClose"` Expr Expr `parser:"@@ ')':ParenClose"` Pos lexer.Position }
Formula building operator for let expressions. These consist of at least one LetBinding, and well as the final formula to substitute them into.
func (LetBuilder) Position ¶
func (b LetBuilder) Position() lexer.Position
type Metadata ¶
type Metadata interface {
// contains filtered or unexported methods
}
The Metadata interface models the possible annotations on QFIDL-LIB files. These correspond to a limited set of the annotations on SMT-LIB files, meaning:
- :source with MetadataSource
- :license with MetadataLicense
- :category with MetadataCategory
- :status with MetadataStatus
- :notes with MetadataNotes
type MetadataCategory ¶
type MetadataCategory struct {
Category StringLit `parser:"'(':ParenOpen 'set-info':Symbol ':category':Attribute @StringLit ')':ParenClose"`
}
type MetadataLicense ¶
type MetadataLicense struct {
License StringLit `parser:"'(':ParenOpen 'set-info':Symbol ':license':Attribute @StringLit ')':ParenClose"`
}
type MetadataNotes ¶
type MetadataNotes struct {
Notes Symbol `parser:"'(':ParenOpen 'set-info':Symbol ':notes':Attribute @Symbol ')':ParenClose"`
}
type MetadataSource ¶
type MetadataSource struct {
Source Symbol `parser:"'(':ParenOpen 'set-info':Symbol ':source':Attribute @Symbol ')':ParenClose"`
}
type MetadataStatus ¶
type MetadataStatus struct {
Status Status `parser:"'(':ParenOpen 'set-info':Symbol ':status':Attribute @Symbol ')':ParenClose"`
}
type NotBuilder ¶
type NotBuilder struct { Argument Expr `parser:"'(':ParenOpen 'not':Symbol @@ ')':ParenClose"` Pos lexer.Position }
NotBuilder represents the formula building operator for boolean negation. It only takes one argument - the thing to negate.
func (NotBuilder) Position ¶
func (b NotBuilder) Position() lexer.Position
type Number ¶
Number represents either a positive or negative number. It's wrapped by a NumberAtom.
type NumberAtom ¶
type NumberAtom struct { Num Number `parser:"( @Numeral | '(':ParenOpen @( '-':Symbol Numeral ) ')':ParenClose )"` Pos lexer.Position }
NumberAtom represents either a numeral or its negation. Remember that the grammar has no support for negative numbers, so they are built with the negation operator.
func (NumberAtom) Position ¶
func (a NumberAtom) Position() lexer.Position
type Sort ¶
type Sort int
Sort is an enumeration of all the sorts we support, specifically Bool and Int.
type Status ¶
type Status int
Status is a wrapper to express whether a particular instance is satisfiable or not. This is the general way Golang does enums, it seems.
type StringLit ¶
type StringLit string
StringLit is a wrapper type around string literals. We need this to allow for escaping.
type Symbol ¶
type Symbol string
Symbol is a wrapper type for identifiers. We need to have custom parsing logic due to complex symbols, so we use this type to do the conversion.
type SymbolAtom ¶
SymbolAtom represents a bare symbol. It can sort Bool or Int, depending on context.
func (SymbolAtom) Position ¶
func (a SymbolAtom) Position() lexer.Position