package Ġorg . abs _ models . c row bar . executions Ċ Ċ import Ġorg . abs _ models . c row bar . data .* Ċ import Ġorg . abs _ models . c row bar . data . Function Ċ import Ġorg . abs _ models . c row bar . interfaces . evaluate S MT Ċ import Ġorg . abs _ models . c row bar . interfaces . generate S MT Ċ import Ġorg . abs _ models . c row bar . main . output Ċ import Ġorg . abs _ models . c row bar . tree . Logic Node Ċ import Ġorg . abs _ models . c row bar . tree . Static Node Ċ import Ġorg . abs _ models . c row bar . tree . Symbolic Leaf Ċ import Ġorg . abs _ models . frontend . type checker . Type Ċ import Ġorg . abs _ models . frontend . type checker . Unknown Type Ċ Ċ class ĠAbstract Evaluation Ġ( val Ġfram ing : ĠMap < Location , ĠAE Loc Set >, ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġsubst Map : ĠMutable Map < Location , ĠTerm > Ġ= Ġmutable Map Of () Ċ ){ ĊĊĠĠĠ Ġinit { ĊĠĠĠĠĠĠĠ Ġinit Subst Map () ĊĠĠĠĠĠĠĠ Ġ// print F ram ing () ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġprivate Ġfun Ġinit Subst Map (){ ĊĠĠĠĠĠĠĠ Ġfor ( location Ġin Ġthis . fr aming . keys ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġthis . subst Map [ location ] Ġ= ĠUnknown Term ( location ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġprivate Ġfun Ġprint F ram ing (){ ĊĠĠĠĠĠĠĠ Ġoutput ( this . fr aming . toList (). join ToString ("\ n ") Ġ{ Ġpair Ġ-> Ġ"${ pair . first . pretty Print () }\ t \ t ${ pair . second . pretty Print () }" Ġ}) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġfun Ġprint Subst Map (){ ĊĠĠĠĠĠĠĠ Ġoutput ( this . subst Map . toList (). join ToString ("\ n ") Ġ{ Ġpair Ġ-> Ġ"${ pair . first . pretty Print () }\ t \ t ${ pair . second . pretty Print () }" Ġ} Ġ+ Ġ"\ n ") ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġfun Ġprint Raw Subst Map () Ġ{ ĊĠĠĠĠĠĠĠ Ġoutput ( this . subst Map . toList (). join ToString ("\ n ") Ġ{ Ġpair Ġ-> Ġ"${ pair . first . pretty Print () }\ t \ t ${ pair . second }" Ġ}) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġfun Ġevaluate ( l Ġ: ĠS ymbolic Leaf ) Ġ: ĠBoolean Ġ{ ĊĠĠĠĠĠĠĠ Ġ// output ("$ l ") ĊĠĠĠĠĠĠĠ Ġif Ġ( l Ġis ĠStatic Node ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġreturn Ġfalse ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġl Ġas ĠLogic Node ĊĠĠĠĠĠĠĠ Ġif ( l . is Evalu ated ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġreturn Ġl . isValid ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġval Ġpre Ġ= Ġthis . eval ( this . de up dat ify ( l . ante )) ĊĠĠĠĠĠĠĠ Ġ// output ("${ l . ante . pretty Print () }") ĊĠĠĠĠĠĠĠ Ġ// output ("$ pre ") ĊĠĠĠĠĠĠĠ Ġinit Subst Map () ĊĠĠĠĠĠĠĠ Ġval Ġpost Ġ= Ġthis . eval ( this . de up dat ify ( Not ( l . succ ))) ĊĊĠĠĠĠĠĠĠ Ġ// output ("${ l . succ }") ĊĠĠĠĠĠĠĠ Ġ// output ("${ post . to S MT () }") ĊĊĠĠĠĠĠĠĠ Ġval Ġs mt Rep Ġ= Ġgenerate S MT ( pre , Ġpost ) ĊĊĠĠĠĠĠĠĠ Ġ// output ( smt Rep ) ĊĊĠĠĠĠĠĠĠ Ġreturn Ġevaluate S MT ( smt Rep ) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġfun Ġevaluate And Pre cond ( l Ġ: ĠS ymbolic Leaf ) Ġ: ĠPair < Boolean , ĠLogic Element >{ ĊĠĠĠĠĠĠĠ Ġ// output ("$ l ") ĊĠĠĠĠĠĠĠ Ġif Ġ( l Ġis ĠStatic Node ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġreturn ĠPair ( false , ĠTrue ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġl Ġas ĠLogic Node ĊĠĠĠĠĠĠĠ Ġif ( l . is Evalu ated ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġreturn ĠPair ( l . isValid , ĠTrue ) ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġval Ġpre Ġ= Ġthis . eval ( this . de up dat ify ( l . ante )) ĊĠĠĠĠĠĠĠ Ġ// output ("${ l . ante . pretty Print () }") ĊĠĠĠĠĠĠĠ Ġ// output ("$ pre ") ĊĠĠĠĠĠĠĠ Ġinit Subst Map () ĊĠĠĠĠĠĠĠ Ġval Ġpost Ġ= Ġthis . eval ( this . de up dat ify ( Not ( l . succ ))) ĊĊĠĠĠĠĠĠĠ Ġ// output ("${ l . succ }") ĊĠĠĠĠĠĠĠ Ġ// output ("${ post . to S MT () }") ĊĊĠĠĠĠĠĠĠ Ġval Ġs mt Rep Ġ= Ġgenerate S MT ( pre , Ġpost ) ĊĊĠĠĠĠĠĠĠ Ġ// output ( smt Rep ) ĊĊĠĠĠĠĠĠĠ Ġreturn ĠPair ( evaluate S MT ( smt Rep ), Ġpre ) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġfun Ġde up dat ify ( input Ġ: ĠLogic Element ) Ġ: ĠLogic Element { ĊĠĠĠĠĠĠĠ Ġreturn Ġwhen ( input ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠUpdate On Formula Ġ-> Ġ{ apply ( input . update ); Ġde up dat ify ( input . target )} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠUpdate On Term Ġ-> Ġ{ apply ( input . update ); Ġde up dat ify ( input . target )} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠFunction Ġ-> ĠFunction ( input . name , Ġinput . params . map Ġ{ Ġp Ġ-> Ġthis . de up dat ify ( p ) Ġas ĠTerm Ġ}) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠPredicate Ġ-> ĠPredicate ( input . name , Ġinput . params . map Ġ{ Ġp Ġ-> Ġthis . de up dat ify ( p ) Ġas ĠTerm Ġ}) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠImp l Ġ-> ĠImp l ( this . de up dat ify ( input . left ) Ġas ĠFormula , Ġthis . de up dat ify ( input . right ) Ġas ĠFormula ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠAnd Ġ-> ĠAnd ( this . de up dat ify ( input . left ) Ġas ĠFormula , Ġthis . de up dat ify ( input . right ) Ġas ĠFormula ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠOr Ġ-> ĠOr ( this . de up dat ify ( input . left ) Ġas ĠFormula , Ġthis . de up dat ify ( input . right ) Ġas ĠFormula ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠNot Ġ-> ĠNot ( this . de up dat ify ( input . left ) Ġas ĠFormula ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġelse Ġ-> Ġinput ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ// ĠApply Ġthe Ġupdate Ġto Ġthe Ġsubst Map ĊĠĠĠ Ġfun Ġapply ( update Ġ: ĠUpdate Element ){ ĊĠĠĠĠĠĠĠ Ġ// print Subst Map () ĊĠĠĠĠĠĠĠ Ġ// output ("$ update ") ĊĠĠĠĠĠĠĠ Ġwhen ( update ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠChain Update Ġ-> Ġ{ this . apply ( update . left ); Ġthis . apply ( update . right )} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠElement ary Update Ġ-> Ġconcrete Apply ( update . lhs , Ġupdate . rhs ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠAbstract Update Ġ-> Ġabstract Apply ( update . name , Ġupdate . accessible , Ġupdate . assign able ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġprivate Ġfun Ġconcrete Apply ( elem Ġ: ĠConcrete Location , Ġterm Ġ: ĠTerm ){ ĊĠĠĠĠĠĠĠ Ġval Ġvalue Ġ= Ġthis . eval ( term ) ĊĊĠĠĠĠĠĠĠ Ġ// ĠExpand Ġthe Ġconcrete Ġupdate Ġto Ġthe Ġabstract Ġlocation Ġconcerned ĊĠĠĠĠĠĠĠ Ġfor ( pair Ġin Ġthis . fr aming [ elem ] !!. locs ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġloc Ġ= Ġpair . second ĊĠĠĠĠĠĠĠĠĠĠĠ Ġassert ( loc Ġis ĠAE Location ) ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġwhen ( val Ġaux Ġ= Ġthis . subst Map [ loc ] !! ){ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠPrec ise On Abstract Term Ġ-> Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġaux . updates [ elem ] Ġ= Ġvalue Ġas ĠTerm ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġthis . subst Map [ loc ] Ġ= Ġaux ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠAbstract Term Ġ-> Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġthis . subst Map [ loc ] Ġ= ĠPrec ise On Abstract Term ( mutable Map Of ( Pair ( elem , Ġvalue Ġas ĠTerm )), Ġaux ) ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġelse Ġ-> Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġthrow ĠException (" Un fore seen Ġvalue Ġfor Ġabstract Ġlocation Ġ$ loc : Ġ$ aux ") ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġ// this . subst Map [ loc ] Ġ= ĠConcrete On Abstract Term ( elem , Ġvalue Ġas ĠTerm , Ġthis . subst Map [ loc ] Ġas ĠAbstract Term ) ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġthis . subst Map . remove ( elem ) ĊĠĠĠĠĠĠĠ Ġthis . subst Map [ elem ] Ġ= Ġvalue Ġas ĠTerm ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ// ĠApply Ġthe Ġabstract Ġupdate Ġto Ġthe Ġcurrent Ġsubst Map ĊĠĠĠ Ġprivate Ġfun Ġabstract Apply ( name : ĠConcrete Name , Ġaccessible Ġ: ĠAE Loc Set , Ġassignable Ġ: AE Loc Set ){ ĊĠĠĠĠĠĠĠ Ġ// print Subst Map () ĊĠĠĠĠĠĠĠ Ġ// output ("${ name . name }") ĊĠĠĠĠĠĠĠ Ġval Ġmax Ar ity Ġ= Ġassignable . locs . size ĊĠĠĠĠĠĠĠ Ġval Ġlist Accessible Value Ġ= Ġaccessible . locs . map Ġ{ Ġpair Ġ-> Ġ Ġthis . subst Map [ pair . second ] !!} ĊĊĠĠĠĠĠĠĠ Ġ// ĠThis Ġlist Ġis Ġused Ġfor Ġthe Ġar ity ĊĠĠĠĠĠĠĠ Ġval Ġlist Direct Assignable Ġ= Ġassignable . locs . map Ġ{ Ġpair Ġ-> Ġpair . second Ġ} ĊĠĠĠĠĠĠĠ Ġ// val Ġlist Indirect Assignable Ġ= Ġlist Direct Assignable . map Ġ{ Ġloc Ġ-> Ġthis . fr aming [ loc ] Ġ}. map Ġ{ Ġloc Set Ġ-> Ġloc Set ?. locs !!. map Ġ{ Ġpair Ġ-> Ġpair . second Ġ} Ġ}. flatten () ĊĊĠĠĠĠĠĠĠ Ġ// output ("$ list Direct Assignable ") ĊĊĠĠĠĠĠĠĠ Ġ// ĠSplit Ġaccording Ġto Ġhas To ĊĠĠĠĠĠĠĠ Ġval Ġlist Has To Direct Assignable Ġ= Ġassignable . locs . filter Ġ{ Ġit . first Ġ}. map Ġ{ Ġpair Ġ-> Ġpair . second } ĊĠĠĠĠĠĠĠ Ġval Ġlist Other Direct Assignable Ġ= Ġassignable . locs . filter { ! it . first }. map Ġ{ Ġpair Ġ-> Ġpair . second Ġ} ĊĊĊĊĠĠĠĠĠĠĠ Ġ// ĠFind Ġthe Ġconcrete Ġlocations Ġthat Ġare Ġincluded Ġin Ġthe Ġhas To Ġabstract Ġlocations ĊĠĠĠĠĠĠĠ Ġval Ġlist Concrete Has To Indirect Assignable Ġ= Ġlist Has To Direct Assignable . map Ġ{ Ġloc Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠ Ġthis . fr aming [ loc ] ĊĠĠĠĠĠĠĠ Ġ}. map Ġ{ Ġloc Set Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠ Ġloc Set ?. locs !!. map Ġ{ Ġit . second Ġ}. filter Is Instance < Concrete Location >() ĊĠĠĠĠĠĠĠ Ġ}. flatten () ĊĊĠĠĠĠĠĠĠ Ġ// output ("$ assign able ") ĊĠĠĠĠĠĠĠ Ġ// output ("${ list Other Direct Assignable }") ĊĊĠĠĠĠĠĠĠ Ġval Ġlist Other Indirect Assignable Ġ= Ġlist Has To Direct Assignable . map Ġ{ Ġloc Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠ Ġthis . fr aming [ loc ] ĊĠĠĠĠĠĠĠ Ġ}. flatMap Ġ{ Ġloc Set Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠ Ġloc Set ?. locs !!. filter Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġit . second Ġ! is ĠConcrete Location ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ}. map Ġ{ Ġpair Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġpair . second ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġ} Ġ+ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġlist Other Direct Assignable . map Ġ{ Ġloc Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġthis . fr aming [ loc ] ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ}. flatMap Ġ{ Ġloc Set Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġloc Set ?. locs !!. map Ġ{ Ġpair Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġpair . second ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĊĊĠĠĠĠĠĠĠ Ġ// ĠTodo : ĠI sol ate Ġabstract Ġlocations Ġthat Ġare Ġel igible Ġto Ġbecome Ġprecise On Abstract Term Ġand Ġreconstruct Ġthe ĠTerm ĊĊĊĠĠĠĠĠĠĠ Ġvar Ġextra Ar ity Ġ= Ġmax Ar ity ĊĊĠĠĠĠĠĠĠ Ġ// ĠUpdate Ġthe Ġvalues Ġof Ġthe Ġhas To Ġlocations ĊĠĠĠĠĠĠĠ Ġfor ( loc Ġin Ġlist Has To Direct Assignable Ġ+ Ġlist Concrete Has To Indirect Assignable ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġvar Ġtype Ġ: ĠType Ġ= ĠUnknown Type . INSTANCE ĊĠĠĠĠĠĠĠĠĠĠĠ Ġif ( loc Ġis ĠPro g Var ){ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġtype Ġ= Ġloc . con cr Type ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġvar Ġar ity Ġ: ĠInt ĊĠĠĠĠĠĠĠĠĠĠĠ Ġif ( list Direct Assignable . contains ( loc )){ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġar ity Ġ= Ġlist Direct Assignable . indexOf ( loc ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġelse { ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġar ity Ġ= Ġextra Ar ity ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġextra Ar ity ++ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġupdate Value Ġ= ĠFull Abstract Term ( name , Ġar ity , Ġmax Ar ity , Ġlist Accessible Value , Ġtype ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġthis . subst Map [ loc ] Ġ= Ġupdate Value ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġ// Update Ġthe Ġvalues Ġof Ġthe Ġdirect Ġhas To Ġlocations ĊĠĠĠĠĠĠĠ Ġfor ( loc Ġin Ġlist Other Direct Assignable ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġvar Ġtype Ġ: ĠType Ġ= ĠUnknown Type . INSTANCE ĊĠĠĠĠĠĠĠĠĠĠĠ Ġif ( loc Ġis ĠPro g Var ){ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġtype Ġ= Ġloc . con cr Type ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġif ( loc Ġis ĠField ){ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġtype Ġ= Ġloc . con cr Type ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġupdate Value Ġ= ĠPartial Abstract Term ( name , Ġlist Direct Assignable . indexOf ( loc ), Ġmax Ar ity , Ġlist Accessible Value , Ġthis . subst Map [ loc ] !! , type ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġthis . subst Map [ loc ] Ġ= Ġupdate Value ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġ// ĠUpdate Ġthe Ġvalues Ġof Ġthe Ġindirect Ġnon Ġhas To Ġlocations ĊĠĠĠĠĠĠĠ Ġfor ( loc Ġin Ġlist Other Indirect Assignable ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġvar Ġtype Ġ: ĠType Ġ= ĠUnknown Type . INSTANCE ĊĠĠĠĠĠĠĠĠĠĠĠ Ġif ( loc Ġis ĠPro g Var ){ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġtype Ġ= Ġloc . con cr Type ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġif ( loc Ġis ĠField ){ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġtype Ġ= Ġloc . con cr Type ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġupdate Value Ġ= ĠPartial Abstract Term ( name , Ġextra Ar ity , Ġmax Ar ity , Ġlist Accessible Value , Ġthis . subst Map [ loc ] !! , type ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġextra Ar ity Ġ+= Ġ 1 ĊĠĠĠĠĠĠĠĠĠĠĠ Ġthis . subst Map [ loc ] Ġ= Ġupdate Value ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġ// print Subst Map () ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ// ĠEvaluate Ġthe Ġinput Ġaccording Ġto Ġthe Ġcurrent Ġsubst Map ĊĠĠĠ Ġprivate Ġfun Ġeval ( input : Logic Element ) Ġ: ĠLogic Element { ĊĠĠĠĠĠĠĠ Ġif ( input Ġis ĠLocation Ġ&& Ġthis . subst Map . containsKey ( input )){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġreturn Ġthis . subst Map . getValue ( input ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġwhen ( input ){ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠUpdate Element Ġ-> Ġthrow ĠException (" Can Ġthere Ġreally Ġbe Ġan Ġupdate Ġhere ?? ") ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠDataType Const Ġ-> Ġreturn ĠDataType Const ( input . name , Ġinput . con cr Type , Ġinput . params . map Ġ{ Ġp Ġ-> Ġthis . eval ( p ) Ġas ĠTerm Ġ}) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠFunction Ġ-> Ġreturn ĠFunction ( input . name , Ġinput . params . map Ġ{ Ġp Ġ-> Ġthis . eval ( p ) Ġas ĠTerm Ġ}) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠPredicate Ġ-> Ġreturn ĠPredicate ( input . name , Ġinput . params . map Ġ{ Ġp Ġ-> Ġthis . eval ( p ) Ġas ĠTerm Ġ}) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠImp l Ġ-> Ġreturn ĠImp l ( this . eval ( input . left ) Ġas ĠFormula , Ġthis . eval ( input . right ) Ġas ĠFormula ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠAnd Ġ-> Ġreturn ĠAnd ( this . eval ( input . left ) Ġas ĠFormula , Ġthis . eval ( input . right ) Ġas ĠFormula ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠOr Ġ-> Ġreturn ĠOr ( this . eval ( input . left ) Ġas ĠFormula , Ġthis . eval ( input . right ) Ġas ĠFormula ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠNot Ġ-> Ġreturn ĠNot ( this . eval ( input . left ) Ġas ĠFormula ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠImplements Term Ġ-> Ġreturn ĠImplements Term ( this . eval ( input . variable ) Ġas ĠTerm , Ġinput . interface Type ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠImplements Form Ġ-> Ġreturn ĠImplements Form ( this . eval ( input . variable ) Ġas ĠTerm , Ġinput . interface Type ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠUpdate On Term Ġ-> Ġthrow ĠException (" Can Ġthere Ġreally Ġbe Ġupdate on Term Ġhere ?? ") ĊĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠUpdate On Formula Ġ-> Ġthrow ĠException (" Can Ġthere Ġreally Ġbe Ġupdate Ġon Ġform Ġhere ?? ") ĊĠĠĠĠĠĠĠĠĠĠĠ Ġelse Ġ-> Ġreturn Ġinput ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} Ċ }