(set-option :produce-models true)
            
        ;; propositional level definitions
      
        ;propositional variable type definitions
        (define-sort pvar () (Array Int Real))
        (define-fun component ((x pvar)) Real
          (select x 1))
        (define-fun value ((x pvar)) Real
          (select x 2))
        (define-fun setComponent ((x pvar) (comp Real)) pvar
          (store x 1 comp))
        (define-fun setValue ((x pvar) (val Real)) pvar
          (store x 2 val))   
          ;truth const
        (declare-const pT pvar)
        (assert (and (= (component pT) (~ 1.0)) (= (value pT) 1.0)))
        (declare-const pF pvar)
        (assert (and (= (component pF) (~ 1.0)) (= (value pF) 0.0)))
        
        ;;RELATIONS
        ;eq(x,y) T if x = y, F else
        (define-fun eq ((x pvar) (y pvar)) Bool
            (and (= (component x) (component y)) (= (value x) (value y))))
            
            
        ;g (x,y) true if x > y, false otherwise
        (define-fun g ((x pvar) (y pvar)) Bool
            ;same component
            (ite (= (component x) (component y)) (< (value y) (value x))
            ;values in different components
            ;non-prod, prod
            (ite (and (= (component x) (~ 1.0)) (> (component y) (~ 1.0)))
            ;this case in never reached 
        false 
        ;prod, non-prod
        (ite (and (> (component x) (~ 1.0)) (= (component y) (~ 1.0)))
            ;this case in never reached 
        false 
        ;prod-prod
        (< (component y) (component x))))))
       
        ;geq (x,y) true if x >= y, false otherwise
        (define-fun geq ((x pvar) (y pvar)) Bool
        	(or (eq x y) (g x y)))
            
        ;l (x,y) true if x < y, false otherwise
        (define-fun l ((x pvar) (y pvar)) Bool
        	(not (geq x y)))
    	
        ;leq (x, y) true if x <= y, false otherwise
        (define-fun leq ((x pvar) (y pvar)) Bool
        	(not (g x y)))
        
		
        ;;OPERATIONS
        ;pmin(x,y)
        (define-fun pmin ((x pvar) (y pvar)) pvar
        	(ite (leq x y) x y))

        ;pmax(x,y)
        (define-fun pmax ((x pvar) (y pvar)) pvar
        	(ite (geq x y) x y))
            
        ;weak conjunction = pmin (x, y)
        (define-fun pwcon ((x pvar) (y pvar)) pvar
            (pmin x y))

        ;weak disjunction pmax (x, y)
        (define-fun pwdis ((x pvar) (y pvar)) pvar
            (pmax x y))
        
        ;delta pdelta = 1 iff x = 1, 0 oth.
        (define-fun pdelta ((x pvar)) pvar
            (ite (= (value x) 1.0) pT pF))
        
        ;pcon(x, y)
        (define-fun pcon ((x pvar) (y pvar)) pvar
        (ite (and (<= 0.0 (value x)) (<= 0.0 (value y))
                                 (<= (value x) 1.0) (<= (value y) 1.0))
                            ;they are in the same luk-component
                            (setValue x
                            (ite (<= 0.0 (- (+ (value x) (value y)) 1.0))
                            (- (+ (value x) (value y)) 1.0) 0.0))
                                 ;different components
        (pmin x y)))
        
        ;pimpl(x y) -residuum-
        (define-fun pimpl ((x pvar) (y pvar)) pvar
            (ite (leq x y) pT
            (ite (and (<= 0.0 (value x)) (<= 0.0 (value y))
                                 (<= (value x) 1.0) (<= (value y) 1.0))
                                 ;they are in the same luk-component
                                 (setValue x (+ 1.0 (- (value y) (value x))))
                                 ;different components
        y)))
        
        ;negation (pneg x = x -> 0)
        (define-fun pneg ((x pvar)) pvar
            (pimpl x pF)
        )
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;modal types and functions

        (define-sort var () (Array Int pvar))
        (define-fun valueInWorld ((x var) (world Int)) pvar
            (select x world)
        )
        
        ;truth constants
        (declare-const T var)
        (assert (= (valueInWorld T 0) pT))(assert (= (valueInWorld T 1) pT))(assert (= (valueInWorld T 2) pT))(assert (= (valueInWorld T 3) pT))
        (declare-const F var)(assert (= (valueInWorld F 0) pF))(assert (= (valueInWorld F 1) pF))(assert (= (valueInWorld F 2) pF))(assert (= (valueInWorld F 3) pF))
        
        ;auxiliar var to generate the results
        (declare-const results var)	
              
        ;weak conjunction
        (define-fun wcon ((x var) (y var)) var
            (store (store (store (store results 3 (pwcon (select x 3) (select y 3))) 2  (pwcon (select x 2) (select y 2))) 1  (pwcon (select x 1) (select y 1))) 0  (pwcon (select x 0) (select y 0))))
      
        ;weak disjunction
        (define-fun wdis ((x var) (y var)) var
            (store (store (store (store results 3 (pwdis (select x 3) (select y 3))) 2  (pwdis (select x 2) (select y 2))) 1  (pwdis (select x 1) (select y 1))) 0  (pwdis (select x 0) (select y 0))))
         
        ;delta
        (define-fun delta ((x var)) var
            (store (store (store (store results 3 (pdelta (select x 3))) 2  (pdelta (select x 2))) 1  (pdelta (select x 1))) 0  (pdelta (select x 0))))
        
        ;con(x, y)
        (define-fun con ((x var) (y var)) var
            (store (store (store (store results 3 (pcon (select x 3) (select y 3))) 2  (pcon (select x 2) (select y 2))) 1  (pcon (select x 1) (select y 1))) 0  (pcon (select x 0) (select y 0))))
        

        ;impl(x y) -residuum-
        (define-fun impl ((x var) (y var)) var
            (store (store (store (store results 3 (pimpl (select x 3) (select y 3))) 2  (pimpl (select x 2) (select y 2))) 1  (pimpl (select x 1) (select y 1))) 0  (pimpl (select x 0) (select y 0))))
        
        ;negation (neg x = x -> 0)
        (define-fun neg ((x var)) var
            (store (store (store (store results 3 (pneg (select x 3))) 2  (pneg (select x 2))) 1  (pneg (select x 1))) 0  (pneg (select x 0))))
        

        ;MODAL OPERATIONS
        ;accessibility relation matrix
        ;the values will meet conditions from [skeleton]
        (declare-fun R () (Array Int (Array Int pvar)))
        ;some relations are always false from the skeleton construction. The others, are prop. variables, with the restrictions of the t-norm.
        (assert (= pF (select (select R 0) 0)))(assert (and (= (component (select (select R 0) 1)) (~ 1.0))
                                            (<= 0.0 (value (select (select R 0) 1)))
                                            (<= (value (select (select R 0) 1)) 1.0)))
                    ;limitations for the finitely valued components
                    (assert (and (= (component (select (select R 0) 2)) (~ 1.0))
                                            (<= 0.0 (value (select (select R 0) 2)))
                                            (<= (value (select (select R 0) 2)) 1.0)))
                    ;limitations for the finitely valued components
                    (assert (and (= (component (select (select R 0) 3)) (~ 1.0))
                                            (<= 0.0 (value (select (select R 0) 3)))
                                            (<= (value (select (select R 0) 3)) 1.0)))
                    ;limitations for the finitely valued components
                    (assert (= pF (select (select R 1) 0)))(assert (= pF (select (select R 1) 1)))(assert (= pF (select (select R 1) 2)))(assert (= pF (select (select R 1) 3)))(assert (= pF (select (select R 2) 0)))(assert (= pF (select (select R 2) 1)))(assert (= pF (select (select R 2) 2)))(assert (= pF (select (select R 2) 3)))(assert (= pF (select (select R 3) 0)))(assert (= pF (select (select R 3) 1)))(assert (= pF (select (select R 3) 2)))(assert (= pF (select (select R 3) 3)))
        ;; auxiliary functions
        
        ;box related functions
        
        ;given a var and an index i, returns a list of reals of length nworlds (i.e., a var) with 
        ;at each index p, the value R[i][p] -> var[p]
        (define-fun tfunc ((x var) (orig Int)) var
        (store (store (store (store results 3 (pimpl (select (select R orig) 3) (select x 3))) 2 (pimpl (select (select R orig) 2) (select x 2))) 1 (pimpl (select (select R orig) 1) (select x 1))) 0 (pimpl (select (select R orig) 0) (select x 0))))
        
        ;returns the minimum of a list of variables of lentgh nworlds  
        (define-fun minList ((x var)) pvar
        (pmin (pmin (pmin (select x 0) (select x 1)) (select x 2)) (select x 3)))
        
        ;minSuccessors
        ;takes a variable and an index and returns the corresponging pVar with the value of the minimum 
        ;over the successors of the world given by the index
        (define-fun minSuccessors ((x var) (i Int)) pvar
          (minList (tfunc x i)))
        
        ;box
        (define-fun box ((x var)) var 
         (store (store (store (store results 3 (minSuccessors x 3)) 2 (minSuccessors x 2)) 1 (minSuccessors x 1)) 0 (minSuccessors x 0)))
        
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;diamond functions
        
        ;given a var and an index i, returns a list of reals of length nworlds (i.e., a var) with 
        ;at each index p, the value R[i][p] * var[p]
        (define-fun bfunc ((x var) (orig Int)) var
        (store (store (store (store results 3 (pcon (select (select R orig) 3) (select x 3))) 2 (pcon (select (select R orig) 2) (select x 2))) 1 (pcon (select (select R orig) 1) (select x 1))) 0 (pcon (select (select R orig) 0) (select x 0))))
          
        ;returns the maximum of a list of reals of lentgh nworlds  
        (define-fun maxList ((x var)) pvar
        (pmax (pmax (pmax (select x 0) (select x 1)) (select x 2)) (select x 3)))
        
        ;maxSuccessors
        ;takes a variable and an index and returns the corresponging pVar with the value of the maximum 
        ;over the successors of the world given by the index
        (define-fun maxSuccessors ((x var) (i Int)) pvar
          (maxList (bfunc x i)))
        
        ;diamond
        (define-fun diamond ((x var)) var 
         (store  (store  (store  (store  results 3 (maxSuccessors x 3)) 2 (maxSuccessors x 2)) 1 (maxSuccessors x 1)) 0 (maxSuccessors x 0)))
        
        ;;DECLARATIONS
        ;;;assingments of the variables
        (declare-fun x2 () var)
            (assert (and (= (component (valueInWorld x2 0)) (~ 1.0))
                                        (<= 0.0 (value (valueInWorld x2 0)))
                                        (<= (value (valueInWorld x2 0)) 1.0)))
                ;limitations for the finitely valued components
                (assert (and (= (component (valueInWorld x2 1)) (~ 1.0))
                                        (<= 0.0 (value (valueInWorld x2 1)))
                                        (<= (value (valueInWorld x2 1)) 1.0)))
                ;limitations for the finitely valued components
                (assert (and (= (component (valueInWorld x2 2)) (~ 1.0))
                                        (<= 0.0 (value (valueInWorld x2 2)))
                                        (<= (value (valueInWorld x2 2)) 1.0)))
                ;limitations for the finitely valued components
                (assert (and (= (component (valueInWorld x2 3)) (~ 1.0))
                                        (<= 0.0 (value (valueInWorld x2 3)))
                                        (<= (value (valueInWorld x2 3)) 1.0)))
                ;limitations for the finitely valued components
                (declare-fun x1 () var)
            (assert (and (= (component (valueInWorld x1 0)) (~ 1.0))
                                        (<= 0.0 (value (valueInWorld x1 0)))
                                        (<= (value (valueInWorld x1 0)) 1.0)))
                ;limitations for the finitely valued components
                (assert (and (= (component (valueInWorld x1 1)) (~ 1.0))
                                        (<= 0.0 (value (valueInWorld x1 1)))
                                        (<= (value (valueInWorld x1 1)) 1.0)))
                ;limitations for the finitely valued components
                (assert (and (= (component (valueInWorld x1 2)) (~ 1.0))
                                        (<= 0.0 (value (valueInWorld x1 2)))
                                        (<= (value (valueInWorld x1 2)) 1.0)))
                ;limitations for the finitely valued components
                (assert (and (= (component (valueInWorld x1 3)) (~ 1.0))
                                        (<= 0.0 (value (valueInWorld x1 3)))
                                        (<= (value (valueInWorld x1 3)) 1.0)))
                ;limitations for the finitely valued components
                
        
        ;declaration of the constants
        
        
        ;the values of parts of the functions are fixed following the skeleton definition
        
                        (assert (= (select (box (impl x1 x2)) 0)
                            (pimpl (select (select R 0) 1)
                                (select (impl x1 x2) 1))))
                        (assert (= (select (box x1) 0)
                            (pimpl (select (select R 0) 2)
                                (select x1 2))))
                        (assert (= (select (box x2) 0)
                            (pimpl (select (select R 0) 3)
                                (select x2 3))))

;;;PROBLEM
        (assert (l (valueInWorld (impl (box (impl x1 x2)) (impl (box x1) (box x2))) 0) (valueInWorld T 0)))
                

(check-sat)
        ;SHOWS
        (get-value((component (select (select R 0) 0))))
                    (get-value((value (select (select R 0) 0))))
                    (get-value((component (select (select R 0) 1))))
                    (get-value((value (select (select R 0) 1))))
                    (get-value((component (select (select R 0) 2))))
                    (get-value((value (select (select R 0) 2))))
                    (get-value((component (select (select R 0) 3))))
                    (get-value((value (select (select R 0) 3))))
                    (get-value((component (select (select R 1) 0))))
                    (get-value((value (select (select R 1) 0))))
                    (get-value((component (select (select R 1) 1))))
                    (get-value((value (select (select R 1) 1))))
                    (get-value((component (select (select R 1) 2))))
                    (get-value((value (select (select R 1) 2))))
                    (get-value((component (select (select R 1) 3))))
                    (get-value((value (select (select R 1) 3))))
                    (get-value((component (select (select R 2) 0))))
                    (get-value((value (select (select R 2) 0))))
                    (get-value((component (select (select R 2) 1))))
                    (get-value((value (select (select R 2) 1))))
                    (get-value((component (select (select R 2) 2))))
                    (get-value((value (select (select R 2) 2))))
                    (get-value((component (select (select R 2) 3))))
                    (get-value((value (select (select R 2) 3))))
                    (get-value((component (select (select R 3) 0))))
                    (get-value((value (select (select R 3) 0))))
                    (get-value((component (select (select R 3) 1))))
                    (get-value((value (select (select R 3) 1))))
                    (get-value((component (select (select R 3) 2))))
                    (get-value((value (select (select R 3) 2))))
                    (get-value((component (select (select R 3) 3))))
                    (get-value((value (select (select R 3) 3))))
                    (get-value((component (select x2 0))))
                (get-value((value (select x2 0))))
                (get-value((component (select x2 1))))
                (get-value((value (select x2 1))))
                (get-value((component (select x2 2))))
                (get-value((value (select x2 2))))
                (get-value((component (select x2 3))))
                (get-value((value (select x2 3))))
                (get-value((component (select x1 0))))
                (get-value((value (select x1 0))))
                (get-value((component (select x1 1))))
                (get-value((value (select x1 1))))
                (get-value((component (select x1 2))))
                (get-value((value (select x1 2))))
                (get-value((component (select x1 3))))
                (get-value((value (select x1 3))))
                