test_temporallogic.py 文件源码

def test_encode(self):
        self.assertEqual(AP("a").encode(42), ('a___42.0', ['(declare-const a___42.0 Bool)']))
        self.assertEqual(AP("a").encode(), ('a___0.0', ['(declare-const a___0.0 Bool)']))
        self.assertEqual(AP("a").encode(0.5), ('a___0.5', ['(declare-const a___0.5 Bool)']))
        self.assertEqual(AP(None, (1, 2), operator.ge, 42, ('x', 'y')).encode(),
                         ('(>= (+ (* 1.0 x___0.0) (* 2.0 y___0.0)) 42)',
                          ['(declare-const x___0.0 Real)', '(declare-const y___0.0 Real)']))
        self.assertEqual(AP(None, (1, 2), operator.ge, 42, ('x', 'y')).encode(42),
                         ('(>= (+ (* 1.0 x___42.0) (* 2.0 y___42.0)) 42)',
                          ['(declare-const x___42.0 Real)', '(declare-const y___42.0 Real)']))
        self.assertEqual(AP(None, None, operator.ne, 42, ('x', 'y')).encode(),
                         ('(distinct (+ x___0.0 y___0.0) 42)',
                          ['(declare-const x___0.0 Real)', '(declare-const y___0.0 Real)']))
        self.assertEqual(AP(None, None, operator.eq, 42, 'x').encode(),
                         ('(= x___0.0 42)', ['(declare-const x___0.0 Real)']))
        self.assertEqual(AP(None, (3,), gt, 42, 'x').encode(),
                         ('(> (* 3.0 x___0.0) 42)', ['(declare-const x___0.0 Real)']))
        self.assertEqual(AP(None, (3,), gt, 42, 'x').encode(0.5),
                         ('(and (>= (* 3.0 x___0.0) 42) (and (> (* 3.0 x___0.5) 42) (>= (* 3.0 x___1.0) 42)))',
                          ['(declare-const x___0.0 Real)', '(declare-const x___0.5 Real)',
                           '(declare-const x___1.0 Real)']))