Cedar.SymCC.Decoder

This file functions for parsing SMT models produced by CVC5, and turning them into Interpretations, which can then be used to construct concrete counterexamples for property violations (i.e., Cedar requests and entities).

The included parser recognizes the subset of SMTLib syntax that can appear in a model of a formula emitted by SymCC.Encoder.

source

@[reducible, inline]

abbrev Cedar.SymCC.Decoder.Result (α : Type u_1) :

Type u_1

Equations

Cedar.SymCC.Decoder.Result α = Except String α

Instances For

source

@[irreducible]

def Cedar.SymCC.Decoder.defaultLit (eidOf : Spec.EntityType → String) :

TermType → Term

Equations

One or more equations did not get rendered due to their size.
Cedar.SymCC.Decoder.defaultLit eidOf (Cedar.SymCC.TermType.prim pty) = Cedar.SymCC.Term.prim (Cedar.SymCC.Decoder.defaultPrim✝ eidOf pty)
Cedar.SymCC.Decoder.defaultLit eidOf ty.option = Cedar.SymCC.Term.none ty
Cedar.SymCC.Decoder.defaultLit eidOf ty.set = Cedar.SymCC.Term.set Cedar.Data.Set.empty ty

Instances For

source

def Cedar.SymCC.Decoder.defaultUDF (eidOf : Spec.EntityType → String) (f : UUF) :

UDF

Equations

Cedar.SymCC.Decoder.defaultUDF eidOf f = { arg := f.arg, out := f.out, table := Cedar.Data.Map.empty, default := Cedar.SymCC.Decoder.defaultLit eidOf f.out }

Instances For

source

def Cedar.SymCC.Decoder.eidOfForEntities (εs : SymEntities) (ety : Spec.EntityType) :

String

Equations

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

Instances For

source

def Cedar.SymCC.Decoder.defaultInterpretation (εs : SymEntities) :

Interpretation

Equations

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

Instances For

source

def Cedar.SymCC.Decoder.decode (model : String) (enc : EncoderState) :

Result Interpretation

Returns an Interpretation that corresponds to the given model, generated by CVC5 for a formula emitted by the encoder. This function assumes the EncoderSate enc is produced by the encoder when applied to a set of terms ts and the environment εnv. If εnv is well-formed, the terms ts are well-formed with respect to εnv.entities, and CVC5 is sound, the the resulting Interpretation satisfies ts and is well-formed with respect to εnv.entities.

Equations

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

Instances For