package Ġorg . jetbrains . research . k ex . smt Ċ Ċ import Ġorg . jetbrains . research . k ex . Inheritance Info Ċ import Ġorg . jetbrains . research . k ex . config . k ex Config Ċ import Ġorg . jetbrains . research . k fg . type . Type Factory Ċ import Ġorg . jetbrains . research . k the l per . assert . fail Ċ import Ġorg . jetbrains . research . k the l per . assert . unreachable Ċ import Ġorg . jetbrains . research . k the l per . logging . log Ċ Ċ private Ġval Ġengine Ġ= Ġk ex Config . getString Value (" smt ", Ġ" engine ") ĊĠĠĠ Ġ?: Ġunreachable Ġ{ Ġlog . error (" No ĠS MT Ġengine Ġspecified ") Ġ} Ċ Ċ class ĠS MT Proxy Solver ( ĊĠĠĠ Ġtf : ĠType Factory , ĊĠĠĠ Ġval Ġsolver : ĠAbstract S MT Solver Ġ= Ġget Solver ( tf , Ġengine ) Ċ ) Ġ: ĠAbstract S MT Solver Ġby Ġsolver Ġ{ ĊĊĠĠĠ Ġcompanion Ġobject Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġsol vers Ġ= Ġrun Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġloader Ġ= ĠThread . currentThread (). context ClassLoader ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġresource Ġ= Ġloader . getResource AsStream (" sol vers . json ") ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ?: Ġfail Ġ{ Ġlog . error (" Could Ġnot Ġload Ġs mt Ġsolver Ġinheritance Ġinfo ") Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġinheritance Info Ġ= ĠInherit ance Info . fromJson ( resource . buffered Reader (). read Text ()) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġresource . close () ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġinheritance Info . in her itors . associate Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġit . name Ġto Ġloader . load Class ( it . in her itor Class ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġfun Ġget Solver ( tf : ĠType Factory , Ġengine : ĠString ): ĠAbstract S MT Solver Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġsolver Class Ġ= Ġsol vers [ engine ] Ġ?: Ġunreachable Ġ{ Ġlog . error (" Unknown Ġengine Ġname : Ġ$ engine ") Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġconstructor Ġ= Ġsolver Class . get Constructor ( Type Factory :: class . java ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġreturn Ġconstructor . newInstance ( tf ) Ġas ĠAbstract S MT Solver ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġconstructor ( tf : ĠType Factory , Ġengine : ĠString ) Ġ: Ġthis ( tf , Ġget Solver ( tf , Ġengine )) Ċ } Ċ