84     : Solver(Context), Type(Context.int_const("Type")),  in RandomFunctionGenerator()
101   Solver.add(inSetConstraint(Type, kFunctionTypes));  in RandomFunctionGenerator()
113   Solver.add(ContiguousEnd == OverlapBegin);  in RandomFunctionGenerator()
114   Solver.add(OverlapEnd == LoopBegin);  in RandomFunctionGenerator()
115   Solver.add(LoopEnd == AlignedLoopBegin);  in RandomFunctionGenerator()
116   Solver.add(AlignedLoopEnd == AcceleratorBegin);  in RandomFunctionGenerator()
119   Solver.add(ContiguousBegin == 0);  in RandomFunctionGenerator()
120   Solver.add(AcceleratorEnd == kMaxSize);  in RandomFunctionGenerator()
122   Solver.add(ContiguousEnd <= kMaxIndividualSize + 1);  in RandomFunctionGenerator()
124   Solver.add(OverlapEnd <= kMaxOverlapSize + 1);  in RandomFunctionGenerator()
127   Solver.add(OverlapBegin == OverlapEnd || OverlapBegin >= 2);  in RandomFunctionGenerator()
133   Solver.add(inSetConstraint(AlignedAlignment, kLoopAlignments));  in RandomFunctionGenerator()
134   Solver.add(AlignedLoopBegin == AlignedLoopEnd || AlignedLoopBegin >= 64);  in RandomFunctionGenerator()
135   Solver.add(AlignedLoopBlockSize >= AlignedAlignment);  in RandomFunctionGenerator()
136   Solver.add(AlignedLoopBlockSize >= LoopBlockSize);  in RandomFunctionGenerator()
139   Solver.add(  in RandomFunctionGenerator()
144   Solver.add(IsMemcpy ||  in RandomFunctionGenerator()
148   Solver.add(inSetConstraint(ElementClass, kElementClasses));  in RandomFunctionGenerator()
151     Solver.add(LoopBegin == LoopEnd);  in RandomFunctionGenerator()
153     Solver.add(AlignedLoopBegin == AlignedLoopEnd);  in RandomFunctionGenerator()
155     Solver.add(AcceleratorBegin == AcceleratorEnd);  in RandomFunctionGenerator()
207   if (Solver.check() != z3::sat)  in next()
210   z3::model m = Solver.get_model();  in next()
246   Solver.add(!CurrentLayout);  in next()
262   Solver.add(inSetConstraint(Begin, kAnchors));  in addBoundsAndAnchors()
263   Solver.add(inSetConstraint(End, kAnchors));  in addBoundsAndAnchors()
264   Solver.add(Begin >= 0);  in addBoundsAndAnchors()
265   Solver.add(Begin <= End);  in addBoundsAndAnchors()
266   Solver.add(End <= kMaxSize);  in addBoundsAndAnchors()
273   Solver.add(inSetConstraint(LoopBlockSize, kLoopBlockSize));  in addLoopConstraints()
274   Solver.add(LoopBegin == LoopEnd ||  in addLoopConstraints()