file

type BoolOp ¶

type BoolOp int

The BoolOp type represents the the associative boolean operations. That is:

• Impliciation
• AND
• OR
• XOR

func (b *BoolOp) Capture(values []string) error

func (b BoolOp) String() string

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 (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.

func (c *CmpOp) Capture(values []string) error

func (c CmpOp) String() string

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 (b CmpOpBuilder) Position() lexer.Position

type CmpSym ¶

type CmpSym struct {
	LHS Symbol `parser:"@Symbol"`
	RHS Symbol `parser:"@Symbol"`
}

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.

func (a DiffAtom) Position() lexer.Position

type DiffExpr ¶

type DiffExpr interface {
	Position() lexer.Position
	// contains filtered or unexported methods
}

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

func (e *EquOp) Capture(values []string) error

func (e EquOp) String() string

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 (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 )*"`

	// This flag reports whether a footer was present. The footer is a check-sat
	// 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.

func Parse(input io.Reader) (ret *File, err error)

func (file File) GetStatus() Status

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 (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 (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 (b NotBuilder) Position() lexer.Position

type Number ¶

type Number struct {
	Value *big.Int
}

Number represents either a positive or negative number. It's wrapped by a NumberAtom.

func (n *Number) Capture(values []string) error

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 (a NumberAtom) Position() lexer.Position

type Sort ¶

type Sort int

Sort is an enumeration of all the sorts we support, specifically Bool and Int.

const (
	SortBool Sort = iota
	SortInt
)

func (sort *Sort) Capture(values []string) error

func (sort Sort) String() string

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.

const (
	StatusUnsat Status = iota
	StatusSat
	StatusUnknown
)

func (stat *Status) Capture(values []string) error

func (stat Status) String() string

type StringLit ¶

type StringLit string

StringLit is a wrapper type around string literals. We need this to allow for escaping.

func (str *StringLit) Capture(values []string) error

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.

func (sym *Symbol) Capture(values []string) error

type SymbolAtom ¶

type SymbolAtom struct {
	Name Symbol `parser:"@Symbol"`
	Pos  lexer.Position
}

SymbolAtom represents a bare symbol. It can sort Bool or Int, depending on context.

func (a SymbolAtom) Position() lexer.Position

type Version ¶

type Version struct {
	Major uint64
	Minor uint64
}

The Version struct documents what library version the input file was written with. It has the format N.M, and it implements the Capture interface to parse that string to integers.

func (v *Version) Capture(values []string) (err error)