Documentation

Cedar.SymCC.Interpretation

Interpretations #

An Interpretation is a structure that binds term variables to literal terms and uninterpreted functions (UUF) to interpreted ones (UDF). In practice, Interpretations are obtained from low-level models returned by SMT solvers.

When a symbolic structure (such as a term, request, function, or entities) is interpreted with respect to an Interpretation, the result is a literal symbolic structure.

source
structure Cedar.SymCC.Interpretation :
Type

An Interpretation consists of three maps:

  • vars maps variables to literal terms of the same type;
  • funs maps uninterpreted functions to intepreted functions; and
  • partials maps partial application terms to literals of the right type.

A partial application term represents the application of an operator to a correctly typed literal outside of the operator's domain---for example, the application of option.get to a .none term. The SMTLib language treats all such operators as total, and it picks an arbitrary value of the right type as the result of the application.

Instances For
    source
    def Cedar.SymCC.UnaryFunction.interpret (I : Interpretation) :
    UnaryFunction → UnaryFunction
    Equations
    Instances For
      source
      def Cedar.SymCC.Factory.option.get' (I : Interpretation) (t : Term) :
      Term
      Equations
      Instances For
        source
        def Cedar.SymCC.Factory.ext.ipaddr.addrV4' (I : Interpretation) (t : Term) :
        Term
        Equations
        Instances For
          source
          def Cedar.SymCC.Factory.ext.ipaddr.prefixV4' (I : Interpretation) (t : Term) :
          Term
          Equations
          Instances For
            source
            def Cedar.SymCC.Factory.ext.ipaddr.addrV6' (I : Interpretation) (t : Term) :
            Term
            Equations
            Instances For
              source
              def Cedar.SymCC.Factory.ext.ipaddr.prefixV6' (I : Interpretation) (t : Term) :
              Term
              Equations
              Instances For
                source
                @[irreducible]
                def Cedar.SymCC.Term.interpret (I : Interpretation) :
                Term → Term
                Equations
                Instances For
                  source
                  def Cedar.SymCC.SymRequest.interpret (I : Interpretation) (req : SymRequest) :
                  SymRequest
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Cedar.SymCC.SymTags.interpret (I : Interpretation) (τags : SymTags) :
                    SymTags
                    Equations
                    Instances For
                      source
                      def Cedar.SymCC.SymEntityData.interpret (I : Interpretation) (d : SymEntityData) :
                      SymEntityData
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Cedar.SymCC.SymEntities.interpret (I : Interpretation) (es : SymEntities) :
                        SymEntities
                        Equations
                        Instances For
                          source
                          def Cedar.SymCC.SymEnv.interpret (I : Interpretation) (env : SymEnv) :
                          SymEnv
                          Equations
                          Instances For