test_generator.py 文件源码

def test_d(self):
        for goal, gamma, max_k in [d_general_even_parity(), d1(), d2(), d3()]:
            g = Generator(gamma, normalizator=normalization.NormalizatorNop)
            gnf = Generator(gamma, normalizator=normalization.Normalizator)
            gNC = Generator(gamma, normalizator=normalization.NormalizatorNop, cache=CacheNop)
            gnfNC = Generator(gamma, normalizator=normalization.Normalizator, cache=CacheNop)

            res = []
            for k in range(1, max_k + 1):
                # check static generator
                s_num = get_num(gamma, k, goal)
                s_trees = set(tr.tree for tr in ts(gamma, k, goal, 0))
                self.assertEqual(s_num, len(s_trees))
                for t in s_trees:
                    self.assertTrue(t.is_well_typed(gamma))

                # check generator
                g_num = g.get_num(k, goal)
                self.assertEqual(s_num, g_num)
                res.append(g_num)
                #print(g_num)

                # check generator in nf
                self.assertEqual(s_num, gnf.get_num(k, goal))
                for i in range(10):
                    t = gnf.gen_one(k, goal)
                    if s_num == 0:
                        self.assertIsNone(t)
                    else:
                        self.assertTrue(t.is_well_typed(gamma))

                # check generator without cache
                self.assertEqual(s_num, gNC.get_num(k, goal))

                # check generator in nf without cache
                self.assertEqual(s_num, gnfNC.get_num(k, goal))

            # second run should have the same results
            # but it should be much faster
            start = time.time()
            for k in range(1, max_k + 1):
                g_num = g.get_num(k, goal)
                self.assertEqual(res[k - 1], g_num)
            end = time.time()
            self.assertLess(end - start, REALLY_SHORT_TIME)