semantics-analysis-tr.maude

load semantics-basics/smt-conversion.maude
load semantics-basics/semantics-basics-narrowing.maude

*** Test transformer with while language module
***load language-semantics/while-semantics-concrete.maude
***set trace on .

*** Create views for SMT types
view Integer from TRIV to REAL-INTEGER is
  sort Elt to Integer .
endv
view Real from TRIV to REAL-INTEGER is
  sort Elt to Real .
endv
view Boolean from TRIV to REAL-INTEGER is
  sort Elt to Boolean .
endv

fmod PAIRSVAR is
    sorts PairSVar PairSVarL NePairSVarL .
    subsort PairSVar < NePairSVarL < PairSVarL .

    *** Definition of a list of symbolic variable-value pairs
    op nil : -> PairSVarL [ctor] .
    op __ : PairSVarL PairSVarL -> PairSVarL [ctor assoc id: nil prec 25] .
endfm

fmod SMT-CONNECTION is
    pr SMT-CONVERSION .
    pr PAIRSVAR .

    *** Import stores as map structures that map variables to SMT types
    protecting MAP{Qid, Integer} * (sort Map{Qid, Integer} to IStoreS) * (op _|->_ to _|->Is_ ) .
    protecting MAP{Qid, Real}    * (sort Map{Qid, Real} to RStoreS)    * (op _|->_ to _|->Rs_ ) .
    protecting MAP{Qid, Boolean} * (sort Map{Qid, Boolean} to BStoreS) * (op _|->_ to _|->Bs_ ) .

    sort AssignmentSMT .

    *** Define an satisfying assignment returned by the SMT hook
    op _<--_ : Real Real                 -> AssignmentSMT [ctor] .
    op _<--_ : Integer Integer           -> AssignmentSMT [ctor] .
    op _<--_ : Boolean Boolean           -> AssignmentSMT [ctor] .
    op _,_ : AssignmentSMT AssignmentSMT -> AssignmentSMT .
    op failed :                          -> AssignmentSMT [ctor] .

    *** Operator defined in Python using a hook
    *** Given a Boolean constraint returns a satisfying assignment to the symbolic variables it may contain
    op get-SMTassignment : Boolean -> AssignmentSMT [special (id-hook SpecialHubSymbol)] .

    *** Symbolic variable initialization pair
    op _,_ : Qid Integer -> PairSVar [ctor] .
    op _,_ : Qid Real    -> PairSVar [ctor] .
    op _,_ : Qid Boolean -> PairSVar [ctor] .
endfm

fmod NARROWING-BASICS is
    protecting INT-FVP * (
        sort Bool to BoolFVP,
        sort Int to IntFVP,
        sort Nat to NatFVP,
        sort NzNat to NzNatFVP,
        op true to tt,
        op false to ff
      ) .
endfm

*** Create views for FVP types
view IntFVP from TRIV to NARROWING-BASICS is
  sort Elt to IntFVP .
endv
view BoolFVP from TRIV to NARROWING-BASICS is
  sort Elt to BoolFVP .
endv

fmod NARROWING-CONVERSION is
    pr NARROWING-BASICS .
    pr META-LEVEL .
    pr LEXICAL .
    pr CONVERSION .

    op toIntFVP : Int -> IntFVP .
    op toBoolFVP : Bool -> BoolFVP .
    op errIntFVP : -> IntFVP [ctor] .

    var I      : Int .
    var MConst : Constant .

    eq toIntFVP(0) = (0).IntFVP .
    eq toIntFVP(1) = (1).IntFVP .
    eq toIntFVP(I) = toIntFVP(I + (- 1)) + (1).IntFVP [owise] .
    ***eq toIntFVP(I) = downTerm(getTerm(metaParse(['NARROWING-BASICS], tokenize(string(I, 10)), 'IntFVP)), errIntFVP) .
    eq toBoolFVP(true) = tt .
    eq toBoolFVP(false) = ff .

    op trBool : Constant -> Constant .
    eq trBool('true.Bool) = 'tt.BoolFVP .
    eq trBool('false.Bool) = 'ff.BoolFVP .
    eq trBool(MConst) = MConst [owise] .
endfm

fmod NARROWING-FMOD is
    
    pr NARROWING-CONVERSION .
    pr PAIRSVAR .
    *** Import stores as map structures that map variables to FVP types
    protecting MAP{Qid, IntFVP}  * (sort Map{Qid, IntFVP}  to IStoreN) * (op _|->_ to _|->In_ ) .
    protecting MAP{Qid, BoolFVP} * (sort Map{Qid, BoolFVP} to BStoreN) * (op _|->_ to _|->Bn_ ) .

    *** Narrowing variable initialization pair
    op _,_ : Qid IntFVP  -> PairSVar [ctor] .
    op _,_ : Qid BoolFVP -> PairSVar [ctor] .
endfm

fmod SMT-AND-NARROWING is
    pr SMT-CONNECTION .
    pr NARROWING-FMOD .
endfm

fmod MODULE-TRANSFORMER is
    pr STRING-OPS .
    pr SMT-AND-NARROWING .

    sorts TrType NonNrw .
    subsort NonNrw < TrType .
    
    *** Define the transformation types
    ops symb conc maudeSE : -> NonNrw [ctor] . ***clconc
    op narrowing : -> TrType [ctor] .

    vars InstId StateOp PrOp OpId ModId Q ValOp X Y EvalQ : Qid .
    vars Trm T1 T2 Tcond Tmod TSTR TIL                    : Term .
    vars Cond Cond1 Cond2                                 : Condition .
    vars EqC EqC2                                         : EqCondition .
    var  AttrSet                                          : AttrSet .
    var  RlSet                                            : RuleSet .
    var  Rule                                             : Rule .
    var  ImportList                                       : ImportList .
    var  SortSet                                          : SortSet .
    var  OpDeclSet                                        : OpDeclSet .
    var  OpDecl                                           : OpDecl .
    var  EquationSet                                      : EquationSet .
    var  TrId                                             : TrType .
    var  NonNrwTrId                                       : NonNrw .
    var  Eq                                               : Equation .
    var  M                                                : Module .
    var  FM                                               : FModule .
    var  TL                                               : TypeList .
    var  NeTypeL                                          : NeTypeList .
    var  T                                                : Type .
    var  Import                                           : Import .
    var  TermL                                            : TermList .
    var  NeTL NeTL'                                       : NeTermList .
    var  MVar                                             : Variable .
    var  MConst                                           : Constant .
    var  N                                                : Nat .
    var  Str                                              : String .
    
    *** Program variable generic definition
    op prVar : Qid -> Variable .
    eq prVar(PrOp) = qid("Pr:" + string(PrOp)) .

    *** State variable generic definition
    op stateVar : Qid -> Variable .
    eq stateVar(StateOp) = qid("State:" + string(StateOp)) .
    op stateVar : Qid Nat -> Variable .
    eq stateVar(StateOp, N) = qid("State" + string(N, 10) + ":" + string(StateOp)) .
    op stateVar : Qid String -> Variable .
    eq stateVar(StateOp, Str) = qid("State" + Str + ":" + string(StateOp)) .

    *** Symbolic state generic definition
    op symbState : Qid -> Term .
    eq symbState(StateOp) = '_`{_`}[stateVar(StateOp), 'Constraints:Boolean] .
    op symbState : Qid Nat -> Term .
    eq symbState(StateOp, N) = '_`{_`}[stateVar(StateOp, N), 'Constraints:Boolean] .

    *** FIXME: a comment in the code explaining the meaning of each slot would be valuable?
    *** Concolic state generic definition
    op concolicState : Qid -> Term .
    eq concolicState(StateOp) = '`[_`]`[_`]`[_`][stateVar(StateOp, 0), symbState(StateOp, 1), stateVar(StateOp, "SInit")] .
    op concolicState : Qid Term -> Term .
    eq concolicState(StateOp, T1) = '`[_`]`[_`]`[_`][T1, symbState(StateOp, 1), stateVar(StateOp, "SInit")] .

    *** Construct a symbolic mirror of a given a term. Transform all its Maude variables to use SMT types and stores, and change their name
    op symbMirror : Term Qid -> Term .
    eq symbMirror(T1, ValOp) = modOpStoreRec(T1, ValOp, symb) .
    
    *** Construct a symbolic mirror of a given a term. Transform all its Maude variables to use SMT types and stores, and change their name
    ***op symbMirror : Term Qid RlSide -> Term .
    ***eq symbMirror(T1, ValOp, RlSide) = modVal(modOpStoreRec(T1, symb), ValOp, RlSide) .
    ***op nrwMirror : Term Qid RlSide -> Term .
    ***eq nrwMirror(T1, ValOp, RlSide) = modVal(modOpStoreRec(T1, narrowing), ValOp, RlSide) .

    *** Transform teh rules for a pure symbolic analysis without MaudeSE. For now, rule conditions must be of the form: eval(B, STR) = true
    *** The function symbMirror creates a symbolic mirror of the concrete state
    *** Conditional rules accumulate the condition of the rule in the state Constraints
    *** Every time a conditional rule is to be executed, the satisfiability of the new accumulated Constraints is checked
    op rlToSymbolic : RuleSet Qid ~> RuleSet .
    eq rlToSymbolic(none, ValOp) = none .
    eq rlToSymbolic(rl T1 => T2 [label(InstId) AttrSet] . RlSet, ValOp) = 
          rl '_`{_`}[symbMirror(T1, ValOp), 'Constraints:Boolean]
            => '_`{_`}[symbMirror(T2, ValOp), 'Constraints:Boolean] 
            [label(toSymb(InstId)) AttrSet] .
          rlToSymbolic(RlSet, ValOp) .
    ceq rlToSymbolic(crl T1 => T2 if Cond [label(InstId) AttrSet] . RlSet, ValOp) = 
          crl '_`{_`}[symbMirror(T1, ValOp), 'Constraints:Boolean]
            => '_`{_`}[symbMirror(T2, ValOp), 'Constraints':Boolean]
            if 'Constraints':Boolean := '_and_['Constraints:Boolean, Tcond]
            /\ 'metaCheck[upTerm(upModule('REAL-INTEGER, false)), 'upTerm['Constraints':Boolean]] = 'true.Bool 
            [label(toSymb(InstId)) AttrSet] .
          rlToSymbolic(RlSet, ValOp)
      if (Tcond = 'true.Boolean) := modCondRl(Cond, ValOp, symb)  .
    eq rlToSymbolic(crl T1 => T2 if Cond [label(InstId) AttrSet] . RlSet, ValOp) = 
          crl '_`{_`}[symbMirror(T1, ValOp), 'Constraints:Boolean]
            => '_`{_`}[symbMirror(T2, ValOp), 'Constraints:Boolean]
            if Cond
            [label(toSymb(InstId)) AttrSet] .
          rlToSymbolic(RlSet, ValOp) [owise] .

    *** Transform the rules for a concolic analysis. For now, rule conditions must be of the form: eval(B, STR) = true
    *** The symbolic state advances naturally following the concrete state, executing the same instructions.
    *** The function symbMirror ensures the symbolic state is of the same form as the concrete state at each step, but using symbolic functions and stores
    op rlToConcolic : RuleSet Qid Qid -> RuleSet .
    eq rlToConcolic(none, ValOp, StateOp) = none .
    *** Transform unconditional rules
    eq rlToConcolic(rl T1 => T2 [AttrSet] . RlSet, ValOp, StateOp) =
          (rl '`[_`]`[_`]`[_`][T1, '_`{_`}[symbMirror(T1, ValOp), 'Constraints:Boolean], stateVar(StateOp)]
            =>
            '`[_`]`[_`]`[_`][T2, '_`{_`}[symbMirror(T2, ValOp), 'Constraints:Boolean], stateVar(StateOp)]
            [AttrSet] .)
          rlToConcolic(RlSet, ValOp, StateOp) .
    *** Transform conditional rules to two concolic rules
    *** - Conditional rule 1: Advances the state with the concrete condition Cond and appends Cond to the accumulated Constraints
    *** - Conditional rule 2: Appends not(Cond) to the accumulated Constraints and, if Constraints is satisfiable, re-starts the execution with the new Constraints
    ***                       Re-executing requires re-initializing the concrete store with new satisfying values retrieved from the SMT hook, and resetting the symbolic store

    ceq rlToConcolic(crl T1 => T2 if Cond [label(InstId) AttrSet] . RlSet, ValOp, StateOp) =
          (crl '`[_`]`[_`]`[_`][T1, '_`{_`}[symbMirror(T1, ValOp), 'Constraints:Boolean], stateVar(StateOp)]
            =>
            '`[_`]`[_`]`[_`][T2, '_`{_`}[symbMirror(T2, ValOp), 'Constraints':Boolean], stateVar(StateOp)]
            if Cond
            /\ 'Constraints':Boolean := '_and_['Constraints:Boolean, searchSubVarConst(Tcond, conc)]
            [label(InstId) AttrSet] .)
          (crl '`[_`]`[_`]`[_`][T1, '_`{_`}[symbMirror(T1, ValOp), 'Constraints:Boolean], stateVar(StateOp)]
            =>
            '`[_`]`[_`]`[_`]['updateStore[stateVar(StateOp), 'init-CStore['getStore[stateVar(StateOp)], 'Constraints':Boolean]],
                                '_`{_`}[stateVar(StateOp), 'Constraints':Boolean],
                                stateVar(StateOp)]
            if Cond
            /\ 'Constraints':Boolean := '_and_['Constraints:Boolean, 'not_[searchSubVarConst(Tcond, conc)]]
            /\ 'metaCheck[upTerm(upModule('REAL-INTEGER, false)), 'upTerm['Constraints':Boolean]] = 'true.Bool
            [label(qid(string(InstId) + "-bis")) AttrSet] .)
          rlToConcolic(RlSet, ValOp, StateOp)
        if (Tcond = 'true.Bool) := Cond
        /\ hasEval(Tcond) .
    
    eq rlToConcolic(crl T1 => T2 if Cond [AttrSet] . RlSet, ValOp, StateOp) = 
          (crl '`[_`]`[_`]`[_`][T1, '_`{_`}[symbMirror(T1, ValOp), 'Constraints:Boolean], stateVar(StateOp)]
            =>
            '`[_`]`[_`]`[_`][T2, '_`{_`}[symbMirror(T2, ValOp), 'Constraints:Boolean], stateVar(StateOp)]
            if Cond
            [AttrSet] .)
          rlToConcolic(RlSet, ValOp, StateOp) [owise] .
    ***eq rlToConcolic(Rule RlSet, StateOp) = Rule rlToConcolic(RlSet, StateOp) [owise] .

    *** Transform the rules for an analysis with MaudeSE or narrowing
    *** - Transform the terms and conditions to use symbolic/FVP eval functions and symbolic/FVP stores
    op rlToSE : RuleSet Qid TrType -> RuleSet .
    eq rlToSE(none, ValOp, TrId) = none .
    eq rlToSE(rl T1 => T2 [label(InstId) AttrSet] . RlSet, ValOp, TrId) = (rl modOpStoreRec(T1, ValOp, TrId) => modOpStoreRec(T2, ValOp, TrId) 
                                                                      [label(toSymb(InstId)) AttrSet] .)
                                                                    rlToSE(RlSet, ValOp, TrId) .
    eq rlToSE(crl T1 => T2 if Cond [label(InstId) AttrSet] . RlSet, ValOp, TrId) = (crl modOpStoreRec(T1, ValOp, TrId) => modOpStoreRec(T2, ValOp, TrId) 
                                                                              if modCondRl(Cond, ValOp, TrId) 
                                                                              [label(toSymb(InstId)) AttrSet] .)
                                                                            rlToSE(RlSet, ValOp, TrId) .
    eq rlToSE(Rule RlSet, ValOp, TrId) = Rule rlToSE(RlSet, ValOp, TrId) [owise] .

    op rlToNarrowing : RuleSet Qid -> RuleSet .
    eq rlToNarrowing(none, ValOp) = none .
    eq rlToNarrowing(rl T1 => T2 [AttrSet] . RlSet, ValOp) = rlToSE(rl T1 => T2 [AttrSet narrowing] ., ValOp, narrowing) rlToNarrowing(RlSet, ValOp) .
    eq rlToNarrowing(crl T1 => T2 if ('eval[NeTL:NeTermList] = 'true.Bool) [label(InstId) AttrSet] . RlSet, ValOp) =
                      (rl modOpStoreRec(T1, ValOp, narrowing) => extNrwSt(modOpStoreRec(T1, ValOp, narrowing), modOpStoreRec('eval[NeTL:NeTermList], ValOp, narrowing)) [narrowing AttrSet] .)
                      (rl extNrwSt(modOpStoreRec(T1, ValOp, narrowing), trBool('true.Bool)) => modOpStoreRec(T2, ValOp, narrowing) [label(toSymb(InstId)) narrowing AttrSet] .)
                    rlToNarrowing(RlSet, ValOp) .
    eq rlToNarrowing(crl T1 => T2 if ('eval[NeTL:NeTermList] = 'false.Bool) [label(InstId) AttrSet] . RlSet, ValOp) =
                      (rl modOpStoreRec(T1, ValOp, narrowing) => extNrwSt(modOpStoreRec(T1, ValOp, narrowing), modOpStoreRec('eval[NeTL:NeTermList], ValOp, narrowing)) [narrowing AttrSet] .)
                      (rl extNrwSt(modOpStoreRec(T1, ValOp, narrowing), trBool('false.Bool)) => modOpStoreRec(T2, ValOp, narrowing) [label(toSymb(InstId)) narrowing AttrSet] .)
                    rlToNarrowing(RlSet, ValOp) .
    eq rlToNarrowing(crl T1 => T2 if 'not_['eval[NeTL:NeTermList]] = 'true.Bool [AttrSet] . RlSet, ValOp) = rlToNarrowing(crl T1 => T2 if ('eval[NeTL:NeTermList] = 'false.Bool) [AttrSet] . RlSet, ValOp) .
    eq rlToNarrowing(Rule RlSet, ValOp) = Rule rlToNarrowing(RlSet, ValOp) [owise] .

    ***op rlToClConcolic : RuleSet Qid -> RuleSet .
    ***eq rlToClConcolic(none, StateOp) = none .
    ***eq rlToClConcolic(rl T1 => T2 [AttrSet] . RlSet, StateOp) = rlToConcolic(rl T1 => T2 [AttrSet] . RlSet, StateOp)
    ***                                                               rlToClConcolic(RlSet, StateOp) .
    ***ceq rlToClConcolic(crl T1 => T2 if Cond [label(InstId) AttrSet] . RlSet, StateOp) = (crl '`[_`]`[_`]`[_`]`[_`][T1, '_`{_`}[stateVar(StateOp), 'Constraints:Boolean], 'STRInit:Stores]
    ***                                                                                      =>
    ***                                                                                      '`[_`]`[_`]`[_`]`[_`][T2, '_`{_`}[stateVar(StateOp), 'Constraints':Boolean], 'STRInit:Stores]
    ***                                                                                      if 'Constraints':Boolean := '_and_['Constraints:Boolean, subT(Tcond, 'STR:Stores, 'getStore[stateVar(StateOp)])]
    ***                                                                                      /\ 'metaCheck[upTerm(upModule('REAL-INTEGER, false)), 'upTerm[Tcond]] = 'true.Bool
    ***                                                                                      [label(InstId) AttrSet] .)
    ***                                                                                      rlToConcolic(RlSet, StateOp)
    ***    if (Tcond = 'true.Boolean) := Cond .
    
    ***op inclClConcCrl : Qid -> RuleSet .
    ***eq inclClConcCrl(StateOp) = (crl '`[_`]`[_`]`[_`]`[_`][T1, '_`{_`}[stateVar(StateOp), 'Constraints:Boolean], 'STRInit:Stores]
    ***                                =>
    ***                                '`[_`]`[_`]`[_`]`[_`][subT('updateProgram[T2, 'getProgram[stateVar(StateOp)]], 'STR:Stores, 'init-CStore['STRInit:Stores, 'Constraints':Boolean]),
    ***                                                            '_`{_`}['updateStore[stateVar(StateOp), 'STRInit:Stores], 'Constraints':Boolean], '_+_['N:Nat, 's_['0.Nat]], 'STRInit:Stores]
    ***                                if 'metaCheck[upTerm(upModule('REAL-INTEGER, false)), 'upTerm['Constraints:Boolean]] = 'true.Bool
    ***                                [label(qid("re-exec")) AttrSet] .)

    ***op modSEImports : ImportList -> ImportList .
    ***eq modSEImports(ImportList) = ImportList .
    ***eq modSEImports(nil) = nil .
    ***eq modSEImports((protecting 'MAP{X, Y} .) ImportList) = (protecting 'MAP{X, Y} .) 
    ***                                                        (protecting 'MAP{X, toSMTSorts(Y)} .) 
    ***                                                        modSEImports(ImportList) .
    ***eq modSEImports(Import ImportList) = Import modSEImports(ImportList) [owise] .

    ***op inclSEImports : ImportList -> ImportList .
    ***eq inclSEImports(ImportList) = ImportList . ***modSEImports(ImportList)
                                   ***(protecting 'MAP{'Var, 'Integer} * (sort 'Map`{'Var`,'Integer`} to 'IStoreS) * (op '_|->_ to '_|->Is_ [ctor]) .)
                                   ***(protecting 'MAP{'Var, 'Real} * (sort 'Map`{'Var`,'Real`} to 'RStoreS) * (op '_|->_ to '_|->Rs_ [ctor]) .)
                                   ***(protecting 'MAP{'Var, 'Boolean} * (sort 'Map`{'Var`,'Boolean`} to 'BStoreS) * (op '_|->_ to '_|->Bs_ [ctor]) .)
                                   ***(protecting 'REAL-INTEGER .)
                                   ***(protecting 'META-LEVEL .)
                                   ***(protecting 'SMT-CONNECTION .)
                                   ***(protecting 'SE-LOCS-MOD .)
                                   ***(protecting 'LIST{'Location} * (sort 'List`{Location`} to 'Path) .)
                                   ***(protecting 'LIST{'PairVarValue} .)
                                   ***(protecting 'LIST{'Inst} * (sort 'List`{Inst`} to 'Program) .)

    *** Include new sorts for symbolic/concolic execution states
    op inclSESorts : SortSet -> SortSet .
    eq inclSESorts(SortSet) = SortSet ; 'SEState ; 'ConstrainedStart ; 'ConcolicState .

    op trSorts : TypeList TrType -> TypeList .
    eq trSorts(TL, narrowing) = toNRWSorts(TL) .
    eq trSorts(TL, TrId) = toSMTSorts(TL) [owise] .

    *** Transform a list of Maude types to their symbolic representation
    op toSMTSorts : TypeList -> TypeList .
    eq toSMTSorts(nil)        = nil .
    eq toSMTSorts('Bool TL)   = 'Boolean toSMTSorts(TL) .
    eq toSMTSorts('Int TL)    = 'Integer toSMTSorts(TL) .
    eq toSMTSorts('Rat TL)    = 'Real toSMTSorts(TL) .
    eq toSMTSorts('Zero TL)   = 'Integer toSMTSorts(TL) .
    eq toSMTSorts('IStore TL) = 'IStoreS toSMTSorts(TL) .
    eq toSMTSorts('RStore TL) = 'RStoreS toSMTSorts(TL) .
    eq toSMTSorts('BStore TL) = 'BStoreS toSMTSorts(TL) .
    eq toSMTSorts(T TL) = T toSMTSorts(TL) [owise] .

    *** TODO: Maybe fuse with toSMTSorts and dissambiguate with TypeTr annotation at the level
    *** Transform a list of Maude types to their narrowing representation
    op toNRWSorts : TypeList -> TypeList .
    eq toNRWSorts(nil)        = nil .
    eq toNRWSorts('Bool TL)   = 'BoolFVP toNRWSorts(TL) .
    eq toNRWSorts('Int TL)    = 'IntFVP toNRWSorts(TL) .
    eq toNRWSorts('Zero TL)   = 'IntFVP toNRWSorts(TL) .
    eq toNRWSorts('IStore TL) = 'IStoreN toNRWSorts(TL) .
    eq toNRWSorts('BStore TL) = 'BStoreN toNRWSorts(TL) .
    eq toNRWSorts(T TL) = T toNRWSorts(TL) [owise] .

    *** Append an "S" to an input Qid to represent its symbolic representation
    op toSymb : Qid -> Qid .
    eq toSymb(OpId) = qid(string(OpId) + "S") .

    *** Extend states using the modified state constructor for narrowing.
    *** If the term is a constant or a variable, leave it as is
    op extNrwSt : Qid -> Qid .
    op extNrwSt : Term Term -> Term .
    eq extNrwSt(Q) = qid(string(Q) + "[_]") .
    eq extNrwSt(OpId[NeTL], T2) = extNrwSt(OpId)[NeTL, T2] .
    eq extNrwSt(T1, T2) = T1 [owise] .

    *** Transform an operator signature to use SMT types
    op trOps : OpDecl TrType -> OpDecl .
    eq trOps((op Q : TL -> T [AttrSet] .), TrId) = (op Q : trSorts(TL, TrId) -> trSorts(T, TrId) [AttrSet] .) .

    *** The transformation for symbolic execution transforms the eval functions and the semantic value wrapper to use SMT types and changes the function names
    op modOpSigSE : OpDeclSet Qid Qid TrType -> OpDeclSet .
    eq modOpSigSE(none, StateOp, ValOp, TrId) = none .
    *** NOTE: ValOp represents a wrapper for a semantically-relevant value, not syntax 'val
    eq modOpSigSE((op Q : NeTypeL -> StateOp [ctor AttrSet] .) OpDeclSet, StateOp, ValOp, narrowing) = (op Q : NeTypeL -> StateOp [ctor AttrSet] .)
                                                                                                        (op extNrwSt(Q) : NeTypeL 'BoolFVP -> StateOp [ctor AttrSet] .)
                                                                                                        modOpSigSE(OpDeclSet, StateOp, ValOp, narrowing) . 
    eq modOpSigSE((op ValOp : TL -> T [AttrSet] .) OpDeclSet, StateOp, ValOp, TrId)   = trOps(op ValOp : TL -> T [AttrSet] ., TrId)
                                                                                modOpSigSE(OpDeclSet, StateOp, ValOp, TrId) . 
    eq modOpSigSE((op 'eval : TL -> T [AttrSet] .) OpDeclSet, StateOp, ValOp, TrId)   = trOps(op toSymb('eval) : TL -> T [AttrSet] ., TrId)
                                                                                modOpSigSE(OpDeclSet, StateOp, ValOp, TrId) . 
    eq modOpSigSE((op 'evalI : TL -> T [AttrSet] .) OpDeclSet, StateOp, ValOp, TrId)  = trOps(op toSymb('evalI) : TL -> T [AttrSet] ., TrId)
                                                                                modOpSigSE(OpDeclSet, StateOp, ValOp, TrId) . 
    eq modOpSigSE((op 'evalR : TL -> T [AttrSet] .) OpDeclSet, StateOp, ValOp, TrId)  = trOps(op toSymb('evalR) : TL -> T [AttrSet] ., TrId)
                                                                                modOpSigSE(OpDeclSet, StateOp, ValOp, TrId) . 
    eq modOpSigSE((op 'evalB : TL -> T [AttrSet] .) OpDeclSet, StateOp, ValOp, TrId)  = trOps(op toSymb('evalB) : TL -> T [AttrSet] ., TrId)
                                                                                modOpSigSE(OpDeclSet, StateOp, ValOp, TrId) .
    eq modOpSigSE(OpDecl OpDeclSet, StateOp, ValOp, TrId) = OpDecl modOpSigSE(OpDeclSet, StateOp, ValOp, TrId) [owise] .

    *** The transformation for concolic execution duplicates the operator declarations and 
    *** transforms one of the copies to use symbolic evaluation functions and symbolic semantic value wrapper (using the symbolic execution transformation)
    op modOpSigConc : OpDeclSet Qid Qid TrType -> OpDeclSet .
    eq modOpSigConc(OpDeclSet, StateOp, ValOp, TrId) = OpDeclSet modOpSigSE(OpDeclSet, StateOp, ValOp, TrId) .

    *** Include constructors symbolic/concolic state constructors depending on original state and functional operators
    op inclSEOps : Qid -> OpDeclSet .
    eq inclSEOps(StateOp) = *** Constructor for symbolic state, appends the accumulated constraints to the original state 
                            (op '_`{_`} : StateOp 'Boolean -> 'SEState [ctor] .)
                            *** Define state with initial constraints
                            (op '_where_ : StateOp 'Boolean -> 'ConstrainedStart [ctor] .)
                            *** Define the concolic dual state core constructor and its extension to keep track of initial programs
                            (op '`[_`]`[_`]`[_`] : StateOp 'SEState StateOp -> 'ConcolicState [ctor] .)
                            *** TODO: This should not "contain" a State, it should "extend" it (at the same term level)
                            ***   - Do it at modOp level
                            *** (op '_`[_`] : StateOp 'BoolFVP -> StateOp [ctor] .)                            
                            *** Construct the symbolic Stores structure with the three symbolic stores
                            (op '_|_|_ : 'IStoreS 'RStoreS 'BStoreS -> 'Stores [ctor] .)
                            (op '_|_ : 'IStoreS 'BStoreS -> 'Stores [ctor] .)
                            *** Construct the FVP-typed store Stores structure for narrowing
                            (op '_|_ : 'IStoreN 'BStoreN -> 'Stores [ctor] .)
                            *** Initialize the input concrete stores with the symbolic stores and
                            *** values satisfying Boolean constrains retrieved from the SMT hook 
                            (op 'init-CStore : 'Stores 'Boolean -> 'Stores [none] .)
                            (op 'init-CStore : 'Stores 'Stores 'Boolean -> 'Stores [none] .)
                            *** Only insert if var is not already assigned
                            (op 'insertFirst : 'Qid 'Int  'IStore -> 'IStore [none] .)
                            (op 'insertFirst : 'Qid 'Rat  'RStore -> 'RStore [none] .)
                            (op 'insertFirst : 'Qid 'Bool 'BStore -> 'BStore [none] .)
                            *** Apply a symbolic assignment retrieved from the SMT hook to a concrete store.
                            *** The symbolic store is used to match the assigned variable. 
                            (op '$apply-SMTassignment : 'Stores 'Stores 'AssignmentSMT -> 'Stores [none] .)
                            *** Initialize a concrete store with default values from a symbolic store
                            (op 'initialize-def : 'IStore 'IStoreS -> 'IStore [none] .)
                            (op 'initialize-def : 'RStore 'RStoreS -> 'RStore [none] .)
                            (op 'initialize-def : 'BStore 'BStoreS -> 'BStore [none] .)
                            ***(op 'size : 'Boolean -> 'Nat [none] .)
                            *** Create a concolic dual state with the concrete and symbolic state objects, and the symbolic variable-value pairs
                            (op 'startC : StateOp 'PairSVarL -> 'ConcolicState [none] .)
                            *** Create a concolic dual state with initial constraints
                            (op 'startC : 'ConstrainedStart 'PairSVarL -> 'ConcolicState [none] .)
                            *** Initialize the concolic state
                            (op '$startC : StateOp 'PairSVarL 'Stores 'Boolean -> 'ConcolicState [none] .)
                            *** Create a symbolic state for MaudeSE or narrowing execution
                            (op 'startSE : StateOp 'PairSVarL 'Stores -> StateOp [none] .) .

    *** Transform operator declarations depending on the transformation type
    op modSEOps : OpDeclSet Qid Qid TrType -> OpDeclSet .
    eq modSEOps(OpDeclSet, StateOp, ValOp, conc) = modOpSigConc(OpDeclSet, StateOp, ValOp, conc)
                                                   inclSEOps(StateOp) .
    *** NOTE: modified to keep concrete definitions when added narrowing to maintain old unchanged definitions
    eq modSEOps(OpDeclSet, StateOp, ValOp, TrId) = modOpSigConc(OpDeclSet, StateOp, ValOp, TrId)
                                                   inclSEOps(StateOp) [owise] .

    *** Transform operator ids to their symbolic representation
    op modSEOpIds : Qid -> Qid .
    eq modSEOpIds('_==_)  = '_===_ .
    eq modSEOpIds('_=/=_) = '_=/==_ . 
    eq modSEOpIds('_quo_) = '_div_ . 
    eq modSEOpIds('rat)   = 'toReal . 
    eq modSEOpIds('eval)  = toSymb('eval) .
    eq modSEOpIds('evalI) = toSymb('evalI) .
    eq modSEOpIds('evalR) = toSymb('evalR) .
    eq modSEOpIds('evalB) = toSymb('evalB) .
    eq modSEOpIds(Q) = Q [owise] .

    *** Transform a variable to use SMT type and use a new symbolic name
    *** TODO: Generalize variable name change on structures that may contain semantic values (stack, stores, etc.) e.g. (STR LocalSTRList) could be NeLocalSTRList
    op subSEVarSorts : Variable Type TrType -> Variable .
    eq subSEVarSorts(MVar, 'Stores, TrId) = qid(string(toSymb(getName(MVar))) + ":" + string('Stores)) .
    eq subSEVarSorts(MVar, 'IStore, TrId) = qid(string(toSymb(getName(MVar))) + ":" + string(trSorts('IStore, TrId))) .
    eq subSEVarSorts(MVar, 'RStore, TrId) = qid(string(toSymb(getName(MVar))) + ":" + string(trSorts('RStore, TrId))) .
    eq subSEVarSorts(MVar, 'BStore, TrId) = qid(string(toSymb(getName(MVar))) + ":" + string(trSorts('BStore, TrId))) .
    eq subSEVarSorts(MVar, 'Int, TrId) = qid(string(getName(MVar)) + ":" + string(trSorts('Int, TrId))) .
    eq subSEVarSorts(MVar, 'Zero, TrId) = qid(string(getName(MVar)) + ":" + string(trSorts('Int, TrId))) .
    eq subSEVarSorts(MVar, 'Rat, TrId) = qid(string(getName(MVar)) + ":" + string(trSorts('Rat, TrId))) .
    eq subSEVarSorts(MVar, 'Bool, TrId) = qid(string(getName(MVar)) + ":" + string(trSorts('Bool, TrId))) .
    eq subSEVarSorts(MVar, T, TrId) = MVar [owise] .

    *** Transform a variable to use SMT type
    ***op subSEVarSorts : Variable -> Variable .
    ***eq subSEVarSorts(MVar) = qid(string(getName(MVar)) + ":" + string(toSMTSorts(getType(MVar)))) .

    *** Transform a constant's type to SMT
    op subSEConstSortsT : Constant Type TrType -> Constant .
    eq subSEConstSortsT(MConst, 'Stores, TrId) = qid(string(toSymb(getName(MConst))) + "." + string('Stores)) .
    eq subSEConstSortsT(MConst, 'IStore, TrId) = qid(string(toSymb(getName(MConst))) + "." + string(trSorts('IStore, TrId))) .
    eq subSEConstSortsT(MConst, 'RStore, TrId) = qid(string(toSymb(getName(MConst))) + "." + string(trSorts('RStore, TrId))) .
    eq subSEConstSortsT(MConst, 'BStore, TrId) = qid(string(toSymb(getName(MConst))) + "." + string(trSorts('BStore, TrId))) .
    eq subSEConstSortsT(MConst, 'Int, TrId) = qid(string(getName(MConst)) + "." + string(trSorts('Int, TrId))) .
    eq subSEConstSortsT(MConst, 'Zero, TrId) = qid(string(getName(MConst)) + "." + string(trSorts('Int, TrId))) .
    eq subSEConstSortsT(MConst, 'Rat, TrId) = qid(string(getName(MConst)) + "." + string(trSorts('Rat, TrId))) .
    eq subSEConstSortsT(MConst, 'Bool, NonNrwTrId) = qid(string(getName(MConst)) + "." + string(trSorts('Bool, NonNrwTrId))) .
    eq subSEConstSortsT(MConst, 'Bool, narrowing) = trBool(MConst) .
    eq subSEConstSortsT(MConst, T, TrId) = MConst [owise] .
    ***eq subSEConstSortsT(MConst, TrId) = qid(string(getName(MConst)) + "." + string(trSorts(getType(MConst), TrId))) .

    *** Substitute all variables in a TermList with the corresponding term with SMT types
    ***op searchSubVar : TermList -> TermList .
    ***eq searchSubVar(empty)           = empty .
    ***eq searchSubVar(MConst)          = MConst .
    ***eq searchSubVar(MVar)            = subSEVarSorts(MVar, getType(MVar)) .
    ***eq searchSubVar(OpId[NeTL])      = modSEOpIds(OpId)[searchSubVar(NeTL)] .
    ***eq searchSubVar((T1, NeTL))      = searchSubVar(T1), searchSubVar(NeTL) .

    *** Substitute all variables and constants in a TermList with the corresponding term with SMT types
    op searchSubVarConst : TermList TrType -> TermList .
    eq searchSubVarConst(empty, TrId)           = empty .
    eq searchSubVarConst(MConst, TrId)          = subSEConstSortsT(MConst, getType(MConst), TrId) .
    eq searchSubVarConst(MVar, TrId)            = subSEVarSorts(MVar, getType(MVar), TrId) .
    eq searchSubVarConst('val[T1], TrId)        = 'val[T1] .
    eq searchSubVarConst('s_['0.Zero], TrId)    = '1.Integer .
    ceq searchSubVarConst(Q['0.Zero], TrId)     = qid(string(rat(substr(Str, 3, sd(length(Str), 3)), 10), 10) + ".Integer")
      if Str := string(Q)
      /\ substr(Str, 0, 3) = "s_^" .
    eq searchSubVarConst('_*_[NeTL], narrowing) = '_*_[NeTL] .
    eq searchSubVarConst('_/_[NeTL], narrowing) = '_/_[NeTL] .
    eq searchSubVarConst(OpId[NeTL], TrId)      = modSEOpIds(OpId)[searchSubVarConst(NeTL, TrId)] [owise] .
    eq searchSubVarConst((T1, NeTL), TrId)      = searchSubVarConst(T1, TrId), searchSubVarConst(NeTL, TrId) .

    op convert : Constant Type TrType -> Constant .
    eq convert(MConst, T, narrowing) = convertNarrowing(MConst, T) .
    eq convert(MConst, T, TrId) = convertSMT(MConst, T) [owise] .

    op convert : Variable Type TrType -> Variable .
    eq convert(MVar, T, narrowing) = convertNarrowing(MVar, T) .
    eq convert(MVar, T, TrId) = convertSMT(MVar, T) [owise] .

    *** Convert constant with Maude type to the corresponding SMT type
    op convertSMT : Constant Type -> Constant .
    eq convertSMT(MConst, 'Zero)  = 'toInteger[MConst] .
    eq convertSMT(MConst, 'Int)  = 'toInteger[MConst] .
    eq convertSMT(MConst, 'Rat)  = 'toReal[MConst] .
    eq convertSMT(MConst, 'Bool) = 'toBoolean[MConst] .
    eq convertSMT(MConst, T) = MConst [owise] .
    
    *** Convert variable with Maude type to the corresponding SMT type
    op convertSMT : Variable Type -> Variable .
    eq convertSMT(MVar, 'Zero)  = 'toInteger[MVar] .
    eq convertSMT(MVar, 'Int)  = 'toInteger[MVar] .
    eq convertSMT(MVar, 'Rat)  = 'toReal[MVar] .
    eq convertSMT(MVar, 'Bool) = 'toBoolean[MVar] .
    eq convertSMT(MVar, T) = MVar [owise] .

    op convertNarrowing : Constant Type -> Constant .
    eq convertNarrowing(MConst, 'Zero)  = 'toIntFVP[MConst] .
    eq convertNarrowing(MConst, 'Int)  = 'toIntFVP[MConst] .
    eq convertNarrowing(MConst, 'Bool) = 'toBoolFVP[MConst] .
    eq convertNarrowing(MConst, T) = MConst [owise] .

    op convertNarrowing : Variable Type -> Variable .
    eq convertNarrowing(MVar, 'Zero)  = 'toIntFVP[MVar] .
    eq convertNarrowing(MVar, 'Int)  = 'toIntFVP[MVar] .
    eq convertNarrowing(MVar, 'Bool) = 'toBoolFVP[MVar] .
    eq convertNarrowing(MVar, T) = MVar [owise] .

    *** Recursively transform terms to use symbolic stores and convert constants to SMT values
    ***op subSETermSTR : Term TrType -> Term .
    ***eq subSETermSTR(MConst, TrId)          = convert(MConst, getType(MConst), TrId) .
    ***eq subSETermSTR(MVar, TrId)            = subSEVarSorts(MVar, getType(MVar), TrId) .
    ***eq subSETermSTR('val[T1], TrId)        = 'val[T1] .
    ***eq subSETermSTR('s_['0.Zero], TrId)    = '1.Integer .
    ***ceq subSETermSTR(Q['0.Zero], TrId)     = qid(string(rat(substr(Str, 3, sd(length(Str), 3)), 10), 10) + ".Integer")
    ***  if Str := string(Q)
    ***  /\ substr(Str, 0, 3) = "s_^" .
    ***eq subSETermSTR('_*_[NeTL], narrowing) = '_*_[NeTL] .
    ***eq subSETermSTR(OpId[NeTL], TrId)      = modSEOpIds(OpId)[modOpStoreRec(NeTL, TrId)] [owise] .

    op modStoreT : Constant Type Qid TrType -> Term .
    op modStoreT : Variable Type Qid TrType -> Term .
    op modStoreT : Term Qid TrType -> Term .
    eq modStoreT(MConst, 'Stores, ValOp, TrId) = subSEConstSortsT(MConst, 'Stores, TrId) .
    eq modStoreT(MConst, 'IStore, ValOp, TrId) = subSEConstSortsT(MConst, 'IStore, TrId) .
    eq modStoreT(MConst, 'RStore, ValOp, TrId) = subSEConstSortsT(MConst, 'RStore, TrId) .
    eq modStoreT(MConst, 'BStore, ValOp, TrId) = subSEConstSortsT(MConst, 'BStore, TrId) .
    eq modStoreT(MConst, T, ValOp, TrId) = MConst [owise] .
    eq modStoreT(MVar, 'Stores, ValOp, TrId)   = subSEVarSorts(MVar, 'Stores, TrId) .
    eq modStoreT(MVar, 'IStore, ValOp, TrId)   = subSEVarSorts(MVar, 'IStore, TrId) .
    eq modStoreT(MVar, 'RStore, ValOp, TrId)   = subSEVarSorts(MVar, 'RStore, TrId) .
    eq modStoreT(MVar, 'BStore, ValOp, TrId)   = subSEVarSorts(MVar, 'BStore, TrId) .
    eq modStoreT(MVar, T, ValOp, TrId) = MVar [owise] .
    eq modStoreT(MConst, ValOp, TrId)                = modStoreT(MConst, getType(MConst), ValOp, TrId) .
    eq modStoreT(MVar, ValOp, TrId)                  = modStoreT(MVar, getType(MVar), ValOp, TrId) .
    eq modStoreT('_|->I_[T1, T2], ValOp, TrId)       = toSymb('_|->I_)[T1, searchSubVarConst(T2, TrId)] .
    eq modStoreT('_|->R_[T1, T2], ValOp, TrId)       = toSymb('_|->R_)[T1, searchSubVarConst(T2, TrId)] .
    eq modStoreT('_|->B_[T1, T2], ValOp, TrId)       = toSymb('_|->B_)[T1, searchSubVarConst(T2, TrId)] .
    eq modStoreT('_`,_[T1, T2], ValOp, TrId)         = '_`,_[modStoreT(T1, ValOp, TrId), modStoreT(T2, ValOp, TrId)] .
    eq modStoreT('insert[T1, MConst, TSTR], ValOp, TrId)     = 'insert[T1, convert(MConst, getType(MConst), TrId), modStoreT(TSTR, ValOp, TrId)] .
    eq modStoreT('insert[T1, MVar, TSTR], ValOp, TrId)       = 'insert[T1, convert(MVar, getType(MVar), TrId), modStoreT(TSTR, ValOp, TrId)] .
    eq modStoreT('_==_[T1, MConst], ValOp, TrId)             = modSEOpIds('_==_)[modStoreT(T1, ValOp, TrId), searchSubVarConst(MConst, TrId)] .
    eq modStoreT('_==_[T1, MVar], ValOp, TrId)               = modSEOpIds('_==_)[modStoreT(T1, ValOp, TrId), searchSubVarConst(MVar, TrId)] .
    eq modStoreT('_=/=_[T1, MConst], ValOp, TrId)            = modSEOpIds('_=/=_)[modStoreT(T1, ValOp, TrId), searchSubVarConst(MConst, TrId)] .
    eq modStoreT('_=/=_[T1, MVar], ValOp, TrId)              = modSEOpIds('_=/=_)[modStoreT(T1, ValOp, TrId), searchSubVarConst(MVar, TrId)] .
    eq modStoreT(ValOp[T1], ValOp, TrId)                  = ValOp[searchSubVarConst(T1, TrId)] .
    ***eq modStoreT(ValOp[MConst], ValOp, TrId)                 = ValOp[convert(MConst, getType(MConst), TrId)] .
    ***eq modStoreT(ValOp[MVar], ValOp, TrId)                   = ValOp[convert(MVar, getType(MVar), TrId)] .
    eq modStoreT(OpId[NeTL], ValOp, TrId)                    = modSEOpIds(OpId)[modOpStoreRec(NeTL, ValOp, TrId)] [owise] .


    *** Transform terms in a list to use symbolic stores
    op modOpStoreRec : TermList Qid TrType -> TermList .
    eq modOpStoreRec(empty, ValOp, TrId)           = empty .
    eq modOpStoreRec((T1, TermL), ValOp, TrId)     = modStoreT(T1, ValOp, TrId), modOpStoreRec(TermL, ValOp, TrId) .

    op hasEval : TermList -> Bool .
    eq hasEval(empty)        = false .
    eq hasEval(MConst)       = false .
    eq hasEval(MVar)         = false .
    eq hasEval('eval[NeTL])  = true .
    eq hasEval('evalI[NeTL]) = true .
    eq hasEval('evalR[NeTL]) = true .
    eq hasEval('evalB[NeTL]) = true .
    eq hasEval(OpId[NeTL])   = hasEval(NeTL) [owise] .
    eq hasEval((T1, NeTL))  = (hasEval(T1) or hasEval(NeTL)) .

    *** Transform variables and constants within conditions to use SMT types
    op modCond : Condition Qid TrType -> Condition .
    eq modCond(T1 = T2, ValOp, TrId)        = (modOpStoreRec(T1, ValOp, TrId) = searchSubVarConst(T2, TrId)) .
    eq modCond(T1 := T2, ValOp, TrId)       = (T1 := T2) .
    ***eq modCond(T1 => T2)       = (T1 => T2) .
    eq modCond(EqC /\ EqC2, ValOp, TrId)    = modCond(EqC, ValOp, TrId) /\ modCond(EqC2, ValOp, TrId) .
    eq modCond(Cond1 /\ Cond2, ValOp, TrId) = modCond(Cond1, ValOp, TrId) /\ modCond(Cond2, ValOp, TrId) .
    eq modCond(Cond, ValOp, TrId) = Cond [owise] .

    op modCondRl : Condition Qid TrType -> Condition .
    eq modCondRl(nil, ValOp, TrId)            = nil .
    eq modCondRl(T1 = T2, ValOp, TrId)        = if not hasEval(T1) then
                                                ('toBoolean[T1] = searchSubVarConst(T2, TrId))
                                              else
                                                (modOpStoreRec(T1, ValOp, TrId) = searchSubVarConst(T2, TrId))
                                              fi .
    ***eq modCondRl(T1 = T2, ValOp, TrId)        = (modOpStoreRec(T1, ValOp, TrId) = searchSubVarConst(T2, TrId)) [owise] .
    eq modCondRl(T1 := T2, ValOp, TrId)       = (T1 := T2) .
    ***eq modCondRl(T1 => T2)       = (T1 => T2) .
    eq modCondRl(EqC /\ EqC2, ValOp, TrId)    = modCondRl(EqC, ValOp, TrId) /\ modCondRl(EqC2, ValOp, TrId) .
    eq modCondRl(Cond1 /\ Cond2, ValOp, TrId) = modCondRl(Cond1, ValOp, TrId) /\ modCondRl(Cond2, ValOp, TrId) .
    eq modCondRl(Cond, ValOp, TrId) = Cond [owise] .

    *** Patch eval function definition to use symbolic stores and convert values
    op patchEvalSESTR : Equation Qid TrType -> Equation .
    eq patchEvalSESTR(eq 'eval[NeTL]   = T2 [AttrSet] ., ValOp, TrId)        = (eq toSymb('eval)[modOpStoreRec(NeTL, ValOp, TrId)] = modOpStoreRec(T2, ValOp, TrId) [AttrSet] .) .
    eq patchEvalSESTR(eq 'evalI[NeTL]  = T2 [AttrSet] ., ValOp, TrId)        = (eq toSymb('evalI)[modOpStoreRec(NeTL, ValOp, TrId)] = modOpStoreRec(T2, ValOp, TrId) [AttrSet] .) .
    eq patchEvalSESTR(eq 'evalR[NeTL]  = T2 [AttrSet] ., ValOp, TrId)        = (eq toSymb('evalR)[modOpStoreRec(NeTL, ValOp, TrId)] = modOpStoreRec(T2, ValOp, TrId) [AttrSet] .) .
    ***eq patchEvalSESTR(eq 'evalB[NeTL]  = T2 [AttrSet] .)        = (eq toSymb('evalB)[modOpStoreRec(NeTL)] = modOpStoreRec(T2) [AttrSet] .) .
    eq patchEvalSESTR(ceq 'eval[NeTL]  = T2 if EqC [AttrSet] ., ValOp, TrId) = (ceq toSymb('eval)[modOpStoreRec(NeTL, ValOp, TrId)] = modOpStoreRec(T2, ValOp, TrId) if modCond(EqC, ValOp, TrId) [AttrSet] .) .
    eq patchEvalSESTR(ceq 'evalI[NeTL] = T2 if EqC [AttrSet] ., ValOp, TrId) = (ceq toSymb('evalI)[modOpStoreRec(NeTL, ValOp, TrId)] = modOpStoreRec(T2, ValOp, TrId) if modCond(EqC, ValOp, TrId) [AttrSet] .) .
    eq patchEvalSESTR(ceq 'evalR[NeTL] = T2 if EqC [AttrSet] ., ValOp, TrId) = (ceq toSymb('evalR)[modOpStoreRec(NeTL, ValOp, TrId)] = modOpStoreRec(T2, ValOp, TrId) if modCond(EqC, ValOp, TrId) [AttrSet] .) .
    ***eq patchEvalSESTR(ceq 'evalB[NeTL] = T2 if EqC [AttrSet] .) = (ceq toSymb('evalB)[modOpStoreRec(NeTL)] = modOpStoreRec(T2) if modCond(EqC) [AttrSet] .) .
    eq patchEvalSESTR(Eq, ValOp, TrId) = Eq [owise] .
  
    *** Transform the eval functions definition to convert values to SMT types and patch the stores to the symbolic definition
    op modSEEqs : EquationSet Qid TrType -> EquationSet .
    eq modSEEqs(none, ValOp, TrId) = none .
    eq modSEEqs(eq 'evalI['val['I:Int], NeTL] = MVar [AttrSet] . EquationSet, ValOp, TrId)  = (eq toSymb('evalI)[modOpStoreRec(('val['I:Int], NeTL), ValOp, TrId)] = convert(MVar, getType(MVar), TrId) [AttrSet] .)
                                                                                              modSEEqs(EquationSet, ValOp, TrId) .
    eq modSEEqs(eq 'evalR['val['R:Rat], NeTL] = MVar [AttrSet] . EquationSet, ValOp, TrId)  = (eq toSymb('evalR)[modOpStoreRec(('val['R:Rat], NeTL), ValOp, TrId)] = convert(MVar, getType(MVar), TrId) [AttrSet] .)
                                                                                              modSEEqs(EquationSet, ValOp, TrId) .
    eq modSEEqs(eq 'eval['val['B:Bool], NeTL] = MVar [AttrSet] . EquationSet, ValOp, TrId) = (eq toSymb('eval)[modOpStoreRec(('val['B:Bool], NeTL), ValOp, TrId)] = convert(MVar, getType(MVar), TrId) [AttrSet] .)
                                                                                              modSEEqs(EquationSet, ValOp, TrId) .
    eq modSEEqs(eq 'evalI[ValOp['I:Int], NeTL] = MVar [AttrSet] . EquationSet, ValOp, TrId) = (eq toSymb('evalI)[(ValOp['I:Int], modOpStoreRec(NeTL, ValOp, TrId))] = convert(MVar, getType(MVar), TrId) [AttrSet] .)
                                                                                              (eq toSymb('evalI)[(ValOp['I:Integer], modOpStoreRec(NeTL, ValOp, TrId))] = searchSubVarConst(MVar, TrId) [AttrSet] .)
                                                                                              modSEEqs(EquationSet, ValOp, TrId) .
    eq modSEEqs(eq 'evalR[ValOp['R:Rat], NeTL] = MVar [AttrSet] . EquationSet, ValOp, TrId) = (eq toSymb('evalR)[(ValOp['R:Rat],modOpStoreRec(NeTL, ValOp, TrId))] = convert(MVar, getType(MVar), TrId) [AttrSet] .)
                                                                                              (eq toSymb('evalR)[(ValOp['R:Real],modOpStoreRec(NeTL, ValOp, TrId))] = searchSubVarConst(MVar, TrId) [AttrSet] .)
                                                                                              modSEEqs(EquationSet, ValOp, TrId) .
    eq modSEEqs(eq 'eval[ValOp['B:Bool], NeTL] = MVar [AttrSet] . EquationSet, ValOp, TrId) = (eq toSymb('eval)[(ValOp['B:Bool], modOpStoreRec(NeTL, ValOp, TrId))] = convert(MVar, getType(MVar), TrId) [AttrSet] .)
                                                                                              (eq toSymb('eval)[(ValOp['B:Boolean], modOpStoreRec(NeTL, ValOp, TrId))] = searchSubVarConst(MVar, TrId) [AttrSet] .)
                                                                                              modSEEqs(EquationSet, ValOp, TrId) .
    eq modSEEqs(Eq EquationSet, ValOp, TrId) = patchEvalSESTR(Eq, ValOp, TrId) modSEEqs(EquationSet, ValOp, TrId) [owise] .
    
    *** Transformation for concolic execution duplicates the equation set and transforms one of the copies with the symbolic execution transformation
    op modConcEqs : EquationSet Qid TrType -> EquationSet .
    eq modConcEqs(EquationSet, ValOp, TrId) = EquationSet modSEEqs(EquationSet, ValOp, TrId) .

    *** Transform equations according to transformation type
    op modEqs : EquationSet Qid TrType -> EquationSet .
    eq modEqs(EquationSet, ValOp, conc) = modConcEqs(EquationSet, ValOp, conc) .
    eq modEqs(EquationSet, ValOp, TrId) = modSEEqs(EquationSet, ValOp, TrId) [owise] .

    *** Include equational definitions for injected operators 
    op inclSEEqs : Qid -> EquationSet .
    eq inclSEEqs(StateOp) = *** Initialize symbolic variables in a concrete store with concrete values satisfying the accumulated Constraints (concrete store might be pre-initialized)
                            (eq 'init-CStore['STRS:Stores, 'Constraints:Boolean] = '$apply-SMTassignment['_|_|_['empty.IStore, 'empty.RStore, 'empty.BStore], 'STRS:Stores, 'get-SMTassignment['Constraints:Boolean]] [none] .)
                            (eq 'init-CStore['STR:Stores, 'STRS:Stores, 'Constraints:Boolean] = '$apply-SMTassignment['STR:Stores, 'STRS:Stores, 'get-SMTassignment['Constraints:Boolean]] [none] .)
                            *** Fill the gaps in a given concrete store with values satisfying the accumulated constraints. An initial store can only be provided at the beginning, new iterations use empty stores.
                            (eq '$apply-SMTassignment['_|_|_['ISTR:IStore, 'RSTR:RStore, 'BSTR:BStore], '_|_|_['ISTRS:IStoreS, '_`,_['_|->Rs_['Var:Qid, 'R:Real], 'RSTRS:RStoreS], 'BSTRS:BStoreS], '_<--_['R:Real, 'Rconc:Real]]          = '_|_|_['initialize-def['ISTR:IStore, 'ISTRS:IStoreS], '_`,_['insertFirst['Var:Qid, 'toRat['Rconc:Real], 'RSTR:RStore], 'initialize-def['empty.RStore, 'RSTRS:RStoreS]], 'initialize-def['BSTR:BStore, 'BSTRS:BStoreS]] [none] .)
                            (eq '$apply-SMTassignment['_|_|_['ISTR:IStore, 'RSTR:RStore, 'BSTR:BStore], '_|_|_['_`,_['_|->Is_['Var:Qid, 'I:Integer], 'ISTRS:IStoreS], 'RSTRS:RStoreS, 'BSTRS:BStoreS], '_<--_['I:Integer, 'Iconc:Integer]] = '_|_|_['_`,_['insertFirst['Var:Qid, 'toInt['Iconc:Integer], 'ISTR:IStore], 'initialize-def['empty.IStore, 'ISTRS:IStoreS]], 'initialize-def['RSTR:RStore, 'RSTRS:RStoreS], 'initialize-def['BSTR:BStore, 'BSTRS:BStoreS]] [none] .)
                            (eq '$apply-SMTassignment['_|_|_['ISTR:IStore, 'RSTR:RStore, 'BSTR:BStore], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, '_`,_['_|->Bs_['Var:Qid, 'B:Boolean], 'BSTRS:BStoreS]], '_<--_['B:Boolean, 'Bconc:Boolean]] = '_|_|_['initialize-def['ISTR:IStore, 'ISTRS:IStoreS], 'initialize-def['RSTR:RStore, 'RSTRS:RStoreS], '_`,_['insertFirst['Var:Qid, 'toBool['Bconc:Boolean], 'BSTR:BStore], 'initialize-def['empty.BStore, 'BSTRS:BStoreS]]] [none] .)
                            (eq '$apply-SMTassignment['_|_|_['ISTR:IStore, 'RSTR:RStore, 'BSTR:BStore], '_|_|_['ISTRS:IStoreS, '_`,_['_|->Rs_['Var:Qid, 'R:Real], 'RSTRS:RStoreS], 'BSTRS:BStoreS], '_`,_['_<--_['R:Real, 'Rconc:Real], 'AssignmentSMT:AssignmentSMT]]          = '$apply-SMTassignment['_|_|_['ISTR:IStore, 'insertFirst['Var:Qid, 'toRat['Rconc:Real], 'RSTR:RStore], 'BSTR:BStore], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS], 'AssignmentSMT:AssignmentSMT] [none] .)
                            (eq '$apply-SMTassignment['_|_|_['ISTR:IStore, 'RSTR:RStore, 'BSTR:BStore], '_|_|_['_`,_['_|->Is_['Var:Qid, 'I:Integer], 'ISTRS:IStoreS], 'RSTRS:RStoreS, 'BSTRS:BStoreS], '_`,_['_<--_['I:Integer, 'Iconc:Integer], 'AssignmentSMT:AssignmentSMT]] = '$apply-SMTassignment['_|_|_['insertFirst['Var:Qid, 'toInt['Iconc:Integer], 'ISTR:IStore], 'RSTR:RStore, 'BSTR:BStore], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS], 'AssignmentSMT:AssignmentSMT] [none] .)
                            (eq '$apply-SMTassignment['_|_|_['ISTR:IStore, 'RSTR:RStore, 'BSTR:BStore], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, '_`,_['_|->Bs_['Var:Qid, 'B:Boolean], 'BSTRS:BStoreS]], '_`,_['_<--_['B:Boolean, 'Bconc:Boolean], 'AssignmentSMT:AssignmentSMT]] = '$apply-SMTassignment['_|_|_['ISTR:IStore, 'RSTR:RStore, 'insertFirst['Var:Qid, 'toBool['Bconc:Boolean], 'BSTR:BStore]], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS], 'AssignmentSMT:AssignmentSMT] [none] .)
                            (eq '$apply-SMTassignment['STR:Stores, 'STRS:Stores, 'failed.AssignmentSMT] = 'STR:Stores [none] .)
                            (eq '$apply-SMTassignment['_|_|_['ISTR:IStore, 'RSTR:RStore, 'BSTR:BStore], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS], '_<--_['true.Boolean, 'true.Boolean]] = '_|_|_['initialize-def['ISTR:IStore, 'ISTRS:IStoreS], 'initialize-def['RSTR:RStore, 'RSTRS:RStoreS], 'initialize-def['BSTR:BStore, 'BSTRS:BStoreS]] [none] .)
                            
                            *** Recursively initialize symbolic variables with default values in concrete store 
                            (eq 'initialize-def['ISTR:IStore, 'empty.IStoreS] = 'ISTR:IStore [none] .)
                            (eq 'initialize-def['RSTR:RStore, 'empty.RStoreS] = 'RSTR:RStore [none] .)
                            (eq 'initialize-def['BSTR:BStore, 'empty.BStoreS] = 'BSTR:BStore [none] .)
                            (eq 'initialize-def['ISTR:IStore, '_`,_['_|->Is_['Var:Qid, 'I:Integer], 'ISTRS:IStoreS]] = 'initialize-def['insertFirst['Var:Qid, '0.Zero, 'ISTR:IStore], 'ISTRS:IStoreS] [none] .)
                            (eq 'initialize-def['RSTR:RStore, '_`,_['_|->Rs_['Var:Qid, 'R:Real],    'RSTRS:RStoreS]] = 'initialize-def['insertFirst['Var:Qid, '0.Zero, 'RSTR:RStore], 'RSTRS:RStoreS] [none] .)
                            (eq 'initialize-def['BSTR:BStore, '_`,_['_|->Bs_['Var:Qid, 'B:Boolean], 'BSTRS:BStoreS]] = 'initialize-def['insertFirst['Var:Qid, 'true.Bool, 'BSTR:BStore], 'BSTRS:BStoreS] [none] .)
                           
                            *** Boolean simplification
                            (eq 'not_['not_['B:Boolean]] = 'B:Boolean [none] .)

                            *** Insert only if variable has not been already assigned
                            (eq 'insertFirst['Var:Qid, 'I:Int,  'ISTR:IStore] = 'if_then_else_fi['_==_['_`[_`]['ISTR:IStore, 'Var:Qid], 'undefined.Rat], 'insert['Var:Qid, 'I:Int, 'ISTR:IStore], 'ISTR:IStore] [none] .)
                            (eq 'insertFirst['Var:Qid, 'R:Rat,  'RSTR:RStore] = 'if_then_else_fi['_==_['_`[_`]['RSTR:RStore, 'Var:Qid], 'undefined.Rat], 'insert['Var:Qid, 'R:Rat, 'RSTR:RStore], 'RSTR:RStore] [none] .)
                            (eq 'insertFirst['Var:Qid, 'B:Bool, 'BSTR:BStore] = 'if_then_else_fi['_==_['_`[_`]['BSTR:BStore, 'Var:Qid], 'undefined.Bool], 'insert['Var:Qid, 'B:Bool, 'BSTR:BStore], 'BSTR:BStore] [none] .)
                            
                            ***(eq 'size['C1:Boolean] = ''s_['0.Nat] [none] .)
                            ***(eq 'size['_and_['C1:Boolean, 'Constraints:Boolean]] = ''s_['0.Nat] + 'size['Constraints:Boolean] [none] .)
                            
                            (eq 'startC[stateVar(StateOp), 'SVDeclL:PairSVarL]                       = '$startC[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_|_['empty.IStoreS, 'empty.RStoreS, 'empty.BStoreS], 'true.Boolean] [none] .)
                            (eq 'startC['_where_[stateVar(StateOp), 'B:Boolean], 'SVDeclL:PairSVarL] = '$startC[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_|_['empty.IStoreS, 'empty.RStoreS, 'empty.BStoreS], 'B:Boolean] [none] .)
                            
                            (eq '$startC[stateVar(StateOp), 'nil.PairSVarL, 'STR:Stores, 'B:Boolean] = '`[_`]`[_`]`[_`]['updateStore[stateVar(StateOp), 'init-CStore['getStore[stateVar(StateOp)], 'STR:Stores, 'B:Boolean]], '_`{_`}['updateStore[stateVar(StateOp), 'STR:Stores], 'B:Boolean], 'updateStore[stateVar(StateOp), 'STR:Stores]] [none] .)
                            (eq '$startC[stateVar(StateOp), '__['_`,_['Var:Qid, 'I1:Integer], 'SVDeclL:PairSVarL], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS], 'B:Boolean] = '$startC[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_|_['insert['Var:Qid, 'I1:Integer, 'ISTRS:IStoreS], 'RSTRS:RStoreS, 'BSTRS:BStoreS], 'B:Boolean] [none] .)
                            (eq '$startC[stateVar(StateOp), '__['_`,_['Var:Qid, 'R1:Real],    'SVDeclL:PairSVarL], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS], 'B:Boolean] = '$startC[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_|_['ISTRS:IStoreS, 'insert['Var:Qid, 'R1:Real, 'RSTRS:RStoreS], 'BSTRS:BStoreS], 'B:Boolean] [none] .)
                            (eq '$startC[stateVar(StateOp), '__['_`,_['Var:Qid, 'B1:Boolean], 'SVDeclL:PairSVarL], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS], 'B:Boolean] = '$startC[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'insert['Var:Qid, 'B1:Boolean, 'BSTRS:BStoreS]], 'B:Boolean] [none] .)
                            
                            (eq 'startSE[stateVar(StateOp), 'nil.PairSVarL, 'STR:Stores] = 'updateStore[stateVar(StateOp), 'STR:Stores] [none] .)
                            (eq 'startSE[stateVar(StateOp), '__['_`,_['Var:Qid, 'I1:Integer], 'SVDeclL:PairSVarL], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS]] = 'startSE[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_|_['insert['Var:Qid, 'I1:Integer, 'ISTRS:IStoreS], 'RSTRS:RStoreS, 'BSTRS:BStoreS]] [none] .)
                            (eq 'startSE[stateVar(StateOp), '__['_`,_['Var:Qid, 'R1:Real],    'SVDeclL:PairSVarL], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS]] = 'startSE[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_|_['ISTRS:IStoreS, 'insert['Var:Qid, 'R1:Real, 'RSTRS:RStoreS], 'BSTRS:BStoreS]] [none] .)
                            (eq 'startSE[stateVar(StateOp), '__['_`,_['Var:Qid, 'B1:Boolean], 'SVDeclL:PairSVarL], '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'BSTRS:BStoreS]] = 'startSE[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_|_['ISTRS:IStoreS, 'RSTRS:RStoreS, 'insert['Var:Qid, 'B1:Boolean, 'BSTRS:BStoreS]]] [none] .)
                            *** Similar definition for starting narrowing execution
                            (eq 'startSE[stateVar(StateOp), '__['_`,_['Var:Qid, 'I1:IntFVP], 'SVDeclL:PairSVarL], '_|_['ISTRN:IStoreN, 'BSTRN:BStoreN]] = 'startSE[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_['insert['Var:Qid, 'I1:IntFVP, 'ISTRN:IStoreN], 'BSTRN:BStoreN]] [none] .)
                            (eq 'startSE[stateVar(StateOp), '__['_`,_['Var:Qid, 'B1:BoolFVP], 'SVDeclL:PairSVarL], '_|_['ISTRN:IStoreN, 'BSTRN:BStoreN]] = 'startSE[stateVar(StateOp), 'SVDeclL:PairSVarL, '_|_['ISTRN:IStoreN, 'insert['Var:Qid, 'B1:BoolFVP, 'BSTRN:BStoreN]]] [none] .) .


    *** Transform rules depending on transformation type
    op modRl : RuleSet Qid Qid TrType -> RuleSet .
    eq modRl(RlSet, StateOp, ValOp, symb) = rlToSymbolic(RlSet, ValOp) .
    eq modRl(RlSet, StateOp, ValOp, conc) = rlToConcolic(RlSet, ValOp, StateOp) .
    eq modRl(RlSet, StateOp, ValOp, maudeSE) = rlToSE(RlSet, ValOp, maudeSE) .
    eq modRl(RlSet, StateOp, ValOp, narrowing) = rlToNarrowing(RlSet, ValOp) .
    ***eq modRl(RlSet, clconc) = rlToClConcolic(RlSet, StateOp) inclClConcCrl(StateOp) .

    *** NOTE: MaudeSE does not work with smod
    *** Transform a module M considering the original State sort, an auxiliary value operator, and the transfotmation id (symb, conc, maudeSE)
    *** The transformation modifies operators, equations and rewrite rules, and it is specific for the target transformation type
    op trMod : Module Qid Qid TrType -> Module .
    eq trMod(M, StateOp, ValOp, TrId) = mod 'TRANSFORMED-MOD is
                                          getImports(M)
                                          sorts inclSESorts(getSorts(M)) .
                                          getSubsorts(M)
                                          modSEOps(getOps(M), StateOp, ValOp, TrId)
                                          getMbs(M)
                                          modEqs(getEqs(M), ValOp, TrId) inclSEEqs(StateOp)
                                          modRl(getRls(M), StateOp, ValOp, TrId)
                                          ***getStrats(M)
                                          ***getSds(M)
                                        endm .

    *** Fuses a module and a functional module into one
    op fuseMods : Module FModule -> Module .
    eq fuseMods(M, FM) = mod getName(M) is
                            getImports(M) getImports(FM)
                            sorts getSorts(M) ; getSorts(FM) .
                            getSubsorts(M) getSubsorts(FM)
                            getOps(M) getOps(FM)
                            getMbs(M) getMbs(FM)
                            getEqs(M) getEqs(FM)
                            getRls(M)
                            ***getStrats(M) getStrats(FM)
                            ***getSds(M) getSds(FM)
                          endm .

    *** Transform a module to include the symbolic/concolic execution requirements.
    *** TODO: Evaluate whether fusing with full MODULE-TRANSFORMER instead
    op transformModSymb : Qid Qid Qid TrType -> Module .
    eq transformModSymb(ModId, StateOp, ValOp, TrId) = transformModSymb(upModule(ModId, true), StateOp, ValOp, TrId) .
    op transformModSymb : Module Qid TrType -> Module .
    eq transformModSymb(M, StateOp, TrId) = transformModSymb(M, StateOp, 'placeholderVal, TrId) .
    op transformModSymb : Module Qid Qid TrType -> Module .
    eq transformModSymb(M, StateOp, ValOp, TrId) = fuseMods(trMod(M, StateOp, ValOp, TrId), upModule('SMT-AND-NARROWING, true)) .
    
    *** Transform module to concolic
    op concTr : Module Qid -> Module .
    eq concTr(M, StateOp) = transformModSymb(M, StateOp, conc) .

    op narrowingTr : Module Qid -> Module .
    eq narrowingTr(M, StateOp) = transformModSymb(M, StateOp, narrowing) .

endfm

mod VERIFICATION-COMMANDS is

    pr MODULE-TRANSFORMER .
    pr LEXICAL .

    vars ModId StateOp PrOp SearchType ValOp TargetSt FoldQ : Qid .
    var  TrId                                               : TrType .
    var  PatternSEState                                     : Term .
    var  InitSEState                                        : String . 
    var  SearchCond                                         : Condition .
    var  Bound                                              : Bound .
    var  SolN                                               : Nat .
    var  NeModIdList                                        : NeQidList .
    var  M                                                  : Module .
    var  SVDeclL                                            : PairSVarL .
    var  SymbCond                                           : Boolean .
    var  VariantOpSet                                       : VariantOptionSet .

    op searchTr : Module Qid Qid TrType Qid String Term Condition Qid Bound Nat PairSVarL Boolean -> ResultTriple .
    eq searchTr(M, StateOp, ValOp, TrId, TargetSt,
                  InitSEState,
                  PatternSEState,
                  SearchCond,
                  SearchType,
                  Bound,
                  SolN,
                  SVDeclL,
                  SymbCond)
                  =
                  metaSearch(transformModSymb(M, StateOp, ValOp, TrId),
                             'startC['_where_[getTerm(metaParse(M,
                                                                 tokenize(InitSEState),
                                                                 StateOp)),
                                              searchSubVarConst(upTerm(SymbCond), TrId)],
                                     searchSubVarConst(upTerm(SVDeclL), TrId)],
                             PatternSEState,
                             SearchCond,
                             SearchType,
                             Bound,
                             SolN) .
    
    op searchPathTr : Module Qid Qid TrType Qid String Term Condition Qid Bound Nat PairSVarL Boolean -> Trace? .
    eq searchPathTr(M, StateOp, ValOp, TrId, TargetSt,
                    InitSEState,
                    PatternSEState,
                    SearchCond,
                    SearchType,
                    Bound,
                    SolN,
                    SVDeclL,
                    SymbCond)
                    =
                    metaSearchPath(transformModSymb(M, StateOp, ValOp, TrId),
                                   'startC['_where_[getTerm(metaParse(M,
                                                                       tokenize(InitSEState),
                                                                       StateOp)),
                                                    searchSubVarConst(upTerm(SymbCond), TrId)],
                                           searchSubVarConst(upTerm(SVDeclL), TrId)],
                                   PatternSEState,
                                   SearchCond,
                                   SearchType,
                                   Bound,
                                   SolN) .
    
    op searchSymb : Module Qid Qid String Term Condition Qid Bound Nat PairSVarL Boolean -> ResultTriple .
    eq searchSymb(M, StateOp, ValOp,
                  InitSEState,
                  PatternSEState,
                  SearchCond,
                  SearchType,
                  Bound,
                  SolN,
                  SVDeclL,
                  SymbCond)
                  = searchTr(M, StateOp, ValOp, symb, 'SEState,
                             InitSEState,
                             PatternSEState,
                             SearchCond,
                             SearchType,
                             Bound,
                             SolN,
                             SVDeclL,
                             SymbCond) .

    op searchConcolic : Module Qid Qid String Term Condition Qid Bound Nat PairSVarL Boolean -> ResultTriple .
    eq searchConcolic(M, StateOp, ValOp,
                      InitSEState,
                      PatternSEState,
                      SearchCond,
                      SearchType,
                      Bound,
                      SolN,
                      SVDeclL,
                      SymbCond)
                      = searchTr(M, StateOp, ValOp, conc, 'ConcolicState,
                                 InitSEState,
                                 PatternSEState,
                                 SearchCond,
                                 SearchType,
                                 Bound,
                                 SolN,
                                 SVDeclL,
                                 SymbCond) .

    op searchPathConcolic : Module Qid Qid String Term Condition Qid Bound Nat PairSVarL Boolean -> Trace? .
    eq searchPathConcolic(M, StateOp, ValOp,
                          InitSEState,
                          PatternSEState,
                          SearchCond,
                          SearchType,
                          Bound,
                          SolN,
                          SVDeclL,
                          SymbCond)
                          = searchPathTr(M, StateOp, ValOp, conc, 'ConcolicState,
                                         InitSEState,
                                         PatternSEState,
                                         SearchCond,
                                         SearchType,
                                         Bound,
                                         SolN,
                                         SVDeclL,
                                         SymbCond) .

    op searchNarrowing : Module Qid Qid String Term Qid Bound Qid VariantOptionSet Nat PairSVarL -> NarrowingSearchResult? .
    eq searchNarrowing(M, StateOp, ValOp,
                        InitSEState,
                        PatternSEState,
                        SearchType,
                        Bound,
                        FoldQ,
                        VariantOpSet,
                        SolN,
                        SVDeclL)
                        = metaNarrowingSearch(transformModSymb(M, StateOp, ValOp, narrowing),
                                              'startSE[getTerm(metaParse(M,
                                                                        tokenize(InitSEState),
                                                                        StateOp)),
                                                      searchSubVarConst(upTerm(SVDeclL), narrowing),
                                                      '_|_['empty.IStoreN, 'empty.BStoreN]],
                                              PatternSEState,
                                              SearchType,
                                              Bound,
                                              FoldQ,
                                              VariantOpSet,
                                              SolN) .

    op searchPathNarrowing : Module Qid Qid String Term Qid Bound Qid VariantOptionSet Nat PairSVarL -> NarrowingSearchPathResult? .
    eq searchPathNarrowing(M, StateOp, ValOp,
                            InitSEState,
                            PatternSEState,
                            SearchType,
                            Bound,
                            FoldQ,
                            VariantOpSet,
                            SolN,
                            SVDeclL)
                            = metaNarrowingSearchPath(transformModSymb(M, StateOp, ValOp, narrowing),
                                                      'startSE[getTerm(metaParse(M,
                                                                                tokenize(InitSEState),
                                                                                StateOp)),
                                                              searchSubVarConst(upTerm(SVDeclL), narrowing),
                                                              '_|_['empty.IStoreN, 'empty.BStoreN]],
                                                      PatternSEState,
                                                      SearchType,
                                                      Bound,
                                                      FoldQ,
                                                      VariantOpSet,
                                                      SolN) .
endm

mod MAUDE-SE-EXT is

    pr VERIFICATION-COMMANDS .
    pr META-SMT-SEARCH . 

    vars StateOp PrOp ValOp TrId SearchType Logic : Qid .
    var  PatternSEState                           : Term .
    var  InitSEState                              : String . 
    var  SearchCond                               : Condition .
    var  Bound                                    : Bound .
    var  SolN                                     : Nat .
    var  NeModIdList                              : NeQidList .
    var  Fold                                     : Bool .
    var  M                                        : Module .
    var  SVDeclL                                  : PairSVarL .

    op searchMaudeSE : Module Qid Qid String Term Condition Qid Bound Nat Qid Bool PairSVarL -> SmtResult2? .
    eq searchMaudeSE(M, StateOp, ValOp,
                     InitSEState,
                     PatternSEState,
                     SearchCond,
                     SearchType,
                     Bound,
                     SolN,
                     Logic, Fold,
                     SVDeclL)
                     = metaSmtSearch(transformModSymb(M, StateOp, ValOp, maudeSE),
                                     'startSE[getTerm(metaParse(transformModSymb(M, StateOp, ValOp, maudeSE),
                                                                                  tokenize(InitSEState),
                                                                                  StateOp)),
                                                                searchSubVarConst(upTerm(SVDeclL), maudeSE), 
                                                                '_|_|_['empty.IStoreS, 'empty.RStoreS, 'empty.BStoreS]],
                                     PatternSEState,
                                     modCond(SearchCond, ValOp, maudeSE),
                                     SearchType,
                                     Bound,
                                     SolN,
                                     Logic, Fold) .
    
    op searchPathMaudeSE : Module Qid Qid String Term Condition Qid Bound Nat Qid Bool PairSVarL -> Trace2Result? .
    eq searchPathMaudeSE(M, StateOp, ValOp,
                         InitSEState,
                         PatternSEState,
                         SearchCond,
                         SearchType,
                         Bound,
                         SolN,
                         Logic, Fold,
                         SVDeclL)
                         = metaSmtSearchPath(transformModSymb(M, StateOp, ValOp, maudeSE),
                                             'startSE[getTerm(metaParse(transformModSymb(M, StateOp, ValOp, maudeSE),
                                                                                  tokenize(InitSEState),
                                                                                  StateOp)),
                                                                searchSubVarConst(upTerm(SVDeclL), maudeSE), 
                                                                '_|_|_['empty.IStoreS, 'empty.RStoreS, 'empty.BStoreS]],
                                             PatternSEState,
                                             modCond(SearchCond, ValOp, maudeSE),
                                             SearchType,
                                             Bound,
                                             SolN,
                                             Logic, Fold) .
endm