Delay2x2.smt2~

(define-sort WireVoltage () (_ BitVec 2) )
(define-const wire-Neg WireVoltage (_ bv3 2) )
(define-const wire-Gnd WireVoltage (_ bv0 2) )
(define-const wire-Pos WireVoltage (_ bv1 2) )

(define-fun RowVoltage ((t Bool)) WireVoltage
	(ite t wire-Pos wire-Neg )
)


(define-fun ColTruth ((v WireVoltage)) Bool
	(ite (= v wire-Gnd) false true)
)

; The polarities
(declare-const M11P Bool) ; True means positive
(declare-const M12P Bool)
(declare-const M21P Bool)
(declare-const M22P Bool)

(define-fun MemristorValue((prior Bool)(polarity Bool)(Vr WireVoltage)(Vc WireVoltage)) Bool
	(ite polarity
		(ite (bvsgt Vr Vc) true
			(ite (= Vr Vc) prior false )
		)

		(ite (bvsgt Vc Vr ) true
			(ite (= Vr Vc) prior false )
		)
	)
)



(define-fun BothCols ((M11 Bool) (M12 Bool) (M21 Bool) (M22 Bool)) Bool
	(and
		(or M11 M21)
		(or M12 M22)
	)
)




;This is the weak rule

(assert (forall ((r1p Bool) (r2p Bool) (M11 Bool) (M12 Bool) (M21 Bool) (M22 Bool))

	(=
		(BothCols
			
				(MemristorValue
					M11
					M11P
					(RowVoltage r1p)
					wire-Gnd
				)
			
				(MemristorValue
					M12
					M12P
					(RowVoltage r1p)
					wire-Gnd
				)

				(MemristorValue
					M21
					M21P
					(RowVoltage r2p)
					wire-Gnd
				)
			
				(MemristorValue
					M22
					M22P
					(RowVoltage r2p)
					wire-Gnd
				)
						
		)
		
		r1p
	)
))


(check-sat)
(get-value ( M11P M12P M21P M22P) )