Syntax-guided synthesis, sort-erased

Where checkSat asks whether constraints can be satisfied, checkSynth asks for a function that satisfies them for every input. The shape of that function is what a Grammar restricts.

The pieces fit together in one order: set the sygus option (s.setOption "sygus" "true"), declare the universally quantified variables with declareSygusVar, declare the functions to synthesize with synthFun, constrain them with addSygusConstraint, then checkSynth and read each function back with getSynthSolution. findSynth is the other entry point — it enumerates terms of interest rather than solving a conjecture.

Synthesis-mode monadic environments

A synthesis check splits the world in three, as a check-sat does: a solution can be read only where one was found. As for the sat monads, only checkSynth enters these, and each is indexed by the solver that answered, so a solution cannot be read off another solver.

structure Cvc.Untyped.Solver.EnvSolvedT [Ω] (solver : Solver) (m : Type → Type) (α : Type) : Type

Code running where the solver last found a synthesis solution.

• wrap :: (
• toEnv : Cvc.EnvT m α
• )

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSolvedT.instMonad [Ω] {m✝ : Type → Type} {s✝ : Solver} [Monad m✝] : Monad (s✝.EnvSolvedT m✝)

Equations

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

@[reducible, inline]

abbrev Cvc.Untyped.Solver.EnvSolved [Ω] : Solver → (α : Type) → Type

Code running where the solver last found a synthesis solution.

Equations

• s✝.EnvSolved = s✝.EnvSolvedT BaseIO

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSolvedT.instMonadExceptError [Ω] {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : MonadExcept Error (s✝.EnvSolvedT m✝)

Equations

• Cvc.Untyped.Solver.EnvSolvedT.instMonadExceptError = { throw := fun {α : Type} => Cvc.Untyped.Solver.EnvSolvedT.throw, tryCatch := fun {α : Type} => Cvc.Untyped.Solver.EnvSolvedT.tryCatch }

def Cvc.Untyped.Solver.EnvSolvedT.throw [Ω] {α✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : Error → s✝.EnvSolvedT m✝ α✝

Fails with e.

Equations

• Cvc.Untyped.Solver.EnvSolvedT.throw e✝ = { toEnv := throw e✝ }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSolvedT.instMonadLiftEnvSolvedOfMonadOfMonadLiftTBaseIO [Ω] {m✝ : Type → Type} {s✝ : Solver} [Monad m✝] [MonadLiftT BaseIO m✝] : MonadLift s✝.EnvSolved (s✝.EnvSolvedT m✝)

Equations

• Cvc.Untyped.Solver.EnvSolvedT.instMonadLiftEnvSolvedOfMonadOfMonadLiftTBaseIO = { monadLift := fun {α : Type} => Cvc.Untyped.Solver.EnvSolvedT.liftMonadVersion✝ }

def Cvc.Untyped.Solver.EnvSolvedT.pure [Ω] {α✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : α✝ → s✝.EnvSolvedT m✝ α✝

Returns a.

Equations

• Cvc.Untyped.Solver.EnvSolvedT.pure a✝ = { toEnv := pure a✝ }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSolvedT.instMonadLiftIOOfMonadLiftTBaseIO [Ω] {m✝ : Type → Type} {s✝ : Solver} [MonadLiftT BaseIO m✝] : MonadLift IO (s✝.EnvSolvedT m✝)

Equations

• Cvc.Untyped.Solver.EnvSolvedT.instMonadLiftIOOfMonadLiftTBaseIO = { monadLift := fun {α : Type} => Cvc.Untyped.Solver.EnvSolvedT.liftIO✝ }

def Cvc.Untyped.Solver.EnvSolvedT.bind [Ω] {α✝ β✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : s✝.EnvSolvedT m✝ α✝ → (α✝ → s✝.EnvSolvedT m✝ β✝) → s✝.EnvSolvedT m✝ β✝

Runs a, then f on its result.

Equations

• a✝.bind f✝ = { toEnv := (Cvc.Untyped.Solver.EnvSolvedT.toEnv✝ a✝).bind fun (a : α✝) => Cvc.Untyped.Solver.EnvSolvedT.toEnv✝ (f✝ a) }

def Cvc.Untyped.Solver.EnvSolvedT.tryCatch [Ω] {α✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : s✝.EnvSolvedT m✝ α✝ → (Error → s✝.EnvSolvedT m✝ α✝) → s✝.EnvSolvedT m✝ α✝

Runs code, handing any error it fails with to errorDo.

Equations

• code✝.tryCatch errorDo✝ = { toEnv := (Cvc.Untyped.Solver.EnvSolvedT.toEnv✝ code✝).tryCatch fun (e : Cvc.Error) => Cvc.Untyped.Solver.EnvSolvedT.toEnv✝ (errorDo✝ e) }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSolvedT.instMonadLift [Ω] {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : MonadLift m✝ (s✝.EnvSolvedT m✝)

Equations

• Cvc.Untyped.Solver.EnvSolvedT.instMonadLift = { monadLift := fun {α : Type} => Cvc.Untyped.Solver.EnvSolvedT.transformLift✝ }

structure Cvc.Untyped.Solver.EnvUnsolvableT [Ω] (solver : Solver) (m : Type → Type) (α : Type) : Type

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

• wrap :: (
• toEnv : Cvc.EnvT m α
• )

def Cvc.Untyped.Solver.EnvUnsolvableT.pure [Ω] {α✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : α✝ → s✝.EnvUnsolvableT m✝ α✝

Returns a.

Equations

• Cvc.Untyped.Solver.EnvUnsolvableT.pure a✝ = { toEnv := pure a✝ }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvUnsolvableT.instMonadLiftEnvUnsolvableOfMonadOfMonadLiftTBaseIO [Ω] {m✝ : Type → Type} {s✝ : Solver} [Monad m✝] [MonadLiftT BaseIO m✝] : MonadLift s✝.EnvUnsolvable (s✝.EnvUnsolvableT m✝)

Equations

• Cvc.Untyped.Solver.EnvUnsolvableT.instMonadLiftEnvUnsolvableOfMonadOfMonadLiftTBaseIO = { monadLift := fun {α : Type} => Cvc.Untyped.Solver.EnvUnsolvableT.liftMonadVersion✝ }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvUnsolvableT.instMonadLift [Ω] {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : MonadLift m✝ (s✝.EnvUnsolvableT m✝)

Equations

• Cvc.Untyped.Solver.EnvUnsolvableT.instMonadLift = { monadLift := fun {α : Type} => Cvc.Untyped.Solver.EnvUnsolvableT.transformLift✝ }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvUnsolvableT.instMonadExceptError [Ω] {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : MonadExcept Error (s✝.EnvUnsolvableT m✝)

Equations

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

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvUnsolvableT.instMonad [Ω] {m✝ : Type → Type} {s✝ : Solver} [Monad m✝] : Monad (s✝.EnvUnsolvableT m✝)

Equations

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

def Cvc.Untyped.Solver.EnvUnsolvableT.tryCatch [Ω] {α✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : s✝.EnvUnsolvableT m✝ α✝ → (Error → s✝.EnvUnsolvableT m✝ α✝) → s✝.EnvUnsolvableT m✝ α✝

Runs code, handing any error it fails with to errorDo.

Equations

• code✝.tryCatch errorDo✝ = { toEnv := (Cvc.Untyped.Solver.EnvUnsolvableT.toEnv✝ code✝).tryCatch fun (e : Cvc.Error) => Cvc.Untyped.Solver.EnvUnsolvableT.toEnv✝ (errorDo✝ e) }

def Cvc.Untyped.Solver.EnvUnsolvableT.throw [Ω] {α✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : Error → s✝.EnvUnsolvableT m✝ α✝

Fails with e.

Equations

• Cvc.Untyped.Solver.EnvUnsolvableT.throw e✝ = { toEnv := throw e✝ }

def Cvc.Untyped.Solver.EnvUnsolvableT.bind [Ω] {α✝ β✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : s✝.EnvUnsolvableT m✝ α✝ → (α✝ → s✝.EnvUnsolvableT m✝ β✝) → s✝.EnvUnsolvableT m✝ β✝

Runs a, then f on its result.

Equations

• a✝.bind f✝ = { toEnv := (Cvc.Untyped.Solver.EnvUnsolvableT.toEnv✝ a✝).bind fun (a : α✝) => Cvc.Untyped.Solver.EnvUnsolvableT.toEnv✝ (f✝ a) }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvUnsolvableT.instMonadLiftIOOfMonadLiftTBaseIO [Ω] {m✝ : Type → Type} {s✝ : Solver} [MonadLiftT BaseIO m✝] : MonadLift IO (s✝.EnvUnsolvableT m✝)

Equations

• Cvc.Untyped.Solver.EnvUnsolvableT.instMonadLiftIOOfMonadLiftTBaseIO = { monadLift := fun {α : Type} => Cvc.Untyped.Solver.EnvUnsolvableT.liftIO✝ }

@[reducible, inline]

abbrev Cvc.Untyped.Solver.EnvUnsolvable [Ω] : Solver → (α : Type) → Type

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

Equations

• s✝.EnvUnsolvable = s✝.EnvUnsolvableT BaseIO

structure Cvc.Untyped.Solver.EnvSynthUnknownT [Ω] (solver : Solver) (m : Type → Type) (α : Type) : Type

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

• wrap :: (
• toEnv : Cvc.EnvT m α
• )

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSynthUnknownT.instMonadLift [Ω] {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : MonadLift m✝ (s✝.EnvSynthUnknownT m✝)

Equations

• Cvc.Untyped.Solver.EnvSynthUnknownT.instMonadLift = { monadLift := fun {α : Type} => Cvc.Untyped.Solver.EnvSynthUnknownT.transformLift✝ }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSynthUnknownT.instMonad [Ω] {m✝ : Type → Type} {s✝ : Solver} [Monad m✝] : Monad (s✝.EnvSynthUnknownT m✝)

Equations

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

def Cvc.Untyped.Solver.EnvSynthUnknownT.bind [Ω] {α✝ β✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : s✝.EnvSynthUnknownT m✝ α✝ → (α✝ → s✝.EnvSynthUnknownT m✝ β✝) → s✝.EnvSynthUnknownT m✝ β✝

Runs a, then f on its result.

Equations

• a✝.bind f✝ = { toEnv := (Cvc.Untyped.Solver.EnvSynthUnknownT.toEnv✝ a✝).bind fun (a : α✝) => Cvc.Untyped.Solver.EnvSynthUnknownT.toEnv✝ (f✝ a) }

@[reducible, inline]

abbrev Cvc.Untyped.Solver.EnvSynthUnknown [Ω] : Solver → (α : Type) → Type

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

Equations

• s✝.EnvSynthUnknown = s✝.EnvSynthUnknownT BaseIO

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSynthUnknownT.instMonadExceptError [Ω] {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : MonadExcept Error (s✝.EnvSynthUnknownT m✝)

Equations

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

def Cvc.Untyped.Solver.EnvSynthUnknownT.tryCatch [Ω] {α✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : s✝.EnvSynthUnknownT m✝ α✝ → (Error → s✝.EnvSynthUnknownT m✝ α✝) → s✝.EnvSynthUnknownT m✝ α✝

Runs code, handing any error it fails with to errorDo.

Equations

• code✝.tryCatch errorDo✝ = { toEnv := (Cvc.Untyped.Solver.EnvSynthUnknownT.toEnv✝ code✝).tryCatch fun (e : Cvc.Error) => Cvc.Untyped.Solver.EnvSynthUnknownT.toEnv✝ (errorDo✝ e) }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSynthUnknownT.instMonadLiftEnvSynthUnknownOfMonadOfMonadLiftTBaseIO [Ω] {m✝ : Type → Type} {s✝ : Solver} [Monad m✝] [MonadLiftT BaseIO m✝] : MonadLift s✝.EnvSynthUnknown (s✝.EnvSynthUnknownT m✝)

Equations

• Cvc.Untyped.Solver.EnvSynthUnknownT.instMonadLiftEnvSynthUnknownOfMonadOfMonadLiftTBaseIO = { monadLift := fun {α : Type} => Cvc.Untyped.Solver.EnvSynthUnknownT.liftMonadVersion✝ }

def Cvc.Untyped.Solver.EnvSynthUnknownT.throw [Ω] {α✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : Error → s✝.EnvSynthUnknownT m✝ α✝

Fails with e.

Equations

• Cvc.Untyped.Solver.EnvSynthUnknownT.throw e✝ = { toEnv := throw e✝ }

def Cvc.Untyped.Solver.EnvSynthUnknownT.pure [Ω] {α✝ : Type} {m✝ : Type → Type} [Monad m✝] {s✝ : Solver} : α✝ → s✝.EnvSynthUnknownT m✝ α✝

Returns a.

Equations

• Cvc.Untyped.Solver.EnvSynthUnknownT.pure a✝ = { toEnv := pure a✝ }

@[instance_reducible]

instance Cvc.Untyped.Solver.EnvSynthUnknownT.instMonadLiftIOOfMonadLiftTBaseIO [Ω] {m✝ : Type → Type} {s✝ : Solver} [MonadLiftT BaseIO m✝] : MonadLift IO (s✝.EnvSynthUnknownT m✝)

Equations

• Cvc.Untyped.Solver.EnvSynthUnknownT.instMonadLiftIOOfMonadLiftTBaseIO = { monadLift := fun {α : Type} => Cvc.Untyped.Solver.EnvSynthUnknownT.liftIO✝ }

What a synthesis check answered

def Cvc.Untyped.SynthResult : Type

The outcome of a synthesis check.

Equations

• Cvc.Untyped.SynthResult = cvc5.SynthResult

def Cvc.Untyped.SynthResult.toString (r : SynthResult) : String

A string representation of this synthesis result.

Equations

• r.toString = (Cvc.Untyped.SynthResult.toUnsafe✝ r).toString

@[instance_reducible]

instance Cvc.Untyped.SynthResult.instToString : ToString SynthResult

Equations

• Cvc.Untyped.SynthResult.instToString = { toString := Cvc.Untyped.SynthResult.toString }

def Cvc.Untyped.SynthResult.hasSolution (r : SynthResult) : Bool

True if the synthesis query has a solution.

Equations

• r.hasSolution = (Cvc.Untyped.SynthResult.toUnsafe✝ r).hasSolution

def Cvc.Untyped.SynthResult.hasNoSolution (r : SynthResult) : Bool

True if the synthesis query has no solution. In this case, it was determined that there was no solution.

Equations

• r.hasNoSolution = (Cvc.Untyped.SynthResult.toUnsafe✝ r).hasNoSolution

def Cvc.Untyped.SynthResult.isUnknown (r : SynthResult) : Bool

True if the result of the synthesis query could not be determined.

Equations

• r.isUnknown = (Cvc.Untyped.SynthResult.toUnsafe✝ r).isUnknown

def Cvc.Untyped.SynthResult.isSolved? (r : SynthResult) : Res (Option Bool)

Whether a solution was found, or none if the solver could not tell.

The three-way answer of Result.isSat?, at synthesis: some true if a solution exists and was found, some false if the conjecture has none, none if the solver gave up.

Equations

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

def Cvc.Untyped.SynthResult.isSolved (r : SynthResult) : Res Bool

Whether a solution was found, failing if the solver gave up.

Equations

• r.isSolved = do let x ← r.isSolved? match x with | some solved => pure solved | none => Cvc.throwUser "unexpected unknown synthesis result"

Driving synthesis

def Cvc.Untyped.Solver.declareSygusVar [Ω] (s : Solver) (symbol : String) (srt : Srt) : Env Term

Declares a universally quantified variable of the given sort.

Equations

• s.declareSygusVar symbol srt = Cvc.runUnsafe'✝ ((Cvc.Untyped.Solver.toUnsafe✝ s).declareSygusVar symbol (Cvc.Srt.toUnsafe✝ srt))

def Cvc.Untyped.Solver.synthFun [Ω] (s : Solver) (symbol : String) (boundVars : BVars) (srt : Srt) (grammar : Option Grammar := none) : Env Term

Declares a function to synthesize.

boundVars are the function's parameters and srt its codomain. A grammar restricts the shape of the candidates; without one, any term of the right sort is allowed. The grammar must have been built over these very parameters.

Equations

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

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

Adds a formula the synthesized functions must satisfy.

Equations

• s.addSygusConstraint t = Cvc.runUnsafe'✝ ((Cvc.Untyped.Solver.toUnsafe✝ s).addSygusConstraint t)

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

The constraints added so far.

Equations

• s.getSygusConstraints = Cvc.runUnsafe'✝ (Cvc.Untyped.Solver.toUnsafe✝ s).getSygusConstraints

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

Adds a formula the synthesized functions may assume.

Equations

• s.addSygusAssume t = Cvc.runUnsafe'✝ ((Cvc.Untyped.Solver.toUnsafe✝ s).addSygusAssume t)

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

The assumptions added so far.

Equations

• s.getSygusAssumptions = Cvc.runUnsafe'✝ (Cvc.Untyped.Solver.toUnsafe✝ s).getSygusAssumptions

def Cvc.Untyped.Solver.addSygusInvConstraint [Ω] (s : Solver) (inv pre trans 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.

Equations

• s.addSygusInvConstraint inv pre trans post = Cvc.runUnsafe'✝ ((Cvc.Untyped.Solver.toUnsafe✝ s).addSygusInvConstraint inv pre trans post)

Rejecting an unexpected answer

What a synthesis branch falls back on when the caller did not expect that answer.

def Cvc.Untyped.Solver.unexpectedSolved [Ω] (s : Solver) (dumpConstraints : Bool := false) {α : Type} : s.EnvSolved α

Fails because a solution was unexpected.

Equations

• s.unexpectedSolved dumpConstraints = liftM (Cvc.Untyped.Solver.unexpectedSynth✝ s "solved" dumpConstraints)

def Cvc.Untyped.Solver.unexpectedUnsolvable [Ω] (s : Solver) (dumpConstraints : Bool := false) {α : Type} : s.EnvUnsolvable α

Fails because having no solution was unexpected.

Equations

• s.unexpectedUnsolvable dumpConstraints = liftM (Cvc.Untyped.Solver.unexpectedSynth✝ s "unsolvable" dumpConstraints)

def Cvc.Untyped.Solver.unexpectedSynthUnknown [Ω] (s : Solver) (dumpConstraints : Bool := false) {α : Type} : s.EnvSynthUnknown α

Fails because the solver giving up was unexpected.

Equations

• s.unexpectedSynthUnknown dumpConstraints = liftM (Cvc.Untyped.Solver.unexpectedSynth✝ s "unknown" dumpConstraints)

Checking a synthesis conjecture

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

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

Equations

• s.checkSynthResult = Cvc.Untyped.SynthResult.ofUnsafe✝ <$> Cvc.runUnsafe'✝ (Cvc.Untyped.Solver.toUnsafe✝ s).checkSynth

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

Tries to find another solution, as a raw result.

Equations

• s.checkSynthNextResult = Cvc.Untyped.SynthResult.ofUnsafe✝ <$> Cvc.runUnsafe'✝ (Cvc.Untyped.Solver.toUnsafe✝ s).checkSynthNext

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

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

A branch left out fails if its answer comes; getSynthSolution is available in ifSolved.

Equations

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

def Cvc.Untyped.Solver.checkSynthNext {m : Type → Type} [Ω] [Monad m] [MonadLiftT BaseIO m] (s : Solver) {α : Type} (ifSolved : s.EnvSolvedT m α := liftM (s.unexpectedSolved false)) (ifUnsolvable : s.EnvUnsolvableT m α := liftM (s.unexpectedUnsolvable false)) (ifUnknown : s.EnvSynthUnknownT m α := liftM (s.unexpectedSynthUnknown 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

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

def Cvc.Untyped.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 (s.unexpectedSynthUnknown 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 = s.checkSynth ifSolved ifUnsolvable ifUnknown

Where a solution was found

def Cvc.Untyped.Solver.getSynthSolution [Ω] (s : Solver) (fn : Term) : s.EnvSolved Term

The solution found for fn, a function synthFun declared.

Equations

• s.getSynthSolution fn = liftM (Cvc.runUnsafe'✝ ((Cvc.Untyped.Solver.toUnsafe✝ s).getSynthSolution fn))

def Cvc.Untyped.Solver.getSynthSolutions [Ω] (s : Solver) (fns : Terms) : s.EnvSolved Terms

The solution found for fn, a function synthFun declared.

Equations

• s.getSynthSolutions fns = liftM (Cvc.runUnsafe'✝ ((Cvc.Untyped.Solver.toUnsafe✝ s).getSynthSolutions fns))

def Cvc.Untyped.Solver.findSynth [Ω] (s : Solver) (target : Synth.FindTarget) (grammar : Option Grammar := none) : Env (Option Term)

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

A grammar restricts what may be enumerated; without one, the last synthFun's grammar is used, and cvc5 refuses if it had none.

Equations

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

def Cvc.Untyped.Solver.findSynth! [Ω] (s : Solver) (target : Synth.FindTarget) (grammar : Option Grammar := none) : Env Term

findSynth, failing rather than answering none.

Equations

• s.findSynth! target grammar = s.findSynth target grammar >>= Cvc.someOrThrowUser "cvc5 found no term of interest"

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

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

Continues the enumeration the last findSynth or findSynthNext started.

Equations

• s.findSynthNext = Cvc.runUnsafe'✝ do let t ← (Cvc.Untyped.Solver.toUnsafe✝ s).findSynthNext pure (if t.isNull = true then none else some t)

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

findSynthNext, failing rather than answering none.

Equations

• s.findSynthNext! = s.findSynthNext >>= Cvc.someOrThrowUser "cvc5 found no further term of interest"

def Cvc.Untyped.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.Untyped.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.