Syntax-guided synthesis, typed

Declare the universally quantified variables (declareSygusVar) and the functions to find (synthFun), constrain them (addSygusConstraint), then checkSynth, whose ifSolved branch can read a solution with getSynthSolution. A Grammar σ carries its parameters, so synthFun takes only the grammar and answers a Term σ; synthAnyFun takes the signature instead.

@[reducible, inline]

abbrev Cvc.Typed.SynthResult : Type

The outcome of a synthesis check.

Equations

• Cvc.Typed.SynthResult = Cvc.Untyped.SynthResult

@[reducible, inline]

abbrev Cvc.Typed.Solver.EnvSolvedT [Ω] (s : Solver) (m : Type → Type) (α : Type) : Type

Code running where the solver last found a synthesis solution.

Equations

• s.EnvSolvedT = Cvc.Untyped.Solver.EnvSolvedT s

@[reducible, inline]

abbrev Cvc.Typed.Solver.EnvSolved [Ω] (s : Solver) (α : Type) : Type

Code running where the solver last found a synthesis solution.

Equations

• s.EnvSolved = Cvc.Untyped.Solver.EnvSolved s

@[reducible, inline]

abbrev Cvc.Typed.Solver.EnvUnsolvableT [Ω] (s : Solver) (m : Type → Type) (α : Type) : Type

Code running where the solver last showed the synthesis conjecture has no solution.

Equations

• s.EnvUnsolvableT = Cvc.Untyped.Solver.EnvUnsolvableT s

@[reducible, inline]

abbrev Cvc.Typed.Solver.EnvUnsolvable [Ω] (s : Solver) (α : Type) : Type

Code running where the solver last showed the synthesis conjecture has no solution.

Equations

• s.EnvUnsolvable = Cvc.Untyped.Solver.EnvUnsolvable s

@[reducible, inline]

abbrev Cvc.Typed.Solver.EnvSynthUnknownT [Ω] (s : Solver) (m : Type → Type) (α : Type) : Type

Code running where the solver last gave up on a synthesis conjecture.

Equations

• s.EnvSynthUnknownT = Cvc.Untyped.Solver.EnvSynthUnknownT s

@[reducible, inline]

abbrev Cvc.Typed.Solver.EnvSynthUnknown [Ω] (s : Solver) (α : Type) : Type

Code running where the solver last gave up on a synthesis conjecture.

Equations

• s.EnvSynthUnknown = Cvc.Untyped.Solver.EnvSynthUnknown s

def Cvc.Typed.Solver.declareSygusVar [Ω] (s : Solver) (α : Type) [ToTyp α] (symbol : String) : Env (Term α)

Declares a universally quantified variable of the sort α describes.

Takes its type explicitly, like Solver.declareConstAs.

Equations

• s.declareSygusVar α symbol = do let __do_lift ← Cvc.Srt.of α Cvc.Untyped.Solver.declareSygusVar s symbol __do_lift

def Cvc.Typed.Solver.synthFun [Ω] (s : Solver) {σ : Type} (symbol : String) (g : Grammar σ) : Env (Term σ)

Declares a function to synthesize, restricted to what g generates, at g's signature.

Equations

• s.synthFun symbol g = Cvc.Untyped.Solver.synthFun s symbol g.erase.boundVars g.erase.startSrt (some g.erase)

def Cvc.Typed.Solver.synthAnyFun' [Ω] (s : Solver) (symbol : String) (boundVars : BVars) (α : Type) [ToTyp α] : Env (Term (BVars.signatureTo α boundVars))

Declares a function to synthesize, unrestricted, over boundVars and with codomain α.

Equations

• s.synthAnyFun' symbol boundVars α = do let __do_lift ← Cvc.Srt.of α Cvc.Untyped.Solver.synthFun s symbol boundVars.erase __do_lift

@[reducible, inline]

abbrev Cvc.Typed.Solver.synthAnyFun [Ω] (s : Solver) {α : Type} [ToTyp α] (symbol : String) (boundVars : BVars) : Env (Term (BVars.signatureTo α boundVars))

Declares a function to synthesize, unrestricted, over boundVars and with codomain α.

Equations

• s.synthAnyFun symbol boundVars = s.synthAnyFun' symbol boundVars α

def Cvc.Typed.Solver.addSygusConstraint [Ω] (s : Solver) (t : Term Bool) : Env Unit

Adds a formula the synthesized functions must satisfy.

Equations

• s.addSygusConstraint t = Cvc.Untyped.Solver.addSygusConstraint s t

def Cvc.Typed.Solver.getSygusConstraints [Ω] (s : Solver) : Env (Terms Bool)

The formulas added by addSygusConstraint.

Equations

• s.getSygusConstraints = Cvc.Untyped.Solver.getSygusConstraints s

def Cvc.Typed.Solver.addSygusAssume [Ω] (s : Solver) (t : Term Bool) : Env Unit

Adds a formula the synthesized functions may assume.

Equations

• s.addSygusAssume t = Cvc.Untyped.Solver.addSygusAssume s t

def Cvc.Typed.Solver.getSygusAssumptions [Ω] (s : Solver) : Env (Terms Bool)

The formulas added by addSygusAssume.

Equations

• s.getSygusAssumptions = Cvc.Untyped.Solver.getSygusAssumptions s

def Cvc.Typed.Solver.addSygusInvConstraint [Ω] (s : Solver) {α β γ δ : Type} (inv : Term α) (pre : Term β) (trans : Term γ) (post : Term δ) : Env Unit

Constrains inv to be an inductive invariant of the transition system.

pre must imply inv, inv must be preserved by trans, and inv must imply post. inv, pre and post are predicates over a state, trans one over two states; cvc5 checks that their signatures agree.

Equations

• s.addSygusInvConstraint inv pre trans post = Cvc.Untyped.Solver.addSygusInvConstraint s inv pre trans post

def Cvc.Typed.Solver.checkSynthResult [Ω] (s : Solver) : Env SynthResult

Tries to solve the synthesis conjecture, as a raw result.

Equations

• s.checkSynthResult = Cvc.Untyped.Solver.checkSynthResult s

def Cvc.Typed.Solver.checkSynthNextResult [Ω] (s : Solver) : Env SynthResult

Tries to find another solution, as a raw result.

Equations

• s.checkSynthNextResult = Cvc.Untyped.Solver.checkSynthNextResult s

def Cvc.Typed.Solver.checkSynth {m : Type → Type} [Ω] [Monad m] [MonadLiftT BaseIO m] (s : Solver) {α : Type} (ifSolved : s.EnvSolvedT m α := liftM (Untyped.Solver.unexpectedSolved s false)) (ifUnsolvable : s.EnvUnsolvableT m α := liftM (Untyped.Solver.unexpectedUnsolvable s false)) (ifUnknown : s.EnvSynthUnknownT m α := liftM (Untyped.Solver.unexpectedSynthUnknown s false)) : EnvT m α

Tries to solve the synthesis conjecture, and runs the branch for the answer.

ifSolved runs in s.EnvSolved, where getSynthSolution is available. An omitted branch throws if its answer comes up.

Equations

• s.checkSynth ifSolved ifUnsolvable ifUnknown = Cvc.Untyped.Solver.checkSynth s ifSolved ifUnsolvable ifUnknown

def Cvc.Typed.Solver.checkSynthNext {m : Type → Type} [Ω] [Monad m] [MonadLiftT BaseIO m] (s : Solver) {α : Type} (ifSolved : s.EnvSolvedT m α := liftM (Untyped.Solver.unexpectedSolved s false)) (ifUnsolvable : s.EnvUnsolvableT m α := liftM (Untyped.Solver.unexpectedUnsolvable s false)) (ifUnknown : s.EnvSynthUnknownT m α := liftM (Untyped.Solver.unexpectedSynthUnknown s false)) : s.EnvSolvedT m α

Tries to find another solution to the synthesis conjecture, with checkSynth's branches.

Only possible where a solution was already found.

Equations

• s.checkSynthNext ifSolved ifUnsolvable ifUnknown = Cvc.Untyped.Solver.checkSynthNext s ifSolved ifUnsolvable ifUnknown

def Cvc.Typed.Solver.checkSynth? {m : Type → Type} [Ω] [Monad m] [MonadLiftT BaseIO m] {α : Type} (s : Solver) (ifSolved : s.EnvSolvedT m (Option α) := pure none) (ifUnsolvable : s.EnvUnsolvableT m (Option α) := pure none) (ifUnknown : s.EnvSynthUnknownT m (Option α) := liftM (Untyped.Solver.unexpectedSynthUnknown s false)) : EnvT m (Option α)

checkSynth, whose solved and unsolvable branches default to none.

An unknown answer still fails, as with checkSat?.

Equations

• s.checkSynth? ifSolved ifUnsolvable ifUnknown = Cvc.Untyped.Solver.checkSynth? s ifSolved ifUnsolvable ifUnknown

def Cvc.Typed.Solver.getSynthSolution [Ω] (s : Solver) {σ : Type} (fn : Term σ) : s.EnvSolved (Term σ)

The solution found for a synthesized function.

A solution has the signature of the function it solves for, so the index carries across.

Equations

• s.getSynthSolution fn = Cvc.Untyped.Solver.getSynthSolution s fn

def Cvc.Typed.Solver.getSynthSolutions [Ω] (s : Solver) {σ : Type} (fns : Terms σ) : s.EnvSolved (Terms σ)

The solution found for a synthesized function.

A solution has the signature of the function it solves for, so the index carries across.

Equations

• s.getSynthSolutions fns = Cvc.Untyped.Solver.getSynthSolutions s fns

def Cvc.Typed.Solver.findSynth [Ω] (s : Solver) {σ : Type} (target : Synth.FindTarget) (g : Grammar σ) : Env (Option (Term σ))

Enumerates a term of interest, rather than solving a conjecture, none if cvc5 finds none.

The grammar says what may be enumerated, and its start sort is what comes back.

Equations

• s.findSynth target g = Cvc.Untyped.Solver.findSynth s target (some g.erase)

def Cvc.Typed.Solver.findSynth! [Ω] (s : Solver) {σ : Type} (target : Synth.FindTarget) (g : Grammar σ) : Env (Term σ)

findSynth, failing rather than answering none.

Equations

• s.findSynth! target g = Cvc.Untyped.Solver.findSynth! s target (some g.erase)

def Cvc.Typed.Solver.findAnySynth [Ω] (s : Solver) (target : Synth.FindTarget) : Env (Option Untyped.Term)

Enumerates a term of interest with no grammar to restrict it, none if cvc5 finds none.

Sort-erased, nothing saying what sort the answer has; Untyped.Term.typeCheck puts an index on.

Equations

• s.findAnySynth target = Cvc.Untyped.Solver.findSynth s target

def Cvc.Typed.Solver.findAnySynth! [Ω] (s : Solver) (target : Synth.FindTarget) : Env Untyped.Term

findAnySynth, failing rather than answering none.

Equations

• s.findAnySynth! target = Cvc.Untyped.Solver.findSynth! s target

def Cvc.Typed.Solver.findSynthNext [Ω] (s : Solver) : Env (Option Untyped.Term)

Enumerates the next term of interest, none if cvc5 finds none.

Sort-erased, like findAnySynth.

Equations

• s.findSynthNext = Cvc.Untyped.Solver.findSynthNext s

def Cvc.Typed.Solver.findSynthNext! [Ω] (s : Solver) : Env Untyped.Term

findSynthNext, failing rather than answering none.

Equations

• s.findSynthNext! = Cvc.Untyped.Solver.findSynthNext! s

def Cvc.Typed.Symbols.Sig.Idents.declareSygusIn {S : Sig} [Ω] [Symbols S] (solver : Solver) (idents : S.Idents) : Env S.Terms

Declares some identifiers as sygus-variables in solver.

Equations

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

def Cvc.Typed.Symbols.Sig.Idents.declareSygusAtIn {S : Sig} [Ω] [Symbols S] (k : Nat) (solver : Solver) (idents : S.Idents) : Env (S.TermsAt k)

Declares some identifiers as sygus-variables in solver, named for step k.

Equations

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