SyGuS grammars, sort-erased

A grammar restricts the shape of a term the solver is allowed to produce — the candidates a synthFun may return, or the shape of an interpolant or abduct.

Two kinds of variable go into one: the parameters (BVar) the synthesized term may mention, and the non-terminals (NT) the rules are written over. An NT converts to a term, since a non-terminal appears inside its own rules, but has no coercion to BVar, so it cannot be passed as a parameter by mistake.

A grammar freezes once it is used. addRule and friends answer a new Grammar, so the type reads as though grammars were persistent values, but the object underneath is shared: once a grammar has been passed to synthFun, cvc5 rejects every further rule with Grammar cannot be modified after passing it as an argument to synthFun. Build a grammar completely before using it.

Non-terminal symbols

structure Cvc.Untyped.NT [Ω] : Type

A grammar's non-terminal symbol: a bound variable, kept apart from parameters by its type.

• ofBVar :: (
• bvar : Cvc.Untyped.BVar
• )

@[instance_reducible]

instance Cvc.Untyped.instBEqNT {inst✝ : Ω} : BEq NT

Equations

• Cvc.Untyped.instBEqNT = { beq := Cvc.Untyped.instBEqNT.beq }

def Cvc.Untyped.instBEqNT.beq {inst✝ : Ω} : NT → NT → Bool

Equations

• Cvc.Untyped.instBEqNT.beq { bvar := a } { bvar := b } = (a == b)
• Cvc.Untyped.instBEqNT.beq x✝¹ x✝ = false

def Cvc.Untyped.instOrdNT.ord {inst✝ : Ω} : NT → NT → Ordering

Equations

• Cvc.Untyped.instOrdNT.ord { bvar := a } { bvar := b } = (compare a b).then Ordering.eq

@[instance_reducible]

instance Cvc.Untyped.instOrdNT {inst✝ : Ω} : Ord NT

Equations

• Cvc.Untyped.instOrdNT = { compare := Cvc.Untyped.instOrdNT.ord }

def Cvc.Untyped.instHashableNT.hash {inst✝ : Ω} : NT → UInt64

Equations

• Cvc.Untyped.instHashableNT.hash { bvar := a } = mixHash 0 (hash a)

@[instance_reducible]

instance Cvc.Untyped.instHashableNT {inst✝ : Ω} : Hashable NT

Equations

• Cvc.Untyped.instHashableNT = { hash := Cvc.Untyped.instHashableNT.hash }

@[reducible, inline]

abbrev Cvc.Untyped.NTs [Ω] : Type

An array of non-terminal symbols.

Equations

• Cvc.Untyped.NTs = Array Cvc.Untyped.NT

def Cvc.Untyped.NT.mk [Ω] (srt : Srt) (name : String) : Env NT

A non-terminal symbol of the given sort.

Equations

• Cvc.Untyped.NT.mk srt name = do let __do_lift ← Cvc.Untyped.BVar.mk srt name pure { bvar := __do_lift }

def Cvc.Untyped.NT.toBVar [Ω] (nt : NT) : BVar

Turns itself into a bound variable, explicitly only: a non-terminal is not a parameter.

Equations

• nt.toBVar = Cvc.Untyped.NT.bvar✝ nt

def Cvc.Untyped.NT.toTerm [Ω] (nt : NT) : Term

Turns itself into a term, which is how a non-terminal appears inside its own rules.

Equations

• nt.toTerm = nt.toBVar.toTerm

@[instance_reducible]

instance Cvc.Untyped.NT.instCoeTerm [Ω] : Coe NT Term

Equations

• Cvc.Untyped.NT.instCoeTerm = { coe := Cvc.Untyped.NT.toTerm }

@[instance_reducible]

instance Cvc.Untyped.NT.instToString [Ω] : ToString NT

Equations

• Cvc.Untyped.NT.instToString = { toString := toString ∘ Cvc.Untyped.NT.toTerm }

Grammars

A grammar is built through a solver, but any solver of the scope accepts it.

def Cvc.Untyped.Solver.mkGrammar [Ω] (s : Solver) (boundVars : BVars) (start : NT) (others : NTs := #[]) : Env Grammar

A grammar over the given parameters, starting at start.

boundVars are the parameters of the synthFun this grammar will constrain, and must be the very same variables that function is declared with. others are the further non-terminals the rules may mention: every one has to be declared here. A non-terminal unreachable from start is left out of the grammar.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Grammar.mk [Ω] (boundVars : BVars) (start : NT) (others : NTs := #[]) : Env Grammar

Solver.mkGrammar, without a solver at hand.

Equations

• Cvc.Untyped.Grammar.mk boundVars start others = do let s ← Cvc.Untyped.Solver.new s.mkGrammar boundVars start others

def Cvc.Untyped.Grammar.signatureSrt [Ω] (g : Grammar) : Env Srt

The sort of the functions the grammar generates.

The parameters' sorts arrowed onto the start symbol's, flattened as a curried Lean arrow is, or the start symbol's sort alone when there are no parameters.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Grammar.addRule [Ω] (g : Grammar) (nt : NT) (rule : Term) : Env Grammar

Adds a production rule.

nt must be one of the non-terminals this grammar was declared with, and rule must have its sort. Neither is visible in a signature, so both are checked when the rule is added.

Equations

• g.addRule nt rule = Cvc.Untyped.Grammar.withRaw✝ g ((Cvc.Untyped.Grammar.raw✝ g).addRule nt.toTerm rule)

def Cvc.Untyped.Grammar.addRules [Ω] (g : Grammar) (nt : NT) (rules : Terms) : Env Grammar

Adds a production rule.

nt must be one of the non-terminals this grammar was declared with, and rule must have its sort. Neither is visible in a signature, so both are checked when the rule is added.

Equations

• g.addRules nt rules = Cvc.Untyped.Grammar.withRaw✝ g ((Cvc.Untyped.Grammar.raw✝ g).addRules nt.toTerm rules)

def Cvc.Untyped.Grammar.addAnyConstant [Ω] (g : Grammar) (nt : NT) : Env Grammar

Allows any constant of the non-terminal's sort.

Equations

• g.addAnyConstant nt = Cvc.Untyped.Grammar.withRaw✝ g ((Cvc.Untyped.Grammar.raw✝ g).addAnyConstant nt.toTerm)

def Cvc.Untyped.Grammar.addAnyVariable [Ω] (g : Grammar) (nt : NT) : Env Grammar

Allows any of the grammar's parameters that has the non-terminal's sort.

Equations

• g.addAnyVariable nt = Cvc.Untyped.Grammar.withRaw✝ g ((Cvc.Untyped.Grammar.raw✝ g).addAnyVariable nt.toTerm)

smt.grammar!

A grammar written as one block, BNF-style, with smt! terms as its alternatives:

smt.grammar! s (x y : Int) where
  start : Int  := x | y | if cnd then start else start
  cnd   : Bool := start ≤ start

• s is any solver of the scope; the binders after it are the grammar's parameters.
• Each line declares a non-terminal and its sort, then its alternatives separated by |. The first line's is the start symbol.
• Inside the alternatives a non-terminal or parameter stands for its term, so rules mention one another and themselves freely. Every non-terminal is made before any rule is added.
• ?const and ?var are cvc5's "any constant" and "any parameter" of the non-terminal's sort.

A sort is written as a Lean type (Int) or a Srt value (int).

Extending a grammar afterwards

smt.grammar! answers the grammar alone, its parameters and non-terminals being made out of sight, so nothing can be added to it later. Two forms with the same body answer them too:

• smt.mkGrammar! s … where … answers grammar × NT₁ × NT₂ × … without parameters, and (grammar × PARAM₁ × …) × NT₁ × NT₂ × … with some, in declaration order. The parameters are grouped with the grammar so that one cannot be taken for a non-terminal by position.

• smt.letGrammar! g ← s … where … is a do element binding g, the parameters and the non-terminals under the names the block declares, so the order cannot be got wrong:

  smt.letGrammar! g ← s (x y : Int) where
    start : Int  := x | y
    cnd   : Bool := start ≤ start
  let g ← g.addRule start (← smt! if cnd then start else start)
  

  A parameter is bound as a BVar and a non-terminal as an NT, both converting to terms. A name never used afterwards draws no unused-variable warning.

In these two forms a non-terminal may be declared without alternatives, nt : sort alone, for its rules to be added afterwards — rules computed from data, say, which a block cannot spell:

smt.letGrammar! g ← s (x : Int) where
  start : Int := x | start + num
  num   : Int
let mut g := g
for k in [3, 7] do g ← g.addRule num (← Term.mkInt k)

smt.grammar! refuses such a line, since the grammar it answers cannot be extended.

A grammar can be extended until it is used for synthesis, after which cvc5 rejects new rules. A non-terminal unreachable from the start symbol is left out of the grammar until a rule reaches it.

All three forms are scoped in each layer, as smt! is: open Cvc.Untyped selects this one.

def Cvc.smtGrammarAlt.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.smtGrammarAlt : Category

One alternative of a smt.grammar! rule.

Equations

• Lean.Parser.Category.smtGrammarAlt = { }

def Cvc.smtGrammarAny : Lean.ParserDescr

?const or ?var: any constant, or any parameter, of the non-terminal's sort.

Equations

• Cvc.smtGrammarAny = Lean.ParserDescr.node `Cvc.smtGrammarAny 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "?" false) (Lean.ParserDescr.const `ident))

def Cvc.smtGrammarTerm : Lean.ParserDescr

An alternative that is a term.

Equations

• Cvc.smtGrammarTerm = Lean.ParserDescr.node `Cvc.smtGrammarTerm 1022 (Lean.ParserDescr.cat `smtTerm 0)

def Lean.Parser.Category.smtGrammarRule : Category

One line of a smt.grammar!: a non-terminal, its sort, and its alternatives.

Equations

• Lean.Parser.Category.smtGrammarRule = { }

def Cvc.smtGrammarRule.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtGrammarRule : Lean.ParserDescr

nt : sort := alt | alt | …, or nt : sort alone, its rules to be added afterwards.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.smtGrammarBody : Category

What follows smt.grammar!: the solver, the parameters, and the rules.

Equations

• Lean.Parser.Category.smtGrammarBody = { }

def Cvc.smtGrammarBody.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtGrammarBody : Lean.ParserDescr

s (x : Int) … where followed by the rules, one per line.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.grammarU : Lean.ParserDescr

A sort-erased grammar; smt.grammar! under open Cvc.Untyped.

Equations

• Cvc.grammarU = Lean.ParserDescr.node `Cvc.grammarU 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "grammarU! ") (Lean.ParserDescr.cat `smtGrammarBody 0))

def Cvc.grammarT : Lean.ParserDescr

A typed grammar; smt.grammar! under open Cvc.Typed.

Equations

• Cvc.grammarT = Lean.ParserDescr.node `Cvc.grammarT 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "grammarT! ") (Lean.ParserDescr.cat `smtGrammarBody 0))

def Cvc.mkGrammarU : Lean.ParserDescr

A sort-erased grammar and its parts; smt.mkGrammar! under open Cvc.Untyped.

Equations

• Cvc.mkGrammarU = Lean.ParserDescr.node `Cvc.mkGrammarU 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "mkGrammarU! ") (Lean.ParserDescr.cat `smtGrammarBody 0))

def Cvc.mkGrammarT : Lean.ParserDescr

A typed grammar and its parts; smt.mkGrammar! under open Cvc.Typed.

Equations

• Cvc.mkGrammarT = Lean.ParserDescr.node `Cvc.mkGrammarT 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "mkGrammarT! ") (Lean.ParserDescr.cat `smtGrammarBody 0))

def Cvc.Untyped.«termSmt.grammar!_» : Lean.ParserDescr

A sort-erased SyGuS grammar, written as one BNF-style block whose alternatives are smt! terms.

smt.grammar! s (x y : Int) where
  start : Int := x | y | start + start

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.«termSmt.mkGrammar!_» : Lean.ParserDescr

smt.grammar!, also answering its parameters and non-terminals, to extend it afterwards.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.«doElemSmt.letGrammar!_←_» : Lean.ParserDescr

smt.grammar! as a do element, binding the grammar, its parameters and its non-terminals.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Ext.mentions (name : Lean.Name) (stx : Lean.Syntax) : Bool

Whether an identifier of this name occurs anywhere in a piece of syntax.

Equations

• Cvc.Ext.mentions name stx = (stx.find? fun (s : Lean.Syntax) => s.isIdent && s.getId == name).isSome

def Cvc.Ext.mkTuple : List (Lean.TSyntax `term) → Lean.MacroM (Lean.TSyntax `term)

A right-nested tuple of the given terms, (a, b, c); a single term stands for itself.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Ext.mkTuple [] = Lean.Macro.throwUnsupported
• Cvc.Ext.mkTuple [t] = pure t

def Cvc.Ext.mkProd : List (Lean.TSyntax `term) → Lean.MacroM (Lean.TSyntax `term)

The right-nested product of the given types, α × β × γ; a single type stands for itself.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Ext.mkProd [] = Lean.Macro.throwUnsupported
• Cvc.Ext.mkProd [t] = pure t

def Cvc.Ext.ruleAlts (rule : Lean.Syntax) : Array Lean.Syntax

The alternatives of one smt.grammar! rule, none when it only declares its non-terminal.

Equations

• Cvc.Ext.ruleAlts rule = if rule[3].isNone = true then #[] else rule[3][1].getSepArgs

def Cvc.Ext.expandGrammar (layer : Layer) (body : Lean.Syntax) (withParts : Bool := false) : Lean.MacroM (Lean.TSyntax `term)

Expands the body of a smt.grammar! or smt.mkGrammar! for the given layer.

With withParts, the result carries what the grammar was built from as well as the grammar, so that it can be extended afterwards: grammar × NT₁ × NT₂ × … without parameters, and (grammar × PARAM₁ × …) × NT₁ × NT₂ × … with some, the grouping keeping the two apart.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Ext.letGrammarPattern (g : Lean.Ident) (body : Lean.Syntax) : Lean.MacroM (Lean.TSyntax `term)

The pattern smt.letGrammar! g ← … binds: g, the parameters and the non-terminals.

They are grouped as smt.mkGrammar! answers them, and named as the block declares them.

Equations

• One or more equations did not get rendered due to their size.