Lines Matching full:context
23 : Context(std::make_unique<WatchedLiteralsSolver>()), A(Context.arena()) { in DataflowAnalysisContextTest()
26 DataflowAnalysisContext Context; member in __anondd45ead80111::DataflowAnalysisContextTest
33 EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula())); in TEST_F()
38 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true))); in TEST_F()
39 EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeLiteral(false))); in TEST_F()
40 EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom()))); in TEST_F()
45 EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeLiteral(true))); in TEST_F()
46 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false))); in TEST_F()
47 EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom()))); in TEST_F()
52 Context.addFlowConditionConstraint(FC, A.makeLiteral(false)); in TEST_F()
53 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true))); in TEST_F()
54 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(false))); in TEST_F()
55 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom()))); in TEST_F()
60 Context.addFlowConditionConstraint(FC, A.makeLiteral(false)); in TEST_F()
61 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(true))); in TEST_F()
62 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false))); in TEST_F()
63 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom()))); in TEST_F()
69 Context.addFlowConditionConstraint(FC, C); in TEST_F()
70 EXPECT_TRUE(Context.flowConditionImplies(FC, C)); in TEST_F()
76 Context.addInvariant(C); in TEST_F()
77 EXPECT_TRUE(Context.flowConditionImplies(FC, C)); in TEST_F()
84 Context.addInvariant(A.makeImplies(C, D)); in TEST_F()
85 Context.addFlowConditionConstraint(FC, C); in TEST_F()
86 EXPECT_TRUE(Context.flowConditionImplies(FC, D)); in TEST_F()
92 Context.addFlowConditionConstraint(FC1, C1); in TEST_F()
96 Atom FC2 = Context.forkFlowCondition(FC1); in TEST_F()
97 EXPECT_TRUE(Context.flowConditionImplies(FC2, C1)); in TEST_F()
102 Context.addFlowConditionConstraint(FC2, C2); in TEST_F()
103 EXPECT_TRUE(Context.flowConditionImplies(FC2, C2)); in TEST_F()
104 EXPECT_FALSE(Context.flowConditionImplies(FC1, C2)); in TEST_F()
113 Context.addFlowConditionConstraint(FC1, C1); in TEST_F()
114 Context.addFlowConditionConstraint(FC1, C3); in TEST_F()
117 Context.addFlowConditionConstraint(FC2, C2); in TEST_F()
118 Context.addFlowConditionConstraint(FC2, C3); in TEST_F()
120 Atom FC3 = Context.joinFlowConditions(FC1, FC2); in TEST_F()
121 EXPECT_FALSE(Context.flowConditionImplies(FC3, C1)); in TEST_F()
122 EXPECT_FALSE(Context.flowConditionImplies(FC3, C2)); in TEST_F()
123 EXPECT_TRUE(Context.flowConditionImplies(FC3, C3)); in TEST_F()
134 EXPECT_TRUE(Context.equivalentFormulas(X, X)); in TEST_F()
136 EXPECT_FALSE(Context.equivalentFormulas(X, Y)); in TEST_F()
139 EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X)); in TEST_F()
141 EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X)); in TEST_F()
144 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X)); in TEST_F()
146 EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X)); in TEST_F()
148 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True)); in TEST_F()
150 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X)); in TEST_F()
153 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X)); in TEST_F()
155 EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X)); in TEST_F()
157 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X)); in TEST_F()
159 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False)); in TEST_F()
162 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X))); in TEST_F()
164 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X))); in TEST_F()
167 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z), in TEST_F()
170 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(A.makeAnd(X, Y), Z), in TEST_F()