---(
 Extending BOOL, RAT and INT with SMT variables  of the form b(x), i(x)
 and r(x)
 
 BoolExp (Bool extended with SMT variables) expressions can be checked for
 satisfiability using smtCheck that transforms a BoolExp into a BoolExpression 

)---)


--- Identifiers for variables
fmod SMT-VAR-ID is
    sort SMTVarId .
endfm


fmod ALT-BOOLEAN-EXPR is
  including SMT-VAR-ID .
  including BOOL .

  sort BoolExp .
  subsort Bool < BoolExp .
  
  sort BoolVar .
  subsort BoolVar < BoolExp .
  op b : SMTVarId -> BoolVar [ctor] .

  op not_ : BoolExp -> BoolExp [ditto] .
  op _and_ : BoolExp BoolExp -> BoolExp [ditto] .
  op _xor_ : BoolExp BoolExp -> BoolExp [ditto] .
  op _or_ : BoolExp BoolExp -> BoolExp [ditto] .
  op _implies_ : BoolExp BoolExp -> BoolExp [ditto] .

  op _===_ : BoolExp BoolExp -> BoolExp [comm prec 51] .
  op _=/==_ : BoolExp BoolExp -> BoolExp [comm prec 51] .
  op _?_:_ : BoolExp BoolExp BoolExp -> BoolExp [gather (e e e) prec 71] .

  vars A B C : BoolExp .

--- from BOOL-OPS
  eq true and A = A .
  eq false and A = false .
  eq A and A = A .
  eq false xor A = A .
  eq A xor A = false .

---(
  eq A and (B xor C) = A and B xor A and C .
  eq not A = A xor true .
  eq A or B = A and B xor A xor B .
  eq A implies B = not(A xor A and B) .
)---)

  eq true implies A  = A .
  eq false implies A = true .
  eq A implies true  = true .

  eq false or A = A .

--- some basic equations
  eq A === A = true .

  eq (true ===  false) = (false).Bool .
  eq (true =/== false) = (true).Bool .

  eq true  ? A : B = A .
  eq false ? A : B = B .
endfm


--- Integer expressions
fmod ALT-INTEGER-EXPR is
  protecting ALT-BOOLEAN-EXPR .
  including INT .

  sort IntExp .
  subsort Int < IntExp .

  sort IntVar .
  subsort IntVar < IntExp .
  op i : SMTVarId -> IntVar [ctor] .

  op -_ : IntExp -> IntExp [ditto] .
  op _+_ : IntExp IntExp -> IntExp [ditto] .
  op _*_ : IntExp IntExp -> IntExp [ditto] .
  op _-_ : IntExp IntExp -> IntExp [ditto] .

  op _<_ : IntExp IntExp -> BoolExp [ditto] .
  op _<=_ : IntExp IntExp -> BoolExp [ditto] .
  op _>_ : IntExp IntExp -> BoolExp [ditto].
  op _>=_ : IntExp IntExp -> BoolExp [ditto] .

  op _===_ : IntExp IntExp -> BoolExp [comm prec 51] .
  op _=/==_ : IntExp IntExp -> BoolExp [comm prec 51] .
  op _?_:_ : BoolExp IntExp IntExp -> IntExp [gather (e e e) prec 71] .

--- The following operators are currently not supported.
---( 
  op _div_ : IntExp IntExp -> IntExp [gather (E e) prec 31] . 
  op _mod_ : IntExp IntExp -> IntExp [gather (E e) prec 31] .
  op _divisible_ : IntExp IntExp -> BoolExp [prec 51] .
)---)

  vars A B : IntExp .
  vars I J : Int .

--- some basic equations
  --- eq A === A = true .
  --- eq A <= A = true .
  --- eq A >= A = true .

  eq (A ===  B) = A <= B and A >= B .
  eq (A =/== B) = A < B  or  A > B .

  eq true  ? A : B = A .
  eq false ? A : B = B .
endfm

--- Because RAT includes INT, ALT-REAL must include ALT-INTEGER.
fmod ALT-REAL-INTEGER-EXPR is
  including SMT-VAR-ID .
  protecting ALT-INTEGER-EXPR .
  including RAT .

  sort RExp .
  subsort Rat < RExp .
  subsort IntExp < RExp .

  sort RVar StRExp .
  subsort RVar < StRExp < RExp .
  op r : SMTVarId -> RVar [ctor] .

  op -_ : RExp -> RExp [ditto] .
  op _+_ : RExp RExp -> RExp [ditto] .
  op _*_ : RExp RExp -> RExp [ditto] .
  op _-_ : RExp RExp -> RExp [ditto] .
  op _/_ : RExp RExp -> RExp [ditto] .

  op -_ : StRExp -> StRExp [ditto] .
  op _+_ : StRExp RExp -> StRExp [ditto] .
  op _*_ : StRExp RExp -> StRExp [ditto] .

  op _-_ : StRExp RExp -> StRExp [ditto] .
  op _-_ : RExp StRExp -> StRExp [ditto] .
  op _/_ : StRExp RExp -> StRExp [ditto] .
  op _/_ : RExp StRExp -> StRExp [ditto] .

  op _<_ : RExp RExp -> BoolExp [ditto] .
  op _<=_ : RExp RExp -> BoolExp [ditto] .
  op _>_ : RExp RExp -> BoolExp [ditto] .
  op _>=_ : RExp RExp -> BoolExp [ditto] .

  op _===_ : RExp RExp -> BoolExp [comm prec 51] .
  op _=/==_ : RExp RExp -> BoolExp [comm prec 51] .
  op _?_:_ : BoolExp RExp RExp -> RExp [gather (e e e) prec 71] .
  --- op _?_:_ : BoolExp Int Int -> Int [ditto] .

  op toReal : IntExp -> RExp .
  op toInteger : RExp -> IntExp .
  op isInteger : RExp -> BoolExp .

  vars A B C : RExp .
  var RV : RVar .
  var I : Int .
  vars R R' S : Rat .

--- some basic equations
  --- eq A === A = true .
  --- eq A <= A = true .
  --- eq A >= A = true .
  eq (A ===  B) = A <= B and A >= B .
  eq (A =/== B) = A <  B  or A >  B .

  eq 0 + A = A .
  eq A - B = A + (- B) .
  eq A + (- A) = 0 .
  eq - (A + B) = (- A) + (- B) .
  eq - (- A) = A .

  eq (A + C <=  B + C) = (A <=  B) .
  eq (A + C <   B + C) = (A <   B) .
  eq (A + C >=  B + C) = (A >=  B) .
  eq (A + C >   B + C) = (A >   B) .
  eq (A + C === B + C) = (A === B) .

---(
--- some simplification for human readability
  eq (0 <= R + - RV) = (RV <= R) .
  eq (0 <  R + - RV) = (RV <  R) .
  eq (0 >= R + - RV) = (RV >= R) .
  eq (0 >  R + - RV) = (RV >  R) .

  ceq (RV <= R) and (RV <= R') = RV <= R if R <= R' .
  ceq (RV <  R) and (RV <  R') = RV <  R if R <= R' .
  ceq (RV >= R) and (RV >= R') = RV <= R if R >= R' .
  ceq (RV >  R) and (RV >  R') = RV <  R if R >= R' .

  ceq (RV <= R + A) and (RV <= R' + A) = RV <= R + A if R <= R' .
  ceq (RV <  R + A) and (RV <  R' + A) = RV <  R + A if R <= R' .
  ceq (RV >= R + A) and (RV >= R' + A) = RV <= R + A if R >= R' .
  ceq (RV >  R + A) and (RV >  R' + A) = RV <  R + A if R >= R' .

  eq (A <= B) and (A >= B) = (A === B) .
)---

  eq toReal(I) = I .
  eq toInteger(R) = floor(R) .

  eq isInteger(I) = true .
  eq isInteger(R) = floor(R) === R .
endfm


--- from an old version of the HybridSynchAADL implementation
fmod META-SMT-CONSTANT-TRANS is
  protecting META-LEVEL .
  protecting CONVERSION .

  vars T T' : Term .

  sort Nat? .
  subsort Nat < Nat? .
  op error : -> Nat? [ctor] .

  op metaTrIntC : Term -> TermQid [memo] .
  eq metaTrIntC(T) = qid(string(downTerm(T,error),10) + ".Integer")  .

  op metaTrRatC : Term -> TermQid [memo] .
  eq metaTrRatC('_/_[T,T']) 
   = qid(string(downTerm(T,error),10) + "/" + string(downTerm(T',error),10) + ".Real") .

  eq metaTrRatC(T) = qid(string(downTerm(T,error),10) + "/1.Real") [owise] .
endfm


--- translate ALT-SMT exps to SMT exps
fmod SMT-EXP-TRANS is
  protecting REAL-INTEGER .
  protecting ALT-REAL-INTEGER-EXPR .
  protecting META-SMT-CONSTANT-TRANS * (op __ : NatList NatList -> NatList to _#_) . 

  op trBool : BoolExp ~> Boolean .
  op trInt  : IntExp ~> Integer .
  op trReal : RExp ~> Real .

  var B : Bool .
  var I : Int .
  var R : Rat .
  var ID : SMTVarId .
  vars BE BE1 BE2 : BoolExp .
  vars IE IE1 IE2 : IntExp .
  vars RE RE1 RE2 : RExp .

  var C  : Constant .
  var Q  : Qid .
  var T : Term .
  var TL : TermList .

  --- error terms for downTerm
  op error : ~> Boolean [ctor] .
  op error : ~> Integer [ctor] .
  op error : ~> Real [ctor] .

  --- translation for atoms
  op trRealAtom : Rat ~> Real [memo].
  eq trRealAtom(R) = downTerm(metaTrRatC(upTerm(R)),error) .

  op trIntAtom  : Int ~> Integer [memo] .
  eq trIntAtom(I) = downTerm(metaTrIntC(upTerm(I)),error) .

  --- translation for variables
  op trRealVar : RVar ~> Real [memo] .
  eq trRealVar(r(ID)) 
   = downTerm(qid($varid2str(upTerm(ID)) + ":Real"), error) .

  op trIntVar : IntVar ~> Integer [memo] .
  eq trIntVar(i(ID)) 
   = downTerm(qid($varid2str(upTerm(ID)) + ":Integer"), error) .

  op trBoolVar : BoolVar ~> Boolean [memo] .
  eq trBoolVar(b(ID)) 
   = downTerm(qid($varid2str(upTerm(ID)) + ":Boolean"), error) .

--- Boolean
  eq trBool(true)  = true .
  eq trBool(false) = false .
  eq trBool(b(ID)) = trBoolVar(b(ID)) .

  eq trBool(not BE) = not trBool(BE) .
  eq trBool(BE1 and BE2) = trBool(BE1) and trBool(BE2) .
  eq trBool(BE1 xor BE2) = trBool(BE1) xor trBool(BE2) .
  eq trBool(BE1 or  BE2) = trBool(BE1) or  trBool(BE2) .
  eq trBool(BE1 implies BE2) = trBool(BE1) implies trBool(BE2) .

  eq trBool(BE1 ===  BE2) = trBool(BE1) ===  trBool(BE2) .
  eq trBool(BE1 =/== BE2) = trBool(BE1) =/== trBool(BE2) .

  eq trBool(BE ? BE1 : BE2) = trBool(BE) ? trBool(BE1) : trBool(BE2) .

--- Integer
  eq trInt(I) = trIntAtom(I) .
  eq trInt(i(ID)) = trIntVar(i(ID)) .

  eq trInt(- IE) = - trInt(IE) .
  eq trInt(IE1 + IE2) = trInt(IE1) + trInt(IE2) .
  eq trInt(IE1 * IE2) = trInt(IE1) * trInt(IE2) .
  eq trInt(IE1 - IE2) = trInt(IE1) - trInt(IE2) .

  eq trBool(IE1 <  IE2) = trInt(IE1) <  trInt(IE2) .
  eq trBool(IE1 <= IE2) = trInt(IE1) <= trInt(IE2) .
  eq trBool(IE1 >  IE2) = trInt(IE1) >  trInt(IE2) .
  eq trBool(IE1 >= IE2) = trInt(IE1) >= trInt(IE2) .

  eq trBool(IE1 ===  IE2) = trInt(IE1) ===  trInt(IE2) .
  eq trBool(IE1 =/== IE2) = trInt(IE1) =/== trInt(IE2) .

  eq trInt(BE ? IE1 : IE2) = trBool(BE) ? trInt(IE1) : trInt(IE2) .

--- Real
  eq trReal(R) = trRealAtom(R) . 
  eq trReal(r(ID)) = trRealVar(r(ID)) .

  eq trReal(- RE) = - trReal(RE) .
  eq trReal(RE1 + RE2) = trReal(RE1) + trReal(RE2) .
  eq trReal(RE1 * RE2) = trReal(RE1) * trReal(RE2) .
  eq trReal(RE1 - RE2) = trReal(RE1) - trReal(RE2) .
  eq trReal(RE1 / RE2) = trReal(RE1) / trReal(RE2) .

  eq trBool(RE1 <  RE2) = trReal(RE1) <  trReal(RE2) .
  eq trBool(RE1 <= RE2) = trReal(RE1) <= trReal(RE2) .
  eq trBool(RE1 >  RE2) = trReal(RE1) >  trReal(RE2) .
  eq trBool(RE1 >= RE2) = trReal(RE1) >= trReal(RE2) .

  eq trBool(RE1 ===  RE2) = trReal(RE1) ===  trReal(RE2) .
  eq trBool(RE1 =/== RE2) = trReal(RE1) =/== trReal(RE2) .

  eq trReal(BE ? RE1 : RE2) = trBool(BE) ? trReal(RE1) : trReal(RE2) .

  eq trReal(toReal(IE)) = toReal(trInt(IE)) .
  eq trInt(toInteger(RE)) = toInteger(trReal(RE)) .
  eq trBool(isInteger(RE)) = isInteger(trReal(RE)) . 

--- SMTVarId
  op $varid2str : Term ~> String .
  op $varid2str-L : TermList ~> String .
  eq $varid2str(C) = string(getName(C)) . 
  eq $varid2str(Q[TL]) = string(Q) + "_" + $varid2str-L(TL) . 
  eq $varid2str-L(empty) = "" .
  eq $varid2str-L( (T, TL)) = $varid2str(T) + "_" + $varid2str-L(TL) .
endfm



fmod ALT-SMT-CHECK is
  protecting SMT-EXP-TRANS .

   var BE : BoolExp .

   --- Satisfiability check 
   op smtCheck : BoolExp -> Bool .
   eq smtCheck(true) = true .
   eq smtCheck(false) = false .
   eq smtCheck(BE) = metaCheck(['ALT-SMT-CHECK], upTerm(trBool(BE))) [owise] .
endfm

